English
If p is an invariant submodule for f and f is IsFinitelySemisimple, then f.restrict hp is IsFinitelySemisimple.
Русский
Если p инвариантно относительно f и f IsFinitelySemisimple, тогда f|_p IsFinitelySemisimple.
LaTeX
$$$ p \in f.invtSubmodule \Rightarrow IsFinitelySemisimple(LinearMap.restrict f p) \\ (IsFinitelySemisimple(f))$$$
Lean4
theorem restrict {p : Submodule R M} (hp : p ∈ f.invtSubmodule) (hf : f.IsFinitelySemisimple) :
IsFinitelySemisimple (f.restrict hp) := by
intro q hq₁ hq₂
have := invtSubmodule.map_subtype_mem_of_mem_invtSubmodule f hp hq₁
let e : q ≃ₗ[R] q.map p.subtype := p.equivSubtypeMap q
rw [e.isSemisimple_iff ((LinearMap.restrict f hp).restrict hq₁) (LinearMap.restrict f this) rfl]
exact hf _ this (Finite.map q p.subtype)
