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 (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} [] (p : ) :
Type u_1

The Galois group of a polynomial.

Equations
• p.Gal = (p.SplittingField ≃ₐ[F] p.SplittingField)
Instances For
instance Polynomial.Gal.instGroup {F : Type u_1} [] (p : ) :
Group p.Gal
Equations
instance Polynomial.Gal.instFintype {F : Type u_1} [] (p : ) :
Fintype p.Gal
Equations
instance Polynomial.Gal.instCoeFunForallSplittingField {F : Type u_1} [] (p : ) :
CoeFun p.Gal fun (x : p.Gal) => p.SplittingFieldp.SplittingField
Equations
• One or more equations did not get rendered due to their size.
instance Polynomial.Gal.applyMulSemiringAction {F : Type u_1} [] (p : ) :
MulSemiringAction p.Gal p.SplittingField
Equations
• = AlgEquiv.applyMulSemiringAction
theorem Polynomial.Gal.ext {F : Type u_1} [] (p : ) {σ : p.Gal} {τ : p.Gal} (h : xp.rootSet p.SplittingField, σ x = τ x) :
σ = τ
def Polynomial.Gal.uniqueGalOfSplits {F : Type u_1} [] (p : ) (h : ) :
Unique p.Gal

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

Equations
• = { default := 1, uniq := }
Instances For
instance Polynomial.Gal.instUniqueOfFactSplitsId {F : Type u_1} [] (p : ) [h : Fact ()] :
Unique p.Gal
Equations
instance Polynomial.Gal.uniqueGalZero {F : Type u_1} [] :
Equations
• Polynomial.Gal.uniqueGalZero =
instance Polynomial.Gal.uniqueGalOne {F : Type u_1} [] :
Equations
• Polynomial.Gal.uniqueGalOne =
instance Polynomial.Gal.uniqueGalC {F : Type u_1} [] (x : F) :
Unique (Polynomial.C x).Gal
Equations
instance Polynomial.Gal.uniqueGalX {F : Type u_1} [] :
Unique Polynomial.X.Gal
Equations
instance Polynomial.Gal.uniqueGalXSubC {F : Type u_1} [] (x : F) :
Unique (Polynomial.X - Polynomial.C x).Gal
Equations
instance Polynomial.Gal.uniqueGalXPow {F : Type u_1} [] (n : ) :
Unique (Polynomial.X ^ n).Gal
Equations
instance Polynomial.Gal.instAlgebraSplittingFieldOfFactSplitsAlgebraMap {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [h : Fact (Polynomial.Splits () p)] :
Algebra p.SplittingField E
Equations
instance Polynomial.Gal.instIsScalarTowerSplittingField {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [h : Fact (Polynomial.Splits () p)] :
IsScalarTower F p.SplittingField E
Equations
• =
def Polynomial.Gal.restrict {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :
(E ≃ₐ[F] E) →* p.Gal

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

Equations
Instances For
theorem Polynomial.Gal.restrict_surjective {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] [Normal F E] :
def Polynomial.Gal.mapRoots {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :
(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
Instances For
theorem Polynomial.Gal.mapRoots_bijective {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [h : Fact (Polynomial.Splits () p)] :
def Polynomial.Gal.rootsEquivRoots {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :
(p.rootSet p.SplittingField) (p.rootSet E)

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

Equations
Instances For
instance Polynomial.Gal.galActionAux {F : Type u_1} [] (p : ) :
MulAction p.Gal (p.rootSet p.SplittingField)
Equations
instance Polynomial.Gal.smul {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :
SMul p.Gal (p.rootSet E)
Equations
• = { smul := fun (ϕ : p.Gal) (x : (p.rootSet E)) => (ϕ .symm x) }
theorem Polynomial.Gal.smul_def {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] (ϕ : p.Gal) (x : (p.rootSet E)) :
ϕ x = (ϕ .symm x)
instance Polynomial.Gal.galAction {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :
MulAction p.Gal (p.rootSet E)

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

Equations
theorem Polynomial.Gal.galAction_isPretransitive {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] (hp : ) :
MulAction.IsPretransitive p.Gal (p.rootSet E)
@[simp]
theorem Polynomial.Gal.restrict_smul {F : Type u_1} [] {p : } {E : Type u_2} [] [Algebra F E] [Fact (Polynomial.Splits () p)] (ϕ : E ≃ₐ[F] E) (x : (p.rootSet E)) :
(() ϕ x) = ϕ x

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

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

Polynomial.Gal.galAction as a permutation representation

Equations
Instances For
theorem Polynomial.Gal.galActionHom_restrict {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] (ϕ : E ≃ₐ[F] E) (x : (p.rootSet E)) :
(( (() ϕ)) x) = ϕ x
theorem Polynomial.Gal.galActionHom_injective {F : Type u_1} [] (p : ) (E : Type u_2) [] [Algebra F E] [Fact (Polynomial.Splits () p)] :

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

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

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

Equations
Instances For
theorem Polynomial.Gal.restrictDvd_def {F : Type u_1} [] {p : } {q : } [Decidable (q = 0)] (hpq : p q) :
= if hq : q = 0 then 1 else Polynomial.Gal.restrict p q.SplittingField
theorem Polynomial.Gal.restrictDvd_surjective {F : Type u_1} [] {p : } {q : } (hpq : p q) (hq : q 0) :
def Polynomial.Gal.restrictProd {F : Type u_1} [] (p : ) (q : ) :
(p * q).Gal →* p.Gal × q.Gal

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

Equations
Instances For
theorem Polynomial.Gal.restrictProd_injective {F : Type u_1} [] (p : ) (q : ) :

Polynomial.Gal.restrictProd is actually a subgroup embedding.

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

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

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

Polynomial.Gal.restrict for the composition of polynomials.

Equations
Instances For
theorem Polynomial.Gal.restrictComp_surjective {F : Type u_1} [] (p : ) (q : ) (hq : q.natDegree 0) :
theorem Polynomial.Gal.card_of_separable {F : Type u_1} [] {p : } (hp : p.Separable) :
Fintype.card p.Gal = FiniteDimensional.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} [] {p : } [] (p_irr : ) (p_deg : p.natDegree.Prime) :
p.natDegree Fintype.card p.Gal