English
The hom component satisfies the relation: (limitCompWhiskeringRightIsoLimitComp F G).hom ⋅ whiskerRight (limit.π G j) F = limit.π (G ⋙ (whiskeringRight C D E).obj F) j.
Русский
Гом-компонент удовлетворяет: (limitCompWhiskeringRightIsoLimitComp F G).hom ⋅ whiskerRight (limit.π G j) F = limit.π (G ⋙ (whiskeringRight ...).obj F) j.
LaTeX
$$$(limitCompWhiskeringRightIsoLimitComp\\,F\\,G).hom \\;\\gg\\; \\mathrm{whiskerRight} (\\mathrm{limit}.\\pi\\,G\\,j)\\,F = \\mathrm{limit}.\\pi\\bigl(G \\cdot ((\\mathrm{whiskeringRight}\\;C\\;D\\;E).\\mathrm{obj} F)\\bigr)\\,j$$$
Lean4
noncomputable instance : PreservesLimitsOfShape J (colim : (K ⥤ D ⥤ C) ⥤ _) :=
preservesLimitsOfShape_of_evaluation _ _
(fun d =>
let i :
(colim : (K ⥤ D ⥤ C) ⥤ _) ⋙ (evaluation D C).obj d ≅
colimit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip :=
NatIso.ofComponents
(fun X =>
(colimitObjIsoColimitCompEvaluation _ _) ≪≫
(by exact HasColimit.isoOfNatIso (Iso.refl _)) ≪≫ (colimitObjIsoColimitCompEvaluation _ _).symm)
(fun {F G} η => colimit_obj_ext (fun j => by simp [← NatTrans.comp_app_assoc]))
preservesLimitsOfShape_of_natIso (i ≪≫ colimitFlipIsoCompColim _).symm)
