Commit 2025-02-15 21:17 74e8a3eb

View on Github →

feat(CategoryTheory/Monoidal): yoneda embedding of Mon_ C (#21394)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Created Mathlib/CategoryTheory/Monoidal/Yoneda.lean

added def Mon_ClassOfRepresentableBy

added theorem Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy

added theorem essImage_yonedaMon

added def monoidOfMon_Class

added def yonedaMon

added def yonedaMonFullyFaithful

added def yonedaMonObj

added def yonedaMonObjMon_ClassOfRepresentableBy

added def yonedaMonObjRepresentableBy

added theorem yonedaMon_naturality