Theorems · Definition · category theory
HomologicalComplex.ExactAt
{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 → ι → PropA homological complex K is exact at i if the short complex K.sc i is exact.
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
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
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- CategoryTheory.ShortComplex.Exactproof · cited by 292
- HomologicalComplex.scproof · cited by 205
Cited by49
Results whose statement or proof uses this declaration.
- HomologicalComplex.Acyclicproof · cited by 28
- HomologicalComplex.exactAt_iff_isZero_homologystatement · cited by 13
- HomologicalComplex.exactAt_of_isSupportedstatement · cited by 11
- HomologicalComplex.exactAt_iff'statement · cited by 10
- HomologicalComplex.ExactAt.isZero_homologystatement and proof · cited by 7
- quasiIsoAt_iff_exactAtstatement and proof · cited by 5
- CochainComplex.exactAt_of_isGEstatement · cited by 5
- exactAt_iff_of_quasiIsoAtstatement and proof · cited by 4
- CochainComplex.exactAt_of_isLEstatement · cited by 4
- HomologicalComplex.ExactAt.opstatement and proof · cited by 4
- HomologicalComplex.ExactAt.unopstatement and proof · cited by 4
- CochainComplex.isLE_iffstatement and proof · cited by 3