English
Under equivalence, the dual formula for the inverse leg: colimit.ι G k composed with the inverse of the equivalence iso equals G.map counitInv at k composed with w.hom at (e.inverse.obj k) and finally with colimit.ι F at that object.
Русский
При эквивалентности двойная формула для обратной стороны: colimit.ι G k после обратного изоморфизма эквивалентности равна G.map counitInv на k, затем w.hom на e.inverse.obj k, затем colimit.ι F на e.inverse.obj k.
LaTeX
$$$ \\operatorname{colimit.ι} G k \\; \\circ (\\operatorname{HasColimit.isoOfEquivalence} e w)^{\\mathrm{inv}} = \\operatorname{G.map} (e.counitInv.app k) \\circ w.hom.app (e.inverse.obj k) \\circ \\operatorname{colimit.ι} F (e.inverse.obj k) $$$
Lean4
@[simp]
theorem isoOfEquivalence_inv_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F)
(k : K) :
colimit.ι G k ≫ (HasColimit.isoOfEquivalence e w).inv =
G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k) :=
by simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]
