English
If a morphism f is factored through a connected colimit and all corresponding pullbacks with a morphism g are zero, then the composite f with g is zero; i.e., vanishing is detected via pullbacks.
Русский
Если отображение f факторизуется через связанный колимит и все соответствующие вытягивания с г равны нулю, то композиция f с g равна нулю; то есть нуль определяется через вытягивания.
LaTeX
$$$\forall j,\ \mathrm{pullback.snd}(c.\iota.app j)\ f \circ f \circ g = 0\Rightarrow f\circ g = 0$$$
Lean4
/-- Detecting vanishing of a morphism factoring through a connected colimit by pulling back along
the inclusions of the colimit. -/
theorem pullback_zero_ext [HasZeroMorphisms C] [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 : c.pt ⟶ Y}
(hf : ∀ j, pullback.snd (c.ι.app j) f ≫ f ≫ g = 0) : f ≫ g = 0 :=
by
suffices f ≫ g = f ≫ 0 by simpa
exact hc.pullback_hom_ext (by simpa using hf)
