exists_algEquiv_matrix_divisionRing

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 \\prod_{c \\in \\mathrm{isotypicComponents} \\; R\\; M} \\mathrm{End}_R(c.1)$$$

Lean4

/-- The **Wedderburn–Artin Theorem**, algebra form: an Artinian simple algebra is isomorphic
to a matrix algebra over a division algebra. -/
theorem exists_algEquiv_matrix_divisionRing :
    ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (_ : DivisionRing D) (_ : Algebra R₀ D),
      Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D) :=
  by
  have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R
  classical exact ⟨n, hn, _, _, _, ⟨e⟩⟩

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