Commit 2023-04-22 23:05 19b2ce61

View on Github →

feat: port CategoryTheory.Limits.Presheaf (#3208)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Elements.lean

Created Mathlib/CategoryTheory/Limits/Presheaf.lean

added def CategoryTheory.ColimitAdj.Elements.initial

added theorem CategoryTheory.ColimitAdj.extendAlongYoneda_map

added theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj.hom_ext

added theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj

added def CategoryTheory.ColimitAdj.isInitial

added def CategoryTheory.ColimitAdj.restrictYonedaHomEquiv

added theorem CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural

added def CategoryTheory.ColimitAdj.restrictedYoneda

added def CategoryTheory.ColimitAdj.restrictedYonedaYoneda

added theorem CategoryTheory.coconeOfRepresentable_naturality

added theorem CategoryTheory.coconeOfRepresentable_pt

added theorem CategoryTheory.coconeOfRepresentable_ι_app

added def CategoryTheory.functorToRepresentables