Injective objects in the category of $R$-modules

theorem Module.injective_object_of_injective_module (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [inj : Module.Injective R M] : CategoryTheory.Injective (ModuleCat.of R M)

theorem Module.injective_module_of_injective_object (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [inj : CategoryTheory.Injective (ModuleCat.of R M)] : Module.Injective R M

theorem Module.injective_iff_injective_object (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Module.Injective R M ↔ CategoryTheory.Injective (ModuleCat.of R M)

instance ModuleCat.ulift_injective_of_injective (R : Type u) (M : Type v) [Ring R] [Small.{v, u} R] [AddCommGroup M] [Module R M] [CategoryTheory.Injective (ModuleCat.of R M)] : CategoryTheory.Injective (ModuleCat.of R (ULift.{v', v} M))

Equations

• ⋯ = ⋯