Category of $R$-modules has enough injectives

we lift enough injectives of abelian groups to arbitrary $R$-modules by adjoint functors restrictScalars ⊣ coextendScalars

Implementation notes

This file is not part of Algebra/Module/Injective.lean to prevent import loop: enough-injectives of abelian groups needs Algebra/Module/Injective.lean and this file needs enough-injectives of abelian groups.

instance instEnoughInjectivesModuleCatIntInstRingIntModuleCategory : CategoryTheory.EnoughInjectives (ModuleCat ℤ)

Equations

• instEnoughInjectivesModuleCatIntInstRingIntModuleCategory = (_ : CategoryTheory.EnoughInjectives (ModuleCat ℤ))

theorem ModuleCat.enoughInjectives (R : Type u) [Ring R] : CategoryTheory.EnoughInjectives (ModuleCat R)

instance instEnoughInjectivesModuleCatModuleCategory (R : Type u) [Ring R] [UnivLE.{u, v} ] : CategoryTheory.EnoughInjectives (ModuleCat R)

Equations

• (_ : CategoryTheory.EnoughInjectives (ModuleCat R)) = (_ : CategoryTheory.EnoughInjectives (ModuleCat R))