Commit 2023-04-24 05:58 928dcd53

View on Github →

feat: port CategoryTheory.Preadditive.Yoneda.Basic (#3603)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean

added def CategoryTheory.preadditiveCoyoneda

added def CategoryTheory.preadditiveCoyonedaObj

added def CategoryTheory.preadditiveYoneda

added def CategoryTheory.preadditiveYonedaObj

added theorem CategoryTheory.whiskering_preadditiveCoyoneda

added theorem CategoryTheory.whiskering_preadditiveYoneda