comp_coconePointUniqueUpToIso_hom

English

The homomorphism from a colimit composed with the isomorphism cocone is equal to the cocone's component.

Русский

Гомоморфизм колимита при композиции с изоморфизмом кокона равен компоненте кокона.

LaTeX

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

Lean4

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

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