Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-07 06:14 a7784aad

View on Github →

feat(category_theory/*): Yoneda extension is Kan (#9574)

Proved that (F.elements)ᵒᵖ ≌ costructured_arrow yoneda F.
Verified that the yoneda extension is indeed the left Kan extension along the yoneda embedding.

Estimated changes

Modified src/category_theory/elements.lean

added def category_theory.category_of_elements.costructured_arrow_yoneda_equivalence

added theorem category_theory.category_of_elements.costructured_arrow_yoneda_equivalence_naturality

added def category_theory.category_of_elements.from_costructured_arrow

added theorem category_theory.category_of_elements.from_costructured_arrow_obj_mk

added theorem category_theory.category_of_elements.from_to_costructured_arrow_eq

added def category_theory.category_of_elements.to_costructured_arrow

added theorem category_theory.category_of_elements.to_from_costructured_arrow_eq

Modified src/category_theory/limits/presheaf.lean

added def category_theory.colimit_adj.extend_along_yoneda_iso_Kan

added def category_theory.colimit_adj.extend_along_yoneda_iso_Kan_app

added theorem category_theory.colimit_adj.extend_along_yoneda_map