Noetherian objects in ModuleCat #
The categorical subobjects of an R-module are order-isomorphic to its submodules. Consequently
an algebraically Noetherian module is a Noetherian object of ModuleCat R.
instance
ModuleCat.isNoetherianObject_of_isNoetherian
{R : Type u}
[Ring R]
(M : ModuleCat R)
[IsNoetherian R ↑M]
:
An algebraically Noetherian module is a Noetherian object of ModuleCat R.