Mathlib Changelog
Changelog
About
Github
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