English
Let t be a colimit cocone for a functor F : J → C. Then there is a natural bijection between morphisms t.pt → W and cocones on F with apex W; i.e. (t.pt → W) ≃ (F ⟶ (const J).obj W).
Русский
Пусть t — колимитный кокон для функтору F : J → C. Тогда существует естественная биекция между морфизмами t.pt → W и коконами над F с вершиной W; т. е. (t.pt → W) ≃ (F ⟶ (const J).obj W).
LaTeX
$$$(t.\mathrm{pt} \to W) \cong (F \to (\mathrm{const}\ J).\mathrm{obj} W)$$$
Lean4
/-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
a cocone on `F` with cone point `W`. -/
def homEquiv (h : IsColimit t) {W : C} : (t.pt ⟶ W) ≃ (F ⟶ (const J).obj W)
where
toFun f := (t.extend f).ι
invFun
ι :=
h.desc
{ pt := W
ι }
left_inv f := h.hom_ext (by simp)
right_inv ι := by cat_disch
