English
If there exists a squarefree polynomial p with aeval f p = 0, then f is semisimple.
Русский
Если существует квадратно-свободный многочлен p such that aeval f p = 0, то f семисемпсим.
LaTeX
$$$ \exists p \; Squarefree(p) \land aeval(f, p) = 0 \Rightarrow IsSemisimple(f)$$$
Lean4
theorem isSemisimple_of_squarefree_aeval_eq_zero {p : K[X]} (hp : Squarefree p) (hpf : aeval f p = 0) :
f.IsSemisimple :=
by
rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M), mem_annihilator, ← IsTorsionBy, ←
isTorsionBySet_singleton_iff, isTorsionBySet_iff_is_torsion_by_span] at hpf
let R := K[X] ⧸ Ideal.span { p }
have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)
have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite
have : IsArtinianRing R := .of_finite K R
have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R
letI : Module R (AEval' f) := Module.IsTorsionBySet.module hpf
let e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span { p })] AEval' f :=
{ AddMonoidHom.id _ with map_smul' := fun _ _ ↦ rfl }
exact (e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance
