colimit_obj_ext — Mathlib

English

In a colimit diagram, two arrows from the colimit object coincide if and only if they become equal after composing with all injections.

Русский

В диаграмме колимита два отображения из объекта колимита совпадают тогда и только тогда, когда они совпадают после композиции с всеми инъекциями.

LaTeX

$$$\forall j,\ (colimit.ι H j).app k \\circ f = (colimit.ι H j).app k \circ g \Rightarrow f = g$$$

Lean4

@[ext]
theorem colimit_obj_ext {H : J ⥤ K ⥤ C} [HasColimitsOfShape J C] {k : K} {W : C} {f g : (colimit H).obj k ⟶ W}
    (w : ∀ j, (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g) : f = g :=
  by
  apply (cancel_epi (colimitObjIsoColimitCompEvaluation H k).inv).1
  ext j
  simpa using w j

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