isoColimitUncurryWhiskeringLeft₂

English

If limits exist for K1 and K2 and G preserves the two-variable limit, then the uncurry of whiskering Left₂ yields a limit.

Русский

Если пределы существуют для K1 и K2 и G сохраняет пределы двумерной формы, то uncurry от whiskeringLeft₂ даёт предел.

LaTeX

$$$[HasLimit K1] \\wedge [HasLimit K2] \\wedge [PreservesLimit₂ K1 K2 G] \\Rightarrow HasLimit (uncurry.obj (whiskeringLeft₂ C|>.obj K1|>.obj K2|>.obj G))$$$

Lean4

/-- Extract the isomorphism between
`colim (uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G))` and
`(G.obj (colim K₁)).obj (colim K₂)` from a `PreservesColimit₂` instance, provided the relevant
colimits exist. -/
noncomputable def isoColimitUncurryWhiskeringLeft₂ :
    colimit (uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)) ≅ (G.obj <| colimit K₁).obj (colimit K₂) :=
  isoObjCoconePointsOfIsColimit G (colimit.isColimit _) (colimit.isColimit _) (colimit.isColimit _) |>.symm

Похожие утверждения