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.

Main definitions

• Polynomial.Gal p: the Galois group of a polynomial p.
• Polynomial.Gal.restrict p E: the restriction homomorphism Gal(E/F) → 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

• p.Gal = Gal(p.SplittingField/F)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• p.instFintypeGal = { elems := Polynomial.instFintypeGal._aux_1 p, complete := ⋯ }

@[instance_reducible]

noncomputable instance Polynomial.instEquivLikeGalSplittingField {F : Type u_1} [Field F] (p : Polynomial F) : EquivLike p.Gal p.SplittingField p.SplittingField

Equations

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

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

@[instance_reducible]

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

Equations

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

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

theorem Polynomial.Gal.ext_iff {F : Type u_1} [Field F] {p : Polynomial F} {σ τ : p.Gal} : σ = τ ↔ ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x

@[instance_reducible]

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

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

Equations

• Polynomial.Gal.uniqueGalOfSplits p h = { default := 1, uniq := ⋯ }

@[instance_reducible]

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

Equations

• Polynomial.Gal.instUniqueOfFactSplits p = Polynomial.Gal.uniqueGalOfSplits p ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalZero = Polynomial.Gal.uniqueGalOfSplits 0 ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalOne = Polynomial.Gal.uniqueGalOfSplits 1 ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalC x = Polynomial.Gal.uniqueGalOfSplits (Polynomial.C x) ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalX = Polynomial.Gal.uniqueGalOfSplits Polynomial.X ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalXSubC x = Polynomial.Gal.uniqueGalOfSplits (Polynomial.X - Polynomial.C x) ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.uniqueGalXPow n = Polynomial.Gal.uniqueGalOfSplits (Polynomial.X ^ n) ⋯

@[instance_reducible]

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

Equations

• Polynomial.Gal.instAlgebraSplittingFieldOfFactSplitsMapAlgebraMap p E = (Polynomial.IsSplittingField.lift p.SplittingField p ⋯).toAlgebra

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

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

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

Equations

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

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

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

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

Equations

• Polynomial.Gal.mapRoots p E = Set.MapsTo.restrict (⇑(IsScalarTower.toAlgHom F p.SplittingField E)) (p.rootSet p.SplittingField) (p.rootSet E) ⋯

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 (map (algebraMap F E) p).Splits] : Function.Bijective (mapRoots p E)

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

A bijection between rootSet p p.SplittingField and rootSet p E. This is an auxilliary definition used to define the Galois-equivariant Polynomial.Gal.rootsEquivRoots, but we keep this definition public to help prove facts about galAction.

Equations

• Polynomial.Gal.rootsEquivRootsAux p E = Equiv.ofBijective (Polynomial.Gal.mapRoots p E) ⋯

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

A bijection between rootSet p E and rootSet p E' when p splits in both E and E'. This bijection is Galois-equivariant, see smul_rootsEquivRoots.

Equations

• Polynomial.Gal.rootsEquivRoots p E E' = (Polynomial.Gal.rootsEquivRootsAux p E).symm.trans (Polynomial.Gal.rootsEquivRootsAux p E')

@[instance_reducible]

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

Equations

• Polynomial.Gal.galActionAux p = { smul := fun (ϕ : p.Gal) => Set.MapsTo.restrict (⇑ϕ) (p.rootSet p.SplittingField) (p.rootSet p.SplittingField) ⋯, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

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

Equations

• Polynomial.Gal.smul p E = { smul := fun (ϕ : p.Gal) (x : ↑(p.rootSet E)) => (Polynomial.Gal.rootsEquivRootsAux p E) (ϕ • (Polynomial.Gal.rootsEquivRootsAux 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 (map (algebraMap F E) p).Splits] (ϕ : p.Gal) (x : ↑(p.rootSet E)) : ϕ • x = (rootsEquivRootsAux p E) (ϕ • (rootsEquivRootsAux p E).symm x)

theorem Polynomial.Gal.smul_rootsEquivRoots {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) (E' : Type u_3) [Field E] [Field E'] [Algebra F E] [Algebra F E'] [Fact (map (algebraMap F E) p).Splits] [Fact (map (algebraMap F E') p).Splits] (g : p.Gal) (x : ↑(p.rootSet E)) : g • (rootsEquivRoots p E E') x = (rootsEquivRoots p E E') (g • x)

@[instance_reducible]

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

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

Equations

• Polynomial.Gal.galAction p E = { toSMul := Polynomial.Gal.smul p E, mul_smul := ⋯, one_smul := ⋯ }

theorem Polynomial.Gal.galAction_isPretransitive {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] (hp : Irreducible p) : MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

@[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 (map (algebraMap F E) p).Splits] (ϕ : Gal(E/F)) (x : ↑(p.rootSet E)) : ↑((restrict p E) ϕ • x) = ϕ ↑x

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

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

Polynomial.Gal.galAction as a permutation representation

Equations

• Polynomial.Gal.galActionHom p E = MulAction.toPermHom p.Gal ↑(p.rootSet 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 (map (algebraMap F E) p).Splits] (ϕ : Gal(E/F)) (x : ↑(p.rootSet E)) : ↑(((galActionHom p E) ((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 (map (algebraMap F E) p).Splits] : Function.Injective ⇑(galActionHom p E)

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

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

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 q.SplittingField

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

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

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

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

Equations

• Polynomial.Gal.restrictProd p q = (Polynomial.Gal.restrictDvd ⋯).prod (Polynomial.Gal.restrictDvd ⋯)

theorem Polynomial.Gal.restrictProd_injective {F : Type u_1} [Field F] (p q : Polynomial F) : Function.Injective ⇑(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₁ q₁ p₂ q₂ : Polynomial F} (hq₁ : q₁ ≠ 0) (hq₂ : q₂ ≠ 0) (h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits) (h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits) : (map (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)).Splits

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

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

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

Polynomial.Gal.restrict for the composition of polynomials.

Equations

• Polynomial.Gal.restrictComp p q hq = Polynomial.Gal.restrict p (p.comp q).SplittingField

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

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

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 p.natDegree) : p.natDegree ∣ Nat.card p.Gal