exists_end_ringEquiv — Mathlib

English

There exists an equivalence between End_R(M) and a product of matrix rings built from simple components.

Русский

Существует эквалентность между End_R(M) и произведением матричных колец, построенных из простых компонент.

LaTeX

$$$\\exists n, S, d, \\text{IsSimpleModule}(R,S_i) \\land \\text{End}_R(M) \\cong \\prod_i \\mathrm{Mat}_{\\;d_i}(\\mathrm{End}_R(S_i))$$$

Lean4

theorem exists_end_ringEquiv :
    ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
      (∀ i, IsSimpleModule R (S i)) ∧
        (∀ i, NeZero (d i)) ∧ Nonempty (End R M ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (End R (S i))) :=
  have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_end_algEquiv ℕ R M;
  ⟨n, S, d, hS, hd, ⟨e⟩⟩

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