Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-04 05:39 e902cae5

View on Github →

feat(category_theory/limits/cofinal): better API for cofinal functors (#4276) This PR

Proves that F : C ⥤ D being cofinal is equivalent to colimit (F ⋙ G) ≅ colimit G for all G : D ⥤ E. (Previously we just had the implication.)
Proves that if F is cofinal then limit (F.op ⋙ H) ≅ limit H for all H: Dᵒᵖ ⥤ E.

Estimated changes

Modified src/category_theory/is_connected.lean

added theorem category_theory.zag_symmetric

added theorem category_theory.zigzag_symmetric

Modified src/category_theory/limits/cofinal.lean

added theorem category_theory.cofinal.cofinal_of_colimit_comp_coyoneda_iso_punit

added def category_theory.cofinal.colimit_comp_coyoneda_iso

added def category_theory.cofinal.cones_equiv

added def category_theory.cofinal.extend_cone

added def category_theory.cofinal.extend_cone_cocone_to_cone

added def category_theory.cofinal.extend_cone_cone_to_cocone

added theorem category_theory.cofinal.has_limit_of_comp

added def category_theory.cofinal.is_limit_extend_cone_equiv

added def category_theory.cofinal.is_limit_whisker_equiv

added def category_theory.cofinal.limit_cone_comp

added theorem category_theory.cofinal.limit_cone_comp_aux

added def category_theory.cofinal.limit_cone_of_comp

added def category_theory.cofinal.limit_iso'

added def category_theory.cofinal.limit_iso

added theorem category_theory.cofinal.limit_pre_is_iso_aux

added theorem category_theory.cofinal.zigzag_of_eqv_gen_quot_rel

Modified src/category_theory/limits/limits.lean

added theorem category_theory.limits.is_limit.of_cone_equiv_apply_desc

added theorem category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.colimit_eq

added theorem category_theory.limits.types.colimit_equiv_quot_apply

added def category_theory.limits.types.quot.rel

Created src/category_theory/limits/yoneda.lean

added def category_theory.coyoneda.colimit_cocone

added def category_theory.coyoneda.colimit_cocone_is_colimit

added def category_theory.coyoneda.colimit_coyoneda_iso

Modified src/category_theory/opposites.lean