Theorems · Definition · category theory
CategoryTheory.ShortComplex.cycles
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasLeftHomology] → CThe cycles of a short complex, given by the K field of a chosen left homology data.
- Cited by
- 220 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 10 definitions · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.LeftHomologyData.Kproof · cited by 233
- CategoryTheory.ShortComplex.HasLeftHomologystatement and proof · cited by 132
- CategoryTheory.ShortComplex.leftHomologyDataproof · cited by 83
Cited by253
Results whose statement or proof uses this declaration.
- HomologicalComplex.cyclesproof · cited by 164
- CategoryTheory.ShortComplex.iCyclesstatement · cited by 100
- CategoryTheory.ShortComplex.homologyπstatement · cited by 71
- CategoryTheory.ShortComplex.toCyclesstatement · cited by 47
- CategoryTheory.ShortComplex.cyclesMapstatement · cited by 42
- CategoryTheory.ShortComplex.liftCyclesstatement · cited by 32
- CategoryTheory.ShortComplex.leftHomologyπstatement · cited by 29
- CategoryTheory.ShortComplex.LeftHomologyData.cyclesIsostatement · cited by 28
- CategoryTheory.ShortComplex.exact_of_f_is_kernelproof · cited by 22
- CategoryTheory.ShortComplex.moduleCatCyclesIsostatement · cited by 20
- CategoryTheory.ShortComplex.liftCycles_istatement · cited by 18
- CategoryTheory.ShortComplex.toCycles_istatement · cited by 16
Showing the 200 most cited of 253.