Commit 2023-11-29 19:15 7ba68976

View on Github →

feat: category of $R$-modules has enough injectives (#7392)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Created Mathlib/Algebra/Category/ModuleCat/Injective.lean

added theorem ModuleCat.enoughInjectives

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/Preadditive/Injective.lean

added def CategoryTheory.Adjunction.injectivePresentationOfMap

added theorem CategoryTheory.EnoughInjectives.of_adjunction

added theorem CategoryTheory.EnoughInjectives.of_equivalence

modified theorem CategoryTheory.Equivalence.enoughInjectives_iff