The Abel-Ruffini Theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
solvable_by_rad F E: the intermediate field of solvable-by-radicals elements
Main results #
- the Abel-Ruffini Theorem
solvable_by_rad.is_solvable': An irreducible polynomial with a root that is solvable by radicals has a solvable Galois group.
theorem
gal_mul_is_solvable
{F : Type u_1}
[field F]
{p q : polynomial F}
(hp : is_solvable p.gal)
(hq : is_solvable q.gal) :
is_solvable (p * q).gal
theorem
gal_prod_is_solvable
{F : Type u_1}
[field F]
{s : multiset (polynomial F)}
(hs : ∀ (p : polynomial F), p ∈ s → is_solvable p.gal) :
theorem
gal_is_solvable_of_splits
{F : Type u_1}
[field F]
{p q : polynomial F}
(hpq : fact (polynomial.splits (algebra_map F q.splitting_field) p))
(hq : is_solvable q.gal) :
theorem
gal_is_solvable_tower
{F : Type u_1}
[field F]
(p q : polynomial F)
(hpq : polynomial.splits (algebra_map F q.splitting_field) p)
(hp : is_solvable p.gal)
(hq : is_solvable (polynomial.map (algebra_map F p.splitting_field) q).gal) :
theorem
gal_X_pow_sub_one_is_solvable
{F : Type u_1}
[field F]
(n : ℕ) :
is_solvable (polynomial.X ^ n - 1).gal
theorem
gal_X_pow_sub_C_is_solvable_aux
{F : Type u_1}
[field F]
(n : ℕ)
(a : F)
(h : polynomial.splits (ring_hom.id F) (polynomial.X ^ n - 1)) :
is_solvable (polynomial.X ^ n - ⇑polynomial.C a).gal
theorem
splits_X_pow_sub_one_of_X_pow_sub_C
{F : Type u_1}
[field F]
{E : Type u_2}
[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_is_solvable
{F : Type u_1}
[field F]
(n : ℕ)
(x : F) :
is_solvable (polynomial.X ^ n - ⇑polynomial.C x).gal
inductive
is_solvable_by_rad
(F : Type u_1)
[field F]
{E : Type u_2}
[field E]
[algebra F E] :
E → Prop
- base : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α : F), is_solvable_by_rad F (⇑(algebra_map F E) α)
- add : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α β : E), is_solvable_by_rad F α → is_solvable_by_rad F β → is_solvable_by_rad F (α + β)
- neg : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α : E), is_solvable_by_rad F α → is_solvable_by_rad F (-α)
- mul : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α β : E), is_solvable_by_rad F α → is_solvable_by_rad F β → is_solvable_by_rad F (α * β)
- inv : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α : E), is_solvable_by_rad F α → is_solvable_by_rad F α⁻¹
- rad : ∀ {F : Type u_1} [_inst_1 : field F] {E : Type u_2} [_inst_2 : field E] [_inst_3 : algebra F E] (α : E) (n : ℕ), n ≠ 0 → is_solvable_by_rad F (α ^ n) → is_solvable_by_rad F α
Inductive definition of solvable by radicals
The intermediate field of solvable-by-radicals elements
Equations
- solvable_by_rad F E = {to_subalgebra := {carrier := is_solvable_by_rad F _inst_3, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}, neg_mem' := _, inv_mem' := _}
theorem
solvable_by_rad.induction
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(P : ↥(solvable_by_rad F E) → Prop)
(base : ∀ (α : F), P (⇑(algebra_map F ↥(solvable_by_rad F E)) α))
(add : ∀ (α β : ↥(solvable_by_rad F E)), P α → P β → P (α + β))
(neg : ∀ (α : ↥(solvable_by_rad F E)), P α → P (-α))
(mul : ∀ (α β : ↥(solvable_by_rad F E)), P α → P β → P (α * β))
(inv : ∀ (α : ↥(solvable_by_rad F E)), P α → P α⁻¹)
(rad : ∀ (α : ↥(solvable_by_rad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α)
(α : ↥(solvable_by_rad F E)) :
P α
theorem
solvable_by_rad.is_integral
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : ↥(solvable_by_rad F E)) :
is_integral F α
def
solvable_by_rad.P
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : ↥(solvable_by_rad F E)) :
Prop
The statement to be proved inductively
Equations
- solvable_by_rad.P α = is_solvable (minpoly F α).gal
theorem
solvable_by_rad.induction3
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α : ↥(solvable_by_rad F E)}
{n : ℕ}
(hn : n ≠ 0)
(hα : solvable_by_rad.P (α ^ n)) :
An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.
theorem
solvable_by_rad.induction2
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α β γ : ↥(solvable_by_rad F E)}
(hγ : γ ∈ F⟮α, β⟯)
(hα : solvable_by_rad.P α)
(hβ : solvable_by_rad.P β) :
An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.
theorem
solvable_by_rad.induction1
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
{α β : ↥(solvable_by_rad F E)}
(hβ : β ∈ F⟮α⟯)
(hα : solvable_by_rad.P α) :
An auxiliary induction lemma, which is generalized by solvable_by_rad.is_solvable.
theorem
solvable_by_rad.is_solvable
{F : Type u_1}
[field F]
{E : Type u_2}
[field E]
[algebra F E]
(α : ↥(solvable_by_rad F E)) :
is_solvable (minpoly F α).gal
theorem
solvable_by_rad.is_solvable'
{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α : is_solvable_by_rad F α) :
Abel-Ruffini Theorem (one direction): An irreducible polynomial with an
is_solvable_by_rad root has solvable Galois group