The absolute Galois group of a field, taken at its separable closure

For a normal extension E/F an automorphism of E is determined by, and determined on, the separable closure of F in E: restriction

Gal(E/F) → Gal(separableClosure F E / F)

is an isomorphism of topological groups, TauCeti.separableClosureRestrictEquiv. Specialised to E = AlgebraicClosure F this identifies Mathlib's Field.absoluteGaloisGroup F, defined through the algebraic closure, with TauCeti.AbsoluteGaloisGroup F = Gal(SeparableClosure F / F), which is the carrier every Galois-cohomological statement is written against.

Which of the two closures is used is not a matter of taste. TauCeti.mem_perfectClosure_iff_fixed says that the elements of a normal E/F fixed by every F-automorphism are exactly the elements purely inseparable over F. So for an imperfect F the fixed field of Field.absoluteGaloisGroup F is the purely inseparable closure of F and not F itself, while over the separable closure InfiniteGalois.mem_range_algebraMap_iff_fixed gives the fixed field F that a Galois descent argument needs. The two groups are nonetheless the same topological group, which is what lets a property of the group and its topology alone be read off for one from the other.

Only such properties transport along the isomorphism as they stand; a statement mentioning the extension, its intermediate fields or the action on E has to be translated first. Both happen here. Compactness of a Galois group is transported unchanged, so Gal(E/F) is profinite for E/F merely normal. The fundamental theorem is translated: the closed subgroups of Gal(E/F) are the fixing subgroups, and they correspond to the intermediate fields of separableClosure F E / F. Intermediate fields of E outside the separable closure are not seen by any fixing subgroup, by IntermediateField.fixingSubgroup_inf_separableClosure, which is why the correspondence is indexed by the separable closure.

Main definitions and results

• TauCeti.AbsoluteGaloisGroup K: the automorphisms of a separable closure of K.
• TauCeti.separableClosureRestrictEquiv: restriction to the separable closure is an isomorphism of topological groups, for any normal extension.
• TauCeti.absoluteGaloisGroupRestrictEquiv: its specialisation comparing Field.absoluteGaloisGroup K with TauCeti.AbsoluteGaloisGroup K.
• TauCeti.fixingSubgroup_fixedField: every closed subgroup is a fixing subgroup.
• TauCeti.intermediateFieldEquivClosedSubgroup: the fundamental theorem of Galois theory for a normal extension.
• TauCeti.mem_perfectClosure_iff_fixed: the fixed field of Gal(E/F) for a normal extension E/F is the relative perfect closure of F in E.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. VI §1, for the convention that the absolute Galois group of a field is taken at its separable closure.

Restriction to the separable closure

theorem AlgEquiv.restrictNormalHom_separableClosure_injective (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [Normal F ↥(_root_.separableClosure F E)] : Function.Injective ⇑(restrictNormalHom ↥(_root_.separableClosure F E))

An F-automorphism of an algebraic extension E/F that is the identity on the separable closure is the identity: the remaining extension is purely inseparable. Normality of the separable closure is needed to form restrictNormalHom; E/F itself need not be normal.

noncomputable def TauCeti.separableClosureRestrictEquiv (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Normal F E] : Gal(E/F) ≃ₜ* Gal(↥(separableClosure F E)/F)

Restriction to the separable closure is an isomorphism of topological groups Gal(E/F) ≃ₜ* Gal(separableClosure F E / F), for a normal extension E/F.

Equations

• TauCeti.separableClosureRestrictEquiv F E = { toMulEquiv := TauCeti.separableClosureRestrictMulEquiv✝ F E, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem TauCeti.separableClosureRestrictEquiv_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (σ : Gal(E/F)) : (separableClosureRestrictEquiv F E) σ = (AlgEquiv.restrictNormalHom ↥(separableClosure F E)) σ

The isomorphism separableClosureRestrictEquiv is the restriction map AlgEquiv.restrictNormalHom, which is what identifies it with the map Mathlib's API is about.

@[simp]

theorem TauCeti.coe_separableClosureRestrictEquiv_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (σ : Gal(E/F)) (x : ↥(separableClosure F E)) : ↑(((separableClosureRestrictEquiv F E) σ) x) = σ ↑x

Restricting σ : Gal(E/F) to the separable closure does not move elements: the image of x ∈ separableClosure F E under separableClosureRestrictEquiv F E σ is σ x, computed in E.

@[simp]

theorem TauCeti.separableClosureRestrictEquiv_symm_apply_coe {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (τ : Gal(↥(separableClosure F E)/F)) (x : ↥(separableClosure F E)) : ((separableClosureRestrictEquiv F E).symm τ) ↑x = ↑(τ x)

The automorphism of E extending τ : Gal(separableClosure F E/F) agrees with τ on the separable closure.

The profinite structure

instance TauCeti.instCompactSpaceAlgEquiv_tauCeti (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Normal F E] : CompactSpace Gal(E/F)

The Galois group of a normal extension is compact, hence, the Krull topology being totally separated, a profinite group: ProfiniteGrp.of Gal(E/F). Mathlib has compactness for a Galois extension, and restriction to the separable closure carries it over.

The Galois correspondence

theorem IntermediateField.fixedField_fixingSubgroup_lift_inf_separableClosure {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (M : IntermediateField F ↥(separableClosure F E)) : fixedField (lift M).fixingSubgroup ⊓ separableClosure F E = lift M

An intermediate field of the separable closure is the part of the fixed field of its fixing subgroup that lies in the separable closure. The fixed field itself can be larger, because a fixing subgroup does not see the purely inseparable elements of E outside the separable closure; in the extreme case M = ⊥ it is all of perfectClosure F E, by TauCeti.mem_perfectClosure_iff_fixed. It is the intersection that is pinned down here, and that is what makes the correspondence below an order isomorphism.

theorem TauCeti.fixingSubgroup_fixedField {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] {H : Subgroup Gal(E/F)} (hH : IsClosed ↑H) : (IntermediateField.fixedField H).fixingSubgroup = H

A closed subgroup of Gal(E/F) is the fixing subgroup of its fixed field, for E/F normal.

def TauCeti.intermediateFieldEquivClosedSubgroup {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] : IntermediateField F ↥(separableClosure F E) ≃o (ClosedSubgroup Gal(E/F))ᵒᵈ

The fundamental theorem of Galois theory in the ambient model. For a normal extension E/F the closed subgroups of Gal(E/F) correspond, inclusion-reversingly, to the intermediate fields of the separable closure separableClosure F E / F; an intermediate field of E outside the separable closure has the same fixing subgroup as its separable part.

Equations

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

@[simp]

theorem TauCeti.intermediateFieldEquivClosedSubgroup_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (M : IntermediateField F ↥(separableClosure F E)) : ↑(OrderDual.ofDual (intermediateFieldEquivClosedSubgroup M)) = (IntermediateField.lift M).fixingSubgroup

The correspondence sends an intermediate field to the fixing subgroup of its lift.

@[simp]

theorem TauCeti.intermediateFieldEquivClosedSubgroup_symm_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (H : ClosedSubgroup Gal(E/F)) : intermediateFieldEquivClosedSubgroup.symm H = IntermediateField.restrict ⋯

The inverse of the correspondence sends a closed subgroup to its fixed field, restricted to the separable closure.

The fixed field of a normal extension

theorem TauCeti.mem_perfectClosure_iff_fixed {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] {x : E} : x ∈ perfectClosure F E ↔ ∀ (σ : Gal(E/F)), σ x = x

The fixed field of Gal(E/F) for a normal extension E/F is the relative perfect closure of F in E, and not F. The two agree exactly when E/F has no nontrivial purely inseparable part, so for E an algebraic closure they agree exactly when F is perfect.

The absolute Galois group

@[reducible, inline]

abbrev TauCeti.AbsoluteGaloisGroup (K : Type u_3) [Field K] : Type u_3

The absolute Galois group of K: the group of automorphisms of a separable closure of K.

This, rather than Mathlib's Field.absoluteGaloisGroup, is the group Galois cohomology is stated at, because it is Kˢ and not an algebraic closure whose invariants are K for every K. It is an abbreviation so that the Krull topology, the profinite structure and the action on Kˢ are the ones Mathlib already provides for Gal(E/F); absoluteGaloisGroupRestrictEquiv compares it with Field.absoluteGaloisGroup.

Equations

• TauCeti.AbsoluteGaloisGroup K = Gal(SeparableClosure K/K)

noncomputable def TauCeti.absoluteGaloisGroupRestrictEquiv (K : Type u_3) [Field K] : Field.absoluteGaloisGroup K ≃ₜ* AbsoluteGaloisGroup K

Mathlib's absolute Galois group and AbsoluteGaloisGroup are the same topological group: restricting an automorphism of an algebraic closure of K to the separable closure is an isomorphism Field.absoluteGaloisGroup K ≃ₜ* AbsoluteGaloisGroup K.

Its forward map is restriction, absoluteGaloisGroupRestrictEquiv_apply, and both directions are computed on elements of SeparableClosure K by coe_absoluteGaloisGroupRestrictEquiv_apply and absoluteGaloisGroupRestrictEquiv_symm_apply_coe. Those lemmas are stated on applications rather than on the isomorphisms themselves, because Field.absoluteGaloisGroup K carries its own derived group and topology instances, so an equation between the isomorphisms is not usable by rw. Closed subgroups and their normal quotients transport along this comparison through ContinuousMulEquiv.closedSubgroupOrderIso and ContinuousMulEquiv.quotientCongr.

Equations

• TauCeti.absoluteGaloisGroupRestrictEquiv K = TauCeti.separableClosureRestrictEquiv K (AlgebraicClosure K)

theorem TauCeti.absoluteGaloisGroupRestrictEquiv_apply (K : Type u_3) [Field K] (σ : Gal(AlgebraicClosure K/K)) : (absoluteGaloisGroupRestrictEquiv K) σ = (AlgEquiv.restrictNormalHom ↥(separableClosure K (AlgebraicClosure K))) σ

The comparison isomorphism is the restriction map AlgEquiv.restrictNormalHom, which is what identifies it with the map Mathlib's API is about.

@[simp]

theorem TauCeti.coe_absoluteGaloisGroupRestrictEquiv_apply (K : Type u_3) [Field K] (σ : Gal(AlgebraicClosure K/K)) (x : SeparableClosure K) : ↑(((absoluteGaloisGroupRestrictEquiv K) σ) x) = σ ↑x

An automorphism of an algebraic closure of K and its image in AbsoluteGaloisGroup K take the same value on an element of SeparableClosure K, computed in the algebraic closure.

@[simp]

theorem TauCeti.absoluteGaloisGroupRestrictEquiv_symm_apply_coe (K : Type u_3) [Field K] (τ : AbsoluteGaloisGroup K) (x : SeparableClosure K) : ((absoluteGaloisGroupRestrictEquiv K).symm τ) ↑x = ↑(τ x)

The automorphism of AlgebraicClosure K extending τ : AbsoluteGaloisGroup K agrees with τ on SeparableClosure K; this is what computes the inverse of the comparison isomorphism.

The coercion to a function carries its type argument explicitly because Field.absoluteGaloisGroup K is a plain definition, so elaboration does not see an element of it as a function on AlgebraicClosure K on its own.

instance TauCeti.instCompactSpaceAbsoluteGaloisGroup_tauCeti (K : Type u_3) [Field K] : CompactSpace (Field.absoluteGaloisGroup K)

Field.absoluteGaloisGroup K is compact. It is a type of its own rather than a notation for Gal(AlgebraicClosure K/K), so the instance has to be transported by hand.

instance TauCeti.instTotallySeparatedSpaceAbsoluteGaloisGroup_tauCeti (K : Type u_3) [Field K] : TotallySeparatedSpace (Field.absoluteGaloisGroup K)

Field.absoluteGaloisGroup K is totally separated, hence totally disconnected and Hausdorff. With compactness this makes it a profinite group, ProfiniteGrp.of (Field.absoluteGaloisGroup K).

instance TauCeti.instSubsingletonAbsoluteGaloisGroupOfIsSepClosed (K : Type u_3) [Field K] [IsSepClosed K] : Subsingleton (AbsoluteGaloisGroup K)

The absolute Galois group of a separably closed field is trivial.