Theorems · Definition · category theory
HomologicalComplex.sc
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
{ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → ι → CategoryTheory.ShortComplex CThe short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).
- Cited by
- 205 results in Mathlib
- Foundations
- Depth 22 from the axioms, rests on 132 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.ShortComplexstatement · cited by 1,850
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- HomologicalComplex.shortComplexFunctorproof · cited by 72
Cited by272
Results whose statement or proof uses this declaration.
- HomologicalComplex.HasHomologyproof · cited by 342
- HomologicalComplex.homologyproof · cited by 209
- HomologicalComplex.cyclesproof · cited by 164
- HomologicalComplex.opcyclesproof · cited by 153
- HomologicalComplex.iCyclesproof · cited by 80
- HomologicalComplex.pOpcyclesproof · cited by 71
- HomologicalComplex.homologyπproof · cited by 69
- HomologicalComplex.homologyιproof · cited by 48
- HomologicalComplex.ExactAtproof · cited by 44
- HomologicalComplex.liftCyclesproof · cited by 22
- CategoryTheory.ShortComplex.ShortExact.δstatement · cited by 22
- groupHomology.isoCycles₁proof · cited by 19
Showing the 200 most cited of 272.