Wedderburn–Artin Theorem

Main results

• IsSimpleRing.tfae: a simple ring is semisimple iff it is Artinian, iff it has a minimal left ideal.

• isSimpleRing_isArtinianRing_iff: a ring is simple Artinian iff it is semisimple, isotypic, and nontrivial.

• IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite: a simple Artinian algebra is isomorphic to a (finite-dimensional) matrix algebra over a division algebra. The division algebra is the opposite of the endomorphism algebra of a simple (i.e., minimal) left ideal.

• IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite: a semisimple algebra is isomorphic to a finite direct product of matrix algebras over division algebras. The division algebras are the opposites of the endomorphism algebras of the simple (i.e., minimal) left ideals.

• IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite: if the simple Artinian / semisimple algebra is finite as a module over a base ring, then the division algebra(s) are also finite over the same ring. If the base ring is an algebraically closed field, the only finite-dimensional division algebra over it is itself, and we obtain IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed and IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed (in a later file).

theorem IsSimpleRing.tfae {R : Type u} [Ring R] [IsSimpleRing R] : [IsSemisimpleRing R, IsArtinianRing R, ∃ (I : Ideal R), IsAtom I].TFAE

A simple ring is semisimple iff it is Artinian, iff it has a minimal left ideal.

theorem IsSimpleRing.isSemisimpleRing_iff_isArtinianRing {R : Type u} [Ring R] [IsSimpleRing R] : IsSemisimpleRing R ↔ IsArtinianRing R

theorem isSimpleRing_isArtinianRing_iff {R : Type u} [Ring R] : IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

@[instance 100]

instance IsSimpleRing.instIsSemisimpleRing (R : Type u) [Ring R] [IsSimpleRing R] [IsArtinianRing R] : IsSemisimpleRing R

theorem IsSimpleRing.isIsotypic (R : Type u) [Ring R] [IsSimpleRing R] [IsArtinianRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : IsIsotypic R M

theorem IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite (R : Type u) [Ring R] [IsSimpleRing R] [IsArtinianRing R] : ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

The Wedderburn–Artin Theorem: an Artinian simple ring is isomorphic to a matrix ring over the opposite of the endomorphism ring of its simple module.

theorem IsSimpleRing.exists_ringEquiv_matrix_divisionRing (R : Type u) [Ring R] [IsSimpleRing R] [IsArtinianRing R] : ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D), Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)

The Wedderburn–Artin Theorem: an Artinian simple ring is isomorphic to a matrix ring over a division ring.

theorem IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSimpleRing R] [IsArtinianRing R] : ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

The Wedderburn–Artin Theorem, algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over the opposite of the endomorphism algebra of its simple module.

theorem IsSimpleRing.exists_algEquiv_matrix_divisionRing (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSimpleRing R] [IsArtinianRing R] : ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

The Wedderburn–Artin Theorem, algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over a division algebra.

theorem IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSimpleRing R] [IsArtinianRing R] [Module.Finite R₀ R] : ∃ (n : ℕ) (_ : NeZero n) (D : Type u) (x : DivisionRing D) (x_1 : Algebra R₀ D) (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

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 IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] (M : Type v) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i)))

theorem IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))))

@[deprecated IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end (since := "2025-11-16")]

theorem IsSemisimpleModule.exists_end_algEquiv (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] (M : Type v) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i)))

Alias of IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end.

@[deprecated IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end (since := "2025-11-16")]

theorem IsSemisimpleModule.exists_end_ringEquiv (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))))

Alias of IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end.

theorem IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] (M : Type v) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 : (i : Fin n) → Algebra R₀ (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

theorem IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))

theorem IsSemisimpleRing.moduleEnd (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : IsSemisimpleRing (Module.End R M)

theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSemisimpleRing R] : ∃ (n : ℕ) (S : Fin n → Ideal R) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))ᵐᵒᵖ)

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 IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSemisimpleRing R] : ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 : (i : Fin n) → Algebra R₀ (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

The Wedderburn–Artin Theorem, algebra form: a semisimple algebra is isomorphic to a product of matrix algebras over division algebras.

theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSemisimpleRing R] [Module.Finite R₀ R] : ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)) (x_1 : (i : Fin n) → Algebra R₀ (D i)) (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

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 IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite (R : Type u) [Ring R] [IsSemisimpleRing R] : ∃ (n : ℕ) (D : Fin n → Ideal R) (d : Fin n → ℕ), (∀ (i : Fin n), IsSimpleModule R ↥(D i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(D i))ᵐᵒᵖ))

The Wedderburn–Artin Theorem: a semisimple ring is isomorphic to a product of matrix rings over the opposite of the endomorphism rings of its simple modules.

theorem IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing (R : Type u) [Ring R] [IsSemisimpleRing R] : ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))

The Wedderburn–Artin Theorem: a semisimple ring is isomorphic to a product of matrix rings over division rings.

instance IsSemisimpleRing.instMatrix (R : Type u) [Ring R] [IsSemisimpleRing R] (n : Type u_2) [Fintype n] [DecidableEq n] : IsSemisimpleRing (Matrix n n R)

instance IsSemisimpleRing.instMulOpposite (R : Type u) [Ring R] [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ

theorem isSemisimpleRing_mulOpposite_iff {R : Type u} [Ring R] : IsSemisimpleRing Rᵐᵒᵖ ↔ IsSemisimpleRing R

theorem isSemisimpleRing_iff_pi_matrix_divisionRing {R : Type u} [Ring R] : IsSemisimpleRing R ↔ ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (x : (i : Fin n) → DivisionRing (D i)), Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))

The existence part of the Artin–Wedderburn theorem.