Theorems · Inductive type · category theory
CategoryTheory.Limits.IsZero
{C : Type u} → [CategoryTheory.Category.{v, u} C] → C → PropAn object X in a category is a zero object if for every object Y
there is a unique morphism to : X → Y and a unique morphism from : Y → X.
This is a characteristic predicate for HasZeroObject.
- Cited by
- 306 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by351
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.IsZero.eq_of_srcstatement and proof · cited by 57
- CategoryTheory.Limits.IsZero.eq_of_tgtstatement and proof · cited by 46
- CategoryTheory.Limits.IsZero.iff_id_eq_zerostatement and proof · cited by 40
- CategoryTheory.Limits.IsZero.of_isostatement and proof · cited by 35
- CategoryTheory.Limits.isZero_zerostatement · cited by 34
- CategoryTheory.ShortComplex.exact_of_isoproof · cited by 18
- CategoryTheory.Functor.map_isZerostatement and proof · cited by 16
- CochainComplex.isZero_of_isStrictlyGEstatement · cited by 13
- HomologicalComplex.exactAt_iff_isZero_homologystatement and proof · cited by 13
- HomologicalComplex.isZero_extend_Xstatement · cited by 12
- CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_monoproof · cited by 11
- CategoryTheory.Limits.IsZero.isostatement and proof · cited by 11
Showing the 200 most cited of 351.