English
IsFinitelySemisimple(f) iff for all invariant p, hp, and finite p, all q ≤ p in invtSubmodule f, there exists r ≤ p with r ∈ invtSubmodule f and disjointness and equality conditions.
Русский
IsFinitelySemisimple(f) эквивалентно условию на подрешётке: для каждого инвариантного p существует q и r с нужными свойствами.
LaTeX
$$$$ f.IsFinitelySemisimple \\iff \\forall p (hp : p \\in invtSubmodule f), Module.Finite R p \\rightarrow \\forall q \\in invtSubmodule f, q \\le p \\rightarrow \\exists r \\le p, r \\in invtSubmodule f \\land Disjoint q r \\land q \\sqcup r = p. $$$$
Lean4
theorem isSemisimple_restrict_iff (p) (hp : p ∈ invtSubmodule f) :
IsSemisimple (LinearMap.restrict f hp) ↔
∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p :=
by
let e : Submodule R[X] (AEval' (f.restrict hp)) ≃o Iic (AEval.mapSubmodule R M f ⟨p, hp⟩) :=
(Submodule.orderIsoMapComap <| AEval.restrict_equiv_mapSubmodule f p hp).trans (Submodule.mapIic _)
simp_rw [IsSemisimple, isSemisimpleModule_iff, e.complementedLattice_iff, disjoint_iff, ←
(OrderIso.Iic _ _).complementedLattice_iff, Iic.complementedLattice_iff, Subtype.forall, Subtype.exists,
Subtype.mk_le_mk, Sublattice.mk_inf_mk, Sublattice.mk_sup_mk, Subtype.mk.injEq, exists_and_left, exists_and_right,
invtSubmodule.mk_eq_bot_iff, exists_prop, and_assoc]
rfl
