Openness of idele norms and finite index of idele-class norms

Let L/K be a finite extension of number fields. The idele norm group N_{L/K}(I_L) contains an idele congruence subgroup of I_K (exists_ideleCongruenceSubgroup_le_range_ideleNormMap), so it is open (isOpen_range_ideleNormMap). Its image N_{L/K}(C_L) in the idele class group therefore contains a ray subgroup (exists_raySubgroup_le_range_ideleClassNormMap): the conductor of L/K exists. Hence N_{L/K}(C_L) is open (isOpen_range_ideleClassNormMap) and, the ray class groups being finite, of finite index in C_K (finiteIndex_range_ideleClassNormMap). No Galois hypothesis is needed.

The modulus is read off the placewise norm criterion mem_range_ideleNormMap_iff. At a finite place unramified in L, every unit of K_v is a norm from K_v ⊗[K] L (TauCeti.exists_unit_preimages_of_isUnramifiedAt). At each of the finitely many ramified places, and at the infinite places, an [L : K]-th power is a norm, and the [L : K]-th powers contain the units congruent to one to a sufficient level (TauCeti.isOpen_range_powMonoidHom), the positive real numbers and all complex numbers. A modulus deep enough at the ramified places and divisible by every real place therefore works.

These are the topological facts about norm groups through which the global class-field correspondence is stated on the open subgroups of finite index of C_K.

Main results

• TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_le_range_ideleNormMap: the idele norm group contains an idele congruence subgroup.
• TauCeti.GlobalNumberFields.isOpen_range_ideleNormMap: the idele norm group is open.
• TauCeti.GlobalNumberFields.exists_raySubgroup_le_range_ideleClassNormMap: the idele-class norm group contains a ray subgroup.
• TauCeti.GlobalNumberFields.isOpen_range_ideleClassNormMap and TauCeti.GlobalNumberFields.finiteIndex_range_ideleClassNormMap: the idele-class norm group is open and of finite index.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §§1 and 2.

theorem TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_le_range_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ∃ (𝔪 : Modulus K), ideleCongruenceSubgroup 𝔪 ≤ (ideleNormMap K L).range

The idele norm group contains an idele congruence subgroup. For a finite extension L/K of number fields there is a modulus 𝔪 of K such that every idele of K congruent to one modulo 𝔪, and a unit at every finite place, is the norm of an idele of L.

theorem TauCeti.GlobalNumberFields.isOpen_range_ideleNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : IsOpen ↑(ideleNormMap K L).range

The idele norm group is open.

theorem TauCeti.GlobalNumberFields.exists_raySubgroup_le_range_ideleClassNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ∃ (𝔪 : Modulus K), raySubgroup 𝔪 ≤ (ideleClassNormMap K L).range

The idele-class norm group contains a ray subgroup. For a finite extension L/K of number fields there is a modulus 𝔪 of K whose ray subgroup lies in N_{L/K}(C_L); classically, the conductor of L/K exists.

theorem TauCeti.GlobalNumberFields.isOpen_range_ideleClassNormMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : IsOpen ↑(ideleClassNormMap K L).range

The idele-class norm group is open.

theorem TauCeti.GlobalNumberFields.finiteIndex_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.FiniteIndex

The idele-class norm group has finite index, since it contains a ray subgroup, whose index is the order of the finite ray class group.