# mathlibdocumentation

ring_theory.simple_module

# Simple Modules #

## Main Definitions #

• is_simple_module indicates that a module has no proper submodules (the only submodules are ⊥ and ⊤).
• is_semisimple_module indicates that every submodule has a complement, or equivalently, the module is a direct sum of simple modules.
• A division_ring structure on the endomorphism ring of a simple module.

## Main Results #

• Schur's Lemma: bijective_or_eq_zero shows that a linear map between simple modules is either bijective or 0, leading to a division_ring structure on the endomorphism ring.

## TODO #

• Artin-Wedderburn Theory
• Unify with the work on Schur's Lemma in a category theory context
@[reducible]
def is_simple_module (R : Type u_1) [ring R] (M : Type u_2) [ M] :
Prop

A module is simple when it has only two submodules, ⊥ and ⊤.

@[reducible]
def is_semisimple_module (R : Type u_1) [ring R] (M : Type u_2) [ M] :
Prop

A module is semisimple when every submodule has a complement, or equivalently, the module is a direct sum of simple modules.

theorem is_simple_module.nontrivial (R : Type u_1) [ring R] (M : Type u_2) [ M] [ M] :
theorem is_simple_module_iff_is_atom {R : Type u_1} [ring R] {M : Type u_2} [ M] {m : M} :
@[simp]
theorem is_simple_module.is_atom {R : Type u_1} [ring R] {M : Type u_2} [ M] {m : M} [hm : m] :
theorem is_semisimple_of_Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [ M] (h : has_Sup.Sup {m : M | = ) :
theorem is_semisimple_module.Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [ M] [ M] :
has_Sup.Sup {m : M | =
@[protected, instance]
def is_semisimple_module.is_semisimple_submodule {R : Type u_1} [ring R] {M : Type u_2} [ M] [ M] {m : M} :
theorem is_semisimple_iff_top_eq_Sup_simples {R : Type u_1} [ring R] {M : Type u_2} [ M] :
has_Sup.Sup {m : M | =
theorem linear_map.injective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] (f : M →ₗ[R] N) :
f = 0
theorem linear_map.injective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] {f : M →ₗ[R] N} (h : f 0) :
theorem linear_map.surjective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ N] (f : M →ₗ[R] N) :
f = 0
theorem linear_map.surjective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ N] {f : M →ₗ[R] N} (h : f 0) :
theorem linear_map.bijective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ N] (f : M →ₗ[R] N) :
f = 0

Schur's Lemma for linear maps between (possibly distinct) simple modules

theorem linear_map.bijective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ M] [ N] {f : M →ₗ[R] N} (h : f 0) :
@[protected, instance]
noncomputable def module.End.division_ring {R : Type u_1} [ring R] {M : Type u_2} [ M] [decidable_eq M)] [ M] :

Schur's Lemma makes the endomorphism ring of a simple module a division ring.

Equations