Theorems · Definition · category theory
CategoryTheory.GradedObjectWithShift
{β : Type w} → [AddCommGroup β] → β → Type u → Type (max w u)A type synonym for β → C, used for β-graded objects in a category C
with a shift functor given by translation by s.
- Defined in
- Mathlib.CategoryTheory.GradedObject
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- CategoryTheory.GradedObjectproof · cited by 239
Cited by30
Results whose statement or proof uses this declaration.
- HomologicalComplex.homologicalComplexToDGOstatement · cited by 10
- HomologicalComplex.dgoToHomologicalComplexstatement and proof · cited by 10
- CategoryTheory.DifferentialObject.objEqToHomstatement and proof · cited by 8
- HomologicalComplex.dgoEquivHomologicalComplexstatement · cited by 4
- HomologicalComplex.dgoEquivHomologicalComplexCounitIsostatement · cited by 3
- HomologicalComplex.dgoEquivHomologicalComplexUnitIsostatement and proof · cited by 3
- CategoryTheory.DifferentialObject.d_squared_applystatement and proof · cited by 1
- CategoryTheory.DifferentialObject.eqToHom_f'statement and proof · cited by 1
- CategoryTheory.DifferentialObject.objEqToHom_dstatement and proof · cited by 1
- HomologicalComplex.homologicalComplexToDGO_map_fstatement · cited by 0
- HomologicalComplex.homologicalComplexToDGO_obj_dstatement · cited by 0
- HomologicalComplex.homologicalComplexToDGO_obj_objstatement · cited by 0