Theorems · Definition · category theory
ComplexShape.up
(α : Type u_2) → [inst : Add α] → [IsRightCancelAdd α] → [One α] → ComplexShape α
The ComplexShape appropriate for cohomology, so d : X i ⟶ X j only when j = i + 1.
- Defined in
- Mathlib.Algebra.Homology.ComplexShape
- Cited by
- 1,123 results in Mathlib
- Foundations
- Depth 9 from the axioms, rests on 20 definitions · uses no axioms
- Assumes
- AddIsRightCancelAddOne
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ComplexShapestatement · cited by 1,684
- IsRightCancelAddstatement and proof · cited by 69
- ComplexShape.up'proof · cited by 27
Cited by1,473
Results whose statement or proof uses this declaration.
- CochainComplexproof · cited by 1,016
- CategoryTheory.HasExtproof · cited by 218
- CochainComplex.HomComplex.Cochain.vstatement · cited by 213
- CategoryTheory.Abelian.Extproof · cited by 191
- HasDerivedCategoryproof · cited by 190
- CochainComplex.mappingConestatement · cited by 181
- DerivedCategoryproof · cited by 165
- CochainComplex.HomComplex.Cochain.ofHomstatement · cited by 121
- CochainComplex.singleFunctorstatement · cited by 111
- DerivedCategory.Qstatement · cited by 102
- CategoryTheory.Abelian.Ext.mk₀proof · cited by 94
- CochainComplex.mappingCone.inrstatement · cited by 79
Showing the 200 most cited of 1,473.