Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 18:09 25df2671

View on Github →

feat(category_theory/limits/presheaf): free cocompletion (#4740) Fill in the missing part of #4401, showing that the yoneda extension is unique. Also adds some basic API around #4401.

Estimated changes

Modified docs/references.bib

Modified src/category_theory/elements.lean

added def category_theory.category_of_elements.map

added theorem category_theory.category_of_elements.map_π

Modified src/category_theory/limits/preserves/basic.lean

added def category_theory.limits.is_colimit_of_preserves

added def category_theory.limits.is_limit_of_preserves

Modified src/category_theory/limits/presheaf.lean

added theorem category_theory.cocone_of_representable_naturality

added theorem category_theory.cocone_of_representable_ι_app

added def category_theory.nat_iso_of_nat_iso_on_representables

added def category_theory.unique_extension_along_yoneda