mathlib3 documentation

algebra.category.Module.simple

Simple objects in the category of R-modules #

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

We prove simple modules are exactly simple objects in the category of R-modules.

source
theorem simple_iff_is_simple_module {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
category_theory.simple (Module.of R M) ↔ is_simple_module R M
source
theorem simple_iff_is_simple_module' {R : Type u_1} [ring R] (M : Module R) :
category_theory.simple M ↔ is_simple_module R ↥M
source
@[protected, instance]
def simple_of_is_simple_module {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_simple_module R M] :
category_theory.simple (Module.of R M)

A simple module is a simple object in the category of modules.

source
@[protected, instance]
def is_simple_module_of_simple {R : Type u_1} [ring R] (M : Module R) [category_theory.simple M] :
is_simple_module R ↥M

A simple object in the category of modules is a simple module.

source
theorem simple_of_finrank_eq_one {R : Type u_1} [ring R] {k : Type u_2} [field k] [algebra k R] {V : Module R} (h : finite_dimensional.finrank k ↥V = 1) :
category_theory.simple V

Any k-algebra module which is 1-dimensional over k is simple.