Theorems · Theorem · category theory
HomologicalComplex.ExactAt.isZero_homology
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i],
K.ExactAt i → CategoryTheory.Limits.IsZero (K.homology i)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- HomologicalComplex.HasHomologystatement and proof · cited by 342
- CategoryTheory.Limits.IsZerostatement · cited by 306
- HomologicalComplex.homologystatement · cited by 209
- HomologicalComplex.ExactAtstatement and proof · cited by 44
- HomologicalComplex.exactAt_iff_isZero_homologyproof · cited by 13
Cited by7
Results whose statement or proof uses this declaration.
- CochainComplex.isZero_of_isLEproof · cited by 1
- DerivedCategory.isLE_iffproof · cited by 1
- HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zeroproof · cited by 1
- CochainComplex.isZero_of_isGEproof · cited by 1
- HomologicalComplex.mono_homologyMap_shortComplexTruncLE_gproof · cited by 1
- DerivedCategory.isGE_iffproof · cited by 1