ι_comp_isoObjConePointsOfIsColimit_inv

English

There is an isomorphism between the colimit of the uncurry construction and the morphism obtained from the colimits of K1 and K2 under G.

Русский

Существует изоморфизм между колимитом uncurry и отображением колимитов K1 и K2 через G.

LaTeX

$$$\\mathrm{colimit}(uncurry.obj(whiskeringLeft₂ C|>.obj K1|>.obj K2|>.obj G)) \\cong (G.obj (\\mathrm{colimit} K1)).obj (\\mathrm{colimit} K2)$$$

Lean4

/-- Characterize the inverse direction of the isomorphism
`PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit. -/
@[reassoc (attr := simp)]
theorem ι_comp_isoObjConePointsOfIsColimit_inv (j : J₁ × J₂) :
    c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
      (G.map <| c₁.ι.app j.1).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) :=
  by
  dsimp [isoObjCoconePointsOfIsColimit, Functor.mapCocone₂]
  cat_disch

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