The norm of the idele-class formation

Let K be a number field, V an open normal subgroup of G_K and E its fixed field, a finite Galois subextension of Kˢ/K. The layer V ◁ G_K of the idele-class formation globalFormation K has top level C_E and ground level C_K (ideleClassLevelEquiv, globalGroundEquiv). This file shows that its norm, the sum of the Galois conjugates, is the norm map of idele classes N_{E/K} : C_E → C_K (norm_ideleClassLevelEquiv). Hence the norm subgroup of the layer is the idele-class norm group N_{E/K}(C_E) (globalGroundEquiv_mem_normSubgroup_iff), and its norm quotient is C_K / N_{E/K}(C_E) (globalNormQuotientEquiv). For a finite Galois extension L/K given abstractly, the layer of fixingOpenNormalSubgroup K L has fixed field the image E of any K-embedding of L, and E has the same idele-class norm group as L, so its norm quotient is C_K / N_{L/K}(C_L) (globalLayerNormQuotientEquiv).

The norm of the layer is computed on an idele a of E: by Formation.levelNorm_top_apply_coe it is the sum of the translates of the class of a by coset representatives of V, which act through their restrictions to E; these restrictions run through Gal(E/K) once each (TauCeti.prod_restrictNormal_out). The product of the Galois conjugates of a is the idele norm N_{E/K}(a) extended back to E (TauCeti.GlobalNumberFields.ideleExtension_ideleNormMap).

More generally, let W' ≤ W be any open subgroups of G_K, with fixed fields F ⊆ L; neither W' need be normal in W nor L/F normal. The levels of W and W' are C_F and C_L (ideleClassLevelEquiv), and the norm Formation.levelNorm between them is the norm map of idele classes N_{L/F} : C_L → C_F (levelNorm_ideleClassLevelEquiv). The cosets of W' in W are the F-embeddings of L into Kˢ, so N_{L/F}(y) is the product of the translates of y ∈ L by their representatives (TauCeti.coe_norm_eq_prod_quotient_out); read in the normal closure M of L/K, this product formula transfers to the ideles of L (TauCeti.GlobalNumberFields.ideleExtension_ideleNormMap_of_algebraMap_norm_eq_prod), which is the identity of the two norms. This is the form in which norms from finite extensions that are not Galois, such as the extension cut out by an open subgroup of G_K that is not normal, are read on idele class groups.

In particular, for an arbitrary layer V ◁ U of globalFormation K, whose ground subgroup U is any open subgroup of G_K, with fixed fields F and L, the norm of the layer is N_{L/F} : C_L → C_F (NormalLayer.norm_ideleClassLevelEquiv), and its norm quotient is C_F / N_{L/F}(C_L) (NormalLayer.ideleClassNormQuotientEquiv). This is the form in which statements about the layers of prime degree inside a given layer, whose ground fields need not be K, are read on number fields.

This identifies the abstract norm quotient that the class formation axioms and the Artin map are stated on with the concrete quotient C_K / N_{E/K}(C_E) that the fundamental inequalities and global reciprocity are about.

Main definitions

• TauCeti.ClassFieldTheory.globalNormQuotientEquiv: the norm quotient of the layer of E is C_K / N_{E/K}(C_E).
• TauCeti.ClassFieldTheory.globalLayerNormQuotientEquiv: the norm quotient of the layer of a finite Galois extension L/K is C_K / N_{L/K}(C_L).
• TauCeti.ClassFieldTheory.NormalLayer.ideleClassNormQuotientEquiv: the norm quotient of a layer whose ground and top subgroups have fixed fields F and L is C_F / N_{L/F}(C_L).

Main results

• TauCeti.ClassFieldTheory.norm_ideleClassLevelEquiv: the norm of the layer of E is the norm map of idele classes N_{E/K}.
• TauCeti.ClassFieldTheory.levelNorm_top_ideleClassLevelEquiv: the norm from the level of an open subgroup with fixed field E to the ground level is N_{E/K}.
• TauCeti.ClassFieldTheory.globalGroundEquiv_mem_normSubgroup_iff: an idele class of K lies in the norm subgroup of the layer of E exactly when it is a norm from C_E.
• TauCeti.ClassFieldTheory.globalGroundEquiv_mem_layerNormSubgroup_iff: the same for the layer of a finite Galois extension L/K and norms from C_L.
• TauCeti.ClassFieldTheory.levelNorm_ideleClassLevelEquiv: the norm between the levels of two open subgroups W' ≤ W with fixed fields F ⊆ L is the norm map of idele classes N_{L/F}.
• TauCeti.ClassFieldTheory.NormalLayer.norm_ideleClassLevelEquiv: the norm of a layer whose ground and top subgroups have fixed fields F and L is the norm map of idele classes N_{L/F}.
• TauCeti.ClassFieldTheory.NormalLayer.ideleClassLevelEquiv_mem_normSubgroup_iff: an idele class of F lies in the norm subgroup of such a layer exactly when it is a norm from C_L.

References

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

theorem TauCeti.ClassFieldTheory.norm_ideleClassLevelEquiv {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = E.toIntermediateField) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ((NormalLayer.ofOpenNormal V).norm (globalFormation K)) ((ideleClassLevelEquiv hV) (Additive.ofMul c)) = (NormalLayer.groundEquivOfOpenNormal (globalFormation K) V) ((globalGroundEquiv K) (Additive.ofMul ((GlobalNumberFields.ideleClassNormMap K ↥E.toIntermediateField) c)))

The norm of the idele-class formation is the idele-class norm: if the fixed field of the open normal subgroup V of G_K is E, then under the identifications of the top and ground levels of the layer V ◁ G_K with C_E and C_K, the norm of the layer is the norm map of idele classes N_{E/K} : C_E → C_K.

theorem TauCeti.ClassFieldTheory.levelNorm_top_ideleClassLevelEquiv {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {W : OpenSubgroup (AbsoluteGaloisGroup K)} (h : W ≤ ⊤) (hW : IntermediateField.fixedField ↑W = E.toIntermediateField) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ((globalFormation K).levelNorm h) ((ideleClassLevelEquiv hW) (Additive.ofMul c)) = (globalGroundEquiv K) (Additive.ofMul ((GlobalNumberFields.ideleClassNormMap K ↥E.toIntermediateField) c))

The norm to the ground level is the idele-class norm: if the fixed field of the open subgroup W of G_K is the finite Galois subextension E, then under the identifications of the levels of W and G_K with C_E and C_K, the norm from the level of W to the ground level is the norm map of idele classes N_{E/K} : C_E → C_K.

theorem TauCeti.ClassFieldTheory.globalGroundEquiv_mem_normSubgroup_iff {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = E.toIntermediateField) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (NormalLayer.groundEquivOfOpenNormal (globalFormation K) V) ((globalGroundEquiv K) (Additive.ofMul c)) ∈ (NormalLayer.ofOpenNormal V).normSubgroup (globalFormation K) ↔ c ∈ (↑(GlobalNumberFields.ideleClassNormMap K ↥E.toIntermediateField)).range

The norm subgroup of the layer of E is N_{E/K}(C_E): an idele class of K lies in the norm subgroup of the layer V ◁ G_K of the idele-class formation, where E is the fixed field of V, exactly when it is the norm of an idele class of E.

noncomputable def TauCeti.ClassFieldTheory.globalNormQuotientEquiv {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = E.toIntermediateField) : Additive (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸ (↑(GlobalNumberFields.ideleClassNormMap K ↥E.toIntermediateField)).range) ≃+ (NormalLayer.ofOpenNormal V).NormQuotient (globalFormation K)

The norm quotient of the layer of E is C_K / N_{E/K}(C_E): if the fixed field of the open normal subgroup V of G_K is E, then the identification globalGroundEquiv of C_K with the ground level of the layer V ◁ G_K of the idele-class formation descends to the quotients by N_{E/K}(C_E) and by the norm subgroup of the layer (globalGroundEquiv_mem_normSubgroup_iff).

@[simp]

theorem TauCeti.ClassFieldTheory.globalNormQuotientEquiv_mk {K : Type} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = E.toIntermediateField) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (globalNormQuotientEquiv E hV) (Additive.ofMul ↑c) = ((NormalLayer.ofOpenNormal V).normQuotientMk (globalFormation K)) ((NormalLayer.groundEquivOfOpenNormal (globalFormation K) V) ((globalGroundEquiv K) (Additive.ofMul c)))

globalNormQuotientEquiv E hV sends the class of c ∈ C_K to the class of c in the norm quotient of the layer.

theorem TauCeti.ClassFieldTheory.globalGroundEquiv_mem_layerNormSubgroup_iff (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (NormalLayer.groundEquivOfOpenNormal (globalFormation K) (fixingOpenNormalSubgroup K L)) ((globalGroundEquiv K) (Additive.ofMul c)) ∈ (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).normSubgroup (globalFormation K) ↔ c ∈ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The norm subgroup of the layer of L is N_{L/K}(C_L): for a finite Galois extension L/K, an idele class of K lies in the norm subgroup of the layer of fixingOpenNormalSubgroup K L exactly when it is the norm of an idele class of L. The fixed field of the layer is the image E of a K-embedding of L into Kˢ, and E and L have the same idele-class norm group (range_ideleClassNormMap_eq_of_algEquiv).

noncomputable def TauCeti.ClassFieldTheory.globalLayerNormQuotientEquiv (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Additive (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸ (↑(GlobalNumberFields.ideleClassNormMap K L)).range) ≃+ (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).NormQuotient (globalFormation K)

The norm quotient of the layer of L is C_K / N_{L/K}(C_L): for a finite Galois extension L/K, the identification globalGroundEquiv of C_K with the ground level of the layer of fixingOpenNormalSubgroup K L in the idele-class formation descends to the quotients by N_{L/K}(C_L) and by the norm subgroup of the layer (globalGroundEquiv_mem_layerNormSubgroup_iff).

@[simp]

theorem TauCeti.ClassFieldTheory.globalLayerNormQuotientEquiv_mk {K : Type} [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (globalLayerNormQuotientEquiv K L) (Additive.ofMul ↑c) = ((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).normQuotientMk (globalFormation K)) ((NormalLayer.groundEquivOfOpenNormal (globalFormation K) (fixingOpenNormalSubgroup K L)) ((globalGroundEquiv K) (Additive.ofMul c)))

globalLayerNormQuotientEquiv K L sends the class of c ∈ C_K to the class of c in the norm quotient of the layer.

Arbitrary layers

theorem TauCeti.ClassFieldTheory.levelNorm_ideleClassLevelEquiv {K : Type} [Field K] [NumberField K] {F L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥L] [Algebra ↥F ↥L] [IsScalarTower (↥F) (↥L) (SeparableClosure K)] {W W' : OpenSubgroup (AbsoluteGaloisGroup K)} (h : W' ≤ W) (hF : IntermediateField.fixedField ↑W = F) (hL : IntermediateField.fixedField ↑W' = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥L) ↥L) : ((globalFormation K).levelNorm h) ((ideleClassLevelEquiv hL) (Additive.ofMul c)) = (ideleClassLevelEquiv hF) (Additive.ofMul ((GlobalNumberFields.ideleClassNormMap ↥F ↥L) c))

The norm between two levels of the idele-class formation is the idele-class norm: if the open subgroups W' ≤ W of G_K have fixed fields F ⊆ L, then under the identifications of the levels of W and W' with C_F and C_L (ideleClassLevelEquiv), the norm Formation.levelNorm from the level of W' to that of W is the norm map of idele classes N_{L/F} : C_L → C_F. The extension L/F need not be normal, nor W' normal in W.

theorem TauCeti.ClassFieldTheory.NormalLayer.norm_ideleClassLevelEquiv {K : Type} [Field K] [NumberField K] {F L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥L] [Algebra ↥F ↥L] [IsScalarTower (↥F) (↥L) (SeparableClosure K)] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hF : IntermediateField.fixedField ↑Lay.ground = F) (hL : IntermediateField.fixedField ↑Lay.top = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥L) ↥L) : (Lay.norm (globalFormation K)) ((ideleClassLevelEquiv hL) (Additive.ofMul c)) = (ideleClassLevelEquiv hF) (Additive.ofMul ((GlobalNumberFields.ideleClassNormMap ↥F ↥L) c))

The norm of an arbitrary layer of the idele-class formation is the idele-class norm: if the ground and top subgroups of a layer V ◁ U of globalFormation K have fixed fields F and L, then under the identifications of its ground and top levels with C_F and C_L (ideleClassLevelEquiv), the norm of the layer is the norm map of idele classes N_{L/F} : C_L → C_F.

theorem TauCeti.ClassFieldTheory.NormalLayer.ideleClassLevelEquiv_mem_normSubgroup_iff {K : Type} [Field K] [NumberField K] {F L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥L] [Algebra ↥F ↥L] [IsScalarTower (↥F) (↥L) (SeparableClosure K)] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hF : IntermediateField.fixedField ↑Lay.ground = F) (hL : IntermediateField.fixedField ↑Lay.top = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥F) ↥F) : (ideleClassLevelEquiv hF) (Additive.ofMul c) ∈ Lay.normSubgroup (globalFormation K) ↔ c ∈ (↑(GlobalNumberFields.ideleClassNormMap ↥F ↥L)).range

The norm subgroup of an arbitrary layer is N_{L/F}(C_L): if the ground and top subgroups of a layer of globalFormation K have fixed fields F and L, an idele class of F lies in the norm subgroup of the layer exactly when it is the norm of an idele class of L.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.ideleClassNormQuotientEquiv {K : Type} [Field K] [NumberField K] {F L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥L] [Algebra ↥F ↥L] [IsScalarTower (↥F) (↥L) (SeparableClosure K)] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hF : IntermediateField.fixedField ↑Lay.ground = F) (hL : IntermediateField.fixedField ↑Lay.top = L) : Additive (NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥F) ↥F ⧸ (↑(GlobalNumberFields.ideleClassNormMap ↥F ↥L)).range) ≃+ Lay.NormQuotient (globalFormation K)

The norm quotient of an arbitrary layer is C_F / N_{L/F}(C_L): if the ground and top subgroups of a layer of globalFormation K have fixed fields F and L, the identification ideleClassLevelEquiv of C_F with the ground level descends to the quotients by N_{L/F}(C_L) and by the norm subgroup of the layer.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.ideleClassNormQuotientEquiv_mk {K : Type} [Field K] [NumberField K] {F L : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [NumberField ↥L] [Algebra ↥F ↥L] [IsScalarTower (↥F) (↥L) (SeparableClosure K)] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hF : IntermediateField.fixedField ↑Lay.ground = F) (hL : IntermediateField.fixedField ↑Lay.top = L) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ↥F) ↥F) : (Lay.ideleClassNormQuotientEquiv hF hL) (Additive.ofMul ↑c) = (Lay.normQuotientMk (globalFormation K)) ((ideleClassLevelEquiv hF) (Additive.ofMul c))

ideleClassNormQuotientEquiv sends the class of c ∈ C_F to the class of c in the norm quotient of the layer.