English
Let p and q be polynomials in F[x]. If p splits over the splitting field of q via the natural map, and p has solvable Galois group, and the Galois group of q mapped to the splitting field of p is solvable, then q itself has a solvable Galois group.
Русский
Пусть p и q — полиномы над полем F. Если p распадается над полем разложений q через естественный отображение, и Gal(p) разрешим, и Gal(q.map( F → p.SplittingField)) разрешим, тогда Gal(q) разрешим.
LaTeX
$$$$\forall p,q \in F[X],\ p.Splits(\mathrm{algebraMap}\ F\ q.SplittingField) \\quad \Rightarrow\ IsSolvable(p.Gal) \\quad \Rightarrow\ IsSolvable\big((q.map(\mathrm{algebraMap}\ F\ p.SplittingField)).Gal\big) \\quad \Rightarrow\ IsSolvable(q.Gal)$$$$
Lean4
theorem gal_isSolvable_tower (p q : F[X]) (hpq : p.Splits (algebraMap F q.SplittingField)) (hp : IsSolvable p.Gal)
(hq : IsSolvable (q.map (algebraMap F p.SplittingField)).Gal) : IsSolvable q.Gal :=
by
let K := p.SplittingField
let L := q.SplittingField
haveI : Fact (p.Splits (algebraMap F L)) := ⟨hpq⟩
let ϕ : (L ≃ₐ[K] L) ≃* (q.map (algebraMap F K)).Gal := (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr
have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
haveI : IsSolvable (K ≃ₐ[F] K) := hp
haveI : IsSolvable (L ≃ₐ[K] L) := solvable_of_solvable_injective ϕ_inj
exact isSolvable_of_isScalarTower F p.SplittingField q.SplittingField
