Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → f = 0

An extensionality lemma for being the zero arrow.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

2 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian