Quotients of the absolute Galois group

TauCeti.quotientFixingSubgroupEquiv identifies the quotient of the Galois group of a normal extension E/F by the fixing subgroup of an intermediate field M normal over F with the Galois group Gal(M/F), as topological groups. This file reads that comparison at E = AlgebraicClosure K, where the quotient is a quotient of Field.absoluteGaloisGroup K:

Field.absoluteGaloisGroup K ⧸ M.fixingSubgroup ≃ₜ* Gal(M/K).

The comparison is restated here rather than left to the reading at Gal(AlgebraicClosure K/K): Field.absoluteGaloisGroup K is a definition carrying its own derived group and topology instances, so a statement about Gal(AlgebraicClosure K/K) is not available to rw at a quotient of Field.absoluteGaloisGroup K. The same reason is recorded for the transported instances in TauCeti.FieldTheory.Galois.AbsoluteGaloisGroup.Basic.

Main results

• TauCeti.absoluteGaloisGroupQuotientEquiv: the isomorphism of topological groups comparing a quotient of Field.absoluteGaloisGroup K with the Galois group of a normal subextension of an algebraic closure of K.

noncomputable def TauCeti.absoluteGaloisGroupQuotientEquiv (K : Type u_1) [Field K] (M : IntermediateField K (AlgebraicClosure K)) [Normal K ↥M] : Field.absoluteGaloisGroup K ⧸ M.fixingSubgroup ≃ₜ* Gal(↥M/K)

The Galois group of a normal subextension of an algebraic closure is a quotient of the absolute Galois group: Field.absoluteGaloisGroup K ⧸ M.fixingSubgroup ≃ₜ* Gal(M/K).

This is quotientFixingSubgroupEquiv read at E = AlgebraicClosure K.

Equations

• TauCeti.absoluteGaloisGroupQuotientEquiv K M = TauCeti.quotientFixingSubgroupEquiv K (AlgebraicClosure K) M

@[simp]

theorem TauCeti.absoluteGaloisGroupQuotientEquiv_mk {K : Type u_1} [Field K] {M : IntermediateField K (AlgebraicClosure K)} [Normal K ↥M] (σ : Gal(AlgebraicClosure K/K)) : (absoluteGaloisGroupQuotientEquiv K M) ↑σ = (AlgEquiv.restrictNormalHom ↥M) σ

The comparison isomorphism sends the class of σ to its restriction to M, whose value at a point of M is σ evaluated there, by AlgEquiv.restrictNormalHom_apply.

@[simp]

theorem TauCeti.absoluteGaloisGroupQuotientEquiv_symm_restrictNormalHom {K : Type u_1} [Field K] {M : IntermediateField K (AlgebraicClosure K)} [Normal K ↥M] (σ : Gal(AlgebraicClosure K/K)) : (absoluteGaloisGroupQuotientEquiv K M).symm ((AlgEquiv.restrictNormalHom ↥M) σ) = ↑σ

The inverse of the comparison isomorphism sends the restriction of σ back to the class of σ; with AlgEquiv.restrictNormalHom_surjective this computes it on every element.