English
On a finite module, IsFinitelySemisimple is equivalent to IsSemisimple.
Русский
На конечном модуле IsFinitelySemisimple эквивалентно IsSemisimple.
LaTeX
$$$ [Module.Finite R M] \Rightarrow (f.IsFinitelySemisimple \iff f.IsSemisimple)$$$
Lean4
protected theorem aeval (p : K[X]) : (aeval f p).IsSemisimple :=
let R := K[X] ⧸ Ideal.span {minpoly K f}
have : Module.Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| Algebra.IsIntegral.isIntegral f).finite
have : IsReduced R :=
(Ideal.isRadical_iff_quotient_reduced _).mp <| span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
isSemisimple_of_squarefree_aeval_eq_zero
((minpoly.isRadical K _).squarefree <|
minpoly.ne_zero <| .of_finite K <| Ideal.Quotient.mkₐ K (.span {minpoly K f}) p) <|
by
rw [←
Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f) fun a h ↦ by
rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h,
aeval_algHom, AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]
