Commit 2020-10-23 22:12 aa590397

View on Github →

feat(category_theory): presheaf is colimit of representables (#4401) Show every presheaf (on a small category) is a colimit of representables, and some related results. Suggestions for better names more than welcome.

Estimated changes

Modified docs/references.bib

Modified src/category_theory/adjunction/default.lean

Modified src/category_theory/adjunction/opposites.lean

added def adjunction.nat_iso_of_left_adjoint_nat_iso

added def adjunction.nat_iso_of_right_adjoint_nat_iso

Created src/category_theory/limits/presheaf.lean

added def category_theory.cocone_of_representable

added theorem category_theory.cocone_of_representable_X

added def category_theory.colimit_adj.elements.initial

added def category_theory.colimit_adj.extend_along_yoneda

added theorem category_theory.colimit_adj.extend_along_yoneda_obj

added def category_theory.colimit_adj.is_extension_along_yoneda

added def category_theory.colimit_adj.is_initial

added def category_theory.colimit_adj.restrict_yoneda_hom_equiv

added theorem category_theory.colimit_adj.restrict_yoneda_hom_equiv_natural

added def category_theory.colimit_adj.restricted_yoneda

added def category_theory.colimit_adj.restricted_yoneda_yoneda

added def category_theory.colimit_adj.yoneda_adjunction

added def category_theory.colimit_of_representable

added def category_theory.extend_along_yoneda_yoneda

added def category_theory.functor_to_representables

Modified src/category_theory/limits/shapes/terminal.lean

added def category_theory.limits.initial_op_of_terminal

added def category_theory.limits.initial_unop_of_terminal

added def category_theory.limits.terminal_op_of_initial

added def category_theory.limits.terminal_unop_of_initial