ι_isoColimit_hom — Mathlib

English

A dual relation asserts how the cocone morphism ι interacts with E.hom and h.isoColimit.hom to produce the colimit's universal map.

Русский

Существует отношения между кокон-морфизмом ι и гомоморфизмами E.hom и h.isoColimit.hom, приводящее к универсальному отображению колимита.

LaTeX

$$$\\text{colimit.ι} \\ g \\; =\\; E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_isoColimit_hom (g : CostructuredArrow L Y) :
    E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom = colimit.ι (CostructuredArrow.proj L Y ⋙ F) g := by
  simpa using h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g

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