English
The forward direction of the limit iso, when composed with the canonical projection maps, yields the corresponding projection on the uncurry whiskered diagram. This expresses the commutativity of the canonical map with the projections through G.
Русский
Прямая сторона предельного изоморфизма, образованная композицией с каноническими проекциями, даёт соответствующую проекцию для uncurry whisker-диаграммы; это выражает совместимость отображений через G.
LaTeX
$$$(PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K_1 K_2 G).hom \\\\;≫ \\\\ (G.map (limit.π K_1 j.1)).app (limit K_2) \\\\;≫ \\\\ (G.obj K_1.obj j.1).map (limit.π K_2 j.2) \\\\;= \\\\ limit.π (uncurry.obj (whiskeringLeft₂ C |>.obj K_1 |>.obj K_2 |>.obj G)) j$$$
Lean4
/-- Characterize the forward direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit. -/
@[reassoc (attr := simp)]
theorem isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π (j : J₁ × J₂) :
(PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom ≫
(G.map (limit.π K₁ j.1)).app (limit K₂) ≫ (G.obj <| K₁.obj j.1).map (limit.π K₂ j.2) =
limit.π (uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)) j :=
isoObjConePointsOfIsColimit_inv_comp_map_π G (limit.isLimit _) (limit.isLimit _) (limit.isLimit _) _
