English
The endomorphism algebra of a semisimple module is isomorphic to the direct product of the endomorphism algebras of its isotypic components.
Русский
Алгебра эндоморфизмов полупрямого модуля изотропно распадается на прямой произведение эндоморфизмов его изотипических компонент.
LaTeX
$$$\\mathrm{End}_R(M) \\cong_{{\\text{ALG}}} \\prod_{c \\in \\mathrm{isotypicComponents} \\; R\\; M} \\mathrm{End}_R(c.1)$$$
Lean4
/-- The endomorphism algebra of a semisimple module is the direct product of the endomorphism
algebras of its isotypic components. -/
noncomputable def endAlgEquiv : Module.End R M ≃ₐ[R₀] Π c : isotypicComponents R M, Module.End R c.1 :=
((sSupIndep_iff _).mp <| sSupIndep_isotypicComponents R M).algEquiv R₀
((sSup_eq_iSup' _).symm.trans <| sSup_isotypicComponents R M) (.of_mem_isotypicComponents ·.2)
