mathlib3 documentation

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 #

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.congr {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] (l : M ≃ₗ[R] N) [is_simple_module R N] :
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} :
theorem is_simple_module_iff_is_coatom {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {m : submodule R M} :
theorem covby_iff_quot_is_simple {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {A B : submodule R M} (hAB : A B) :
@[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] :
@[protected, instance]
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