English
For each pair j = (j1, j2), the inverse part of the canonical limit isomorphism composed with the appropriate projections equals the whiskered projection under G. This describes how the inverse of the limit isomorphism interacts with the canonical projections to the limits of K1 and K2.
Русский
Для пары j=(j1, j2) обратная часть канонического предельного изоморфизма, умноженная на соответствующие проекции, равна проекции, получаемой под whiskering и G. Это описывает взаимодействие обратной стороны с каноническими проекциями к пределам K1 и K2.
LaTeX
$$$(PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K_1 K_2 G).inv \\\\;≫ \\\\ limit.π (uncurry.obj (whiskeringLeft₂ C |>.obj K_1 |>.obj K_2 |>.obj G)) j \\\\;= \\\\ (G.map limit.π K_1 j.1).app (limit K_2) \\\\;≫ \\\\ (G.obj K_1.obj j.1).map (limit.π K_2 j.2)$$$
Lean4
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit. -/
@[reassoc (attr := simp)]
theorem isoLimitUncurryWhiskeringLeft₂_inv_comp_π (j : J₁ × J₂) :
(PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv ≫
limit.π (uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)) j =
(G.map <| limit.π K₁ j.1).app (limit K₂) ≫ (G.obj <| K₁.obj j.1).map (limit.π K₂ j.2) :=
isoObjConePointsOfIsLimit_hom_comp_π G (limit.isLimit _) (limit.isLimit _) (limit.isLimit _) _
