Commit 2022-01-31 14:14 08fed82d

View on Github →

feat(category_theory/preadditive): the Yoneda embedding for preadditive categories (#11740)

Estimated changes

Modified src/category_theory/endomorphism.lean

added theorem category_theory.End.smul_left

added theorem category_theory.End.smul_right

Modified src/category_theory/preadditive/default.lean

Modified src/category_theory/preadditive/opposite.lean

Created src/category_theory/preadditive/yoneda.lean

added def category_theory.preadditive_coyoneda

added def category_theory.preadditive_coyoneda_obj

added def category_theory.preadditive_yoneda

added def category_theory.preadditive_yoneda_obj

added theorem category_theory.whiskering_preadditive_coyoneda

added theorem category_theory.whiskering_preadditive_yoneda