isoObjCoconePointsOfIsColimit — Mathlib

English

Characterize the inverse direction of the isomorphism between the colimit and the mapped cocone's point, showing compatibility with canonical maps.

Русский

Характеризуется обратное направление изоморфизма между колимитом и точкой кокона, отображаемого через G, совместимое с каноническими картами.

LaTeX

$$$(G.obj c1.pt).obj c2.pt \\cong c3.pt \\Rightarrow\\text{(compatibility with injections)}$$$

Lean4

/-- Given a `PreservesColimit₂` instance, extract the isomorphism between
a colimit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` and
`(G.obj c₁).obj c₂` where c₁ (resp. c₂) is a colimit of `K₁` (resp `K₂`). -/
noncomputable def isoObjCoconePointsOfIsColimit {c₁ : Cocone K₁} (hc₁ : IsColimit c₁) {c₂ : Cocone K₂}
    (hc₂ : IsColimit c₂) {c₃ : Cocone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)}
    (hc₃ : IsColimit c₃) : (G.obj c₁.pt).obj c₂.pt ≅ c₃.pt :=
  IsColimit.coconePointUniqueUpToIso (isColimitOfPreserves₂ G hc₁ hc₂) hc₃

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