Global norm subgroups

Let K be a number field. An open normal subgroup V of the absolute Galois group G_K cuts out the finite Galois extension classField K V of K. This file attaches to V its norm subgroup in the idele class group C_K: the norm subgroup of the layer V ◁ G_K of the idele-class formation globalFormation K, read on C_K through the identification globalGroundEquiv of C_K with the ground level. It is the idele-class norm group N_{E/K}(C_E) of the class field E (globalNormSubgroup_eq_range_classField, globalNormSubgroup_eq_range), and of any finite Galois extension L/K whose layer is V (globalNormSubgroup_fixingOpenNormalSubgroup).

The idele-class norm group is open and of finite index (TauCeti.GlobalNumberFields.isOpen_range_ideleClassNormMap, TauCeti.GlobalNumberFields.finiteIndex_range_ideleClassNormMap), so global norm subgroups are open subgroups of finite index of C_K, the objects on which the global class-field correspondence is stated. Transitivity of the formation norm makes the construction monotone in V, so it reverses inclusion of class fields, and the layer G_K itself, which cuts out K, has norm subgroup C_K.

Main definitions

• TauCeti.ClassFieldTheory.globalNormSubgroup: the norm subgroup of C_K cut out by an open normal subgroup of G_K.
• TauCeti.ClassFieldTheory.globalGroundOrderIso: subgroups of C_K are the subgroups of the ground level of the idele-class formation; it carries globalNormSubgroup K V to the norm subgroup of the layer V (globalGroundOrderIso_globalNormSubgroup).

Main results

• TauCeti.ClassFieldTheory.globalNormSubgroup_eq_range_classField: it is N_{E/K}(C_E) for the class field E = classField K V.
• TauCeti.ClassFieldTheory.globalNormSubgroup_eq_range: the same for any finite Galois subextension E of Kˢ/K given as the fixed field of V.
• TauCeti.ClassFieldTheory.globalNormSubgroup_fixingOpenNormalSubgroup: the layer of a finite Galois extension L/K has norm subgroup N_{L/K}(C_L).
• TauCeti.ClassFieldTheory.isOpen_globalNormSubgroup: global norm subgroups are open.
• TauCeti.ClassFieldTheory.finiteIndex_globalNormSubgroup: global norm subgroups have finite index.
• TauCeti.ClassFieldTheory.globalNormSubgroup_mono: inclusion of layer subgroups gives inclusion of norm subgroups.
• TauCeti.ClassFieldTheory.globalNormSubgroup_top: the ground field has norm subgroup C_K.
• TauCeti.ClassFieldTheory.index_globalGroundOrderIso: the ground-level identification preserves the index of an idele-class subgroup.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §§2 and 6.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.

noncomputable def TauCeti.ClassFieldTheory.globalNormSubgroup (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)

The idele-class norm subgroup cut out by an open normal subgroup V of G_K: the norm subgroup of the layer V ◁ G_K of the idele-class formation, read on C_K through globalGroundEquiv. It is the idele-class norm group of the class field of V (globalNormSubgroup_eq_range).

theorem TauCeti.ClassFieldTheory.mem_globalNormSubgroup_iff {K : Type} [Field K] [NumberField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} {c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} : c ∈ globalNormSubgroup K V ↔ (NormalLayer.groundEquivOfOpenNormal (globalFormation K) V) ((globalGroundEquiv K) (Additive.ofMul c)) ∈ (NormalLayer.ofOpenNormal V).normSubgroup (globalFormation K)

An idele class lies in the global norm subgroup of V exactly when, read in the ground level of the layer V ◁ G_K, it lies in the norm subgroup of that layer.

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_eq_range {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = E.toIntermediateField) : globalNormSubgroup K V = (↑(GlobalNumberFields.ideleClassNormMap K ↥E.toIntermediateField)).range

The global norm subgroup of V is N_{E/K}(C_E) for any finite Galois subextension E of Kˢ/K that is the fixed field of V.

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_fixingOpenNormalSubgroup {K : Type} [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : globalNormSubgroup K (fixingOpenNormalSubgroup K L) = (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The global norm subgroup of the layer of L is N_{L/K}(C_L) for a finite Galois extension L/K.

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_eq_range_classField (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : globalNormSubgroup K V = (↑(GlobalNumberFields.ideleClassNormMap K ↥(classField K V))).range

The global norm subgroup of V is N_{E/K}(C_E) for the class field E of V.

instance TauCeti.ClassFieldTheory.normal_globalNormSubgroup (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : (globalNormSubgroup K V).Normal

The global norm subgroup of V is normal in the commutative group C_K, so the norm quotient C_K / N_{E/K}(C_E) is a group.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_globalNormSubgroup_iff_exists {K : Type} [Field K] [NumberField K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} {c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} : c ∈ globalNormSubgroup K V ↔ ∃ (d : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥(classField K V)) ↥(classField K V)), (GlobalNumberFields.ideleClassNormMap K ↥(classField K V)) d = c

An idele class lies in the global norm subgroup of V exactly when it is the norm of an idele class of the class field of V.

noncomputable def TauCeti.ClassFieldTheory.globalGroundOrderIso (K : Type) [Field K] [NumberField K] : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) ≃o Submodule ℤ ↥((globalFormation K).level ⊤)

Subgroups of C_K are the subgroups of the ground level of the idele-class formation. The level of the whole group G_K is C_K, written additively (globalGroundEquiv), so taking preimages along that identification is an order isomorphism. It carries the global norm subgroups to the norm subgroups of the idele-class formation (globalGroundOrderIso_globalNormSubgroup), which transports the laws of the norm subgroups of a class formation to C_K.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_globalGroundOrderIso {K : Type} [Field K] [NumberField K] {H : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} {a : ↥((globalFormation K).level ⊤)} : a ∈ (globalGroundOrderIso K) H ↔ Additive.toMul ((globalGroundEquiv K).symm a) ∈ H

An element of the ground level lies in the image of a subgroup H ≤ C_K under globalGroundOrderIso exactly when the corresponding idele class lies in H.

theorem TauCeti.ClassFieldTheory.index_globalGroundOrderIso (K : Type) [Field K] [NumberField K] (N : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) : ((globalGroundOrderIso K) N).toAddSubgroup.index = N.index

The ground-level order isomorphism preserves the index of every idele-class subgroup.

@[simp]

theorem TauCeti.ClassFieldTheory.globalGroundOrderIso_globalNormSubgroup (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : (globalGroundOrderIso K) (globalNormSubgroup K V) = (globalFormation K).normSubgroup V

globalGroundOrderIso carries the global norm subgroup of V to the norm subgroup of the layer V ◁ G_K of the idele-class formation.

theorem TauCeti.ClassFieldTheory.isOpen_globalNormSubgroup (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : IsOpen ↑(globalNormSubgroup K V)

Global norm subgroups are open.

theorem TauCeti.ClassFieldTheory.finiteIndex_globalNormSubgroup (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : (globalNormSubgroup K V).FiniteIndex

Global norm subgroups have finite index.

Order properties

Shrinking the layer subgroup V enlarges its class field, and a norm from a larger field is a norm from every intermediate field, so globalNormSubgroup K is monotone in V. The top layer G_K cuts out K itself, whose norm subgroup is all of C_K.

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_mono (K : Type) [Field K] [NumberField K] : Monotone (globalNormSubgroup K)

Global norm subgroups are monotone in the layer subgroup. If V ≤ W, then the class field of W is contained in that of V, and every norm from the larger field is a norm from the smaller field.

@[simp]

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_top (K : Type) [Field K] [NumberField K] : globalNormSubgroup K ⊤ = ⊤

The top layer has the whole idele class group as its norm subgroup. It cuts out the ground field itself, whose norm to itself is the identity. This pins the direction of the global class-field correspondence.