mathlib

c6f629bc - feat(category_theory/limits): isos from reindexing limits (#3100)

feat(category_theory/limits): isos from reindexing limits (#3100) Three related constructions which are helpful when identifying "the same limit written different ways". 1. The categories of cones over `F` and `G` are equivalent if `F` and `G` are naturally isomorphic (possibly after changing the indexing category by an equivalence). 2. We can prove two cone points `(s : cone F).X` and `(t.cone F).X` are isomorphic if * both cones are limit cones * their indexing categories are equivalent via some `e : J ≌ K`, * the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`. 3. The chosen limits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic, if there is an equivalence `e : J ≌ K` making the triangle commute up to natural isomorphism. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>