The norm map of ideles and idele classes

Let L / K be an extension of number fields. The norm map of adeles adeleNorm is multiplicative and continuous, so it restricts to a continuous homomorphism of idele groups

ideleNormMap K L : 𝕀_L →ₜ* 𝕀_K.

Its coordinate at a place v of K is the product, over the places w ∣ v of L, of the local norms N_{L_w/K_v} of the coordinates at w. It sends the principal idele of x ∈ Lˣ to the principal idele of N_{L/K}(x), so it descends to a continuous homomorphism of idele class groups

ideleClassNormMap K L : C_L →ₜ* C_K.

Composed with extension of ideles from K to L, both maps are the [L : K]-th power map.

This is the norm in the direction L → K, opposite to the extension maps ideleExtension and ideleClassExtension. It is not to be confused with the absolute idele norm ideleNorm, a homomorphism to ℝ≥0ˣ.

Main definitions

• TauCeti.GlobalNumberFields.ideleNormMap: the norm map 𝕀_L →ₜ* 𝕀_K of idele groups.
• TauCeti.GlobalNumberFields.ideleClassNormMap: the induced norm map C_L →ₜ* C_K of idele class groups.

Main results

• TauCeti.GlobalNumberFields.continuous_ideleNormMap, TauCeti.GlobalNumberFields.continuous_ideleClassNormMap: the relative norm maps are continuous.
• TauCeti.GlobalNumberFields.ideleFiniteCoord_ideleNormMap, TauCeti.GlobalNumberFields.ideleInfiniteCoord_ideleNormMap: the coordinate of the norm of an idele at a place v of K is the product of the local norms of its coordinates at the places above v.
• TauCeti.GlobalNumberFields.ideleNormMap_ofCompletion, TauCeti.GlobalNumberFields.ideleClassNormMap_ofCompletion: the norm of an idele, or of an idele class, concentrated at one infinite place w is concentrated at the place below w, with the local norm as coordinate.
• TauCeti.GlobalNumberFields.ideleNormMap_ofAdicCompletion, TauCeti.GlobalNumberFields.ideleClassNormMap_ofAdicCompletion: the same at a finite place.
• TauCeti.GlobalNumberFields.ideleNormMap_unitEmbedding: the norm of a principal idele is the principal idele of the global norm.
• TauCeti.GlobalNumberFields.ideleNormMap_ideleExtension, TauCeti.GlobalNumberFields.ideleClassNormMap_ideleClassExtension: the norm of an idele, or of an idele class, extended from K is its [L : K]-th power.
• TauCeti.GlobalNumberFields.ideleNormMap_comp, TauCeti.GlobalNumberFields.ideleClassNormMap_comp: norm maps compose in towers.
• TauCeti.GlobalNumberFields.range_ideleClassNormMap_le_of_algHom: a larger extension has a smaller idele-class norm group.
• TauCeti.GlobalNumberFields.range_ideleClassNormMap_eq_of_algEquiv: K-isomorphic extensions have the same idele-class norm group.
• TauCeti.GlobalNumberFields.range_ideleClassNormMap, TauCeti.GlobalNumberFields.index_range_ideleClassNormMap: the idele-class norm group N_{L/K}(C_L) is the image of N_{L/K}(𝕀_L) in C_K, so its index in C_K is the index of Kˣ · N_{L/K}(𝕀_L) in 𝕀_K.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter VI, §2.

noncomputable def TauCeti.GlobalNumberFields.ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L →ₜ* NumberField.IdeleGroup (NumberField.RingOfIntegers K) K

The norm map of ideles N_{L/K} : 𝕀_L →ₜ* 𝕀_K, the restriction of the multiplicative norm map of adeles adeleNorm to units.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_ideleNormMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) : ↑((ideleNormMap K L) x) = (adeleNorm K L) ↑x

The underlying adele of the norm of an idele is the adele norm of its underlying adele.

theorem TauCeti.GlobalNumberFields.continuous_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Continuous ⇑(ideleNormMap K L)

The relative idele norm is continuous for the units topology, which controls both an adele and its inverse.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleFiniteCoord_ideleNormMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) : v.ideleFiniteCoord ((ideleNormMap K L) x) = ∏ᶠ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((↑w).ideleFiniteCoord x)

The finite coordinates of the idele norm. The coordinate of N_{L/K}(x) at a finite place v of K is the product over the places w ∣ v of N_{L_w/K_v}(x_w).

@[simp]

theorem TauCeti.GlobalNumberFields.ideleInfiniteCoord_ideleNormMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) : v.ideleInfiniteCoord ((ideleNormMap K L) x) = ∏ᶠ (w : { w : NumberField.InfinitePlace L // w.LiesOver v }), (Algebra.normUnits v.Completion) ((↑w).ideleInfiniteCoord x)

The infinite coordinates of the idele norm. The coordinate of N_{L/K}(x) at an infinite place v of K is the product over the places w ∣ v of N_{L_w/K_v}(x_w).

theorem TauCeti.GlobalNumberFields.ideleNormMap_ofCompletion {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] (u : w.Completionˣ) : (ideleNormMap K L) ((NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers L) L w) u) = (NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K v) ((Algebra.normUnits v.Completion) u)

The norm of an idele concentrated at one infinite place. If w lies over v, the norm of the idele that is u at w and 1 elsewhere is the idele that is N_{L_w/K_v}(u) at v and 1 elsewhere.

theorem TauCeti.GlobalNumberFields.ideleNormMap_ofAdicCompletion {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)ˣ) : (ideleNormMap K L) ((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers L) L w) u) = (NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) ((Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) u)

The norm of an idele concentrated at one finite place. If w lies over v, the norm of the idele that is u at w and 1 elsewhere is the idele that is N_{L_w/K_v}(u) at v and 1 elsewhere.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNormMap_unitEmbedding (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : Lˣ) : (ideleNormMap K L) ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers L) L) x) = (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) ((Algebra.normUnits K) x)

The norm of a principal idele is the principal idele of the norm of L / K.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNormMap_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : (ideleNormMap K L) ((ideleExtension K L) x) = x ^ Module.finrank K L

The norm of an idele extended from K is its [L : K]-th power.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNormMap_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : (ideleNormMap K L).comp (ideleNormMap L M) = ideleNormMap K M

Norm maps of ideles compose in a tower of number fields.

theorem TauCeti.GlobalNumberFields.principalSubgroup_le_comap_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers L) L ≤ Subgroup.comap (ideleNormMap K L).toMonoidHom (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K)

The norm map of ideles sends principal ideles to principal ideles.

noncomputable def TauCeti.GlobalNumberFields.ideleClassNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleClassGroup (NumberField.RingOfIntegers L) L →ₜ* NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K

The norm map of idele classes N_{L/K} : C_L →ₜ* C_K, induced by the norm map of ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_mk {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) : (ideleClassNormMap K L) ↑x = ↑((ideleNormMap K L) x)

On an idele class, the norm is represented by the norm of a representing idele.

theorem TauCeti.GlobalNumberFields.range_ideleClassNormMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : (ideleClassNormMap K L).range = Subgroup.map (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K)) (ideleNormMap K L).range

The idele-class norm group is the image of the idele norm group: N_{L/K}(C_L) is the image of N_{L/K}(𝕀_L) under the quotient map 𝕀_K → C_K.

theorem TauCeti.GlobalNumberFields.index_range_ideleClassNormMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : (ideleClassNormMap K L).range.index = (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K ⊔ (ideleNormMap K L).range).index

The index of the idele-class norm group: the index of N_{L/K}(C_L) in C_K is the index of Kˣ · N_{L/K}(𝕀_L), the subgroup generated by the principal ideles and the idele norms, in 𝕀_K.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_ofCompletion {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [w.LiesOver v] (u : w.Completionˣ) : (ideleClassNormMap K L) ((NumberField.IdeleClassGroup.ofCompletion (NumberField.RingOfIntegers L) L w) u) = (NumberField.IdeleClassGroup.ofCompletion (NumberField.RingOfIntegers K) K v) ((Algebra.normUnits v.Completion) u)

The norm of an idele class concentrated at one infinite place. If w lies over v, the norm of the class of the idele that is u at w is the class of the idele that is N_{L_w/K_v}(u) at v.

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_ofAdicCompletion {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)ˣ) : (ideleClassNormMap K L) ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers L) L w) u) = (NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) ((Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) u)

The norm of an idele class concentrated at one finite place. If w lies over v, the norm of the class of the idele that is u at w is the class of the idele that is N_{L_w/K_v}(u) at v.

instance TauCeti.GlobalNumberFields.normal_range_ideleClassNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : (↑(ideleClassNormMap K L)).range.Normal

The idele-class norm group N_{L/K}(C_L) is normal in C_K, which is commutative, so the norm quotient C_K / N_{L/K}(C_L) is a group.

theorem TauCeti.GlobalNumberFields.continuous_ideleClassNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Continuous ⇑(ideleClassNormMap K L)

The relative norm on idele classes is continuous for the quotient topology.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_ideleClassExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (ideleClassNormMap K L) ((ideleClassExtension K L) x) = x ^ Module.finrank K L

The norm of an idele class extended from K is its [L : K]-th power.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassNormMap_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : (ideleClassNormMap K L).comp (ideleClassNormMap L M) = ideleClassNormMap K M

Norm maps of idele classes compose in a tower of number fields.

theorem TauCeti.GlobalNumberFields.range_ideleClassNormMap_le_of_algHom {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {M : Type u_3} [Field M] [NumberField M] [Algebra K M] (f : L →ₐ[K] M) : (↑(ideleClassNormMap K M)).range ≤ (↑(ideleClassNormMap K L)).range

A larger extension has a smaller idele-class norm group: if f : L →ₐ[K] M, then N_{M/K}(C_M) ≤ N_{L/K}(C_L). Through f, M is an extension of L, and N_{M/K} = N_{L/K} ∘ N_{M/L}.

theorem TauCeti.GlobalNumberFields.range_ideleClassNormMap_eq_of_algEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {M : Type u_3} [Field M] [NumberField M] [Algebra K M] (e : L ≃ₐ[K] M) : (↑(ideleClassNormMap K L)).range = (↑(ideleClassNormMap K M)).range

K-isomorphic extensions have the same idele-class norm group: if e : L ≃ₐ[K] M, then N_{L/K}(C_L) = N_{M/K}(C_M).