The absolute Galois group of an embedded extension as a fixing subgroup

Let L/K be a field extension and σ : L →ₐ[K] Kˢ a K-embedding of L into a separable closure Kˢ of K. Through σ, the field Kˢ is a separable closure of L as well, so a chosen identification Lˢ ≃ Kˢ over L carries the automorphisms of Lˢ over L onto the automorphisms of Kˢ fixing σ(L) pointwise. This file constructs that identification and proves that it is an isomorphism of topological groups

G_L ≃ₜ* σ.fieldRange.fixingSubgroup ≤ G_K = AbsoluteGaloisGroup K

for the Krull topologies, for any extension L/K embedded in Kˢ; no finiteness is assumed. Separability of L/K is a consequence of the existence of σ and is not assumed either.

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. When L/K is finite the fixing subgroup is open, and TauCeti.FieldTheory.Galois.AbsoluteGaloisGroup.FiniteExtension packages it as the open subgroup galoisSubgroup K L σ with the isomorphism read there, since the open subgroup is the object the cohomological operations along L/K are indexed by.

Main definitions

• TauCeti.separableClosureRingEquiv K L σ: a chosen ring isomorphism Lˢ ≃+* Kˢ extending σ.
• TauCeti.absoluteGaloisGroupEquivFixingSubgroup K L σ: the isomorphism of topological groups G_L ≃ₜ* σ.fieldRange.fixingSubgroup obtained by transport along that identification.

Main results

• TauCeti.absoluteGaloisGroupEquivFixingSubgroup_apply: the isomorphism conjugates by separableClosureRingEquiv K L σ, so it intertwines the actions of G_L on Lˢ and of G_K on Kˢ.

References

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

The identification of separable closures

noncomputable def TauCeti.separableClosureRingEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : SeparableClosure L ≃+* SeparableClosure K

A chosen identification Lˢ ≃+* Kˢ extending σ. Any two separable closures of L are L-isomorphic, and Kˢ is one of them through σ; the L-linearity of the chosen isomorphism is recorded by separableClosureRingEquiv_algebraMap. It is a ring isomorphism rather than an L-algebra isomorphism because the L-algebra structure of Kˢ is not an instance.

Equations

• TauCeti.separableClosureRingEquiv K L σ = (IsSepClosure.equiv L (SeparableClosure L) (SeparableClosure K)).toRingEquiv

@[simp]

theorem TauCeti.separableClosureRingEquiv_algebraMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : L) : (separableClosureRingEquiv K L σ) ((algebraMap L (SeparableClosure L)) x) = σ x

The identification of separable closures restricts to σ on L.

@[simp]

theorem TauCeti.separableClosureRingEquiv_symm_apply_eq_algebraMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : L) : (separableClosureRingEquiv K L σ).symm (σ x) = (algebraMap L (SeparableClosure L)) x

The inverse identification sends σ x back to x.

@[simp]

theorem TauCeti.separableClosureRingEquiv_algebraMap_base (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (c : K) : (separableClosureRingEquiv K L σ) ((algebraMap K (SeparableClosure L)) c) = (algebraMap K (SeparableClosure K)) c

The identification of separable closures fixes the image of K.

@[simp]

theorem TauCeti.separableClosureRingEquiv_symm_algebraMap_base (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (c : K) : (separableClosureRingEquiv K L σ).symm ((algebraMap K (SeparableClosure K)) c) = (algebraMap K (SeparableClosure L)) c

The inverse identification fixes the image of K.

The isomorphism with the fixing subgroup of the image of L

noncomputable def TauCeti.absoluteGaloisGroupEquivFixingSubgroup (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : AbsoluteGaloisGroup L ≃ₜ* ↥σ.fieldRange.fixingSubgroup

The absolute Galois group of L is the subgroup of G_K fixing σ(L) pointwise, as topological groups: conjugation by the identification separableClosureRingEquiv K L σ of separable closures is an isomorphism G_L ≃ₜ* σ.fieldRange.fixingSubgroup for the Krull topologies, for any extension L/K embedded in Kˢ. For a finite L/K this subgroup is open, and the isomorphism is galoisSubgroupEquiv K L σ.

Equations

• TauCeti.absoluteGaloisGroupEquivFixingSubgroup K L σ = { toMulEquiv := TauCeti.fixingSubgroupMulEquiv✝ K L σ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

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

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

@[simp]

theorem TauCeti.absoluteGaloisGroupEquivFixingSubgroup_symm_apply (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (h : ↥σ.fieldRange.fixingSubgroup) (x : SeparableClosure L) : ((absoluteGaloisGroupEquivFixingSubgroup K L σ).symm h) x = (separableClosureRingEquiv K L σ).symm (↑h ((separableClosureRingEquiv K L σ) x))

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