Commit 2020-09-28 04:20 17618222

View on Github →

chore(category_theory/limits): some limit lemmas (#4238) A couple of lemmas characterising definitions which are already there (the first part of #4163)

Estimated changes

Modified src/category_theory/limits/limits.lean

added theorem category_theory.limits.has_colimit.iso_of_nat_iso_hom_desc

added theorem category_theory.limits.has_limit.lift_iso_of_nat_iso_hom

added theorem category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_hom_desc

added theorem category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_inv_desc

added theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc

added theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom

added theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv

added def category_theory.limits.is_colimit.equiv_iso_colimit

added theorem category_theory.limits.is_colimit.equiv_iso_colimit_apply

added theorem category_theory.limits.is_colimit.equiv_iso_colimit_symm_apply

modified def category_theory.limits.is_colimit.map

added theorem category_theory.limits.is_colimit.of_iso_colimit_desc

added theorem category_theory.limits.is_colimit.ι_map

added theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp

added theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp

added def category_theory.limits.is_limit.equiv_iso_limit

added theorem category_theory.limits.is_limit.equiv_iso_limit_apply

added theorem category_theory.limits.is_limit.equiv_iso_limit_symm_apply

added theorem category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_hom

added theorem category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_inv

added theorem category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom

modified def category_theory.limits.is_limit.map

added theorem category_theory.limits.is_limit.map_π

added theorem category_theory.limits.is_limit.of_iso_limit_lift

deleted theorem category_theory.limits.is_limit_map_π

deleted theorem category_theory.limits.ι_is_colimit_map

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

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