Noetherian objects in FGModuleCat

Over a Noetherian ring, every finitely generated module is algebraically Noetherian. The forgetful functor to ModuleCat preserves monomorphisms, reflects isomorphisms, and therefore detects the categorical ascending-chain condition.

instance FGModuleCat.isNoetherianObject {R : Type u} [CommRing R] [IsNoetherianRing R] (M : FGModuleCat R) : CategoryTheory.IsNoetherianObject M

Every finitely generated module over a Noetherian ring is a Noetherian object.