Commit 2023-08-11 19:14 b48610ff

View on Github →

feat: every presheaf on a large category is a colimit of representables (#6387)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

added def CategoryTheory.isColimitTautologicalCocone

added def CategoryTheory.tautologicalCocone

Modified Mathlib/CategoryTheory/StructuredArrow.lean

modified theorem CategoryTheory.CostructuredArrow.eq_mk

added def CategoryTheory.CostructuredArrow.homMk'

modified theorem CategoryTheory.StructuredArrow.eq_mk

modified def CategoryTheory.StructuredArrow.homMk'

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.yonedaEquiv_comp'

added theorem CategoryTheory.yonedaEquiv_comp

added theorem CategoryTheory.yonedaEquiv_naturality'

added theorem CategoryTheory.yonedaEquiv_symm_map

added theorem CategoryTheory.yonedaEquiv_yoneda_map