Commit 2022-03-05 03:06 b0d94624

View on Github →

feat(category_theory/preadditive/injective) : more basic properties and morphisms about injective objects (#12450) This pr dualises the rest of projective.lean

Estimated changes

Modified src/category_theory/preadditive/injective.lean

added def category_theory.injective.d

added theorem category_theory.injective.exact.comp_desc

added def category_theory.injective.exact.desc

added def category_theory.injective.syzygies

added def category_theory.injective.under

added def category_theory.injective.ι