Simple objects in the category of R-modules

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

theorem simple_iff_isSimpleModule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : CategoryTheory.Simple (ModuleCat.of R M) ↔ IsSimpleModule R M

theorem simple_iff_isSimpleModule' {R : Type u_1} [Ring R] (M : ModuleCat R) : CategoryTheory.Simple M ↔ IsSimpleModule R ↑M

instance simple_of_isSimpleModule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSimpleModule R M] : CategoryTheory.Simple (ModuleCat.of R M)

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

instance isSimpleModule_of_simple {R : Type u_1} [Ring R] (M : ModuleCat R) [CategoryTheory.Simple M] : IsSimpleModule R ↑M

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

theorem simple_of_finrank_eq_one {R : Type u_1} [Ring R] {k : Type u_3} [Field k] [Algebra k R] {V : ModuleCat R} (h : Module.finrank k ↑V = 1) : CategoryTheory.Simple V

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