Global existence

Let K be a number field. This file proves the global existence theorem: every open subgroup of finite index of the idele class group C_K is the norm subgroup of a finite abelian extension of K (globalAbelianExistence), and in particular of some finite Galois extension (globalExistence).

The proof is the induction on the index of Milne, Class Field Theory, VII, Theorem 9.5, run in the idele-class formation globalFormation K through ClassFormation.exists_abelianLayer_normSubgroup_eq_of_forall_prime. Its level at an open subgroup W of G_K is the idele class group C_F of the fixed field F of W (ideleClassLevelEquiv), and the norms between levels are the idele-class norms (levelNorm_ideleClassLevelEquiv). The admissible subgroups of a level are those that are open in C_F; they are closed under enlargement and, the idele-class norms being continuous, under preimages by norms. It remains to supply the Kummer case at every level: given a prime p and an open subgroup W with fixed field F, pass to the open subgroup W' fixing E = F(ζ_p), where ζ_p is a primitive p-th root of unity in Kˢ. An open subgroup of C_E containing the p-th powers is the norm subgroup of an abelian extension M/E (exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem, Milne VII, Lemma 9.3). Embedding M into Kˢ over E (exists_intermediateField_range_ideleClassNormMap_eq_of_pow_mem), its norm group is the image of the norm from the level of the open subgroup fixing the image of M.

Main results

• TauCeti.ClassFieldTheory.globalAbelianExistence: every open subgroup of finite index of C_K is the norm subgroup of an abelian layer of G_K.
• TauCeti.ClassFieldTheory.globalExistence: its forgetful form.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §9, Lemma 9.3 and Theorem 9.5.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.

Open subgroups of the levels

The Kummer case at every level

Global existence

theorem TauCeti.ClassFieldTheory.globalAbelianExistence {K : Type} [Field K] [NumberField K] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (hN : IsOpen ↑N) [N.FiniteIndex] : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), V.IsAbelianClassFieldLayer ∧ globalNormSubgroup K V = N

Global existence (Milne VII, Theorem 9.5). For a number field K, every open subgroup of finite index of the idele class group C_K is the norm subgroup of a finite abelian extension of K.

theorem TauCeti.ClassFieldTheory.globalExistence {K : Type} [Field K] [NumberField K] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (hN : IsOpen ↑N) [N.FiniteIndex] : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), globalNormSubgroup K V = N

Global existence, forgetful form. Every open subgroup of finite index of C_K is the norm subgroup of some open normal subgroup of G_K, not necessarily an abelian layer. By norm limitation, replacing a layer by its maximal abelian sublayer does not change its norm subgroup.