Lean4
/-- We can prove two cocone points `(s : Cocone F).pt` and `(t : Cocone G).pt` are isomorphic if
* both cocones are colimit cocones
* 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 cocone points,
allowing relabelling of both the indexing category (up to equivalence)
and the functor (up to natural isomorphism).
-/
@[simps]
def coconePointsIsoOfEquivalence {F : J ⥤ C} {s : Cocone F} {G : K ⥤ C} {t : Cocone G} (P : IsColimit s)
(Q : IsColimit 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 := P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t)
inv := Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s)
hom_inv_id := by
apply hom_ext P; intro j
dsimp [w']
simp only [Limits.Cocone.whisker_ι, fac, invFunIdAssoc_inv_app, whiskerLeft_app, assoc, comp_id,
Limits.Cocones.precompose_obj_ι, fac_assoc, NatTrans.comp_app]
rw [counitInv_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
simp
inv_hom_id := by
apply hom_ext Q
cat_disch }
