Theorems · Inductive type · category theory
CategoryTheory.Limits.HasZeroObject
(C : Type u) → [CategoryTheory.Category.{v, u} C] → PropA category "has a zero object" if it has an object which is both initial and terminal.
- Cited by
- 1,298 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 by1,777
Results whose statement or proof uses this declaration.
- CategoryTheory.Pretriangulatedstatement · cited by 669
- CategoryTheory.Triangulated.TStructurestatement · cited by 318
- CategoryTheory.Pretriangulated.distinguishedTrianglesstatement and proof · cited by 316
- CategoryTheory.Limits.HasZeroObject.zero'statement and proof · cited by 115
- HomologicalComplex.extendstatement and proof · cited by 115
- CochainComplex.singleFunctorstatement and proof · cited by 111
- HomologicalComplex.singlestatement and proof · cited by 110
- CategoryTheory.ProjectiveResolutionstatement · cited by 92
- CategoryTheory.InjectiveResolutionstatement · cited by 90
- CategoryTheory.Triangulated.TStructure.truncGEstatement and proof · cited by 85
- CategoryTheory.ProjectiveResolution.complexstatement and proof · cited by 82
- CategoryTheory.Triangulated.TStructure.truncLTstatement and proof · cited by 78
Showing the 200 most cited of 1,777.