Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 15:51 c6f629bc

View on Github →

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.
  1. 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.

Estimated changes