The Galois group of a product of polynomials

Mathlib embeds the Galois group of a product into the product of the Galois groups, Polynomial.Gal.restrictProd : (p * q).Gal →* p.Gal × q.Gal (Polynomial.Gal.restrictProd_injective), and when p * q ≠ 0 both components are surjective (Polynomial.Gal.restrictDvd_surjective). This file describes the image when p and q are separable. Inside the splitting field L of p * q, the splitting fields L_p and L_q of the two factors embed, and a pair (σ, τ) lies in the image exactly when σ and τ agree on the common part L_p ∩ L_q. So (p * q).Gal is the fibre product of p.Gal and q.Gal over the Galois group of that intersection, and restrictProd is an isomorphism exactly when L_p ∩ L_q = F.

Separability is what makes L/F Galois, which the description of the image uses.

Main results

• Polynomial.Separable.isGalois_splittingField_mul: the splitting field of a product of two separable polynomials is Galois.
• Polynomial.Gal.mem_range_restrictProd_iff: the image of restrictProd consists of the pairs agreeing on L_p ∩ L_q.
• Polynomial.Gal.restrictInfLeft and Polynomial.Gal.restrictInfRight: the two restriction maps to the Galois group of L_p ∩ L_q.
• Polynomial.Gal.mem_range_restrictProd_iff_restrictInfLeft_eq_restrictInfRight: the same image is the fibre product of the restriction maps p.Gal →* Gal((L_p ∩ L_q)/F) and q.Gal →* Gal((L_p ∩ L_q)/F).
• Polynomial.Gal.restrictProd_surjective_iff: restrictProd is surjective iff L_p ∩ L_q = F.
• Polynomial.Gal.restrictProd_surjective_iff_linearDisjoint: for splitting fields, this is equivalent to linear disjointness.
• Polynomial.Gal.restrictProdMulEquiv: linearly disjoint splitting fields give an isomorphism from the Galois group of the product to the product of the two Galois groups.

theorem Polynomial.Separable.isGalois_splittingField_mul {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) : IsGalois F (p * q).SplittingField

The splitting field of a product of two separable polynomials is Galois, even though the product itself need not be separable.

theorem Polynomial.Gal.restrictProd_eq_restrict_prod_restrict {F : Type u_1} [Field F] (p q : Polynomial F) (hpq : p * q ≠ 0) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : restrictProd p q = (restrict p (p * q).SplittingField).prod (restrict q (p * q).SplittingField)

For nonzero p * q, Polynomial.Gal.restrictProd is the joint restriction from the splitting field of p * q to the splitting fields of p and q.

theorem Polynomial.Gal.mem_range_restrictProd_iff {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] (σ : p.Gal) (τ : q.Gal) : (σ, τ) ∈ (restrictProd p q).range ↔ ∀ (x : p.SplittingField) (y : q.SplittingField), (algebraMap p.SplittingField (p * q).SplittingField) x = (algebraMap q.SplittingField (p * q).SplittingField) y → (algebraMap p.SplittingField (p * q).SplittingField) (σ x) = (algebraMap q.SplittingField (p * q).SplittingField) (τ y)

The Galois group of a product is a fibre product. For separable p and q, a pair (σ, τ) : p.Gal × q.Gal lies in the image of Polynomial.Gal.restrictProd if and only if σ and τ agree on the elements that the splitting fields of p and q have in common inside the splitting field of p * q.

noncomputable def Polynomial.Gal.restrictInfLeft {F : Type u_1} [Field F] (p q : Polynomial F) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : p.Gal →* Gal(↥((IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange ⊓ (IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange)/F)

Restriction from p.Gal to the Galois group of the intersection of the images of the splitting fields of p and q inside the splitting field of p * q.

Equations

• Polynomial.Gal.restrictInfLeft p q = (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).restrictNormalHomOfLE ⋯

noncomputable def Polynomial.Gal.restrictInfRight {F : Type u_1} [Field F] (p q : Polynomial F) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : q.Gal →* Gal(↥((IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange ⊓ (IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange)/F)

Restriction from q.Gal to the Galois group of the intersection of the images of the splitting fields of p and q inside the splitting field of p * q.

Equations

• Polynomial.Gal.restrictInfRight p q = (IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).restrictNormalHomOfLE ⋯

theorem Polynomial.Gal.restrictInfLeft_def {F : Type u_1} [Field F] (p q : Polynomial F) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : restrictInfLeft p q = (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).restrictNormalHomOfLE ⋯

The left restriction is the general restriction along the splitting-field embedding. This allows the characteristic API of AlgHom.restrictNormalHomOfLE to be used for it.

theorem Polynomial.Gal.restrictInfRight_def {F : Type u_1} [Field F] (p q : Polynomial F) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : restrictInfRight p q = (IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).restrictNormalHomOfLE ⋯

The right restriction is the general restriction along the splitting-field embedding. This allows the characteristic API of AlgHom.restrictNormalHomOfLE to be used for it.

theorem Polynomial.Gal.mem_range_restrictProd_iff_restrictInfLeft_eq_restrictInfRight {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] (σ : p.Gal) (τ : q.Gal) : (σ, τ) ∈ (restrictProd p q).range ↔ (restrictInfLeft p q) σ = (restrictInfRight p q) τ

The Galois group of a product is the fibre product over the common part. For separable p and q, write L_p and L_q for the images of their splitting fields in the splitting field of p * q. A pair (σ, τ) : p.Gal × q.Gal lies in the image of Polynomial.Gal.restrictProd if and only if σ and τ have the same restriction to L_p ∩ L_q, the two restriction maps p.Gal →* Gal((L_p ∩ L_q)/F) and q.Gal →* Gal((L_p ∩ L_q)/F) being Polynomial.Gal.restrictInfLeft and Polynomial.Gal.restrictInfRight.

theorem Polynomial.Gal.restrictProd_surjective_iff {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : Function.Surjective ⇑(restrictProd p q) ↔ (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange ⊓ (IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange = ⊥

For separable p and q, Polynomial.Gal.restrictProd is surjective if and only if the splitting fields of p and q meet only in F inside the splitting field of p * q.

theorem Polynomial.Gal.restrictProd_surjective_iff_linearDisjoint {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] : Function.Surjective ⇑(restrictProd p q) ↔ (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange.LinearDisjoint ↥(IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange

For separable p and q, Polynomial.Gal.restrictProd is surjective exactly when the images of their splitting fields in the splitting field of p * q are linearly disjoint over the base field.

noncomputable def Polynomial.Gal.restrictProdMulEquiv {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] (h : (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange.LinearDisjoint ↥(IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange) : (p * q).Gal ≃* p.Gal × q.Gal

The Galois group of a product with linearly disjoint splitting fields. For separable p and q whose splitting fields are linearly disjoint inside the splitting field of p * q, joint restriction is an isomorphism (p * q).Gal ≃* p.Gal × q.Gal.

Equations

• Polynomial.Gal.restrictProdMulEquiv hp hq h = MulEquiv.ofBijective (Polynomial.Gal.restrictProd p q) ⋯

@[simp]

theorem Polynomial.Gal.restrictProdMulEquiv_apply {F : Type u_1} [Field F] {p q : Polynomial F} (hp : p.Separable) (hq : q.Separable) [Fact (map (algebraMap F (p * q).SplittingField) p).Splits] [Fact (map (algebraMap F (p * q).SplittingField) q).Splits] (h : (IsScalarTower.toAlgHom F p.SplittingField (p * q).SplittingField).fieldRange.LinearDisjoint ↥(IsScalarTower.toAlgHom F q.SplittingField (p * q).SplittingField).fieldRange) (g : (p * q).Gal) : (restrictProdMulEquiv hp hq h) g = (restrictProd p q) g

The forward map of Polynomial.Gal.restrictProdMulEquiv is joint restriction.