Theorems · Definition · category theory
CategoryTheory.GradedObject
Type w → Type u → Type (max w u)
A type synonym for β → C, used for β-graded objects in a category C.
- Defined in
- Mathlib.CategoryTheory.GradedObject
- Cited by
- 239 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by339
Results whose statement or proof uses this declaration.
- CategoryTheory.GradedObject.HasMapstatement and proof · cited by 99
- CategoryTheory.GradedObject.mapBifunctorstatement and proof · cited by 87
- CategoryTheory.GradedObject.mapObjstatement and proof · cited by 83
- HomologicalComplex₂.toGradedObjectstatement · cited by 71
- CategoryTheory.GradedObject.mapBifunctorMapObjstatement and proof · cited by 64
- CategoryTheory.GradedObject.Monoidal.tensorObjstatement and proof · cited by 54
- CategoryTheory.GradedObject.HasTensorstatement and proof · cited by 49
- CategoryTheory.GradedObject.single₀statement · cited by 30
- CategoryTheory.GradedObject.ιMapObjstatement and proof · cited by 30
- CategoryTheory.GradedObject.mapTrifunctorstatement and proof · cited by 28
- CategoryTheory.GradedObject.Monoidal.ιTensorObjstatement and proof · cited by 26
- CategoryTheory.GradedObjectWithShiftproof · cited by 24
Showing the 200 most cited of 339.