English
The inverse of the comparison isomorphism limitCompWhiskeringRightIsoLimitComp interacts with the projection π by the formula: (limitCompWhiskeringRightIsoLimitComp F G)^{-1} ≫ limit.π (G ⋙ whiskeringRight ...).obj F at j equals whiskerRight (limit.π G j) F.
Русский
Обратная часть композиции предельного сопоставления limitCompWhiskeringRightIsoLimitComp с проекцией π удовлетворяет равенству: (limitCompWhiskeringRightIsoLimitComp F G)^{-1} ≫ limit.π (...)_j = whiskerRight (limit.π G j) F.
LaTeX
$$$\\bigl(limitCompWhiskeringRightIsoLimitComp\\,F\\,G\\bigr)^{-1} \\;\\gg\\; \\mathrm{limit}.\\pi\\bigl(G \\cdot (\\mathrm{whiskeringRight}\\;\\_\\;\\_\\_).\\mathrm{obj} F\\bigr)\\, j = \\mathrm{whiskerRight}\\bigl(\\mathrm{limit}.\\pi\\,G\\,j\\bigr)\\,F$$$
Lean4
@[reassoc (attr := simp)]
theorem limitCompWhiskeringRightIsoLimitComp_inv_π {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).inv ≫ limit.π (G ⋙ (whiskeringRight _ _ _).obj F) j =
whiskerRight (limit.π G j) F :=
by simp [limitCompWhiskeringRightIsoLimitComp]
