Commit 2021-08-28 18:30 e824b88d

View on Github →

refactor(category_theory/limits/final): Symmetric API for final and initial functors (#8808) Dualise the API for cofinal functors to symmetrically support final and initial functors. This PR renames cofinal functors to final functors.

Estimated changes

Renamed src/category_theory/limits/cofinal.lean to src/category_theory/limits/final.lean

deleted def category_theory.cofinal.cocones_equiv

deleted theorem category_theory.cofinal.cofinal_of_colimit_comp_coyoneda_iso_punit

deleted def category_theory.cofinal.colimit_cocone_comp

deleted theorem category_theory.cofinal.colimit_cocone_comp_aux

deleted def category_theory.cofinal.colimit_cocone_of_comp

deleted def category_theory.cofinal.colimit_comp_coyoneda_iso

deleted def category_theory.cofinal.colimit_iso'

deleted def category_theory.cofinal.colimit_iso

deleted theorem category_theory.cofinal.colimit_pre_is_iso_aux

deleted def category_theory.cofinal.cones_equiv

deleted def category_theory.cofinal.extend_cocone

deleted def category_theory.cofinal.extend_cone

deleted def category_theory.cofinal.extend_cone_cocone_to_cone

deleted def category_theory.cofinal.extend_cone_cone_to_cocone

deleted theorem category_theory.cofinal.has_colimit_of_comp

deleted theorem category_theory.cofinal.has_limit_of_comp

deleted def category_theory.cofinal.hom_to_lift

deleted theorem category_theory.cofinal.induction

deleted def category_theory.cofinal.is_colimit_extend_cocone_equiv

deleted def category_theory.cofinal.is_colimit_whisker_equiv

deleted def category_theory.cofinal.is_limit_extend_cone_equiv

deleted def category_theory.cofinal.is_limit_whisker_equiv

deleted def category_theory.cofinal.lift

deleted def category_theory.cofinal.limit_cone_comp

deleted theorem category_theory.cofinal.limit_cone_comp_aux

deleted def category_theory.cofinal.limit_cone_of_comp

deleted def category_theory.cofinal.limit_iso'

deleted def category_theory.cofinal.limit_iso

deleted theorem category_theory.cofinal.limit_pre_is_iso_aux

deleted theorem category_theory.cofinal.zigzag_of_eqv_gen_quot_rel

added def category_theory.functor.final.cocones_equiv

added theorem category_theory.functor.final.cofinal_of_colimit_comp_coyoneda_iso_punit

added def category_theory.functor.final.colimit_cocone_comp

added theorem category_theory.functor.final.colimit_cocone_comp_aux

added def category_theory.functor.final.colimit_cocone_of_comp

added def category_theory.functor.final.colimit_comp_coyoneda_iso

added def category_theory.functor.final.colimit_iso'

added def category_theory.functor.final.colimit_iso

added theorem category_theory.functor.final.colimit_pre_is_iso_aux

added def category_theory.functor.final.extend_cocone

added theorem category_theory.functor.final.has_colimit_of_comp

added def category_theory.functor.final.hom_to_lift

added def category_theory.functor.final.induction

added def category_theory.functor.final.is_colimit_extend_cocone_equiv

added def category_theory.functor.final.is_colimit_whisker_equiv

added def category_theory.functor.final.lift

added theorem category_theory.functor.final.zigzag_of_eqv_gen_quot_rel

added theorem category_theory.functor.final_of_adjunction

added theorem category_theory.functor.final_of_initial_op

added def category_theory.functor.initial.cones_equiv

added def category_theory.functor.initial.extend_cone

added theorem category_theory.functor.initial.has_limit_of_comp

added def category_theory.functor.initial.hom_to_lift

added def category_theory.functor.initial.induction

added def category_theory.functor.initial.is_limit_extend_cone_equiv

added def category_theory.functor.initial.is_limit_whisker_equiv

added def category_theory.functor.initial.lift

added def category_theory.functor.initial.limit_cone_comp

added theorem category_theory.functor.initial.limit_cone_comp_aux

added def category_theory.functor.initial.limit_cone_of_comp

added def category_theory.functor.initial.limit_iso'

added def category_theory.functor.initial.limit_iso

added theorem category_theory.functor.initial.limit_pre_is_iso_aux

added theorem category_theory.functor.initial_of_adjunction

added theorem category_theory.functor.initial_of_final_op

Modified src/topology/sheaves/sheaf_condition/opens_le_cover.lean