Truncations on cochain complexes indexed by the integers.

In this file, we introduce abbreviations for the canonical truncations CochainComplex.truncLE, CochainComplex.truncGE of cochain complexes indexed by ℤ, as well as the conditions CochainComplex.IsStrictlyLE, CochainComplex.IsStrictlyGE, CochainComplex.IsLE, and CochainComplex.IsGE.

@[reducible, inline]

noncomputable abbrev CochainComplex.truncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : CochainComplex C ℤ

If K : CochainComplex C ℤ, this is the canonical truncation ≤ n of K.

@[reducible, inline]

noncomputable abbrev CochainComplex.truncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : CochainComplex C ℤ

If K : CochainComplex C ℤ, this is the canonical truncation ≥ n of K.

noncomputable def CochainComplex.ιTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : K.truncLE n ⟶ K

The canonical map K.truncLE n ⟶ K for K : CochainComplex C ℤ.

noncomputable def CochainComplex.πTruncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : K ⟶ K.truncGE n

The canonical map K ⟶ K.truncGE n for K : CochainComplex C ℤ.

theorem CochainComplex.quasiIsoAt_ιTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n q : ℤ) (hq : q ≤ n) : QuasiIsoAt (K.ιTruncLE n) q

theorem CochainComplex.quasiIsoAt_πTruncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n q : ℤ) (hq : n ≤ q) : QuasiIsoAt (K.πTruncGE n) q

instance CochainComplex.instQuasiIsoAtIntπTruncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : QuasiIsoAt (K.πTruncGE n) n

instance CochainComplex.instQuasiIsoAtIntιTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : QuasiIsoAt (K.ιTruncLE n) n

@[reducible, inline]

noncomputable abbrev CochainComplex.truncLEMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : K.truncLE n ⟶ L.truncLE n

The morphism K.truncLE n ⟶ L.truncLE n induced by a morphism K ⟶ L.

@[reducible, inline]

noncomputable abbrev CochainComplex.truncGEMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : K.truncGE n ⟶ L.truncGE n

The morphism K.truncGE n ⟶ L.truncGE n induced by a morphism K ⟶ L.

@[simp]

theorem CochainComplex.ιTruncLE_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : CategoryTheory.CategoryStruct.comp (truncLEMap φ n) (L.ιTruncLE n) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) φ

@[simp]

theorem CochainComplex.ιTruncLE_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) {Z : CochainComplex C ℤ} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp (truncLEMap φ n) (CategoryTheory.CategoryStruct.comp (L.ιTruncLE n) h) = CategoryTheory.CategoryStruct.comp (K.ιTruncLE n) (CategoryTheory.CategoryStruct.comp φ h)

@[simp]

theorem CochainComplex.πTruncGE_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : CategoryTheory.CategoryStruct.comp (K.πTruncGE n) (truncGEMap φ n) = CategoryTheory.CategoryStruct.comp φ (L.πTruncGE n)

@[simp]

theorem CochainComplex.πTruncGE_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) {Z : CochainComplex C ℤ} (h : L.truncGE n ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.πTruncGE n) (CategoryTheory.CategoryStruct.comp (truncGEMap φ n) h) = CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πTruncGE n) h)

@[reducible, inline]

abbrev CochainComplex.IsStrictlyGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : Prop

The condition that a cochain complex K is strictly ≥ n.

@[reducible, inline]

abbrev CochainComplex.IsStrictlyLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : Prop

The condition that a cochain complex K is strictly ≤ n.

@[reducible, inline]

abbrev CochainComplex.IsGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : Prop

The condition that a cochain complex K is (cohomologically) ≥ n.

@[reducible, inline]

abbrev CochainComplex.IsLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : Prop

The condition that a cochain complex K is (cohomologically) ≤ n.

theorem CochainComplex.isZero_of_isStrictlyGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n := by lia) [K.IsStrictlyGE n] : CategoryTheory.Limits.IsZero (K.X i)

theorem CochainComplex.isZero_of_isStrictlyLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i := by lia) [K.IsStrictlyLE n] : CategoryTheory.Limits.IsZero (K.X i)

theorem CochainComplex.exactAt_of_isGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n := by lia) [K.IsGE n] : HomologicalComplex.ExactAt K i

theorem CochainComplex.exactAt_of_isLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i := by lia) [K.IsLE n] : HomologicalComplex.ExactAt K i

theorem CochainComplex.isZero_of_isGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n := by lia) [K.IsGE n] [HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)

theorem CochainComplex.isZero_of_isLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i := by lia) [K.IsLE n] [HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)

theorem CochainComplex.isStrictlyGE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → CategoryTheory.Limits.IsZero (K.X i)

theorem CochainComplex.isStrictlyLE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero (K.X i)

theorem CochainComplex.isGE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsGE n ↔ ∀ i < n, HomologicalComplex.ExactAt K i

theorem CochainComplex.isLE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsLE n ↔ ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt K i

theorem CochainComplex.isStrictlyLE_of_le {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyLE p] : K.IsStrictlyLE q

theorem CochainComplex.isStrictlyGE_of_ge {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyGE q] : K.IsStrictlyGE p

theorem CochainComplex.isLE_of_le {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsLE p] : K.IsLE q

theorem CochainComplex.isGE_of_ge {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p ≤ q) [K.IsGE q] : K.IsGE p

theorem CochainComplex.isStrictlyLE_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyLE n] : L.IsStrictlyLE n

theorem CochainComplex.isStrictlyGE_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsStrictlyGE n] : L.IsStrictlyGE n

theorem CochainComplex.isLE_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsLE n] : L.IsLE n

theorem CochainComplex.isGE_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsGE n] : L.IsGE n

instance CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : CochainComplex C ℕ) : IsStrictlyGE (HomologicalComplex.extend X ComplexShape.embeddingUpNat) 0

instance CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X : ChainComplex C ℕ) : IsStrictlyLE (HomologicalComplex.extend X ComplexShape.embeddingDownNat) 0

theorem CochainComplex.exists_iso_single {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) [K.IsStrictlyGE n] [K.IsStrictlyLE n] : ∃ (M : C), Nonempty (K ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj M)

A cochain complex that is both strictly ≤ n and ≥ n is isomorphic to a complex (single _ _ n).obj M for some object M.

instance CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) : IsStrictlyGE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n

instance CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) : IsStrictlyLE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n

instance CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyGE n] : CategoryTheory.IsIso (K.πTruncGE n)

instance CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyLE n] : CategoryTheory.IsIso (K.ιTruncLE n)

theorem CochainComplex.isIso_πTruncGE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : CategoryTheory.IsIso (K.πTruncGE n) ↔ K.IsStrictlyGE n

theorem CochainComplex.isIso_ιTruncLE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : CategoryTheory.IsIso (K.ιTruncLE n) ↔ K.IsStrictlyLE n

theorem CochainComplex.quasiIso_πTruncGE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : QuasiIso (K.πTruncGE n) ↔ K.IsGE n

theorem CochainComplex.quasiIso_ιTruncLE_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : QuasiIso (K.ιTruncLE n) ↔ K.IsLE n

instance CochainComplex.instQuasiIsoIntπTruncGEOfIsGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsGE n] : QuasiIso (K.πTruncGE n)

instance CochainComplex.instQuasiIsoIntιTruncLEOfIsLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsLE n] : QuasiIso (K.ιTruncLE n)

theorem CochainComplex.quasiIso_truncGEMap_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : QuasiIso (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

theorem CochainComplex.quasiIso_truncLEMap_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasZeroObject C] [∀ (i : ℤ), HomologicalComplex.HasHomology K i] [∀ (i : ℤ), HomologicalComplex.HasHomology L i] (n : ℤ) : QuasiIso (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i

instance CochainComplex.instIsStrictlyGEObjIntSingleFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) : ((singleFunctor C n).obj A).IsStrictlyGE n

instance CochainComplex.instIsStrictlyLEObjIntSingleFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ) : ((singleFunctor C n).obj A).IsStrictlyLE n

theorem CochainComplex.isStrictlyLE_shift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] (a n' : ℤ) (h : a + n' = n) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyLE n'

theorem CochainComplex.isStrictlyGE_shift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyGE n] (a n' : ℤ) (h : a + n' = n) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyGE n'

theorem CochainComplex.isLE_shift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsLE n] (a n' : ℤ) (h : a + n' = n) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsLE n'

theorem CochainComplex.isGE_shift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsGE n] (a n' : ℤ) (h : a + n' = n) : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsGE n'

@[reducible, inline]

noncomputable abbrev CochainComplex.shortComplexTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n : ℤ) : CategoryTheory.ShortComplex (CochainComplex C ℤ)

The cokernel sequence of the monomorphism K.ιTruncLE n.

theorem CochainComplex.shortComplexTruncLE_shortExact {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n : ℤ) : (K.shortComplexTruncLE n).ShortExact

@[reducible, inline]

noncomputable abbrev CochainComplex.shortComplexTruncLEX₃ToTruncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁

The canonical morphism (K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁.

theorem CochainComplex.g_shortComplexTruncLEX₃ToTruncGE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE n₀).g (K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h) = K.πTruncGE n₁

theorem CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : CochainComplex C ℤ} (h✝ : K.truncGE n₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE n₀).g (CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h) h✝) = CategoryTheory.CategoryStruct.comp (K.πTruncGE n₁) h✝