English
Let J be a small category and F, G : J ⥤ C admit colimits. If w : F ≅ G is an isomorphism of functors, then the canonical morphism coming from transporting along w intertwines the colimit injections: for every j ∈ J, colimit.ι F j followed by (HasColimit.isoOfNatIso w).hom equals w.hom.app j followed by colimit.ι G j.
Русский
Пусть J — малая категория и F, G : J ⥤ C имеют колимиты. Если w : F ≅ G — изоморфизм функторов, то каноническое отображение, полученное перемещением вдоль w, согласуется с инъекциями колимита: для каждого j ∈ J выполняется colimit.ι F j ∘ (HasColimit.isoOfNatIso w).hom = (w.hom).app j ∘ colimit.ι G j.
LaTeX
$$$ \\operatorname{colimit.ι} F j \\circ (\\operatorname{HasColimit.isoOfNatIso} w)^{\\mathrm{hom}} = (w.^{\\mathrm{hom}}_j) \\circ \\operatorname{colimit.ι} G j $$$
Lean4
@[reassoc (attr := simp)]
theorem isoOfNatIso_ι_hom {F G : J ⥤ C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) :
colimit.ι F j ≫ (HasColimit.isoOfNatIso w).hom = w.hom.app j ≫ colimit.ι G j :=
IsColimit.comp_coconePointsIsoOfNatIso_hom _ _ _ _
