Simple quotients of modules

A nonzero module with a coatomic submodule lattice has a simple quotient. In particular this applies to nonzero Noetherian modules. The categorical statement provides an epimorphism to a simple object, so it can be transported along equivalences of module and representation categories.

theorem ModuleCat.exists_epi_simple {R : Type u_1} [Ring R] (M : ModuleCat R) [IsCoatomic (Submodule R ↑M)] (hM : ¬CategoryTheory.Limits.IsZero M) : ∃ (S : ModuleCat R), CategoryTheory.Simple S ∧ ∃ (f : M ⟶ S), CategoryTheory.Epi f

A nonzero module whose submodule lattice is coatomic admits an epimorphism to a simple module.