zero_morphism_ext — Mathlib

English

If a morphism maps every pseudoelement to 0, then the morphism is the zero morphism as a function.

Русский

Если морфизм отправляет каждый псевдоэлемент в 0, то как функция он является нулевым морфизмом.

LaTeX

$$$\\forall a,\\; f(a)=0 \\Rightarrow f=0$$$

Lean4

/-- An extensionality lemma for being the zero arrow. -/
theorem zero_morphism_ext {P Q : C} (f : P ⟶ Q) : (∀ a, f a = 0) → f = 0 := fun h =>
  by
  rw [← Category.id_comp f]
  exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

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