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.

Equations

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

@[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.

Equations

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

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 ℤ.

Equations

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

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 ℤ.

Equations

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

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.

Equations

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

@[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.

Equations

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

@[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.

Equations

• K.IsStrictlyGE n = HomologicalComplex.IsStrictlySupported K (ComplexShape.embeddingUpIntGE 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.

Equations

• K.IsStrictlyLE n = HomologicalComplex.IsStrictlySupported K (ComplexShape.embeddingUpIntLE 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.

Equations

• K.IsGE n = HomologicalComplex.IsSupported K (ComplexShape.embeddingUpIntGE 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.

Equations

• K.IsLE n = HomologicalComplex.IsSupported K (ComplexShape.embeddingUpIntLE 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

theorem CochainComplex.isStrictlyGE_mapHomologicalComplex_obj_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Faithful] [F.PreservesZeroMorphisms] (n : ℤ) : IsStrictlyGE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n ↔ K.IsStrictlyGE n

theorem CochainComplex.isStrictlyLE_mapHomologicalComplex_obj_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Faithful] [F.PreservesZeroMorphisms] (n : ℤ) : IsStrictlyLE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n ↔ K.IsStrictlyLE n

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'

noncomputable def CochainComplex.truncGEXIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n i : ℤ) (hi : n < i := by lia) : (K.truncGE n).X i ≅ K.X i

When K is a cochain complex indexed by ℤ and n < i, this is the isomorphism (K.truncGE n).X i ≅ K.X i.

Equations

• K.truncGEXIso n i hi = HomologicalComplex.truncGEXIso K (ComplexShape.embeddingUpIntGE n) ⋯ ⋯

noncomputable def CochainComplex.truncLEXIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n i : ℤ) (hi : i < n := by lia) : (K.truncLE n).X i ≅ K.X i

When K is a cochain complex indexed by ℤ and i < n, this is the isomorphism (K.truncLE n).X i ≅ K.X i.

Equations

• K.truncLEXIso n i hi = HomologicalComplex.truncLEXIso K (ComplexShape.embeddingUpIntLE n) ⋯ ⋯

noncomputable def CochainComplex.truncGEXIsoOpcycles {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : (K.truncGE n).X n ≅ HomologicalComplex.opcycles K n

When K is a cochain complex indexed by ℤ, this is the isomorphism (K.truncGE n).X n ≅ K.opcycles n.

Equations

• K.truncGEXIsoOpcycles n = HomologicalComplex.truncGEXIsoOpcycles K (ComplexShape.embeddingUpIntGE n) ⋯ ⋯

noncomputable def CochainComplex.truncLEXIsoCycles {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) : (K.truncLE n).X n ≅ HomologicalComplex.cycles K n

When K is a cochain complex indexed by ℤ, this is the isomorphism (K.truncLE n).X n ≅ K.cycles n.

Equations

• K.truncLEXIsoCycles n = HomologicalComplex.truncLEXIsoCycles K (ComplexShape.embeddingUpIntLE n) ⋯ ⋯

theorem CochainComplex.acyclic_truncGE_iff {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) : HomologicalComplex.Acyclic (K.truncGE n₁) ↔ K.IsLE n₀

theorem CochainComplex.acyclic_truncLE_iff {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) [∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) : HomologicalComplex.Acyclic (K.truncLE n₀) ↔ 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.

Equations

• K.shortComplexTruncLE n = HomologicalComplex.shortComplexTruncLE K (ComplexShape.embeddingUpIntLE 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₁ := by lia) : (K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁

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

Equations

• K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = HomologicalComplex.shortComplexTruncLEX₃ToTruncGE K ⋯

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₁ := by lia) : 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₁ := by lia) {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✝

theorem CochainComplex.injective_opcycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℤ) (n₀ n₁ : ℤ) [CategoryTheory.Injective (K.X n₀)] [CategoryTheory.Injective (K.X n₁)] [K.IsStrictlyGE n₀] (hK : HomologicalComplex.ExactAt K n₀) (h : n₀ + 1 = n₁ := by lia) : CategoryTheory.Injective (HomologicalComplex.opcycles K n₁)