English
An auxiliary induction lemma: if γ lies in adjoin(α,β) and P holds for α and β, then P holds for γ.
Русский
Вспомогательная лемма индукции: если γ лежит в адьюнтом(α,β) и P верно для α,β, тогда P верно и для γ.
LaTeX
$$$$\gamma \in F⟮\alpha, \beta⟯ \Rightarrow P(\alpha) \Rightarrow P(\beta) \Rightarrow P(\gamma)$$$$
Lean4
/-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ :=
by
let p := minpoly F α
let q := minpoly F β
have hpq :=
Polynomial.splits_of_splits_mul _ (mul_ne_zero (minpoly.ne_zero (isIntegral α)) (minpoly.ne_zero (isIntegral β)))
(SplittingField.splits (p * q))
let f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField :=
Classical.choice <|
nonempty_algHom_adjoin_of_splits <| by
intro x hx
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx
cases hx with rw [hx]
| inl hx => exact ⟨isIntegral α, hpq.1⟩
| inr hx => exact ⟨isIntegral β, hpq.2⟩
have key : minpoly F γ = minpoly F (f ⟨γ, hγ⟩) :=
by
refine minpoly.eq_of_irreducible_of_monic (minpoly.irreducible (isIntegral γ)) ?_ (minpoly.monic (isIntegral γ))
rw [aeval_algHom_apply, map_eq_zero]
apply (algebraMap (↥F⟮α, β⟯) (solvableByRad F E)).injective
simp only [map_zero, ← aeval_algebraMap_apply]
exact minpoly.aeval F γ
rw [P, key]
refine gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨γ, hγ⟩)⟩ (gal_mul_isSolvable hα hβ)
apply SplittingField.instNormal
