English
The Wedderburn–Artin theorem in algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over the opposite of the endomorphism algebra of its simple module.
Русский
Теорема Уеддерберна–Артин в алгебраической форме: артинское простое алгебро изоморфно матричной алгебре над противоположной End-модуля простого модуля.
LaTeX
$$$\\exists n, I, \\text{IsSimpleModule}(R,I), \\exists e : R \\cong \\mathrm{Mat}_{n}(\\mathrm{End}_R(I)^{op})$$$
Lean4
/-- The **Wedderburn–Artin Theorem**, algebra form, finite case: a finite Artinian simple algebra is
isomorphic to a matrix algebra over a finite division algebra. -/
theorem exists_algEquiv_matrix_divisionRing_finite [Module.Finite R₀ R] :
∃ (n : ℕ) (_ : NeZero n) (D : Type u) (_ : DivisionRing D) (_ : Algebra R₀ D) (_ : Module.Finite R₀ D),
Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D) :=
by
have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R
have := Module.Finite.equiv e.toLinearEquiv
classical
exact
⟨n, hn, _, _, _, .of_surjective (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩,
⟨e⟩⟩
