English
In the finite case, a finite semisimple algebra is isomorphic to a matrix algebra over a finite division algebra, organized by a finite index set.
Русский
В конечном случае конечное полупрямое алгебро изоморфно матричной алгебре над конечным делением кольца, упорядоченным по конечному индексу.
LaTeX
$$$[Module.Finite \\; R_0 \\; R] \\Rightarrow \\exists n, D_i, d_i, (\\forall i, D_i \\text{ division ring}), (\\forall i, Algebra R_0 D_i), (\\forall i, Module.Finite R_0 D_i), (\\forall i, NeZero(d_i)) \\, \and \\, (R \\cong \\prod_i \\mathrm{Mat}_{d_i}(D_i))$$$
Lean4
/-- The **Wedderburn–Artin Theorem**, algebra form, finite case: a finite semisimple algebra is
isomorphic to a product of matrix algebras over finite division algebras. -/
theorem exists_algEquiv_pi_matrix_divisionRing_finite [Module.Finite R₀ R] :
∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (D i)) (_ : ∀ i, Algebra R₀ (D i)) (_ :
∀ i, Module.Finite R₀ (D i)),
(∀ i, NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) :=
by
have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing R₀ R
have := Module.Finite.equiv e.toLinearEquiv
refine ⟨n, D, d, _, _, fun i ↦ ?_, hd, ⟨e⟩⟩
let l := Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ .proj (φ := fun i ↦ Matrix (Fin (d i)) (Fin (d i)) _) i
exact .of_surjective l fun x ↦ ⟨fun j _ _ ↦ Function.update (fun _ ↦ 0) i x j, by simp [l]⟩
