English
For a connected shape J and a colimit cocone c over J, equality of morphisms fg and fh through pullback inclusions is detected by their pullbacks; hence, equality can be checked by comparing the pullbacks along the inclusions of the colimit.
Русский
Для связной формы J и колимитного кокона c равенство гомоморфизмов, проходящих через вклады колимита, определяется их вытягиванием; следовательно, равенство можно проверить по вытягиваниям вдоль инклузий колимита.
LaTeX
$$$\forall j,\ (\mathrm{pullback.snd}(c.\iota.app j)\ f) \circ f\circ g = (\mathrm{pullback.snd}(c.\iota.app j)\ f)\circ f\circ h \Rightarrow f\circ g = f\circ h$$$
Lean4
/-- Detecting equality of morphisms factoring through a connected colimit by pulling back along
the inclusions of the colimit. -/
theorem pullback_hom_ext [HasPullbacks C] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] {F : J ⥤ C}
{c : Cocone F} (hc : IsColimit c) {X Y : C} {f : X ⟶ c.pt} {g h : c.pt ⟶ Y}
(hf : ∀ j, pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h) : f ≫ g = f ≫ h :=
by
refine (hc.pullbackOfHasExactColimitsOfShape f).hom_ext (fun j => ?_)
rw [← cancel_epi (pullbackObjIso _ _ _).inv]
simpa using hf j
