Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 05:13 9f3e7fba

View on Github →

feat(category_theory/limits): further API for commuting limits (#13215) Needed for LTE.

Estimated changes

Modified src/category_theory/functor/currying.lean

added def category_theory.uncurry_obj_flip

Modified src/category_theory/limits/fubini.lean

added def category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim

added theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_hom_π_π

added theorem category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_inv_π_π

Modified src/category_theory/limits/has_limits.lean

added theorem category_theory.limits.has_colimit.iso_of_nat_iso_inv_desc

added theorem category_theory.limits.has_colimit.iso_of_nat_iso_ι_inv

added theorem category_theory.limits.has_limit.iso_of_nat_iso_inv_π

added theorem category_theory.limits.has_limit.lift_iso_of_nat_iso_inv

Modified src/category_theory/limits/is_limit.lean

added theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv_desc

added theorem category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_inv