mathlib documentation

ring_theory.simple_module

Simple Modules #

Main Definitions #

Main Results #

TODO #

@[reducible]
def is_simple_module (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group M] [module R 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) [add_comm_group M] [module R 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) [add_comm_group M] [module R M] [is_simple_module R M] :
theorem is_simple_module_iff_is_atom {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {m : submodule R M} :
@[simp]
theorem is_simple_module.is_atom {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {m : submodule R M} [hm : is_simple_module R m] :
theorem is_semisimple_of_Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] (h : has_Sup.Sup {m : submodule R M | is_simple_module R m} = ) :
theorem is_semisimple_module.Sup_simples_eq_top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] [is_semisimple_module R M] :
@[protected, instance]
theorem is_semisimple_iff_top_eq_Sup_simples {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] :
theorem linear_map.injective_or_eq_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] (f : M →ₗ[R] N) :
theorem linear_map.injective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R 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} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R N] (f : M →ₗ[R] N) :
theorem linear_map.surjective_of_ne_zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R 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} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] [is_simple_module R N] (f : M →ₗ[R] N) :

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} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [is_simple_module R M] [is_simple_module R 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} [add_comm_group M] [module R M] [decidable_eq (module.End R M)] [is_simple_module R M] :

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

Equations