The map of absolute Galois groups induced by a field extension

Let L/K be an arbitrary field extension, not necessarily algebraic, and let τ : Kˢ →ₐ[K] Lˢ be a K-embedding of separable closures; one always exists, since Lˢ is separably closed and Kˢ/K is separable algebraic. Every automorphism g of Lˢ over L maps τ(Kˢ) to itself, because Kˢ/K is normal, and so restricts along τ to an automorphism of Kˢ over K. This gives a continuous homomorphism

absoluteGaloisGroupMap τ : G_L →ₜ* G_K,   τ (absoluteGaloisGroupMap τ g x) = g (τ x).

For a completion K_v of a global field K it is the inclusion of the decomposition group, and it is the group-theoretic input of the localization maps of Galois cohomology. It is the analogue, at the separable closures on which TauCeti.AbsoluteGaloisGroup is built, of Mathlib's Field.absoluteGaloisGroup.mapOfAlgebra for algebraic closures (María Inés de Frutos-Fernández), whose continuity proof is followed here.

The embedding τ is a choice: two embeddings differ by an automorphism h of Kˢ over K (AlgHom.exists_comp_eq_of_normal), and then the two maps differ by conjugation by h (absoluteGaloisGroupMap_comp), which is invisible in cohomology.

Main definitions

• TauCeti.absoluteGaloisGroupMap τ: the continuous homomorphism G_L →ₜ* G_K along τ.

Main results

• TauCeti.absoluteGaloisGroupMap_commutes: τ (absoluteGaloisGroupMap τ g x) = g (τ x).
• TauCeti.absoluteGaloisGroupMap_comp: changing τ by an automorphism h of Kˢ conjugates the map by h.
• TauCeti.absoluteGaloisGroupMap_absoluteGaloisGroupMap: the maps are compatible with composition of extensions.

noncomputable def TauCeti.absoluteGaloisGroupMap {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) : AbsoluteGaloisGroup L →ₜ* AbsoluteGaloisGroup K

The map of absolute Galois groups along an extension L/K, given a K-embedding τ : Kˢ →ₐ[K] Lˢ of separable closures: an automorphism g of Lˢ over L is in particular an automorphism over K, and it restricts along τ to the automorphism of the normal extension Kˢ/K intertwined with g by τ (absoluteGaloisGroupMap_commutes). It is continuous for the Krull topologies: an automorphism of Lˢ fixing the finite extension of L generated by the image of a finite subextension F of Kˢ/K is sent to one fixing F.

Equations

• TauCeti.absoluteGaloisGroupMap τ = { toMonoidHom := τ.restrictNormalHom.comp (AlgEquiv.restrictScalarsHom K), continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.absoluteGaloisGroupMap_commutes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : AbsoluteGaloisGroup L) (x : SeparableClosure K) : τ (((absoluteGaloisGroupMap τ) g) x) = g (τ x)

absoluteGaloisGroupMap τ g is intertwined with g by τ.

theorem TauCeti.absoluteGaloisGroupMap_eq_iff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {g : AbsoluteGaloisGroup L} {h : AbsoluteGaloisGroup K} : (absoluteGaloisGroupMap τ) g = h ↔ ∀ (x : SeparableClosure K), g (τ x) = τ (h x)

absoluteGaloisGroupMap τ g is the unique automorphism of Kˢ intertwined with g by τ.

theorem TauCeti.absoluteGaloisGroupMap_comp {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (h : AbsoluteGaloisGroup K) (g : AbsoluteGaloisGroup L) : (absoluteGaloisGroupMap (τ.comp ↑h)) g = h⁻¹ * (absoluteGaloisGroupMap τ) g * h

Changing the embedding conjugates the map: precomposing τ with an automorphism h of Kˢ over K replaces absoluteGaloisGroupMap τ g by its conjugate h⁻¹ * _ * h.

theorem TauCeti.absoluteGaloisGroupMap_absoluteGaloisGroupMap {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {M : Type u_3} [Field M] [Algebra K M] [Algebra L M] (τ' : SeparableClosure L →ₐ[L] SeparableClosure M) (τ'' : SeparableClosure K →ₐ[K] SeparableClosure M) (hτ : ∀ (x : SeparableClosure K), τ'' x = τ' (τ x)) (g : AbsoluteGaloisGroup M) : (absoluteGaloisGroupMap τ) ((absoluteGaloisGroupMap τ') g) = (absoluteGaloisGroupMap τ'') g

The maps are compatible with composition of extensions K → L → M: if τ'' : Kˢ → Mˢ is the composite of τ : Kˢ → Lˢ and τ' : Lˢ → Mˢ, the map G_M → G_K along τ'' is the composite of the maps G_M → G_L → G_K.