Normalized archimedean absolute values under field extension

For infinite places w ∣ v, the completion map raises the normalized absolute value to the local degree [L_w : K_v]. The underlying ordinary norms agree, but a complex place above a real place doubles the normalization exponent. Multiplying over all places above v gives the global degree [L : K]. These are the archimedean factors in the degree formula for extension of ideles.

Completed extensions at infinite places are finite dimensional, with degree one or two. A place indexed by the places above v carries its proof of lying over v as an instance.

The formulas are in NumberField.InfinitePlace, alongside completionNormalizedAbsValue. For the ordinary norm, use NumberField.InfinitePlace.Completion.norm_completionMap (w := w) x. For the normalized value, use completionNormalizedAbsValue_completionMap (w := w) x for a completion element, and prod_completionNormalizedAbsValue_completionMap (L := L) v x for the product over places above v. Both are pre-simplification rules: simp applies them before expanding the normalized absolute value into a power of the norm.

The degree and multiplicity identities are Mathlib's NumberField.InfinitePlace.mult_mul_finrank and NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §8.

instance NumberField.InfinitePlace.instLiesOverSubtype {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : { w : InfinitePlace L // w.LiesOver v }) : (↑w).LiesOver v

A place indexed by the places above v carries its proof of lying over v as an instance.

instance NumberField.InfinitePlace.instFiniteDimensionalCompletion_tauCeti {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] : FiniteDimensional v.Completion w.Completion

A completed extension at an infinite place is finite dimensional: its degree is one or two.

@[simp]

theorem NumberField.LiesOver.completionMap_comp {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {M : Type u_3} [Field M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] {v : InfinitePlace K} {w : InfinitePlace L} {u : InfinitePlace M} [w.LiesOver v] [u.LiesOver w] : (completionMap w u).comp (completionMap v w) = completionMap v u

Canonical maps between archimedean completions compose in a tower of fields.

@[simp]

theorem NumberField.InfinitePlace.Completion.norm_completionMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (x : v.Completion) : ‖(LiesOver.completionMap v w) x‖ = ‖x‖

Extension of archimedean completions preserves the ordinary norm.

@[simp]

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_completionMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (x : v.Completion) : w.completionNormalizedAbsValue ((LiesOver.completionMap v w) x) = v.completionNormalizedAbsValue x ^ Module.finrank v.Completion w.Completion

Under extension of archimedean completions the normalized absolute value is raised to the local degree. This includes the real-to-complex case and the value at zero.

@[simp]

theorem NumberField.InfinitePlace.prod_completionNormalizedAbsValue_completionMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (v : InfinitePlace K) (x : v.Completion) : ∏ w : { w : InfinitePlace L // w.LiesOver v }, (↑w).completionNormalizedAbsValue ((LiesOver.completionMap v ↑w) x) = v.completionNormalizedAbsValue x ^ Module.finrank K L

The product of normalized absolute values over the infinite places above v is the normalized absolute value at v raised to the global degree.