The field cut out by an open normal subgroup of the absolute Galois group

Class field theory states its correspondences on the Galois side, as bijections between norm subgroups and open normal subgroups V of the absolute Galois group G_F = Gal(Fˢ/F). This file records, once, the dictionary that turns such a subgroup back into a field: the class field classField F V is the fixed field of V inside the separable closure Fˢ. Because G_F is taken at the separable closure, the fixed field of all of G_F is F itself, so no transport between closures intervenes.

By the infinite Galois correspondence the dictionary is faithful: the fixing subgroup of classField F V is V again, classField F V is a finite Galois extension of F whose Galois group is the finite quotient G_F ⧸ V, and every finite Galois subextension of Fˢ arises this way. Subgroup inclusion becomes reverse inclusion of fields, which is how an order-preserving correspondence on subgroups becomes the classical order-reversing correspondence on fields. Finally V is an abelian layer exactly when its class field is an abelian extension.

The same dictionary reads an arbitrary finite normal layer V ◁ U of G_F, whose ground U is any open subgroup: if E and L are the fixed fields of U and V, then L/E is Galois (NormalLayer.isGalois_of_fixedField) and restriction to L identifies the Galois group U ⧸ V of the layer with Gal(L/E) (NormalLayer.galEquivOfFixedField).

Main definitions

• TauCeti.ClassFieldTheory.classField F V: the fixed field of V in Fˢ.
• TauCeti.ClassFieldTheory.galClassFieldEquiv: the Galois group of classField F V over F is the Galois group of the finite normal layer V ◁ G_F.
• TauCeti.ClassFieldTheory.NormalLayer.galEquivOfFixedField: the Galois group of a finite normal layer V ◁ U is Gal(L/E) for the fixed fields E of U and L of V.

Main results

• TauCeti.ClassFieldTheory.fixingSubgroup_classField: the fixing subgroup of the class field of V is V.
• TauCeti.ClassFieldTheory.fixingOpenNormalSubgroup_classField: the bundled open normal subgroup cut out by the class field of V is V.
• TauCeti.ClassFieldTheory.classField_fixingOpenNormalSubgroup: conversely, the class field of the open normal subgroup fixing a finite Galois extension L/F is the image of L in Fˢ.
• TauCeti.ClassFieldTheory.classField_le_classField_iff: classField F W ≤ classField F V if and only if V ≤ W.
• TauCeti.ClassFieldTheory.exists_classField_eq_iff: the class fields are exactly the finite Galois subextensions of Fˢ.
• TauCeti.ClassFieldTheory.finrank_classField: the degree of the class field of V is the index of V.
• TauCeti.ClassFieldTheory.isAbelianGalois_classField_iff: the class field of V is abelian over F if and only if V is an abelian layer.
• TauCeti.ClassFieldTheory.isAbelianClassFieldLayer_fixingOpenNormalSubgroup: the open normal subgroup fixing a finite abelian extension of F is an abelian layer.
• TauCeti.ClassFieldTheory.NormalLayer.isGalois_of_fixedField: the fixed field of the top subgroup of a layer is Galois over the fixed field of its ground subgroup.

References

• J. Neukirch, Algebraic Number Theory, Chapter IV, §1.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §1.

noncomputable def TauCeti.ClassFieldTheory.classField (F : Type u_1) [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : IntermediateField F (SeparableClosure F)

The class field of an open normal subgroup V of the absolute Galois group G_F: the fixed field of V inside the separable closure of F. It is the finite Galois extension of F with Galois group G_F ⧸ V.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_classField {F : Type u_1} [Field F] {V : OpenNormalSubgroup (AbsoluteGaloisGroup F)} {x : SeparableClosure F} : x ∈ classField F V ↔ ∀ σ ∈ V, σ x = x

An element of Fˢ lies in the class field of V exactly when every element of V fixes it.

@[simp]

theorem TauCeti.ClassFieldTheory.fixingSubgroup_classField {F : Type u_1} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : (classField F V).fixingSubgroup = ↑V.toOpenSubgroup

The fixing subgroup of the class field of V is V: an open subgroup is closed, so the infinite Galois correspondence recovers it from its fixed field.

theorem TauCeti.ClassFieldTheory.classField_le_classField_iff (F : Type u_1) [Field F] (V W : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : classField F W ≤ classField F V ↔ V ≤ W

The Galois dictionary reverses inclusions: a larger subgroup cuts out a smaller field. This turns a class-field correspondence that preserves the order on subgroups into the classical order-reversing correspondence on fields.

theorem TauCeti.ClassFieldTheory.classField_injective (F : Type u_1) [Field F] : Function.Injective (classField F)

Distinct open normal subgroups cut out distinct class fields.

@[simp]

theorem TauCeti.ClassFieldTheory.classField_eq_bot_iff {F : Type u_1} [Field F] {V : OpenNormalSubgroup (AbsoluteGaloisGroup F)} : classField F V = ⊥ ↔ ↑V.toOpenSubgroup = ⊤

The class field of V is F exactly when V is the whole absolute Galois group.

instance TauCeti.ClassFieldTheory.finiteDimensional_classField {F : Type u_1} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : FiniteDimensional F ↥(classField F V)

The class field of V is finite over F, because V is open.

instance TauCeti.ClassFieldTheory.isGalois_classField {F : Type u_1} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : IsGalois F ↥(classField F V)

The class field of V is Galois over F, because V is normal.

instance TauCeti.ClassFieldTheory.numberField_classField {F : Type u_1} [Field F] [NumberField F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : NumberField ↥(classField F V)

The class field of an open normal subgroup of G_F is a number field when F is, being a finite extension of F.

@[simp]

theorem TauCeti.ClassFieldTheory.fixingOpenNormalSubgroup_classField {F : Type u_1} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : fixingOpenNormalSubgroup F ↥(classField F V) = V

Cutting out the class field of V and then taking the open normal subgroup that fixes it recovers V.

theorem TauCeti.ClassFieldTheory.classField_fixingOpenNormalSubgroup {F : Type u_1} [Field F] {L : Type u_2} [Field L] [Algebra F L] [FiniteDimensional F L] [IsGalois F L] (ι : L →ₐ[F] SeparableClosure F) : classField F (fixingOpenNormalSubgroup F L) = ι.fieldRange

The class field of the subgroup fixing a finite Galois extension L/F is L, embedded in Fˢ by any F-embedding ι.

theorem TauCeti.ClassFieldTheory.exists_classField_eq_iff {F : Type u_1} [Field F] (L : IntermediateField F (SeparableClosure F)) : (∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)), classField F V = L) ↔ FiniteDimensional F ↥L ∧ IsGalois F ↥L

The class fields are exactly the finite Galois subextensions of Fˢ.

theorem TauCeti.ClassFieldTheory.finrank_classField {F : Type u_1} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : Module.finrank F ↥(classField F V) = (↑V.toOpenSubgroup).index

The degree of the class field of V is the index of V.

noncomputable def TauCeti.ClassFieldTheory.galClassFieldEquiv {F : Type} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : Gal(↥(classField F V)/F) ≃* (NormalLayer.ofOpenNormal V).Gal

The Galois group of a class field is the Galois group of its layer: restriction to classField F V identifies Gal(classField F V / F) with the finite Galois group G_F ⧸ V of the normal layer V ◁ G_F.

@[simp]

theorem TauCeti.ClassFieldTheory.galClassFieldEquiv_symm_mk {F : Type} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) (σ : ↥(NormalLayer.ofOpenNormal V).ground) : (galClassFieldEquiv V).symm ↑σ = (AlgEquiv.restrictNormalHom ↥(classField F V)) ↑σ

The inverse of galClassFieldEquiv sends the class of σ ∈ G_F to the restriction of σ to the class field.

theorem TauCeti.ClassFieldTheory.fixedField_top_ofOpenNormal_eq_classField {F : Type} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).top = classField F V

The fixed field of the top subgroup V of the layer V ◁ G_F is the class field of V.

theorem TauCeti.ClassFieldTheory.coe_galClassFieldEquiv_symm_apply {F : Type} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) (u : ↥(NormalLayer.ofOpenNormal V).ground) (x : ↥(classField F V)) : ↑(((galClassFieldEquiv V).symm ↑u) x) = ↑u ↑x

The inverse of galClassFieldEquiv sends the class of u ∈ G_F to an automorphism of the class field acting as u.

@[simp]

theorem TauCeti.ClassFieldTheory.galOfOpenNormalEquiv_galClassFieldEquiv_restrictNormalHom {F : Type} [Field F] (V : OpenNormalSubgroup (AbsoluteGaloisGroup F)) (σ : AbsoluteGaloisGroup F) : (NormalLayer.galOfOpenNormalEquiv V) ((galClassFieldEquiv V) ((AlgEquiv.restrictNormalHom ↥(classField F V)) σ)) = ↑σ

Read in G_F ⧸ V, galClassFieldEquiv sends the restriction of σ ∈ G_F to the class field to the class of σ.

theorem TauCeti.ClassFieldTheory.isAbelianGalois_classField_iff {F : Type} [Field F] {V : OpenNormalSubgroup (AbsoluteGaloisGroup F)} : IsAbelianGalois F ↥(classField F V) ↔ V.IsAbelianClassFieldLayer

The class field of V is abelian over F exactly when V is an abelian layer.

theorem TauCeti.ClassFieldTheory.isAbelianClassFieldLayer_fixingOpenNormalSubgroup {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] [IsAbelianGalois F L] : (fixingOpenNormalSubgroup F L).IsAbelianClassFieldLayer

The open normal subgroup of G_F fixing a finite abelian extension L/F is an abelian layer.

The fixed fields of an arbitrary layer

theorem TauCeti.ClassFieldTheory.NormalLayer.isGalois_of_fixedField {F : Type} [Field F] (Lay : NormalLayer (AbsoluteGaloisGroup F)) {E L : IntermediateField F (SeparableClosure F)} [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure F)] (hE : IntermediateField.fixedField ↑Lay.ground = E) (hL : IntermediateField.fixedField ↑Lay.top = L) : IsGalois ↥E ↥L

A layer is Galois on fixed fields: if the ground and top subgroups of a layer V ◁ U of G_F have fixed fields E and L, then L/E is a Galois extension.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.galEquivOfFixedField {F : Type} [Field F] (Lay : NormalLayer (AbsoluteGaloisGroup F)) {E L : IntermediateField F (SeparableClosure F)} [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure F)] (hE : IntermediateField.fixedField ↑Lay.ground = E) (hL : IntermediateField.fixedField ↑Lay.top = L) : Lay.Gal ≃* Gal(↥L/↥E)

The Galois group of a layer is the Galois group of its fixed fields: if the ground and top subgroups of a layer V ◁ U of G_F have fixed fields E and L, restriction to L identifies the Galois group U ⧸ V of the layer with Gal(L/E).

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.coe_galEquivOfFixedField_mk_apply {F : Type} [Field F] (Lay : NormalLayer (AbsoluteGaloisGroup F)) {E L : IntermediateField F (SeparableClosure F)} [Algebra ↥E ↥L] [IsScalarTower (↥E) (↥L) (SeparableClosure F)] (hE : IntermediateField.fixedField ↑Lay.ground = E) (hL : IntermediateField.fixedField ↑Lay.top = L) (g : ↥Lay.ground) (x : ↥L) : ↑(((Lay.galEquivOfFixedField hE hL) ↑g) x) = ↑g ↑x

galEquivOfFixedField sends the class of g in the ground subgroup to the restriction of g to L: its value at x ∈ L is g x.