Theorems · Definition · category theory
CategoryTheory.ShortComplex.homology
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasHomology] → CThe homology of a short complex is the left.H field of a chosen homology data.
- Cited by
- 216 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 12 definitions · uses Classical.choice
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.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- CategoryTheory.ShortComplex.HasHomologystatement and proof · cited by 253
- CategoryTheory.ShortComplex.LeftHomologyData.Hproof · cited by 236
- CategoryTheory.ShortComplex.HomologyData.leftproof · cited by 130
- CategoryTheory.ShortComplex.homologyDataproof · cited by 33
Cited by257
Results whose statement or proof uses this declaration.
- HomologicalComplex.homologyproof · cited by 209
- CategoryTheory.Abelian.SpectralObject.Eproof · cited by 169
- CategoryTheory.ShortComplex.homologyMapstatement · cited by 83
- CategoryTheory.ShortComplex.homologyπstatement · cited by 71
- CategoryTheory.ShortComplex.homologyιstatement · cited by 51
- CategoryTheory.ShortComplex.LeftHomologyData.homologyIsostatement · cited by 34
- CategoryTheory.ShortComplex.leftHomologyIsostatement · cited by 27
- CategoryTheory.ShortComplex.RightHomologyData.homologyIsostatement · cited by 27
- CategoryTheory.ShortComplex.rightHomologyIsostatement · cited by 20
- HomologicalComplex.exactAt_iff_isZero_homologyproof · cited by 13
- CategoryTheory.ShortComplex.mapHomologyIsostatement · cited by 12
- CategoryTheory.ShortComplex.moduleCatHomologyIsostatement · cited by 12
Showing the 200 most cited of 257.