Theorems · Theorem · category theory
CochainComplex.isZero_of_isStrictlyLE
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(K : CochainComplex C ℤ) (n i : ℤ),
autoParam (n < i) CochainComplex.isZero_of_isStrictlyLE._auto_1 →
∀ [K.IsStrictlyLE n], CategoryTheory.Limits.IsZero (K.X i)- Cited by
- 8 results in Mathlib
- Foundations
- Depth 55 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
- HomologicalComplex.Xstatement · cited by 1,839
- ComplexShape.upstatement · cited by 1,123
- CochainComplexstatement and proof · cited by 1,016
- CategoryTheory.Limits.IsZerostatement · cited by 306
- ComplexShape.embeddingUpIntLEproof · cited by 21
- CochainComplex.IsStrictlyLEstatement and proof · cited by 20
- HomologicalComplex.isZero_X_of_isStrictlySupportedproof · cited by 7
Cited by8
Results whose statement or proof uses this declaration.
- CochainComplex.isStrictlyLE_iffproof · cited by 2
- CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projectiveproof · cited by 1
- CochainComplex.exists_iso_singleproof · cited by 1
- CochainComplex.isStrictlyLE_shiftproof · cited by 1
- DerivedCategory.from_singleFunctor_obj_eq_zero_of_projectiveproof · cited by 1
- CochainComplex.isKProjective_of_projectiveproof · cited by 0
- DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGEproof · cited by 0
- CochainComplex.isStrictlyLE_of_leproof · cited by 0