Documentation

Mathlib.Algebra.Category.ModuleCat.Injective

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.