# mathlib3documentation

ring_theory.simple_module

# Simple Modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## 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.congr {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] (l : M ≃ₗ[R] N) [ N] :
theorem is_simple_module_iff_is_atom {R : Type u_1} [ring R] {M : Type u_2} [ M] {m : M} :
theorem is_simple_module_iff_is_coatom {R : Type u_1} [ring R] {M : Type u_2} [ M] {m : M} :
(M m)
theorem covby_iff_quot_is_simple {R : Type u_1} [ring R] {M : Type u_2} [ M] {A B : M} (hAB : A B) :
A B (B
@[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) :
theorem linear_map.is_coatom_ker_of_surjective {R : Type u_1} [ring R] {M : Type u_2} [ M] {N : Type u_3} [ N] [ N] {f : M →ₗ[R] N} (hf : function.surjective f) :
@[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
@[protected, instance]
def jordan_holder_module {R : Type u_1} [ring R] {M : Type u_2} [ M] :
Equations