π_of_isColimit — Mathlib

English

Dual to ι_of_isLimit: the π morphisms are given by ht.desc for a colimit cocone ht.

Русский

Дуал к ι_of_isLimit: морфизмы π задаются через ht.desc для колимитного коконa ht.

LaTeX

$$$$ t.\\π_j = ht.desc(\\mathrm{Cofan.mk}(f(j),\\ldots)). $$$$

Lean4

theorem π_of_isColimit {f : J → C} {t : Bicone f} (ht : IsColimit t.toCocone) (j : J) :
    t.π j = ht.desc (Cofan.mk _ fun j' => if h : j' = j then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

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