Theorems · Definition · category theory
CochainComplex.truncGE
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
(K : CochainComplex C ℤ) →
[CategoryTheory.Limits.HasZeroObject C] →
[∀ (i : ℤ), HomologicalComplex.HasHomology K i] → ℤ → CochainComplex C ℤIf K : CochainComplex C ℤ, this is the canonical truncation ≥ n of K.
- Cited by
- 16 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.
Cites8
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.Limits.HasZeroObjectstatement and proof · cited by 1,298
- ComplexShape.upstatement · cited by 1,123
- CochainComplexstatement and proof · cited by 1,016
- HomologicalComplex.HasHomologystatement and proof · cited by 342
- HomologicalComplex.truncGEproof · cited by 20
- ComplexShape.embeddingUpIntGEproof · cited by 20
Cited by21
Results whose statement or proof uses this declaration.
- CochainComplex.πTruncGEstatement · cited by 12
- CochainComplex.truncGEMapstatement · cited by 5
- CochainComplex.πTruncGE_naturalitystatement · cited by 3
- CochainComplex.shortComplexTruncLEX₃ToTruncGEstatement · cited by 3
- CochainComplex.quasiIso_truncGEMap_iffstatement · cited by 2
- DerivedCategory.left_fac_of_isStrictlyGEproof · cited by 2
- DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLEproof · cited by 1
- CochainComplex.Plus.modelCategoryQuillen.exists_quasiIso_injectiveproof · cited by 1
- DerivedCategory.isGE_iffproof · cited by 1
- CochainComplex.quasiIso_πTruncGE_iffstatement · cited by 1
- CochainComplex.g_shortComplexTruncLEX₃ToTruncGEstatement · cited by 1
- CochainComplex.truncGEXIsostatement · cited by 1