English
Let t be a cocone on a diagram F: J ⥤ C which is a colimit. Then for any object W and any two morphisms f, f' : t.pt ⟶ W, if for every j in J we have t.ι.app j ≫ f = t.ι.app j ≫ f', then f = f'. This expresses the uniqueness part of the universal property of a colimit: maps out of a colimit are determined by their compositions with the cocone legs.
Русский
Пусть t является коконом над диаграммой F: J ⥤ C и является колимитом. Тогда для любого объекта W и для любых двух морфизмов f, f' : t.pt ⟶ W, если для каждого j ∈ J выполняется t.ι.app j ≫ f = t.ι.app j ≫ f', то f = f'. Это выражает единственность отображений из колимита, следуя из всеобщности кокона.
LaTeX
$$$\text{IsColimit}(t) \implies \forall W, \forall f,g : t.\mathrm{pt} \to W,\ (\forall j,\ t.\iota.app j \circ f = t.\iota.app j \circ g) \Rightarrow f = g.$$$
Lean4
/-- Two morphisms out of a colimit are equal if their compositions with
each cocone morphism are equal. -/
theorem hom_ext (h : IsColimit t) {W : C} {f f' : t.pt ⟶ W} (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f' := by
rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w
