English
A semisimple ring has a decomposition into a product of matrix rings over the opposite endomorphism rings of its simple modules.
Русский
Полупрямое разложение простых модулей кольца через матричные кольца над противоположной End-модуля.
LaTeX
$$$R \\simeq_{\\text{prod}} \\prod_i \\mathrm{Mat}_{d_i}(\\mathrm{End}_R(S_i))^{op}$$$
Lean4
/-- The **Wedderburn–Artin Theorem**, algebra form: a semisimple algebra is isomorphic to a
product of matrix algebras over the opposite of the endomorphism algebras of its simple modules. -/
theorem exists_algEquiv_pi_matrix_end_mulOpposite :
∃ (n : ℕ) (S : Fin n → Ideal R) (d : Fin n → ℕ),
(∀ i, IsSimpleModule R (S i)) ∧
(∀ i, NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (Module.End R (S i))ᵐᵒᵖ) :=
have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := IsSemisimpleModule.exists_end_algEquiv R₀ R R
⟨n, S, d, hS, hd,
⟨.trans (.opOp R₀ R) <|
.trans (.op <| .trans (.moduleEndSelf R₀) e) <|
.trans (.piMulOpposite _ _) (.piCongrRight fun _ ↦ .symm .mopMatrix)⟩⟩
