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 #
solvableByRad F E: the intermediate field of solvable-by-radicals elements
Main results #
- the Abel-Ruffini Theorem
solvableByRad.isSolvable': An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.
theorem
gal_mul_isSolvable
{F : Type u_1}
[Field F]
{p q : Polynomial F}
:
IsSolvable p.Gal → IsSolvable q.Gal → IsSolvable (p * q).Gal
theorem
gal_prod_isSolvable
{F : Type u_1}
[Field F]
{s : Multiset (Polynomial F)}
(hs : ∀ p ∈ s, IsSolvable p.Gal)
:
theorem
gal_isSolvable_of_splits
{F : Type u_1}
[Field F]
{p q : Polynomial F}
:
Fact (Polynomial.Splits (algebraMap F q.SplittingField) p) → ∀ (hq : IsSolvable q.Gal), IsSolvable p.Gal
theorem
gal_isSolvable_tower
{F : Type u_1}
[Field F]
(p q : Polynomial F)
(hpq : Polynomial.Splits (algebraMap F q.SplittingField) p)
(hp : IsSolvable p.Gal)
(hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal)
:
theorem
gal_X_pow_sub_one_isSolvable
{F : Type u_1}
[Field F]
(n : ℕ)
:
IsSolvable (Polynomial.X ^ n - 1).Gal
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.X ^ n - Polynomial.C a).Gal
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)
theorem
gal_X_pow_sub_C_isSolvable
{F : Type u_1}
[Field F]
(n : ℕ)
(x : F)
:
IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal
Inductive definition of solvable by radicals
- base {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : F) : IsSolvableByRad F ((algebraMap F E) α)
- add {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α β : E) : IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α + β)
- neg {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) : IsSolvableByRad F α → IsSolvableByRad F (-α)
- mul {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α β : E) : IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)
- inv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) : IsSolvableByRad F α → IsSolvableByRad F α⁻¹
- rad {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (n : ℕ) (hn : n ≠ 0) : IsSolvableByRad F (α ^ n) → IsSolvableByRad F α
The intermediate field of solvable-by-radicals elements
Equations
- solvableByRad F E = { carrier := IsSolvableByRad F, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, inv_mem' := ⋯ }
theorem
solvableByRad.induction
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(P : ↥(solvableByRad F E) → Prop)
(base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α))
(add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β))
(neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α))
(mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β))
(inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹)
(rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α)
(α : ↥(solvableByRad F E))
:
P α
theorem
solvableByRad.isIntegral
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : ↥(solvableByRad F E))
:
IsIntegral F α
def
solvableByRad.P
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : ↥(solvableByRad F E))
:
The statement to be proved inductively
Equations
- solvableByRad.P α = IsSolvable (minpoly F α).Gal
theorem
solvableByRad.induction3
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{α : ↥(solvableByRad F E)}
{n : ℕ}
(hn : n ≠ 0)
(hα : P (α ^ n))
:
P α
An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.
theorem
solvableByRad.induction2
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{α β γ : ↥(solvableByRad F E)}
(hγ : γ ∈ F⟮α, β⟯)
(hα : P α)
(hβ : P β)
:
P γ
An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.
theorem
solvableByRad.induction1
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
{α β : ↥(solvableByRad F E)}
(hβ : β ∈ F⟮α⟯)
(hα : P α)
:
P β
An auxiliary induction lemma, which is generalized by solvableByRad.isSolvable.
theorem
solvableByRad.isSolvable
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : ↥(solvableByRad F E))
:
IsSolvable (minpoly F α).Gal
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 α)
:
Abel-Ruffini Theorem (one direction): An irreducible polynomial with an
IsSolvableByRad root has solvable Galois group