Theorems · Theorem · category theory
CategoryTheory.Limits.IsZero.iff_id_eq_zero
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.Limits.IsZero X ↔ CategoryTheory.CategoryStruct.id X = 0- Cited by
- 40 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses propext, Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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.CategoryStruct.idstatement and proof · cited by 6,235
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Category.comp_idproof · cited by 2,119
- CategoryTheory.Category.id_compproof · cited by 1,998
- CategoryTheory.Limits.comp_zeroproof · cited by 365
- CategoryTheory.Limits.zero_compproof · cited by 339
- CategoryTheory.Limits.IsZerostatement and proof · cited by 306
- CategoryTheory.Limits.IsZero.eq_of_srcproof · cited by 57
Cited by40
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.Exact.isZero_X₂proof · cited by 5
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomologyproof · cited by 4
- CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epiproof · cited by 3
- CategoryTheory.Limits.IsZero.of_mono_zeroproof · cited by 3
- CategoryTheory.Pretriangulated.Triangle.isZero₂_iffproof · cited by 3
- CategoryTheory.ShortComplex.exact_map_iff_of_faithfulproof · cited by 3
- CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_monoproof · cited by 3
- HomologicalComplex.isStrictlySupported_mapHomologicalComplex_obj_iffproof · cited by 2
- CategoryTheory.Limits.IsZero.of_epi_zeroproof · cited by 2
- CategoryTheory.Limits.IsInitial.isZeroproof · cited by 2
- HomologicalComplex.exact_of_degreewise_exactproof · cited by 2
- CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomologyproof · cited by 2