English
The forward component of the limit comparison iso intertwines with whiskering on the right: (limitCompWhiskeringRightIsoLimitComp F G).hom ⋅ whiskerRight (limit.π G j) F = limit.π (G ⋙ whiskeringRight ...).obj F at j.
Русский
Передняя часть изоморфизма сравнения пределов совместно с правым взвешиванием: (limitCompWhiskeringRightIsoLimitComp F G).hom ⋅ whiskerRight (limit.π G j) F = limit.π (G ⋙ whiskeringRight ... ) j.
LaTeX
$$$(limitCompWhiskeringRightIsoLimitComp\\,F\\,G).hom \\;\\gg\\; \\mathrm{whiskerRight} (\\mathrm{limit}.\\pi G j) F = \\mathrm{limit}.\\pi\\bigl(G \\cdot (\\mathrm{whiskeringRight}\\;\\_\\;\\_\\_).\\mathrm{obj}F\\bigr)\\;j$$$
Lean4
@[reassoc (attr := simp)]
theorem limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π {C : Type*} [Category C] {D : Type*} [Category D]
{E : Type*} [Category E] {J : Type*} [Category J] [HasLimitsOfShape J D] (F : D ⥤ E) [PreservesLimitsOfShape J F]
(G : J ⥤ C ⥤ D) (j : J) :
(limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
limit.π (G ⋙ (whiskeringRight _ _ _).obj F) j :=
by simp [← Iso.eq_inv_comp]
