Zero finitely generated modules

A finitely generated module with subsingleton carrier is a zero object of the category of finitely generated modules. This criterion supplies the zero components of finite-projective matrix factorizations.

theorem FGModuleCat.isZero_of_subsingleton {R : Type u} [Ring R] (M : FGModuleCat R) (hM : Subsingleton ↑M) : CategoryTheory.Limits.IsZero M

A finitely generated module with subsingleton carrier is a zero object.

instance FGModuleCat.hasZeroObject {R : Type u} [Ring R] : CategoryTheory.Limits.HasZeroObject (FGModuleCat R)

The zero module gives a zero object among finitely generated modules over any ring.