Documentation

Mathlib.FieldTheory.PolynomialGaloisGroup

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 #

Main results #

Other results #

def Polynomial.Gal {F : Type u_1} [Field F] (p : Polynomial F) :
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} [Field F] (p : Polynomial F) :
    Group p.Gal
    Equations
    instance Polynomial.Gal.instFintype {F : Type u_1} [Field F] (p : Polynomial F) :
    Fintype p.Gal
    Equations
    instance Polynomial.Gal.instEquivLikeSplittingField {F : Type u_1} [Field F] (p : Polynomial F) :
    EquivLike p.Gal p.SplittingField p.SplittingField
    Equations
    instance Polynomial.Gal.instAlgEquivClassSplittingField {F : Type u_1} [Field F] (p : Polynomial F) :
    AlgEquivClass p.Gal F p.SplittingField p.SplittingField
    Equations
    • =
    instance Polynomial.Gal.applyMulSemiringAction {F : Type u_1} [Field F] (p : Polynomial F) :
    MulSemiringAction p.Gal p.SplittingField
    Equations
    theorem Polynomial.Gal.ext_iff {F : Type u_1} [Field F] {p : Polynomial F} {σ : p.Gal} {τ : p.Gal} :
    σ = τ xp.rootSet p.SplittingField, σ x = τ x
    theorem Polynomial.Gal.ext {F : Type u_1} [Field F] (p : Polynomial F) {σ : p.Gal} {τ : p.Gal} (h : xp.rootSet p.SplittingField, σ x = τ x) :
    σ = τ

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

    Equations
    Instances For
      Equations
      Equations
      instance Polynomial.Gal.uniqueGalC {F : Type u_1} [Field F] (x : F) :
      Unique (Polynomial.C x).Gal
      Equations
      instance Polynomial.Gal.uniqueGalX {F : Type u_1} [Field F] :
      Unique Polynomial.X.Gal
      Equations
      instance Polynomial.Gal.uniqueGalXSubC {F : Type u_1} [Field F] (x : F) :
      Unique (Polynomial.X - Polynomial.C x).Gal
      Equations
      instance Polynomial.Gal.uniqueGalXPow {F : Type u_1} [Field F] (n : ) :
      Unique (Polynomial.X ^ n).Gal
      Equations
      instance Polynomial.Gal.instIsScalarTowerSplittingField {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 p.SplittingField E
      Equations
      • =
      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) →* p.Gal

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

      Equations
      Instances For
        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)] :
        (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
          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)] :
          (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} [Field F] (p : Polynomial F) :
            MulAction p.Gal (p.rootSet p.SplittingField)
            Equations
            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 p.Gal (p.rootSet E)
            Equations
            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)] (ϕ : p.Gal) (x : (p.rootSet E)) :
            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 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} [Field F] (p : Polynomial F) (E : Type u_2) [Field E] [Algebra F E] [Fact (Polynomial.Splits (algebraMap F E) p)] (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 (Polynomial.Splits (algebraMap F E) p)] (ϕ : E ≃ₐ[F] E) (x : (p.rootSet 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)] :
            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} [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 : (p.rootSet E)) :
              (((Polynomial.Gal.galActionHom p E) ((Polynomial.Gal.restrict p E) ϕ)) x) = ϕ x

              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) :
              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} [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 q.SplittingField
                def Polynomial.Gal.restrictProd {F : Type u_1} [Field F] (p : Polynomial F) (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
                Instances For
                  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 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} [Field F] (p : Polynomial F) (q : Polynomial F) (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} [Field F] (p : Polynomial F) (q : Polynomial F) (hq : q.natDegree 0) :
                  (p.comp q).Gal →* p.Gal

                  Polynomial.Gal.restrict for the composition of polynomials.

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