The absolute Galois group of a finite separable extension as an open subgroup

Let L/K be a finite separable extension and σ : L →ₐ[K] Kˢ a K-embedding of L into a separable closure Kˢ of K. The automorphisms of Kˢ that fix σ(L) pointwise form an open subgroup

galoisSubgroup K L σ ≤ G_K = AbsoluteGaloisGroup K

of index [L : K], and it is the absolute Galois group of L: the isomorphism of topological groups absoluteGaloisGroupEquivFixingSubgroup K L σ : G_L ≃ₜ* σ.fieldRange.fixingSubgroup of TauCeti.FieldTheory.Galois.AbsoluteGaloisGroup.Extension, read at the open subgroup, is an isomorphism G_L ≃ₜ* galoisSubgroup K L σ for the Krull topologies, which is what continuous cohomology depends on.

The embedding is genuine data. Without one there is no homomorphism G_L → G_K induced by the extension L/K, hence no realization of G_L as a subgroup of G_K, and two embeddings cut out conjugate subgroups. Restriction, corestriction and the other subgroup-indexed operations of Galois cohomology along L/K are the operations at galoisSubgroup K L σ, read through galoisSubgroupEquiv K L σ, and their independence of σ is a statement about those operations rather than about the subgroup. The index formula is what discharges the finite-index and index-two hypotheses those operations carry.

Finiteness of L/K enters in three places: it makes the fixing subgroup open, so that it can be packaged as the OpenSubgroup galoisSubgroup K L σ; it is the hypothesis of the finite-degree index formula galoisSubgroup_index; and, through the packaging, it is carried by galoisSubgroupEquiv K L σ and its application lemmas. The identification of separable closures and the isomorphism of Galois groups themselves need no finiteness and live in the imported module. Separability of L/K is a consequence of the existence of σ and is not assumed.

When L/K is normal, every automorphism of Kˢ preserves σ(L), so restriction σ.restrictNormalHom : G_K →* Gal(L/K) along σ is defined; it is surjective with kernel the subgroup fixing σ(L), and quotientFixingSubgroupFieldRangeEquiv K L σ is the induced isomorphism G_K ⧸ Gal(Kˢ/σ(L)) ≃* Gal(L/K). This part uses normality but not finiteness. When L/K is both finite and normal, the subgroup fixing σ(L) is packaged as the open normal subgroup galoisOpenNormalSubgroup K L σ, the level of L among the finite quotients of G_K. When L/K is finite Galois, all embeddings have the same image, the normal closure of L in Kˢ, and fixingOpenNormalSubgroup K L is this subgroup with no embedding chosen.

Main definitions

• TauCeti.galoisSubgroup K L σ: the open subgroup of G_K fixing σ(L) pointwise, for a finite L/K.
• TauCeti.galoisSubgroupEquiv K L σ: the isomorphism of topological groups G_L ≃ₜ* galoisSubgroup K L σ.
• TauCeti.quotientFixingSubgroupFieldRangeEquiv K L σ: for a normal L/K, the isomorphism G_K ⧸ Gal(Kˢ/σ(L)) ≃* Gal(L/K) induced by restriction σ.restrictNormalHom.
• TauCeti.galoisOpenNormalSubgroup K L σ: for a finite normal L/K, the subgroup fixing σ(L) as an open normal subgroup of G_K.
• TauCeti.fixingOpenNormalSubgroup K L: for a finite L/K, the open normal subgroup of G_K fixing the normal closure of L in Kˢ, with no embedding chosen.
• TauCeti.absoluteGaloisGroupExtend K L σ: the injective continuous homomorphism Field.absoluteGaloisGroup L →* Field.absoluteGaloisGroup K between Mathlib's absolute Galois groups, galoisSubgroupEquiv K L σ followed by the inclusion of galoisSubgroup K L σ.

Main results

• TauCeti.galoisSubgroup_index: the index of galoisSubgroup K L σ in G_K is [L : K], so the subgroup fixing σ(L) has finite index (TauCeti.finiteIndex_fixingSubgroup_fieldRange, TauCeti.finiteIndex_galoisSubgroup).
• TauCeti.galoisSubgroupEquiv_apply_separableClosureRingEquiv: the isomorphism intertwines the actions of G_L on Lˢ and of G_K on Kˢ through separableClosureRingEquiv K L σ.
• TauCeti.absoluteGaloisGroupExtend_apply_separableClosureRingEquiv: the embedding of Mathlib's absolute Galois groups intertwines the actions on the identified separable closures.
• TauCeti.mem_range_absoluteGaloisGroupExtend_iff, TauCeti.isOpen_range_absoluteGaloisGroupExtend, TauCeti.index_range_absoluteGaloisGroupExtend: the image of G_L in Mathlib's G_K is the open subgroup galoisSubgroup K L σ, of index [L : K].
• TauCeti.quotientFixingSubgroupFieldRangeEquiv_mk: the isomorphism sends the class of g to σ.restrictNormalHom g.
• TauCeti.exists_galoisOpenNormalSubgroup_eq: every open normal subgroup of G_K is galoisOpenNormalSubgroup K E E.val for a finite Galois intermediate field E of Kˢ/K.
• TauCeti.fixingOpenNormalSubgroup_eq_galoisOpenNormalSubgroup: for a finite Galois L/K, fixingOpenNormalSubgroup K L is galoisOpenNormalSubgroup K L σ for every embedding σ.
• TauCeti.restrictNormalHom_of_compatible: a compatible pair between normal subextensions of Kˢ carries restriction to the larger field to restriction to the smaller field.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I §5 for restriction and corestriction along a finite extension, and Ch. VI §1 for the absolute Galois group at the separable closure.

The open subgroup

noncomputable def TauCeti.galoisSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : OpenSubgroup (AbsoluteGaloisGroup K)

The open subgroup of G_K cut out by a K-embedding of L into Kˢ: the automorphisms of Kˢ fixing σ(L) pointwise. It is open because L/K is finite, and galoisSubgroupEquiv identifies it with the absolute Galois group of L.

Equations

• TauCeti.galoisSubgroup K L σ = { toSubgroup := σ.fieldRange.fixingSubgroup, isOpen' := ⋯ }

@[simp]

theorem TauCeti.galoisSubgroup_toSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : ↑(galoisSubgroup K L σ) = σ.fieldRange.fixingSubgroup

The subgroup underlying galoisSubgroup K L σ is the fixing subgroup of the image of σ.

@[simp]

theorem TauCeti.mem_galoisSubgroup_iff (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] {g : AbsoluteGaloisGroup K} : g ∈ galoisSubgroup K L σ ↔ ∀ (x : L), g (σ x) = σ x

An automorphism of Kˢ lies in galoisSubgroup K L σ exactly when it fixes σ x for every x : L.

theorem TauCeti.galoisSubgroup_index (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : (↑(galoisSubgroup K L σ)).index = Module.finrank K L

The index of galoisSubgroup K L σ is the degree [L : K].

instance TauCeti.finiteIndex_fixingSubgroup_fieldRange (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : σ.fieldRange.fixingSubgroup.FiniteIndex

The subgroup of G_K fixing σ(L) has finite index, namely [L : K]. This is what discharges the finite-index hypothesis of corestriction and of the other operations of Galois cohomology indexed by a subgroup of G_K.

instance TauCeti.finiteIndex_galoisSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : (↑(galoisSubgroup K L σ)).FiniteIndex

galoisSubgroup K L σ has finite index, namely [L : K]: the instance finiteIndex_fixingSubgroup_fieldRange read through galoisSubgroup_toSubgroup.

theorem TauCeti.isOpen_fixingSubgroup_fieldRange (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : IsOpen ↑σ.fieldRange.fixingSubgroup

The subgroup of G_K fixing σ(L) is open, galoisSubgroup K L σ read as a plain subgroup.

theorem TauCeti.galoisSubgroup_eq_top_iff (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : galoisSubgroup K L σ = ⊤ ↔ Module.finrank K L = 1

galoisSubgroup K L σ is all of G_K exactly when L/K is trivial, that is [L : K] = 1.

The isomorphism with the absolute Galois group of L

noncomputable def TauCeti.galoisSubgroupEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : AbsoluteGaloisGroup L ≃ₜ* ↥↑(galoisSubgroup K L σ)

The absolute Galois group of L is the open subgroup of G_K cut out by σ, as topological groups: conjugation by the identification separableClosureRingEquiv K L σ of separable closures is an isomorphism G_L ≃ₜ* galoisSubgroup K L σ for the Krull topologies. It is absoluteGaloisGroupEquivFixingSubgroup K L σ read at the open subgroup.

Equations

• TauCeti.galoisSubgroupEquiv K L σ = TauCeti.absoluteGaloisGroupEquivFixingSubgroup K L σ

@[simp]

theorem TauCeti.galoisSubgroupEquiv_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (g : AbsoluteGaloisGroup L) (y : SeparableClosure K) : ↑((galoisSubgroupEquiv K L σ) g) y = (separableClosureRingEquiv K L σ) (g ((separableClosureRingEquiv K L σ).symm y))

galoisSubgroupEquiv K L σ conjugates by the identification of separable closures.

theorem TauCeti.galoisSubgroupEquiv_apply_separableClosureRingEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (g : AbsoluteGaloisGroup L) (x : SeparableClosure L) : ↑((galoisSubgroupEquiv K L σ) g) ((separableClosureRingEquiv K L σ) x) = (separableClosureRingEquiv K L σ) (g x)

The isomorphism intertwines the Galois actions: the image of g : G_L acts on e x ∈ Kˢ as g acts on x ∈ Lˢ, where e = separableClosureRingEquiv K L σ.

@[simp]

theorem TauCeti.galoisSubgroupEquiv_symm_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (h : ↥↑(galoisSubgroup K L σ)) (x : SeparableClosure L) : ((galoisSubgroupEquiv K L σ).symm h) x = (separableClosureRingEquiv K L σ).symm (↑h ((separableClosureRingEquiv K L σ) x))

The inverse of galoisSubgroupEquiv K L σ conjugates back by the identification of separable closures.

The embedding of Mathlib's absolute Galois groups

noncomputable def TauCeti.absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Field.absoluteGaloisGroup L →* Field.absoluteGaloisGroup K

The absolute Galois group of a finite extension inside that of K, along a K-embedding σ : L →ₐ[K] Kˢ: identify G_L with the open subgroup of G_K fixing σ(L), and include that subgroup in G_K. The two absolute Galois groups use Mathlib's algebraic closures, while the subgroup identification uses Tau Ceti's separable closures; absoluteGaloisGroupRestrictEquiv transports between the two models.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.absoluteGaloisGroupRestrictEquiv_absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : Field.absoluteGaloisGroup L) : (absoluteGaloisGroupRestrictEquiv K) ((absoluteGaloisGroupExtend K L σ) τ) = ↑((galoisSubgroupEquiv K L σ) ((absoluteGaloisGroupRestrictEquiv L) τ))

Reading absoluteGaloisGroupExtend on separable closures gives the inclusion of the open subgroup identified with G_L.

theorem TauCeti.absoluteGaloisGroupExtend_apply_separableClosureRingEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (τ : Field.absoluteGaloisGroup L) (x : SeparableClosure L) : ((absoluteGaloisGroupRestrictEquiv K) ((absoluteGaloisGroupExtend K L σ) τ)) ((separableClosureRingEquiv K L σ) x) = (separableClosureRingEquiv K L σ) (((absoluteGaloisGroupRestrictEquiv L) τ) x)

The embedding of absolute Galois groups intertwines the actions on the identified separable closures.

theorem TauCeti.continuous_absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Continuous ⇑(absoluteGaloisGroupExtend K L σ)

The embedding G_L → G_K induced by an embedding of a finite extension is continuous.

theorem TauCeti.injective_absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Function.Injective ⇑(absoluteGaloisGroupExtend K L σ)

The map G_L → G_K induced by an embedding of a finite extension is injective.

theorem TauCeti.mem_range_absoluteGaloisGroupExtend_iff (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] {g : Field.absoluteGaloisGroup K} : g ∈ (absoluteGaloisGroupExtend K L σ).range ↔ (absoluteGaloisGroupRestrictEquiv K) g ∈ galoisSubgroup K L σ

The image of G_L in G_K is the open subgroup galoisSubgroup K L σ fixing σ(L), read in Mathlib's absolute Galois group through absoluteGaloisGroupRestrictEquiv K.

theorem TauCeti.isOpen_range_absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : IsOpen ↑(absoluteGaloisGroupExtend K L σ).range

The image of G_L in G_K is open.

theorem TauCeti.index_range_absoluteGaloisGroupExtend (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : (absoluteGaloisGroupExtend K L σ).range.index = Module.finrank K L

The image of G_L in G_K has index [L : K].

Normal extensions: the quotient by the open subgroup

noncomputable def TauCeti.quotientFixingSubgroupFieldRangeEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Normal K L] : AbsoluteGaloisGroup K ⧸ σ.fieldRange.fixingSubgroup ≃* Gal(L/K)

The Galois group of a normal extension L embedded by σ is the quotient of G_K by the subgroup fixing σ(L): TauCeti.quotientFixingSubgroupEquiv for the intermediate field σ(L), read on L through σ. It sends the class of g to its restriction σ.restrictNormalHom g along σ (quotientFixingSubgroupFieldRangeEquiv_mk).

Equations

• TauCeti.quotientFixingSubgroupFieldRangeEquiv K L σ = (TauCeti.quotientFixingSubgroupEquiv K (SeparableClosure K) σ.fieldRange).trans σ.equivFieldRange.autCongr.symm

@[simp]

theorem TauCeti.quotientFixingSubgroupFieldRangeEquiv_mk (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Normal K L] (g : AbsoluteGaloisGroup K) : (quotientFixingSubgroupFieldRangeEquiv K L σ) ↑g = σ.restrictNormalHom g

The isomorphism quotientFixingSubgroupFieldRangeEquiv sends the class of g to its restriction σ.restrictNormalHom g.

Restriction along compatible normal subextensions

theorem TauCeti.restrictNormalHom_of_compatible {K : Type u_3} [Field K] {E M : IntermediateField K (SeparableClosure K)} [Normal K ↥E] [Normal K ↥M] (pi : Gal(↥M/K) →* Gal(↥E/K)) (iota : ↥E →ₐ[K] ↥M) (hpiiota : ∀ (g : Gal(↥M/K)) (x : ↥E), iota ((pi g) x) = g (iota x)) (hiota : ∀ (x : ↥E), M.val (iota x) = E.val x) (g : AbsoluteGaloisGroup K) : pi ((AlgEquiv.restrictNormalHom ↥M) g) = (AlgEquiv.restrictNormalHom ↥E) g

Along a compatible pair (pi, iota) between normal subextensions of Kˢ, with iota compatible with their inclusions into Kˢ, pi carries restriction to M to restriction to E.

Finite normal extensions: the open normal subgroup

noncomputable def TauCeti.galoisOpenNormalSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] [Normal K L] : OpenNormalSubgroup (AbsoluteGaloisGroup K)

The level of a finite normal extension: the subgroup Gal(Kˢ/σ(L)) of automorphisms of Kˢ fixing σ(L), an open normal subgroup of Gal(Kˢ/K) because L/K is finite and normal. Its underlying subgroup is the fixing subgroup of σ(L) by definition, so the quotient by it is the domain of quotientFixingSubgroupFieldRangeEquiv K L σ.

Equations

• TauCeti.galoisOpenNormalSubgroup K L σ = { toSubgroup := σ.fieldRange.fixingSubgroup, isOpen' := ⋯, isNormal' := ⋯ }

@[simp]

theorem TauCeti.galoisOpenNormalSubgroup_toSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] [Normal K L] : ↑(galoisOpenNormalSubgroup K L σ).toOpenSubgroup = σ.fieldRange.fixingSubgroup

The subgroup underlying galoisOpenNormalSubgroup K L σ is the fixing subgroup of σ(L).

theorem TauCeti.exists_galoisOpenNormalSubgroup_eq {K : Type u_1} [Field K] (U : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : ∃ (E : IntermediateField K (SeparableClosure K)) (x : FiniteDimensional K ↥E) (x_1 : IsGalois K ↥E), galoisOpenNormalSubgroup K (↥E) E.val = U

Every open normal subgroup of G_K is the level of a finite Galois subextension: it is galoisOpenNormalSubgroup K E E.val for its fixed field E, an intermediate field of Kˢ/K finite and Galois over K.

The fixing subgroup of the normal closure

noncomputable def TauCeti.fixingOpenNormalSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : OpenNormalSubgroup (AbsoluteGaloisGroup K)

The open normal subgroup cut out by a finite extension L/K: the subgroup of G_K = Gal(Kˢ/K) fixing the normal closure of L in Kˢ, that is, fixing the image of every K-embedding of L into Kˢ. When L/K is Galois all these images coincide, so this is TauCeti.galoisOpenNormalSubgroup K L ι for every embedding ι (fixingOpenNormalSubgroup_eq_galoisOpenNormalSubgroup), with no embedding chosen.

Equations

• TauCeti.fixingOpenNormalSubgroup K L = { toSubgroup := (IntermediateField.normalClosure K L (SeparableClosure K)).fixingSubgroup, isOpen' := ⋯, isNormal' := ⋯ }

theorem TauCeti.fixingOpenNormalSubgroup_toSubgroup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : ↑(fixingOpenNormalSubgroup K L).toOpenSubgroup = ι.fieldRange.fixingSubgroup

The subgroup underlying fixingOpenNormalSubgroup K L is the fixing subgroup of the image of any K-embedding ι of the Galois extension L into Kˢ.

theorem TauCeti.fixingOpenNormalSubgroup_eq_galoisOpenNormalSubgroup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : fixingOpenNormalSubgroup K L = galoisOpenNormalSubgroup K L ι

The fixing subgroup of a Galois extension does not depend on the embedding: it is the subgroup TauCeti.galoisOpenNormalSubgroup K L ι fixing the image of any K-embedding ι.

theorem TauCeti.mem_fixingOpenNormalSubgroup_iff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) {σ : AbsoluteGaloisGroup K} : σ ∈ fixingOpenNormalSubgroup K L ↔ ∀ (x : L), σ (ι x) = ι x

An element of G_K lies in fixingOpenNormalSubgroup K L exactly when it fixes the image of a (any) K-embedding ι of the Galois extension L into Kˢ.