Injective finitely generated modules

A monomorphism of finitely generated modules is an injective linear map, so the inclusion of FGModuleCat R into ModuleCat R preserves monomorphisms. Consequently, a finitely generated module that is injective as a module is an injective object of FGModuleCat R.

Main results

• FGModuleCat.forget₂_preservesMonomorphisms: the inclusion of finitely generated modules into all modules preserves monomorphisms.
• FGModuleCat.injective_of_moduleInjective: an injective module that is finitely generated is an injective object of FGModuleCat R.

instance FGModuleCat.forget₂_preservesMonomorphisms {R : Type u} [Ring R] : (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).PreservesMonomorphisms

The inclusion of finitely generated modules into all modules preserves monomorphisms: a monomorphism of finitely generated modules is injective, as one sees by testing it on cyclic submodules.

theorem FGModuleCat.injective_of_moduleInjective {R : Type u} [Ring R] (X : FGModuleCat R) [Module.Injective R ↑X] : CategoryTheory.Injective X

A finitely generated injective module is an injective object of FGModuleCat R.