pushout_zero_ext — Mathlib

English

If g∘f∘pushout.inr(c.π.app j) f = 0 for all j, then g∘f = 0; i.e., vanishing is detected after pushout along the projections of the limit.

Русский

Если для всех j выполняется g∘f∘pushout.inr(c.π.app j) f = 0, то g∘f = 0; нуль определяется после пушаута по проекциям предела.

LaTeX

$$$\forall j,\; g\circ f\circ \mathrm{inr}(c.\pi.app j)\, f = 0 \Rightarrow g\circ f = 0$$$

Lean4

/-- Detecting vanishing of a morphism factoring though a connected limit by pushing out along the
projections of the limit. -/
theorem pushout_zero_ext [HasZeroMorphisms C] [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C]
    {F : J ⥤ C} {c : Cone F} (hc : IsLimit c) {X Y : C} {g : Y ⟶ c.pt} {f : c.pt ⟶ X}
    (hf : ∀ j, g ≫ f ≫ pushout.inr (c.π.app j) f = 0) : g ≫ f = 0 :=
  by
  suffices g ≫ f = 0 ≫ f by simpa
  exact hc.pushout_hom_ext (by simpa using hf)

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