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_C_isSolvable
{F : Type u_1}
[Field F]
(x : F)
:
IsSolvable (Polynomial.Gal (↑Polynomial.C x))
theorem
gal_X_sub_C_isSolvable
{F : Type u_1}
[Field F]
(x : F)
:
IsSolvable (Polynomial.Gal (Polynomial.X - ↑Polynomial.C x))
theorem
gal_X_pow_isSolvable
{F : Type u_1}
[Field F]
(n : ℕ)
:
IsSolvable (Polynomial.Gal (Polynomial.X ^ n))
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))
theorem
gal_prod_isSolvable
{F : Type u_1}
[Field F]
{s : Multiset (Polynomial F)}
(hs : ∀ (p : Polynomial F), p ∈ s → IsSolvable (Polynomial.Gal p))
:
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)
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)))
:
theorem
gal_X_pow_sub_one_isSolvable
{F : Type u_1}
[Field F]
(n : ℕ)
:
IsSolvable (Polynomial.Gal (Polynomial.X ^ n - 1))
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))
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.Gal (Polynomial.X ^ n - ↑Polynomial.C x))
- base: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : F), IsSolvableByRad F (↑(algebraMap F E) α)
- add: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α + β)
- neg: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), IsSolvableByRad F α → IsSolvableByRad F (-α)
- mul: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E), IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α * β)
- inv: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), IsSolvableByRad F α → IsSolvableByRad F α⁻¹
- rad: ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E) (n : ℕ), n ≠ 0 → IsSolvableByRad F (α ^ n) → IsSolvableByRad F α
Inductive definition of solvable by radicals
Instances For
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 α
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 α
def
solvableByRad.P
{F : Type u_1}
[Field F]
{E : Type u_2}
[Field E]
[Algebra F E]
(α : { x // x ∈ solvableByRad F E })
:
The statement to be proved inductively
Instances For
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))
:
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]
{α : { x // x ∈ solvableByRad F E }}
{β : { x // x ∈ solvableByRad F E }}
{γ : { x // x ∈ solvableByRad F E }}
(hγ : γ ∈ F⟮α, β⟯)
(hα : solvableByRad.P α)
(hβ : solvableByRad.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]
{α : { x // x ∈ solvableByRad F E }}
{β : { x // x ∈ solvableByRad F E }}
(hβ : β ∈ F⟮α⟯)
(hα : solvableByRad.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]
(α : { x // x ∈ solvableByRad F E })
:
IsSolvable (Polynomial.Gal (minpoly F α))
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