Lean4
/-- We can prove two cone points `(s : Cone F).pt` and `(t : Cone G).pt` 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`.
This is the most general form of uniqueness of cone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
-/
@[simps]
def conePointsIsoOfEquivalence {F : J ⥤ C} {s : Cone F} {G : K ⥤ C} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
(e : J ≌ K) (w : e.functor ⋙ G ≅ F) : s.pt ≅ t.pt :=
let w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ invFunIdAssoc e G
{ hom := Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s)
inv := P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t)
hom_inv_id := by
apply hom_ext P; intro j
dsimp [w']
simp only [Limits.Cone.whisker_π, Limits.Cones.postcompose_obj_π, fac, whiskerLeft_app, assoc, id_comp,
invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
rw [counit_app_functor, ← Functor.comp_map]
have l : NatTrans.app w.hom j = NatTrans.app w.hom ((𝟭 J).obj j) := by dsimp
rw [l, w.hom.naturality]
simp
inv_hom_id := by
apply hom_ext Q
cat_disch }
