zero_of_map_zero — Mathlib

English

If F preserves zero morphisms and F is faithful, then F reflects zero morphisms: F.map f = 0 implies f = 0.

Русский

Если F сохраняет нулевые морфизмы и является верным, то F отражает нулевые морфизмы: F(m) = 0 ⇒ m = 0.

LaTeX

$$$F\text{ preserves zeros } \land F\text{ faithful } \Rightarrow (F.map f = 0 \Rightarrow f = 0)$$$

Lean4

theorem zero_of_map_zero (F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} (f : X ⟶ Y) (h : F.map f = 0) :
    f = 0 :=
  F.map_injective <| h.trans <| Eq.symm <| F.map_zero _ _

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