comp_coconePointUniqueUpToIso_inv

English

The inverse of the cocone isomorphism intertwines the colimit projections with the cocone projections.

Русский

Обратный изоморфизм кокона взаимодействует между проекциями колимита и кокона.

LaTeX

$$$\\bigl(\\text{colimit.isoColimitCocone } t\\bigr)^{\\,-1} \\circ \\text{colimit.ι}_F j = \\text{cocone}.ι.app j$$$

Lean4

@[reassoc (attr := simp)]
theorem comp_coconePointUniqueUpToIso_inv {F : J ⥤ C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) :
    colimit.ι F j ≫ (IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)).inv = c.ι.app j :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

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