Norm limitation and uniqueness for global norm subgroups

Let K be a number field. Global reciprocity, in the form of the global class formation globalClassFormation K, controls which open normal subgroups of G_K a global norm subgroup N_{L/K}(C_L) ≤ C_K can see:

• norm limitation (globalNormSubgroup_maximalAbelianLayer): a finite Galois extension L/K and its maximal abelian subextension have the same idele-class norm group;
• for an abelian layer W, inclusion of norm subgroups is equivalent to inclusion of the layer subgroups (globalNormSubgroup_le_iff_of_isAbelian); for concrete extensions L/K Galois and M/K abelian this says that N_{L/K}(C_L) ≤ N_{M/K}(C_M) exactly when M embeds in L over K (range_ideleClassNormMap_le_iff_nonempty_algHom);
• uniqueness (globalClassField_unique): two finite abelian extensions of K with the same idele-class norm group are equal.

These are the norm-subgroup laws of an arbitrary class formation (ClassFormation.normSubgroup_maximalAbelianLayer, ClassFormation.normSubgroup_le_iff_of_isAbelian) applied to the global class formation and read on C_K through globalGroundOrderIso.

Main results

• TauCeti.ClassFieldTheory.globalNormSubgroup_maximalAbelianLayer: norm limitation.
• TauCeti.ClassFieldTheory.globalNormSubgroup_le_iff_of_isAbelian: norm subgroups detect the order on abelian layers.
• TauCeti.ClassFieldTheory.range_ideleClassNormMap_le_iff_nonempty_algHom: idele-class norm groups detect embeddings of finite abelian extensions.
• TauCeti.ClassFieldTheory.globalClassField_unique: a finite abelian extension is determined by its idele-class norm group.

References

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

@[simp]

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_maximalAbelianLayer (K : Type) [Field K] [NumberField K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : globalNormSubgroup K V.maximalAbelianLayer = globalNormSubgroup K V

Global norm limitation. A finite Galois extension of a number field and its maximal abelian subextension have the same idele-class norm group.

theorem TauCeti.ClassFieldTheory.globalNormSubgroup_le_iff_of_isAbelian {K : Type} [Field K] [NumberField K] {V W : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hW : W.IsAbelianClassFieldLayer) : globalNormSubgroup K V ≤ globalNormSubgroup K W ↔ V ≤ W

For a finite abelian layer W and any finite layer V of a number field, inclusion of global norm subgroups is equivalent to inclusion of the layer subgroups. On class fields the latter inclusion is reversed.

theorem TauCeti.ClassFieldTheory.globalClassField_unique {K : Type} [Field K] [NumberField K] {V W : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : V.IsAbelianClassFieldLayer) (hW : W.IsAbelianClassFieldLayer) (h : globalNormSubgroup K V = globalNormSubgroup K W) : V = W

Uniqueness of finite abelian global class fields. Two abelian layers of a number field with the same idele-class norm group are equal. The abelianity hypotheses are essential: by norm limitation, every layer has the norm group of its maximal abelian sublayer.

theorem TauCeti.ClassFieldTheory.range_ideleClassNormMap_le_iff_nonempty_algHom {K : Type} [Field K] [NumberField K] (L : Type u_1) (M : Type u_2) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [Field M] [NumberField M] [Algebra K M] [IsAbelianGalois K M] : (↑(GlobalNumberFields.ideleClassNormMap K L)).range ≤ (↑(GlobalNumberFields.ideleClassNormMap K M)).range ↔ Nonempty (M →ₐ[K] L)

Idele-class norm groups detect embeddings of abelian extensions. For finite extensions L/K Galois and M/K abelian, N_{L/K}(C_L) ≤ N_{M/K}(C_M) exactly when M embeds in L over K. This is globalNormSubgroup_le_iff_of_isAbelian read on the fields cut out by the two layers.