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

The Galois group of a polynomial.

Equations

• Eq p.Gal (AlgEquiv F p.SplittingField p.SplittingField)

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

Equations

• Eq (Polynomial.Gal.instGroup p) (inferInstanceAs (Group (AlgEquiv F p.SplittingField p.SplittingField)))

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

Equations

• Eq (Polynomial.Gal.instFintype p) (inferInstanceAs (Fintype (AlgEquiv F p.SplittingField p.SplittingField)))

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

Equations

• Eq (Polynomial.Gal.instEquivLikeSplittingField p) (inferInstanceAs (EquivLike (AlgEquiv F p.SplittingField p.SplittingField) p.SplittingField p.SplittingField))

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

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

Equations

• Eq (Polynomial.Gal.applyMulSemiringAction p) AlgEquiv.applyMulSemiringAction

theorem Polynomial.Gal.ext {F : Type u_1} [Field F] (p : Polynomial F) {σ τ : p.Gal} (h : ∀ (x : p.SplittingField), Membership.mem (p.rootSet p.SplittingField) x → Eq (DFunLike.coe σ x) (DFunLike.coe τ x)) : Eq σ τ

theorem Polynomial.Gal.ext_iff {F : Type u_1} [Field F] {p : Polynomial F} {σ τ : p.Gal} : Iff (Eq σ τ) (∀ (x : p.SplittingField), Membership.mem (p.rootSet p.SplittingField) x → Eq (DFunLike.coe σ x) (DFunLike.coe τ x))

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

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

Equations

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

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

Equations

• Eq (Polynomial.Gal.instUniqueOfFactSplitsId p) (Polynomial.Gal.uniqueGalOfSplits p ⋯)

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

Equations

• Eq Polynomial.Gal.uniqueGalZero (Polynomial.Gal.uniqueGalOfSplits 0 ⋯)

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

Equations

• Eq Polynomial.Gal.uniqueGalOne (Polynomial.Gal.uniqueGalOfSplits 1 ⋯)

def Polynomial.Gal.uniqueGalC {F : Type u_1} [Field F] (x : F) : Unique (DFunLike.coe C x).Gal

Equations

• Eq (Polynomial.Gal.uniqueGalC x) (Polynomial.Gal.uniqueGalOfSplits (DFunLike.coe Polynomial.C x) ⋯)

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

Equations

• Eq Polynomial.Gal.uniqueGalX (Polynomial.Gal.uniqueGalOfSplits Polynomial.X ⋯)

def Polynomial.Gal.uniqueGalXSubC {F : Type u_1} [Field F] (x : F) : Unique (HSub.hSub X (DFunLike.coe C x)).Gal

Equations

• Eq (Polynomial.Gal.uniqueGalXSubC x) (Polynomial.Gal.uniqueGalOfSplits (HSub.hSub Polynomial.X (DFunLike.coe Polynomial.C x)) ⋯)

def Polynomial.Gal.uniqueGalXPow {F : Type u_1} [Field F] (n : Nat) : Unique (HPow.hPow X n).Gal

Equations

• Eq (Polynomial.Gal.uniqueGalXPow n) (Polynomial.Gal.uniqueGalOfSplits (HPow.hPow Polynomial.X n) ⋯)

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

Equations

• Eq (Polynomial.Gal.instAlgebraSplittingFieldOfFactSplitsAlgebraMap p E) (Polynomial.IsSplittingField.lift p.SplittingField p ⋯).toAlgebra

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

def Polynomial.Gal.restrict {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Splits (algebraMap F E) p)] : MonoidHom (AlgEquiv F E E) p.Gal

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

Equations

• Eq (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 (Splits (algebraMap F E) p)] [Normal F E] : Function.Surjective (DFunLike.coe (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 (Splits (algebraMap F E) p)] : (p.rootSet p.SplittingField).Elem → (p.rootSet E).Elem

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

Equations

• Eq (Polynomial.Gal.mapRoots p E) (Set.MapsTo.restrict (DFunLike.coe (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 (Splits (algebraMap F E) p)] : Function.Bijective (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 (Splits (algebraMap F E) p)] : Equiv (p.rootSet p.SplittingField).Elem (p.rootSet E).Elem

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

Equations

• Eq (Polynomial.Gal.rootsEquivRoots p E) (Equiv.ofBijective (Polynomial.Gal.mapRoots p E) ⋯)

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

Equations

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

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

Equations

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

theorem Polynomial.Gal.smul_def {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Splits (algebraMap F E) p)] (ϕ : p.Gal) (x : (p.rootSet E).Elem) : Eq (HSMul.hSMul ϕ x) (DFunLike.coe (rootsEquivRoots p E) (HSMul.hSMul ϕ (DFunLike.coe (rootsEquivRoots p E).symm x)))

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

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

Equations

• Eq (Polynomial.Gal.galAction p E) { toSMul := Polynomial.Gal.smul p E, one_smul := ⋯, mul_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 (Splits (algebraMap F E) p)] (hp : Irreducible p) : MulAction.IsPretransitive p.Gal (p.rootSet E).Elem

theorem Polynomial.Gal.restrict_smul {F : Type u_1} [Field F] {p : Polynomial F} {E : Type u_2} [Field E] [Algebra F E] [Fact (Splits (algebraMap F E) p)] (ϕ : AlgEquiv F E E) (x : (p.rootSet E).Elem) : Eq (HSMul.hSMul (DFunLike.coe (restrict p E) ϕ) x).val (DFunLike.coe ϕ x.val)

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 (Splits (algebraMap F E) p)] : MonoidHom p.Gal (Equiv.Perm (p.rootSet E).Elem)

Polynomial.Gal.galAction as a permutation representation

Equations

• Eq (Polynomial.Gal.galActionHom p E) (MulAction.toPermHom p.Gal (p.rootSet E).Elem)

theorem Polynomial.Gal.galActionHom_restrict {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Splits (algebraMap F E) p)] (ϕ : AlgEquiv F E E) (x : (p.rootSet E).Elem) : Eq (DFunLike.coe (DFunLike.coe (galActionHom p E) (DFunLike.coe (restrict p E) ϕ)) x).val (DFunLike.coe ϕ x.val)

theorem Polynomial.Gal.galActionHom_injective {F : Type u_1} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Splits (algebraMap F E) p)] : Function.Injective (DFunLike.coe (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 q : Polynomial F} (hpq : Dvd.dvd p q) : MonoidHom q.Gal p.Gal

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

Equations

• Eq (Polynomial.Gal.restrictDvd hpq) (if hq : Eq 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 (Eq q 0)] (hpq : Dvd.dvd p q) : Eq (restrictDvd hpq) (if hq : Eq 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 : Dvd.dvd p q) (hq : Ne q 0) : Function.Surjective (DFunLike.coe (restrictDvd hpq))

def Polynomial.Gal.restrictProd {F : Type u_1} [Field F] (p q : Polynomial F) : MonoidHom (HMul.hMul p q).Gal (Prod p.Gal q.Gal)

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

Equations

• Eq (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 (DFunLike.coe (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₁ : Ne q₁ 0) (hq₂ : Ne q₂ 0) (h₁ : Splits (algebraMap F q₁.SplittingField) p₁) (h₂ : Splits (algebraMap F q₂.SplittingField) p₂) : Splits (algebraMap F (HMul.hMul q₁ q₂).SplittingField) (HMul.hMul p₁ p₂)

theorem Polynomial.Gal.splits_in_splittingField_of_comp {F : Type u_1} [Field F] (p q : Polynomial F) (hq : Ne q.natDegree 0) : 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} [Field F] (p q : Polynomial F) (hq : Ne q.natDegree 0) : MonoidHom (p.comp q).Gal p.Gal

Polynomial.Gal.restrict for the composition of polynomials.

Equations

• Eq (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 : Ne q.natDegree 0) : Function.Surjective (DFunLike.coe (restrictComp p q hq))

theorem Polynomial.Gal.card_of_separable {F : Type u_1} [Field F] {p : Polynomial F} (hp : p.Separable) : Eq (Fintype.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) : Dvd.dvd p.natDegree (Fintype.card p.Gal)