English
If p is an invariant submodule for f and f is semisimple, then the restricted endomorphism f|_p is semisimple.
Русский
Если p является инвариантным подпроизведением для f и f семисемпсимален, то ограниченный эндоморфизм f|_p семисемпсим.
LaTeX
$$$ p \in f.invtSubmodule \Rightarrow IsSemisimple(f|_p) \\ (IsSemisimple(f))$$$
Lean4
theorem restrict {p : Submodule R M} (hp : p ∈ f.invtSubmodule) (hf : f.IsSemisimple) : IsSemisimple (f.restrict hp) :=
by
rw [IsSemisimple] at hf ⊢
let e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
(Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans <| Submodule.mapIic _
exact (isSemisimpleModule_iff ..).mpr (e.complementedLattice_iff.mpr inferInstance)
