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.{u_2, 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.

Equations

• K.truncLE n = HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE n)

@[reducible, inline]

noncomputable abbrev CochainComplex.truncGE {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• K.truncGE n = HomologicalComplex.truncGE K (ComplexShape.embeddingUpIntGE n)

noncomputable def CochainComplex.ιTruncLE {C : Type u_1} [CategoryTheory.Category.{u_2, 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 ℤ.

Equations

• K.ιTruncLE n = HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE n)

noncomputable def CochainComplex.πTruncGE {C : Type u_1} [CategoryTheory.Category.{u_2, 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 ℤ.

Equations

• K.πTruncGE n = HomologicalComplex.πTruncGE K (ComplexShape.embeddingUpIntGE n)

@[reducible, inline]

noncomputable abbrev CochainComplex.truncLEMap {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• CochainComplex.truncLEMap φ n = HomologicalComplex.truncLEMap φ (ComplexShape.embeddingUpIntLE n)

@[reducible, inline]

noncomputable abbrev CochainComplex.truncGEMap {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• CochainComplex.truncGEMap φ n = HomologicalComplex.truncGEMap φ (ComplexShape.embeddingUpIntGE n)

@[simp]

theorem CochainComplex.ιTruncLE_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : Prop

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

Equations

• K.IsStrictlyGE n = HomologicalComplex.IsStrictlySupported K (ComplexShape.embeddingUpIntGE n)

@[reducible, inline]

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

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

Equations

• K.IsStrictlyLE n = HomologicalComplex.IsStrictlySupported K (ComplexShape.embeddingUpIntLE n)

@[reducible, inline]

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

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

Equations

• K.IsGE n = HomologicalComplex.IsSupported K (ComplexShape.embeddingUpIntGE n)

@[reducible, inline]

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

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

Equations

• K.IsLE n = HomologicalComplex.IsSupported K (ComplexShape.embeddingUpIntLE n)

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

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

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

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

theorem CochainComplex.isZero_of_isGE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n) [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.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i) [K.IsLE n] [HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)

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

theorem CochainComplex.isStrictlyLE_iff {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℤ} (e : K ≅ L) (n : ℤ) [K.IsGE n] : L.IsGE n

theorem CochainComplex.exists_iso_single {C : Type u_1} [CategoryTheory.Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, 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'