Fixing subgroups of conjugate embeddings

Two embeddings of a finite separable extension into a separable closure differ by an automorphism of that closure. Their images are therefore conjugate intermediate fields, and the Galois correspondence carries them to conjugate open subgroups of the absolute Galois group. This is the subgroup comparison used when transporting restriction, corestriction, and the Evens norm between different choices of embedding.

The automorphism carrying one embedding to the other comes from the transitive action on embeddings in TauCeti.FieldTheory.Normal.Embeddings. Conjugacy of the fixing subgroups follows from the corresponding stabilizer conjugacy theorem. The finer statement TauCeti.exists_galoisSubgroupEquiv_eq_conj says that the two identifications of the absolute Galois group of L with these subgroups differ by conjugation by a single element of G_K.

The same holds for any other way of realizing G_L inside G_K: if a ring isomorphism e : AlgebraicClosure L ≃+* AlgebraicClosure K of algebraic closures extends the embedding σ, then conjugation by e agrees with TauCeti.absoluteGaloisGroupExtend K L σ up to a single inner automorphism of G_K (TauCeti.exists_absoluteGaloisGroupExtend_eq_conj). The isomorphism e restricts to the separable closures because separability over L and over K agree, L/K being separable.

theorem TauCeti.galoisSubgroup_conj (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L] (σ τ : L →ₐ[K] SeparableClosure K) : ∃ (g : AbsoluteGaloisGroup K), ↑(galoisSubgroup K L τ) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ↑(galoisSubgroup K L σ)

The open subgroups of G_K fixing two embedded copies of a finite extension L/K are conjugate. The conjugating automorphism extends the natural K-algebra isomorphism between the two copies of L.

theorem TauCeti.exists_galoisSubgroupEquiv_eq_conj (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L] (σ τ : L →ₐ[K] SeparableClosure K) : ∃ (γ : AbsoluteGaloisGroup K), ∀ (x : AbsoluteGaloisGroup L), ↑((galoisSubgroupEquiv K L τ) x) = γ * ↑((galoisSubgroupEquiv K L σ) x) * γ⁻¹

The identifications of G_L with the subgroups cut out by two embeddings differ by an inner automorphism of G_K: for K-embeddings σ τ : L →ₐ[K] Kˢ there is γ : G_K with galoisSubgroupEquiv K L τ x = γ * galoisSubgroupEquiv K L σ x * γ⁻¹ for every x : G_L. The element γ is the automorphism of Kˢ carrying the identification of separable closures attached to σ to the one attached to τ.

theorem TauCeti.exists_absoluteGaloisGroupExtend_eq_conj (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (e : AlgebraicClosure L ≃+* AlgebraicClosure K) (he : ∀ (x : L), e ((algebraMap L (AlgebraicClosure L)) x) = ↑(σ x)) : ∃ (γ : Field.absoluteGaloisGroup K), ∀ (τ : Field.absoluteGaloisGroup L) (τ' : Field.absoluteGaloisGroup K), (∀ (y : AlgebraicClosure L), e (τ.toRingEquiv y) = τ'.toRingEquiv (e y)) → (absoluteGaloisGroupExtend K L σ) τ = γ * τ' * γ⁻¹

absoluteGaloisGroupExtend is conjugation by any extension of the embedding, up to an inner automorphism of G_K. Let e : AlgebraicClosure L ≃+* AlgebraicClosure K be a ring isomorphism of algebraic closures that extends σ : L →ₐ[K] Kˢ. There is γ : G_K such that, whenever τ' ∈ G_K corresponds to τ ∈ G_L under e (that is, e ∘ τ = τ' ∘ e), the image of τ under absoluteGaloisGroupExtend K L σ is γ * τ' * γ⁻¹. The element γ is the automorphism of Kˢ carrying the restriction of e to the separable closures to separableClosureRingEquiv K L σ.

theorem TauCeti.galoisSubgroup_eq_of_finrank_eq_two (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L] (σ τ : L →ₐ[K] SeparableClosure K) (hL : Module.finrank K L = 2) : galoisSubgroup K L σ = galoisSubgroup K L τ

The subgroup cut out by a quadratic extension is independent of its embedding. For a quadratic extension L/K, any two embeddings of L into the separable closure have the same fixing subgroup of G_K.