The Kummer case of global existence

Let K be a number field containing the p-th roots of unity for a prime p. This file proves the Kummer case of the global existence theorem (Milne, Class Field Theory, VII, Lemma 9.3): every open subgroup N of the idele class group C_K containing the p-th powers is the norm subgroup of a finite abelian extension of K (exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem).

The proof uses an auxiliary Kummer extension: the Kummer field M = K(U_S^{1/p}) of the S-units, cut out by the Kummer layer kummerLayer p (S.unit K), for a finite set S of finite places containing the places above p and generating the ideal class group. Its norm subgroup is contained in N but need not equal it. Write E_S for the Kummer idele subgroup auxiliaryKummerIdeleSubgroup S ∅ p of ideles that are p-th powers at S and at every infinite place and units elsewhere. Then:

• the norm subgroup of M/K is the image of E_S in C_K (globalNormSubgroup_kummerLayer_sUnits). The image of E_S consists of norms, since M/K has exponent p and is unramified outside S, and both subgroups have index p ^ (#S + r₁ + r₂): the image of E_S by the product formula and the S-unit theorem, and the norm subgroup by the norm index theorem [C_K : N_{M/K}(C_M)] = [M : K] together with the Kummer degree of M;
• an open subgroup N contains a ray subgroup, so once S also contains the finite part of its modulus, every element of E_S is a p-th power times an idele of that ray subgroup, and N ⊇ C_Kᵖ contains the image of E_S (auxiliaryKummerIdeleClassSubgroup_le_of_raySubgroup_le).

Hence N contains the norm subgroup of M/K, and upward closure of global norm subgroups (exists_abelianLayer_globalNormSubgroup_eq_of_le) realizes N itself as a norm subgroup.

Together with descent along K(ζ_p)/K and the induction on the index of ClassFormation.exists_abelianLayer_normSubgroup_eq_of_forall_prime, this is the arithmetic input of the global existence theorem.

Main results

• TauCeti.ClassFieldTheory.globalNormSubgroup_kummerLayer_sUnits: the norm subgroup of K(U_S^{1/p})/K is the image of E_S.
• TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem: the Kummer case of global existence.
• TauCeti.ClassFieldTheory.exists_intermediateField_range_ideleClassNormMap_eq_of_pow_mem: the realization of an open subgroup containing the p-th powers as the idele-class norm range of a finite subextension of a separably closed field over K.

References

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

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_kummerLayer_sUnits {K : Type} [Field K] [NumberField K] {p : ℕ} [Fact (Nat.Prime p)] [HasEnoughRootsOfUnity K p] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hcl : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' ↑S) = ⊤) (hpS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑p ∈ v.asIdeal → v ∈ S) : globalNormSubgroup K (kummerLayer p ((↑S).unit K)) = auxiliaryKummerIdeleClassSubgroup S ∅ p

The norm subgroup of the Kummer field of the S-units (Milne VII, Lemma 9.3). Let K contain the p-th roots of unity, and let S be a finite set of finite places containing the places above p and generating the ideal class group. Then the idele-class norm group of K(U_S^{1/p})/K is the image in C_K of the Kummer idele subgroup E_S of ideles that are p-th powers at S and at every infinite place and units elsewhere.

theorem TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem {K : Type} [Field K] [NumberField K] {p : ℕ} [Fact (Nat.Prime p)] [HasEnoughRootsOfUnity K p] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (hN : IsOpen ↑N) (hpow : ∀ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K), c ^ p ∈ N) : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), V.IsAbelianClassFieldLayer ∧ globalNormSubgroup K V = N

The Kummer case of global existence (Milne VII, Lemma 9.3). Let K be a number field containing the p-th roots of unity for a prime p. Every open subgroup of the idele class group C_K containing the p-th powers is the norm subgroup of a finite abelian extension of K.

theorem TauCeti.ClassFieldTheory.exists_intermediateField_range_ideleClassNormMap_eq_of_pow_mem {p : ℕ} [Fact (Nat.Prime p)] {E Ω : Type} [Field E] [NumberField E] [Field Ω] [Algebra E Ω] [IsSepClosed Ω] [HasEnoughRootsOfUnity E p] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers E) E)} (hN : IsOpen ↑N) (hpow : ∀ (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers E) E), c ^ p ∈ N) : ∃ (L : IntermediateField E Ω) (x : NumberField ↥L), (↑(GlobalNumberFields.ideleClassNormMap E ↥L)).range = N

The Kummer case of global existence in a separably closed field. Let E be a number field containing the p-th roots of unity for a prime p, and Ω a separably closed field over E. Every open subgroup of C_E containing the p-th powers is the idele-class norm group of a finite subextension of Ω/E: the image of an E-embedding into Ω of the class field given by exists_abelianLayer_globalNormSubgroup_eq_of_pow_mem.