English
The colimit injection after whiskering interacts with the colimit comparison isomorphism by a simple equality: colimit.ι (G ⋙ whiskeringRight ...).j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom = whiskerRight (colimit.ι G j) F.
Русский
Инъекция колимита после взвешивания справа взаимодействует с изоморфизмом сравнения колимита по простому равенству: colimit.ι(G ⋙ whiskeringRight ...).j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom = whiskerRight (colimit.ι G j) F.
LaTeX
$$$\\operatorname{colimit.\\,ι}\\bigl(G \\!\\cdot\\! (\\mathrm{whiskeringRight}\\;\\_\\;\\_\\_).\\mathrm{obj} F\\bigr)\\; j \\; \\circ \\bigl(\\operatorname{colimitCompWhiskeringRightIsoColimitComp}\\; F\\; G\\bigr).hom = \\mathrm{whiskerRight}\\bigl(\\operatorname{colimit.\\,ι}_G j\\bigr) F$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_colimitCompWhiskeringRightIsoColimitComp_hom {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*}
[Category E] {J : Type*} [Category J] [HasColimitsOfShape J D] (F : D ⥤ E) [PreservesColimitsOfShape J F]
(G : J ⥤ C ⥤ D) (j : J) :
colimit.ι (G ⋙ (whiskeringRight _ _ _).obj F) j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom =
whiskerRight (colimit.ι G j) F :=
by simp [colimitCompWhiskeringRightIsoColimitComp]
