The norm quotient of the idele class group

The idele class norm ‖·‖ : C_K → ℝ>0 of a number field K has a continuous homomorphic section. Fix an infinite place w of K, with multiplicity m_w ∈ {1, 2}. The idele whose w-coordinate is the positive real number t ^ (1 / m_w) and whose other coordinates are 1 (TauCeti.GlobalNumberFields.ideleNormSection) has idele norm t, because the normalized absolute value at w is |·| ^ m_w; its class is a section of the idele class norm.

A continuous map with a continuous right inverse is a quotient map, and a quotient homomorphism of topological groups is open. So the idele norm and the idele class norm are open quotient maps, and the topological first isomorphism theorem identifies the norm quotient C_K / C_K¹ with ℝ>0 as a topological group. This refines the non-compactness of the full idele class group (TauCeti.GlobalNumberFields.IdeleClassGroup.noncompactSpace), in contrast to the compact norm-one idele class group C_K¹. The section also splits the idele class group as a topological group: C_K ≃ C_K¹ × ℝ>0.

Main definitions

• TauCeti.GlobalNumberFields.ideleClassNormSection: the continuous section of the idele class norm at an infinite place, the class of TauCeti.GlobalNumberFields.ideleNormSection.
• TauCeti.GlobalNumberFields.quotientNormOneEquiv: the isomorphism of topological groups C_K / C_K¹ ≃ₜ* ℝ>0 induced by the idele class norm.
• TauCeti.GlobalNumberFields.normOneProdEquiv: the splitting C_K ≃ₜ* C_K¹ × ℝ>0 determined by an infinite place, an instance of ContinuousMulEquiv.kerProdOfRightInverse.

Main results

• TauCeti.GlobalNumberFields.ideleClassNorm_ideleClassNormSection: the section is right inverse to the idele class norm.
• TauCeti.GlobalNumberFields.isOpenQuotientMap_ideleNorm and TauCeti.GlobalNumberFields.isOpenQuotientMap_ideleClassNorm: the norms are open quotient maps.
• TauCeti.GlobalNumberFields.quotientNormOneEquiv_mk: the norm quotient isomorphism is induced by the idele class norm.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.

The section at one infinite place

noncomputable def TauCeti.GlobalNumberFields.ideleClassNormSection (K : Type u_1) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) : NNRealˣ →ₜ* NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K

The continuous section of the idele class norm at the infinite place w: the class of ideleNormSection K w t.

theorem TauCeti.GlobalNumberFields.ideleClassNormSection_apply {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (t : NNRealˣ) : (ideleClassNormSection K w) t = ↑((ideleNormSection K w) t)

The section of the idele class norm at w is the class of the section of the idele norm.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassNorm_ideleClassNormSection {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (t : NNRealˣ) : ideleClassNorm ((ideleClassNormSection K w) t) = t

The section is right inverse to the idele class norm.

The norms are open quotient maps

theorem TauCeti.GlobalNumberFields.isOpenQuotientMap_ideleNorm {K : Type u_1} [Field K] [NumberField K] : IsOpenQuotientMap ⇑ideleNorm

The idele norm is an open quotient map onto ℝ>0: it has a continuous section.

theorem TauCeti.GlobalNumberFields.isOpenQuotientMap_ideleClassNorm {K : Type u_1} [Field K] [NumberField K] : IsOpenQuotientMap ⇑ideleClassNorm

The idele class norm is an open quotient map onto ℝ>0: it has a continuous section.

The norm quotient

noncomputable def TauCeti.GlobalNumberFields.quotientNormOneEquiv (K : Type u_1) [Field K] [NumberField K] : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸ IdeleClassGroup.normOne K ≃ₜ* NNRealˣ

The norm quotient of the idele class group is ℝ>0: the idele class norm induces an isomorphism of topological groups C_K / C_K¹ ≃ₜ* ℝ>0.

@[simp]

theorem TauCeti.GlobalNumberFields.quotientNormOneEquiv_mk {K : Type u_1} [Field K] [NumberField K] (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (quotientNormOneEquiv K) ↑c = ideleClassNorm c

The norm quotient isomorphism sends the class of an idele class to its idele class norm.

The splitting C_K ≃ C_K¹ × ℝ>0

noncomputable def TauCeti.GlobalNumberFields.normOneProdEquiv {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ≃ₜ* ↥(IdeleClassGroup.normOne K) × NNRealˣ

The idele class group splits as C_K¹ × ℝ>0. The infinite place w determines the isomorphism of topological groups sending an idele class c to its norm-one part c · s(‖c‖)⁻¹ and its norm ‖c‖, where s = ideleClassNormSection K w.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_normOneProdEquiv_fst {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ↑((normOneProdEquiv w) c).1 = c * ((ideleClassNormSection K w) (ideleClassNorm c))⁻¹

The norm-one component of the splitting at w is c · s(‖c‖)⁻¹.

@[simp]

theorem TauCeti.GlobalNumberFields.normOneProdEquiv_snd {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ((normOneProdEquiv w) c).2 = ideleClassNorm c

The ℝ>0 component of the splitting is the idele class norm.

@[simp]

theorem TauCeti.GlobalNumberFields.normOneProdEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (p : ↥(IdeleClassGroup.normOne K) × NNRealˣ) : (normOneProdEquiv w).symm p = ↑p.1 * (ideleClassNormSection K w) p.2

The inverse of the splitting multiplies a norm-one idele class by the section at w.