Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C} (Q : C)
  (f : CategoryTheory.Over P), f ≈ CategoryTheory.Over.mk 0 ↔ f.hom = 0

The arrows pseudo-equal to a zero morphism are precisely the zero morphisms.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian