Galois groups of composita as fibre products

Let E/F be a finite Galois extension and let K₁, K₂ be normal subextensions. Restricting automorphisms of E gives a homomorphism Gal(E/F) → Gal(K₁/F) × Gal(K₂/F). This file identifies its image: a pair (σ₁, σ₂) comes from an automorphism of E exactly when σ₁ and σ₂ agree on the elements that K₁ and K₂ have in common inside E. Consequently the map is surjective exactly when K₁ and K₂ meet only in F.

For two finite Galois intermediate fields K and L, Mathlib's IntermediateField.restrictNormalHomSupProd embeds the automorphism group of the compositum K ⊔ L into Gal(K/F) × Gal(L/F). Its range consists of the pairs with equal restrictions to K ⊓ L, so Gal(K ⊔ L / F) is the fibre product Gal(K/F) ×_{Gal(K ⊓ L / F)} Gal(L/F).

Those restriction maps to K ⊓ L are named with AlgHom.restrictNormalHom from TauCeti.FieldTheory.Galois.Restriction. For abstract K₁ and K₂ the intersection lies in E rather than in either of them, and the restriction maps to it are AlgHom.restrictNormalHomOfLE.

Main definitions and results

• AlgEquiv.mem_range_restrictNormalHom_prod_restrictNormalHom_iff: a pair of automorphisms of two normal subextensions of a finite Galois extension extends to the whole extension iff it agrees on common elements.
• AlgEquiv.mem_range_restrictNormalHom_prod_iff_restrictNormalHomOfLE_eq: equivalently, the pair has equal restrictions to the intersection of the two subextensions, so the image is the fibre product over the Galois group of that intersection.
• AlgEquiv.restrictNormalHom_prod_restrictNormalHom_surjective_iff: the joint restriction map is surjective iff the two subextensions meet in F.
• IntermediateField.mem_range_restrictNormalHomSupProd_iff: the Galois group of a compositum of two finite Galois intermediate fields is the fibre product over their intersection.

References

• S. Lang, Algebra, Chapter VI, §1.

theorem AlgEquiv.mem_range_restrictNormalHom_prod_restrictNormalHom_iff {F : Type u_1} {E : Type u_2} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field E] [Field K₁] [Field K₂] [Algebra F E] [Algebra F K₁] [Algebra F K₂] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F K₁] [Normal F K₂] [FiniteDimensional F E] [IsGalois F E] (σ₁ : Gal(K₁/F)) (σ₂ : Gal(K₂/F)) : (σ₁, σ₂) ∈ ((restrictNormalHom K₁).prod (restrictNormalHom K₂)).range ↔ ∀ (x₁ : K₁) (x₂ : K₂), (algebraMap K₁ E) x₁ = (algebraMap K₂ E) x₂ → (algebraMap K₁ E) (σ₁ x₁) = (algebraMap K₂ E) (σ₂ x₂)

Galois groups of composita as fibre products. In a finite Galois extension E/F with normal subextensions K₁ and K₂, a pair (σ₁, σ₂) of automorphisms is the restriction of a single automorphism of E if and only if σ₁ and σ₂ agree on the elements common to K₁ and K₂ inside E.

theorem AlgEquiv.restrictNormalHom_prod_restrictNormalHom_surjective_iff {F : Type u_1} {E : Type u_2} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field E] [Field K₁] [Field K₂] [Algebra F E] [Algebra F K₁] [Algebra F K₂] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F K₁] [Normal F K₂] [FiniteDimensional F E] [IsGalois F E] : Function.Surjective ⇑((restrictNormalHom K₁).prod (restrictNormalHom K₂)) ↔ (IsScalarTower.toAlgHom F K₁ E).fieldRange ⊓ (IsScalarTower.toAlgHom F K₂ E).fieldRange = ⊥

The joint restriction map to two normal subextensions of a finite Galois extension is surjective if and only if the two subextensions meet only in the base field.

theorem AlgEquiv.mem_range_restrictNormalHom_prod_iff_restrictNormalHomOfLE_eq {F : Type u_1} {E : Type u_2} {K₁ : Type u_3} {K₂ : Type u_4} [Field F] [Field E] [Field K₁] [Field K₂] [Algebra F E] [Algebra F K₁] [Algebra F K₂] [Algebra K₁ E] [Algebra K₂ E] [IsScalarTower F K₁ E] [IsScalarTower F K₂ E] [Normal F K₁] [Normal F K₂] [FiniteDimensional F E] [IsGalois F E] (σ₁ : Gal(K₁/F)) (σ₂ : Gal(K₂/F)) : (σ₁, σ₂) ∈ ((restrictNormalHom K₁).prod (restrictNormalHom K₂)).range ↔ ((IsScalarTower.toAlgHom F K₁ E).restrictNormalHomOfLE ⋯) σ₁ = ((IsScalarTower.toAlgHom F K₂ E).restrictNormalHomOfLE ⋯) σ₂

Galois groups of composita as fibre products over the common part. In a finite Galois extension E/F with normal subextensions K₁ and K₂, a pair (σ₁, σ₂) of automorphisms is the restriction of a single automorphism of E if and only if σ₁ and σ₂ have the same restriction to the intersection of K₁ and K₂ inside E. So the image of Gal(E/F) in Gal(K₁/F) × Gal(K₂/F) is the fibre product over Gal((K₁ ∩ K₂)/F) of the two restriction maps AlgHom.restrictNormalHomOfLE.

theorem IntermediateField.mem_range_restrictNormalHomSupProd_iff {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (K L : IntermediateField F E) [IsGalois F ↥K] [IsGalois F ↥L] [FiniteDimensional F ↥K] [FiniteDimensional F ↥L] (σ : Gal(↥K/F)) (τ : Gal(↥L/F)) : (σ, τ) ∈ (K.restrictNormalHomSupProd L).range ↔ (inclusion ⋯).restrictNormalHom σ = (inclusion ⋯).restrictNormalHom τ

The Galois group of a compositum is a fibre product. For finite Galois intermediate fields K and L, the image of Gal(K ⊔ L / F) in Gal(K/F) × Gal(L/F) under IntermediateField.restrictNormalHomSupProd consists of the pairs whose restrictions to K ⊓ L agree. Since restrictNormalHomSupProd is injective, Gal(K ⊔ L / F) is the fibre product Gal(K/F) ×_{Gal(K ⊓ L / F)} Gal(L/F).