endRingEquiv — Mathlib

English

The endomorphism ring of a semisimple module is the direct product of the endomorphism rings of its isotypic components.

Русский

Кольцо эндоморфизмов полупрямого модуля распадается на прямой произведение колец эндоморфизмов его изотипических компонент.

LaTeX

$$$\\mathrm{End}_R(M) \\cong_\\text{(prod)} \\prod_{c \\in \\mathrm{isotypicComponents} \\; R\\; M} \\mathrm{End}_R(c.1)$$$

Lean4

/-- The endomorphism ring of a semisimple module is the direct product of the endomorphism rings
of its isotypic components. -/
noncomputable def endRingEquiv : Module.End R M ≃+* Π c : isotypicComponents R M, Module.End R c.1 :=
  (endAlgEquiv ℕ R M).toRingEquiv

Похожие утверждения