Upward closure and descent of global norm subgroups

Let K be a number field. This file proves the two inputs of global existence that come from global reciprocity alone, as opposed to the Kummer theory of S-units:

• upward closure (exists_abelianLayer_globalNormSubgroup_eq_of_le): a subgroup of C_K containing the norm subgroup of a finite Galois extension is the norm subgroup of a finite abelian extension. More generally, a subgroup containing the idele-class norm group N_{M/K}(C_M) of any finite extension M/K is such a norm subgroup (exists_abelianLayer_globalNormSubgroup_eq_of_range_ideleClassNormMap_le);
• descent along a finite extension (exists_abelianLayer_globalNormSubgroup_eq_of_comap_ideleClassNorm): if L/K is a finite extension and the preimage of N ≤ C_K under the idele-class norm N_{L/K} : C_L → C_K contains a norm subgroup over L, then N is the norm subgroup of a finite abelian extension of K.

Upward closure is the upward closure of the norm subgroups of any class formation (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_le), applied to the global class formation and read on C_K through globalGroundOrderIso. Descent follows by composing norms in the tower M/L/K: N_{M/K}(C_M) = N_{L/K}(N_{M/L}(C_M)) ≤ N.

In the proof of global existence by induction on the index, descent is applied to L = K(ζ_p) to reduce to fields containing the p-th roots of unity, where the Kummer case applies.

Main results

All in the namespace TauCeti.ClassFieldTheory:

• exists_abelianLayer_globalNormSubgroup_eq_of_le: upward closure of global norm subgroups.
• exists_abelianLayer_globalNormSubgroup_eq_of_range_ideleClassNormMap_le: upward closure from the idele-class norm group of any finite extension.
• exists_abelianLayer_globalNormSubgroup_eq_of_comap_ideleClassNorm: descent of norm subgroups along a finite extension.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §9 (Lemmas 9.1 and 9.4).
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.

theorem TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_le {K : Type} [Field K] [NumberField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (h : globalNormSubgroup K V ≤ N) : ∃ (W : OpenNormalSubgroup (AbsoluteGaloisGroup K)), W.IsAbelianClassFieldLayer ∧ globalNormSubgroup K W = N

Upward closure of global norm subgroups. For a number field K, a subgroup of C_K containing the norm subgroup of the finite Galois extension cut out by V is the norm subgroup of a finite abelian extension.

theorem TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_range_ideleClassNormMap_le {K : Type} [Field K] [NumberField K] {M : Type u_1} [Field M] [NumberField M] [Algebra K M] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (h : (↑(GlobalNumberFields.ideleClassNormMap K M)).range ≤ N) : ∃ (W : OpenNormalSubgroup (AbsoluteGaloisGroup K)), W.IsAbelianClassFieldLayer ∧ globalNormSubgroup K W = N

Upward closure from a finite extension. For a number field K, a subgroup of C_K containing the idele-class norm group N_{M/K}(C_M) of a finite extension M/K is the norm subgroup of a finite abelian extension. The extension M need not be Galois, nor lie in the separable closure: the normal closure of an embedding of M into Kˢ is a finite Galois extension with a smaller norm group.

theorem TauCeti.ClassFieldTheory.exists_abelianLayer_globalNormSubgroup_eq_of_comap_ideleClassNorm {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] {N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} {W : OpenNormalSubgroup (AbsoluteGaloisGroup L)} (h : globalNormSubgroup L W ≤ Subgroup.comap (↑(GlobalNumberFields.ideleClassNormMap K L)) N) : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), V.IsAbelianClassFieldLayer ∧ globalNormSubgroup K V = N

Descent of norm subgroups along a finite extension. Let L/K be an extension of number fields and N ≤ C_K. If the preimage of N under the idele-class norm N_{L/K} : C_L → C_K contains the norm subgroup of the layer W of G_L (in particular, if it is that norm subgroup), then N is the norm subgroup of a finite abelian extension of K.