English
Let e: J ≌ K be an equivalence and w: e.functor ⋙ G ≅ F with G having a limit. Then for k in K: (HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k = limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k).
Русский
Пусть e: J ≌ K — эквивалентность и w: e.functor ⋙ G ≅ F, F имеет предел. Тогда для каждого k: (HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k = limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k).
LaTeX
$$$(\\mathrm{HasLimit.isoOfEquivalence}\,e\,w).hom \\gg \\operatorname{limit.}\\pi G k = \\operatorname{limit.}\\pi F (e^{-1}.obj k) \\gg w^{-1}.app (e^{-1}.obj k) \\gg G.map (e.counit.app k)$$$
Lean4
@[simp]
theorem isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G] (e : J ≌ K) (w : e.functor ⋙ G ≅ F)
(k : K) :
(HasLimit.isoOfEquivalence e w).hom ≫ limit.π G k =
limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) :=
by
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
simp
