English
If e is an equivalence J ≌ K and w : e.functor ⋙ G ≅ F, then the legs of F and G relate through the unit/counit data: colimit.ι F j after the equivalence is equal to F.map (e.unit.app j) followed by w.inv.app (e.inverse.obj j) and then colimit.ι G (e.inverse.obj j).
Русский
Если e — эквивалентность J ≌ K и w : e.functor ⋙ G ≅ F, то инъекции колимита связаны через данные единицы/коуниции: colimit.ι F j = F.map (e.unit.app j) затем w.inv.app (e.inverse.obj j) затем colimit.ι G (e.inverse.obj j).
LaTeX
$$$ \\ colimit.ι F j \\; \\circ \\big( \\operatorname{HasColimit.isoOfEquivalence} e w \\big)^{\\mathrm{hom}} = F.map (e.unit.app j) \\; \\circ \\; w.inv.app (e.inverse.obj j) \\; \\circ \\colimit.ι G (e.inverse.obj j) $$
Lean4
@[simp]
theorem isoOfEquivalence_hom_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F)
(j : J) :
colimit.ι F j ≫ (HasColimit.isoOfEquivalence e w).hom = F.map (e.unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _ := by
simp [HasColimit.isoOfEquivalence]
