Theorems · Theorem · category theory
CategoryTheory.Limits.eq_zero_of_image_eq_zero
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
{f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasImage f], CategoryTheory.Limits.image.ι f = 0 → f = 0- Cited by
- 2 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Limits.imagestatement and proof · cited by 124
- CategoryTheory.Limits.HasImagestatement and proof · cited by 107
- CategoryTheory.Limits.image.ιstatement and proof · cited by 104
- CategoryTheory.Limits.factorThruImageproof · cited by 55
- CategoryTheory.Limits.image.facproof · cited by 27
- CategoryTheory.Limits.HasZeroMorphisms.comp_zeroproof · cited by 9
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.nonzero_image_of_nonzeroproof · cited by 0
- CategoryTheory.epi_of_nonzero_to_simpleproof · cited by 0