English
Let G be a bifunctor that preserves a two-variable limit given by cones c1, c2, c3. The inverse of the canonical isomorphism between the cone points, evaluated at a pair j = (j1, j2), satisfies the equation that expresses how the limiting maps decompose through G. In particular, for every pair j = (j1, j2) we have an equality describing how the inverse interacts with the canonical projections to the limit.
Русский
Пусть бифунктор G сохраняет пределы двух переменных для конусов c1, c2, c3. Обратная сторона канонического изоморфизма между точками конуса удовлетворяет тождеству, выражающему разложение через отображения предела. Пусть j = (j1, j2); тогда для каждого такого j выполняется равенство, описывающее взаимодействие обратной стороны с каноническими проекциями в предел.
LaTeX
$$$(\\text{isoObjConePointsOfIsLimit } G hc_1 hc_2 hc_3).inv \\\\;≫ \\\\ (G.map (c_1.π.app j.1)).app c_2.pt \\\\;≫ \\\\ (G.obj <| K_1.obj j.1).map (c_2.π.app j.2) \\\\;= \\\\ c_3.π.app j$$$
Lean4
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoObjConePointsOfIsLimit` w.r.t. the canonical maps to the limit. -/
@[reassoc (attr := simp)]
theorem isoObjConePointsOfIsColimit_inv_comp_map_π (j : J₁ × J₂) :
(isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).inv ≫
(G.map (c₁.π.app j.1)).app c₂.pt ≫ (G.obj <| K₁.obj j.1).map (c₂.π.app j.2) =
c₃.π.app j :=
by
rw [Iso.inv_comp_eq]
simp
