English
If g,h:Y→c.pt and f:c.pt→X are morphisms and for every j in J one has a specified compatibility relation through pushout injections, then g∘f = h∘f; i.e., equality of g,h is detected after pushout along the limit projections.
Русский
Пусть g,h: Y→c.pt и f: c.pt→X — морфизмы; при условии, что для каждого j в J существуют совместимые отношения через инъекции пушаута, то g∘f = h∘f; то есть равенство определяется после пушаута вдоль проекций предела.
LaTeX
$$$\forall j,\; g \circ f \circ \mathrm{inr}(c.\pi.app j) = h \circ f \circ \mathrm{inr}(c.\pi.app j) \Rightarrow g \circ f = h \circ f$$$
Lean4
/-- Detecting equality of morphisms factoring through a connected limit by pushing out along
the projections of the limit. -/
theorem pushout_hom_ext [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] {F : J ⥤ C} {c : Cone F}
(hc : IsLimit c) {X Y : C} {g h : Y ⟶ c.pt} {f : c.pt ⟶ X}
(hf : ∀ j, g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f) : g ≫ f = h ≫ f :=
by
refine (hc.pushoutOfHasExactLimitsOfShape f).hom_ext (fun j => ?_)
rw [← cancel_mono (pushoutObjIso _ _ _).hom]
simpa using hf j
