Galois Groups of Polynomials

In this file, we introduce the Galois group of a polynomial p over a field F, defined as the automorphism group of its splitting field. We also provide some results about some extension E above p.SplittingField, and some specific results about the Galois groups of ℚ-polynomials with specific numbers of non-real roots.

Main definitions

• Polynomial.Gal p: the Galois group of a polynomial p.
• Polynomial.Gal.restrict p E: the restriction homomorphism (E ≃ₐ[F] E) → gal p.
• Polynomial.Gal.galAction p E: the action of gal p on the roots of p in E.

Main results

• Polynomial.Gal.restrict_smul: restrict p E is compatible with gal_action p E.
• Polynomial.Gal.galActionHom_injective: gal p acting on the roots of p in E is faithful.
• Polynomial.Gal.restrictProd_injective: gal (p * q) embeds as a subgroup of gal p × gal q.
• Polynomial.Gal.card_of_separable: For a separable polynomial, its Galois group has cardinality equal to the dimension of its splitting field over F.
• Polynomial.Gal.galActionHom_bijective_of_prime_degree: An irreducible polynomial of prime degree with two non-real roots has full Galois group.

Other results

• Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv: The number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation (i.e. with some imaginary component).

def Polynomial.Gal {F : Type u_1} [Field F] (p : Polynomial F) : Type u_1

The Galois group of a polynomial.

Equations

• Polynomial.Gal p = (Polynomial.SplittingField p ≃ₐ[F] Polynomial.SplittingField p)

instance Polynomial.Gal.instGroup {F : Type u_1} [Field F] (p : Polynomial F) : Group (Polynomial.Gal p)

Equations

• Polynomial.Gal.instGroup p = inferInstanceAs (Group (Polynomial.SplittingField p ≃ₐ[F] Polynomial.SplittingField p))

instance Polynomial.Gal.instFintype {F : Type u_1} [Field F] (p : Polynomial F) : Fintype (Polynomial.Gal p)

Equations

• Polynomial.Gal.instFintype p = inferInstanceAs (Fintype (Polynomial.SplittingField p ≃ₐ[F] Polynomial.SplittingField p))

instance Polynomial.Gal.instCoeFunGalForAllSplittingField {F : Type u_1} [Field F] (p : Polynomial F) : CoeFun (Polynomial.Gal p) fun x => Polynomial.SplittingField p → Polynomial.SplittingField p

Equations

• One or more equations did not get rendered due to their size.

instance Polynomial.Gal.applyMulSemiringAction {F : Type u_1} [Field F] (p : Polynomial F) : MulSemiringAction (Polynomial.Gal p) (Polynomial.SplittingField p)

Equations

• Polynomial.Gal.applyMulSemiringAction p = AlgEquiv.applyMulSemiringAction

theorem Polynomial.Gal.ext {F : Type u_1} [Field F] (p : Polynomial F) {σ : Polynomial.Gal p} {τ : Polynomial.Gal p} (h : ∀ (x : Polynomial.SplittingField p), x ∈ Polynomial.rootSet p (Polynomial.SplittingField p) → ↑σ x = ↑τ x) : σ = τ

def Polynomial.Gal.uniqueGalOfSplits {F : Type u_1} [Field F] (p : Polynomial F) (h : Polynomial.Splits (RingHom.id F) p) : Unique (Polynomial.Gal p)

If p splits in F then the p.gal is trivial.

Equations

• Polynomial.Gal.uniqueGalOfSplits p h = { toInhabited := { default := 1 }, uniq := (_ : ∀ (f : Polynomial.Gal p), f = default) }

instance Polynomial.Gal.instUniqueGal {F : Type u_1} [Field F] (p : Polynomial F) [h : Fact (Polynomial.Splits (RingHom.id F) p)] : Unique (Polynomial.Gal p)

Equations

• Polynomial.Gal.instUniqueGal p = Polynomial.Gal.uniqueGalOfSplits p (_ : Polynomial.Splits (RingHom.id F) p)

instance Polynomial.Gal.uniqueGalZero {F : Type u_1} [Field F] : Unique (Polynomial.Gal 0)

Equations

• Polynomial.Gal.uniqueGalZero = Polynomial.Gal.uniqueGalOfSplits 0 (_ : Polynomial.Splits (RingHom.id F) 0)

instance Polynomial.Gal.uniqueGalOne {F : Type u_1} [Field F] : Unique (Polynomial.Gal 1)

Equations

• Polynomial.Gal.uniqueGalOne = Polynomial.Gal.uniqueGalOfSplits 1 (_ : Polynomial.Splits (RingHom.id F) 1)

instance Polynomial.Gal.uniqueGalC {F : Type u_1} [Field F] (x : F) : Unique (Polynomial.Gal (↑Polynomial.C x))

Equations

• Polynomial.Gal.uniqueGalC x = Polynomial.Gal.uniqueGalOfSplits (↑Polynomial.C x) (_ : Polynomial.Splits (RingHom.id F) (↑Polynomial.C x))

instance Polynomial.Gal.uniqueGalX {F : Type u_1} [Field F] : Unique (Polynomial.Gal Polynomial.X)

Equations

• Polynomial.Gal.uniqueGalX = Polynomial.Gal.uniqueGalOfSplits Polynomial.X (_ : Polynomial.Splits (RingHom.id F) Polynomial.X)

instance Polynomial.Gal.uniqueGalXSubC {F : Type u_1} [Field F] (x : F) : Unique (Polynomial.Gal (Polynomial.X - ↑Polynomial.C x))

Equations

• Polynomial.Gal.uniqueGalXSubC x = Polynomial.Gal.uniqueGalOfSplits (Polynomial.X - ↑Polynomial.C x) (_ : Polynomial.Splits (RingHom.id F) (Polynomial.X - ↑Polynomial.C x))

instance Polynomial.Gal.uniqueGalXPow {F : Type u_1} [Field F] (n : ℕ) : Unique (Polynomial.Gal (Polynomial.X ^ n))

Equations

• Polynomial.Gal.uniqueGalXPow n = Polynomial.Gal.uniqueGalOfSplits (Polynomial.X ^ n) (_ : Polynomial.Splits (RingHom.id F) (Polynomial.X ^ n))

instance Polynomial.Gal.instAlgebraSplittingFieldToCommSemiringToSemifieldInstFieldSplittingFieldToSemiringToDivisionSemiringToSemifield {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [h : Fact (Polynomial.Splits (algebraMap F E) p)] : Algebra (Polynomial.SplittingField p) E

Equations

• One or more equations did not get rendered due to their size.

instance Polynomial.Gal.instIsScalarTowerSplittingFieldInstSMulSplittingFieldToDistribSMulToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingToDistribMulActionToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToModuleRightToCommSemiringToSemiringIdToSMulInstFieldSplittingFieldToSemiringToDivisionSemiringToSemifieldInstAlgebraSplittingFieldToCommSemiringToSemifieldInstFieldSplittingFieldToSemiringToDivisionSemiringToSemifield {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [h : Fact (Polynomial.Splits (algebraMap F E) p)] : IsScalarTower F (Polynomial.SplittingField p) E

Equations

• One or more equations did not get rendered due to their size.

def Polynomial.Gal.restrict {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : (E ≃ₐ[F] E) →* Polynomial.Gal p

Restrict from a superfield automorphism into a member of gal p.

Equations

• Polynomial.Gal.restrict p E = AlgEquiv.restrictNormalHom (Polynomial.SplittingField p)

theorem Polynomial.Gal.restrict_surjective {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] [Normal F E] : Function.Surjective ↑(Polynomial.Gal.restrict p E)

def Polynomial.Gal.mapRoots {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : ↑(Polynomial.rootSet p (Polynomial.SplittingField p)) → ↑(Polynomial.rootSet p E)

The function taking rootSet p p.SplittingField to rootSet p E. This is actually a bijection, see Polynomial.Gal.mapRoots_bijective.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.Gal.mapRoots_bijective {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [h : Fact (Polynomial.Splits (algebraMap F E) p)] : Function.Bijective (Polynomial.Gal.mapRoots p E)

def Polynomial.Gal.rootsEquivRoots {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : ↑(Polynomial.rootSet p (Polynomial.SplittingField p)) ≃ ↑(Polynomial.rootSet p E)

The bijection between rootSet p p.SplittingField and rootSet p E.

Equations

• Polynomial.Gal.rootsEquivRoots p E = Equiv.ofBijective (Polynomial.Gal.mapRoots p E) (_ : Function.Bijective (Polynomial.Gal.mapRoots p E))

instance Polynomial.Gal.galActionAux {F : Type u_1} [Field F] (p : Polynomial F) : MulAction (Polynomial.Gal p) ↑(Polynomial.rootSet p (Polynomial.SplittingField p))

Equations

• One or more equations did not get rendered due to their size.

instance Polynomial.Gal.smul {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : SMul (Polynomial.Gal p) ↑(Polynomial.rootSet p E)

Equations

• Polynomial.Gal.smul p E = { smul := fun ϕ x => ↑(Polynomial.Gal.rootsEquivRoots p E) (ϕ • ↑(Polynomial.Gal.rootsEquivRoots p E).symm x) }

theorem Polynomial.Gal.smul_def {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] (ϕ : Polynomial.Gal p) (x : ↑(Polynomial.rootSet p E)) : ϕ • x = ↑(Polynomial.Gal.rootsEquivRoots p E) (ϕ • ↑(Polynomial.Gal.rootsEquivRoots p E).symm x)

instance Polynomial.Gal.galAction {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : MulAction (Polynomial.Gal p) ↑(Polynomial.rootSet p E)

The action of gal p on the roots of p in E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.Gal.restrict_smul {F : Type u_1} [Field F] {p : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] (ϕ : E ≃ₐ[F] E) (x : ↑(Polynomial.rootSet p E)) : ↑(↑(Polynomial.Gal.restrict p E) ϕ • x) = ↑ϕ ↑x

Polynomial.Gal.restrict p E is compatible with Polynomial.Gal.galAction p E.

def Polynomial.Gal.galActionHom {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : Polynomial.Gal p →* Equiv.Perm ↑(Polynomial.rootSet p E)

Polynomial.Gal.galAction as a permutation representation

Equations

• Polynomial.Gal.galActionHom p E = MulAction.toPermHom (Polynomial.Gal p) ↑(Polynomial.rootSet p E)

theorem Polynomial.Gal.galActionHom_restrict {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] (ϕ : E ≃ₐ[F] E) (x : ↑(Polynomial.rootSet p E)) : ↑(↑(↑(Polynomial.Gal.galActionHom p E) (↑(Polynomial.Gal.restrict p E) ϕ)) x) = ↑ϕ ↑x

theorem Polynomial.Gal.galActionHom_injective {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] : Function.Injective ↑(Polynomial.Gal.galActionHom p E)

gal p embeds as a subgroup of permutations of the roots of p in E.

def Polynomial.Gal.restrictDvd {F : Type u_1} [Field F] {p : Polynomial F} {q : Polynomial F} (hpq : p ∣ q) : Polynomial.Gal q →* Polynomial.Gal p

Polynomial.Gal.restrict, when both fields are splitting fields of polynomials.

Equations

• Polynomial.Gal.restrictDvd hpq = if hq : q = 0 then 1 else Polynomial.Gal.restrict p (Polynomial.SplittingField q)

theorem Polynomial.Gal.restrictDvd_def {F : Type u_1} [Field F] {p : Polynomial F} {q : Polynomial F} [Decidable (q = 0)] (hpq : p ∣ q) : Polynomial.Gal.restrictDvd hpq = if hq : q = 0 then 1 else Polynomial.Gal.restrict p (Polynomial.SplittingField q)

theorem Polynomial.Gal.restrictDvd_surjective {F : Type u_1} [Field F] {p : Polynomial F} {q : Polynomial F} (hpq : p ∣ q) (hq : q ≠ 0) : Function.Surjective ↑(Polynomial.Gal.restrictDvd hpq)

def Polynomial.Gal.restrictProd {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) : Polynomial.Gal (p * q) →* Polynomial.Gal p × Polynomial.Gal q

The Galois group of a product maps into the product of the Galois groups.

Equations

• Polynomial.Gal.restrictProd p q = MonoidHom.prod (Polynomial.Gal.restrictDvd (_ : p ∣ p * q)) (Polynomial.Gal.restrictDvd (_ : q ∣ p * q))

theorem Polynomial.Gal.restrictProd_injective {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) : Function.Injective ↑(Polynomial.Gal.restrictProd p q)

Polynomial.Gal.restrictProd is actually a subgroup embedding.

theorem Polynomial.Gal.mul_splits_in_splittingField_of_mul {F : Type u_1} [Field F] {p₁ : Polynomial F} {q₁ : Polynomial F} {p₂ : Polynomial F} {q₂ : Polynomial F} (hq₁ : q₁ ≠ 0) (hq₂ : q₂ ≠ 0) (h₁ : Polynomial.Splits (algebraMap F (Polynomial.SplittingField q₁)) p₁) (h₂ : Polynomial.Splits (algebraMap F (Polynomial.SplittingField q₂)) p₂) : Polynomial.Splits (algebraMap F (Polynomial.SplittingField (q₁ * q₂))) (p₁ * p₂)

theorem Polynomial.Gal.splits_in_splittingField_of_comp {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) (hq : Polynomial.natDegree q ≠ 0) : Polynomial.Splits (algebraMap F (Polynomial.SplittingField (Polynomial.comp p q))) p

p splits in the splitting field of p ∘ q, for q non-constant.

def Polynomial.Gal.restrictComp {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) (hq : Polynomial.natDegree q ≠ 0) : Polynomial.Gal (Polynomial.comp p q) →* Polynomial.Gal p

Polynomial.Gal.restrict for the composition of polynomials.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.Gal.restrictComp_surjective {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) (hq : Polynomial.natDegree q ≠ 0) : Function.Surjective ↑(Polynomial.Gal.restrictComp p q hq)

theorem Polynomial.Gal.card_of_separable {F : Type u_1} [Field F] {p : Polynomial F} (hp : Polynomial.Separable p) : Fintype.card (Polynomial.Gal p) = FiniteDimensional.finrank F (Polynomial.SplittingField p)

For a separable polynomial, its Galois group has cardinality equal to the dimension of its splitting field over F.

theorem Polynomial.Gal.prime_degree_dvd_card {F : Type u_1} [Field F] {p : Polynomial F} [CharZero F] (p_irr : Irreducible p) (p_deg : Nat.Prime (Polynomial.natDegree p)) : Polynomial.natDegree p ∣ Fintype.card (Polynomial.Gal p)

theorem Polynomial.Gal.splits_ℚ_ℂ {p : Polynomial ℚ} : Fact (Polynomial.Splits (algebraMap ℚ ℂ) p)

theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv (p : Polynomial ℚ) : Finset.card (Set.toFinset (Polynomial.rootSet p ℂ)) = Finset.card (Set.toFinset (Polynomial.rootSet p ℝ)) + Finset.card (Equiv.Perm.support (↑(Polynomial.Gal.galActionHom p ℂ) (↑(Polynomial.Gal.restrict p ℂ) (AlgEquiv.restrictScalars ℚ Complex.conjAe))))

The number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation (i.e. with some imaginary component).

theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree {p : Polynomial ℚ} (p_irr : Irreducible p) (p_deg : Nat.Prime (Polynomial.natDegree p)) (p_roots : Fintype.card ↑(Polynomial.rootSet p ℂ) = Fintype.card ↑(Polynomial.rootSet p ℝ) + 2) : Function.Bijective ↑(Polynomial.Gal.galActionHom p ℂ)

An irreducible polynomial of prime degree with two non-real roots has full Galois group.

theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree' {p : Polynomial ℚ} (p_irr : Irreducible p) (p_deg : Nat.Prime (Polynomial.natDegree p)) (p_roots1 : Fintype.card ↑(Polynomial.rootSet p ℝ) + 1 ≤ Fintype.card ↑(Polynomial.rootSet p ℂ)) (p_roots2 : Fintype.card ↑(Polynomial.rootSet p ℂ) ≤ Fintype.card ↑(Polynomial.rootSet p ℝ) + 3) : Function.Bijective ↑(Polynomial.Gal.galActionHom p ℂ)

An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.