Local norms at the infinite places

Let L / K be an extension of fields and let w be an infinite place of L lying over the infinite place v of K. Through the extension embeddings K_v → ℂ and L_w → ℂ, the norm N_{L_w/K_v} of the completed extension is one of three explicit maps.

• If w is unramified over v, then L_w = K_v and the norm is the inverse of the completion map. Read in ℂ, it is the identity when w.embedding extends v.embedding, and complex conjugation when the conjugate of w.embedding extends it.
• If w is ramified over v, so that w is complex and v is real, then the norm is z ↦ |z|², and the norm group N_{L_w/K_v}(L_wˣ) consists of the positive elements.

At a complex place every unit is moreover an n-th power for every n ≠ 0.

These formulas compute the archimedean components of the norm map of ideles. The norm preserves the normalized absolute value: at a complex place over a real place the source uses the square of the ordinary absolute value, exactly as the norm does.

Main results

• NumberField.InfinitePlace.completionNormalizedAbsValue_norm: the norm preserves normalized absolute values at infinite places.
• NumberField.InfinitePlace.Completion.extensionEmbedding_norm_of_isUnramified: at an unramified place, the norm is the identity in ℂ.
• NumberField.InfinitePlace.Completion.extensionEmbedding_norm_of_isUnramified_conjugate: the same, when the conjugate of w.embedding extends v.embedding; the norm is then complex conjugation.
• NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_norm_of_isReal: at a real place over a real place, the norm is the identity of ℝ.
• NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_norm_of_isRamified: at a complex place over a real place, the norm is Complex.normSq.
• NumberField.InfinitePlace.Completion.mem_normGroup_iff_of_isRamified: at a complex place over a real place, the norms are the positive elements.
• NumberField.InfinitePlace.Completion.mem_range_powMonoidHom: a unit of an archimedean completion that is positive at a real place is an n-th power.

References

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

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_norm_of_isUnramified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (h : IsUnramified K w) [ComplexEmbedding.LiesOver w.embedding v.embedding] (y : w.Completion) : (extensionEmbedding v) ((Algebra.norm v.Completion) y) = (extensionEmbedding w) y

The local norm at an unramified infinite place. If w.embedding extends v.embedding, the norm N_{L_w/K_v} is the identity when read in ℂ through the extension embeddings.

theorem NumberField.InfinitePlace.Completion.extensionEmbedding_norm_of_isUnramified_conjugate {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (h : IsUnramified K w) [ComplexEmbedding.LiesOver (ComplexEmbedding.conjugate w.embedding) v.embedding] (y : w.Completion) : (extensionEmbedding v) ((Algebra.norm v.Completion) y) = (starRingEnd ℂ) ((extensionEmbedding w) y)

The local norm at an unramified infinite place, conjugate case. If the conjugate of w.embedding extends v.embedding, the norm N_{L_w/K_v} is complex conjugation when read in ℂ through the extension embeddings.

theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_norm_of_isReal {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (hv : v.IsReal) (hw : w.IsReal) (y : w.Completion) : (extensionEmbeddingOfIsReal hv) ((Algebra.norm v.Completion) y) = (extensionEmbeddingOfIsReal hw) y

The local norm at a real place over a real place is the identity of ℝ, read through the real extension embeddings.

theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_norm_of_isRamified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (h : IsRamified K w) (hv : v.IsReal) (y : w.Completion) : (extensionEmbeddingOfIsReal hv) ((Algebra.norm v.Completion) y) = Complex.normSq ((extensionEmbedding w) y)

The local norm at a complex place over a real place is z ↦ |z|², read through the extension embeddings K_v → ℝ and L_w → ℂ.

theorem NumberField.InfinitePlace.Completion.mem_normGroup_iff_of_isRamified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (h : IsRamified K w) (hv : v.IsReal) {x : v.Completionˣ} : x ∈ TauCeti.normGroup v.Completion w.Completion ↔ 0 < (extensionEmbeddingOfIsReal hv) ↑x

The norm group at a complex place over a real place consists of the positive elements: read in ℝ and ℂ, the norm N_{L_w/K_v} is z ↦ |z|².

@[simp]

theorem NumberField.InfinitePlace.completionNormalizedAbsValue_norm {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 : w.Completion) : v.completionNormalizedAbsValue ((Algebra.norm v.Completion) x) = w.completionNormalizedAbsValue x

The local field norm preserves the normalized absolute value, including the squared normalization at complex places.

n-th powers at an infinite place

theorem NumberField.InfinitePlace.Completion.mem_range_powMonoidHom {K : Type u_1} [Field K] {w : InfinitePlace K} {n : ℕ} (hn : n ≠ 0) (y : w.Completionˣ) (hy : ∀ (hw : w.IsReal), 0 < (extensionEmbeddingOfIsReal hw) ↑y) : y ∈ (powMonoidHom n).range

Units of an archimedean completion that are positive at a real place are n-th powers. At a real place this is the existence of real n-th roots of positive numbers; at a complex place every unit is an n-th power.