Documentation

Mathlib.FieldTheory.AbelRuffini

The Abel-Ruffini Theorem #

This file proves one direction of the Abel-Ruffini theorem, namely that if an element is solvable by radicals, then its minimal polynomial has solvable Galois group.

Main definitions #

Main results #

source
theorem gal_zero_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal 0)
source
theorem gal_one_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal 1)
source
theorem gal_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.Gal (↑Polynomial.C x))
source
theorem gal_X_isSolvable {F : Type u_1} [Field F] :
IsSolvable (Polynomial.Gal Polynomial.X)
source
theorem gal_X_sub_C_isSolvable {F : Type u_1} [Field F] (x : F) :
IsSolvable (Polynomial.Gal (Polynomial.X - ↑Polynomial.C x))
source
theorem gal_X_pow_isSolvable {F : Type u_1} [Field F] (n : ℕ) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n))
source
theorem gal_mul_isSolvable {F : Type u_1} [Field F] {p : Polynomial F} {q : Polynomial F} :
IsSolvable (Polynomial.Gal p) → IsSolvable (Polynomial.Gal q) → IsSolvable (Polynomial.Gal (p * q))
source
theorem gal_prod_isSolvable {F : Type u_1} [Field F] {s : Multiset (Polynomial F)} (hs : ∀ (p : Polynomial F), p ∈ s → IsSolvable (Polynomial.Gal p)) :
IsSolvable (Polynomial.Gal (Multiset.prod s))
source
theorem gal_isSolvable_of_splits {F : Type u_1} [Field F] {p : Polynomial F} {q : Polynomial F} :
Fact (Polynomial.Splits (algebraMap F (Polynomial.SplittingField q)) p) → IsSolvable (Polynomial.Gal q) → IsSolvable (Polynomial.Gal p)
source
theorem gal_isSolvable_tower {F : Type u_1} [Field F] (p : Polynomial F) (q : Polynomial F) (hpq : Polynomial.Splits (algebraMap F (Polynomial.SplittingField q)) p) (hp : IsSolvable (Polynomial.Gal p)) (hq : IsSolvable (Polynomial.Gal (Polynomial.map (algebraMap F (Polynomial.SplittingField p)) q))) :
IsSolvable (Polynomial.Gal q)
source
theorem gal_X_pow_sub_one_isSolvable {F : Type u_1} [Field F] (n : ℕ) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - 1))
source
theorem gal_X_pow_sub_C_isSolvable_aux {F : Type u_1} [Field F] (n : ℕ) (a : F) (h : Polynomial.Splits (RingHom.id F) (Polynomial.X ^ n - 1)) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - ↑Polynomial.C a))
source
theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type u_3} [Field F] {E : Type u_4} [Field E] (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : Polynomial.Splits i (Polynomial.X ^ n - ↑Polynomial.C a)) :
Polynomial.Splits i (Polynomial.X ^ n - 1)
source
theorem gal_X_pow_sub_C_isSolvable {F : Type u_1} [Field F] (n : ℕ) (x : F) :
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - ↑Polynomial.C x))
source
inductive IsSolvableByRad (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] :
E → Prop

Inductive definition of solvable by radicals

Instances For
    source
    def solvableByRad (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :
    IntermediateField F E

    The intermediate field of solvable-by-radicals elements

    Instances For
      source
      theorem solvableByRad.induction {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : { x // x ∈ solvableByRad F E } → Prop) (base : (α : F) → P (↑(algebraMap F { x // x ∈ solvableByRad F E }) α)) (add : (α β : { x // x ∈ solvableByRad F E }) → P α → P β → P (α + β)) (neg : (α : { x // x ∈ solvableByRad F E }) → P α → P (-α)) (mul : (α β : { x // x ∈ solvableByRad F E }) → P α → P β → P (α * β)) (inv : (α : { x // x ∈ solvableByRad F E }) → P α → P α⁻¹) (rad : (α : { x // x ∈ solvableByRad F E }) → (n : ℕ) → n ≠ 0 → P (α ^ n) → P α) (α : { x // x ∈ solvableByRad F E }) :
      P α
      source
      theorem solvableByRad.isIntegral {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x ∈ solvableByRad F E }) :
      IsIntegral F α
      source
      def solvableByRad.P {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x ∈ solvableByRad F E }) :
      Prop

      The statement to be proved inductively

      Instances For
        source
        theorem solvableByRad.induction3 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x ∈ solvableByRad F E }} {n : ℕ} (hn : n ≠ 0) (hα : solvableByRad.P (α ^ n)) :
        solvableByRad.P α

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        source
        theorem solvableByRad.induction2 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x ∈ solvableByRad F E }} {β : { x // x ∈ solvableByRad F E }} {γ : { x // x ∈ solvableByRad F E }} (hγ : γ ∈ F⟮α, β⟯) (hα : solvableByRad.P α) (hβ : solvableByRad.P β) :
        solvableByRad.P γ

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        source
        theorem solvableByRad.induction1 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : { x // x ∈ solvableByRad F E }} {β : { x // x ∈ solvableByRad F E }} (hβ : β ∈ F⟮α⟯) (hα : solvableByRad.P α) :
        solvableByRad.P β

        An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.

        source
        theorem solvableByRad.isSolvable {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : { x // x ∈ solvableByRad F E }) :
        IsSolvable (Polynomial.Gal (minpoly F α))
        source
        theorem solvableByRad.isSolvable' {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {q : Polynomial F} (q_irred : Irreducible q) (q_aeval : ↑(Polynomial.aeval α) q = 0) (hα : IsSolvableByRad F α) :
        IsSolvable (Polynomial.Gal q)

        Abel-Ruffini Theorem (one direction): An irreducible polynomial with an IsSolvableByRad root has solvable Galois group