Wedderburn-Artin Theorem

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

theorem IsSimpleRing.isIsotypic (R : Type u) [Ring R] [IsSimpleRing R] [IsArtinianRing R] : IsIsotypic R R

@[instance 100]

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

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.