Augmentation and truncation of ℕ-indexed (co)chain complexes.

@[simp]

theorem ChainComplex.truncate_obj_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) (i : ℕ) : HomologicalComplex.X (ChainComplex.truncate.obj C) i = HomologicalComplex.X C (i + 1)

@[simp]

theorem ChainComplex.truncate_obj_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) (i : ℕ) (j : ℕ) : HomologicalComplex.d (ChainComplex.truncate.obj C) i j = HomologicalComplex.d C (i + 1) (j + 1)

@[simp]

theorem ChainComplex.truncate_map_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] : ∀ {X Y : ChainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), HomologicalComplex.Hom.f (ChainComplex.truncate.map f) i = HomologicalComplex.Hom.f f (i + 1)

def ChainComplex.truncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (ChainComplex V ℕ) (ChainComplex V ℕ)

The truncation of an ℕ-indexed chain complex, deleting the object at 0 and shifting everything else down.

def ChainComplex.truncateTo {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) : ChainComplex.truncate.obj C ⟶ (ChainComplex.single₀ V).obj (HomologicalComplex.X C 0)

There is a canonical chain map from the truncation of a chain map C to the "single object" chain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 1 0 in degree 0, and zero otherwise.

def ChainComplex.augment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) : ChainComplex V ℕ

We can "augment" a chain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

@[simp]

theorem ChainComplex.augment_X_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) : HomologicalComplex.X (ChainComplex.augment C f w) 0 = X

@[simp]

theorem ChainComplex.augment_X_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) (i : ℕ) : HomologicalComplex.X (ChainComplex.augment C f w) (i + 1) = HomologicalComplex.X C i

@[simp]

theorem ChainComplex.augment_d_one_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) : HomologicalComplex.d (ChainComplex.augment C f w) 1 0 = f

@[simp]

theorem ChainComplex.augment_d_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) (i : ℕ) (j : ℕ) : HomologicalComplex.d (ChainComplex.augment C f w) (i + 1) (j + 1) = HomologicalComplex.d C i j

def ChainComplex.truncateAugment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) : ChainComplex.truncate.obj (ChainComplex.augment C f w) ≅ C

Truncating an augmented chain complex is isomorphic (with components the identity) to the original complex.

@[simp]

theorem ChainComplex.truncateAugment_hom_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) (i : ℕ) : HomologicalComplex.Hom.f (ChainComplex.truncateAugment C f w).hom i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C i)

@[simp]

theorem ChainComplex.truncateAugment_inv_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) {X : V} (f : HomologicalComplex.X C 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 1 0) f = 0) (i : ℕ) : HomologicalComplex.Hom.f (ChainComplex.truncateAugment C f w).inv i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (ChainComplex.truncate.obj (ChainComplex.augment C f w)) i)

@[simp]

theorem ChainComplex.chainComplex_d_succ_succ_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) (i : ℕ) : HomologicalComplex.d C (i + 2) 0 = 0

def ChainComplex.augmentTruncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) : ChainComplex.augment (ChainComplex.truncate.obj C) (HomologicalComplex.d C 1 0) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C (1 + 1) (0 + 1)) (HomologicalComplex.d C (0 + 1) 0) = 0) ≅ C

Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

@[simp]

theorem ChainComplex.augmentTruncate_hom_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) : HomologicalComplex.Hom.f (ChainComplex.augmentTruncate C).hom 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C 0)

@[simp]

theorem ChainComplex.augmentTruncate_hom_f_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) (i : ℕ) : HomologicalComplex.Hom.f (ChainComplex.augmentTruncate C).hom (i + 1) = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C (i + 1))

@[simp]

theorem ChainComplex.augmentTruncate_inv_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) : HomologicalComplex.Hom.f (ChainComplex.augmentTruncate C).inv 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C 0)

@[simp]

theorem ChainComplex.augmentTruncate_inv_f_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : ChainComplex V ℕ) (i : ℕ) : HomologicalComplex.Hom.f (ChainComplex.augmentTruncate C).inv (i + 1) = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C (i + 1))

def ChainComplex.toSingle₀AsComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V) (f : C ⟶ (ChainComplex.single₀ V).obj X) : ChainComplex V ℕ

A chain map from a chain complex to a single object chain complex in degree zero can be reinterpreted as a chain complex.

This is the inverse construction of truncateTo.

@[simp]

theorem CochainComplex.truncate_obj_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) (i : ℕ) (j : ℕ) : HomologicalComplex.d (CochainComplex.truncate.obj C) i j = HomologicalComplex.d C (i + 1) (j + 1)

@[simp]

theorem CochainComplex.truncate_obj_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) (i : ℕ) : HomologicalComplex.X (CochainComplex.truncate.obj C) i = HomologicalComplex.X C (i + 1)

@[simp]

theorem CochainComplex.truncate_map_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] : ∀ {X Y : CochainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), HomologicalComplex.Hom.f (CochainComplex.truncate.map f) i = HomologicalComplex.Hom.f f (i + 1)

def CochainComplex.truncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (CochainComplex V ℕ) (CochainComplex V ℕ)

The truncation of an ℕ-indexed cochain complex, deleting the object at 0 and shifting everything else down.

def CochainComplex.toTruncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) : (CochainComplex.single₀ V).obj (HomologicalComplex.X C 0) ⟶ CochainComplex.truncate.obj C

There is a canonical chain map from the truncation of a cochain complex C to the "single object" cochain complex consisting of the truncated object C.X 0 in degree 0. The components of this chain map are C.d 0 1 in degree 0, and zero otherwise.

def CochainComplex.augment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) : CochainComplex V ℕ

We can "augment" a cochain complex by inserting an arbitrary object in degree zero (shifting everything else up), along with a suitable differential.

@[simp]

theorem CochainComplex.augment_X_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) : HomologicalComplex.X (CochainComplex.augment C f w) 0 = X

@[simp]

theorem CochainComplex.augment_X_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) (i : ℕ) : HomologicalComplex.X (CochainComplex.augment C f w) (i + 1) = HomologicalComplex.X C i

@[simp]

theorem CochainComplex.augment_d_zero_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) : HomologicalComplex.d (CochainComplex.augment C f w) 0 1 = f

@[simp]

theorem CochainComplex.augment_d_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) (i : ℕ) (j : ℕ) : HomologicalComplex.d (CochainComplex.augment C f w) (i + 1) (j + 1) = HomologicalComplex.d C i j

def CochainComplex.truncateAugment {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) : CochainComplex.truncate.obj (CochainComplex.augment C f w) ≅ C

Truncating an augmented cochain complex is isomorphic (with components the identity) to the original complex.

@[simp]

theorem CochainComplex.truncateAugment_hom_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) (i : ℕ) : HomologicalComplex.Hom.f (CochainComplex.truncateAugment C f w).hom i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C i)

@[simp]

theorem CochainComplex.truncateAugment_inv_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) {X : V} (f : X ⟶ HomologicalComplex.X C 0) (w : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d C 0 1) = 0) (i : ℕ) : HomologicalComplex.Hom.f (CochainComplex.truncateAugment C f w).inv i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (CochainComplex.truncate.obj (CochainComplex.augment C f w)) i)

@[simp]

theorem CochainComplex.cochainComplex_d_succ_succ_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) (i : ℕ) : HomologicalComplex.d C 0 (i + 2) = 0

def CochainComplex.augmentTruncate {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) : CochainComplex.augment (CochainComplex.truncate.obj C) (HomologicalComplex.d C 0 1) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C 0 1) (HomologicalComplex.d C 1 (1 + 1)) = 0) ≅ C

Augmenting a truncated complex with the original object and morphism is isomorphic (with components the identity) to the original complex.

@[simp]

theorem CochainComplex.augmentTruncate_hom_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) : HomologicalComplex.Hom.f (CochainComplex.augmentTruncate C).hom 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C 0)

@[simp]

theorem CochainComplex.augmentTruncate_hom_f_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) (i : ℕ) : HomologicalComplex.Hom.f (CochainComplex.augmentTruncate C).hom (i + 1) = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C (i + 1))

@[simp]

theorem CochainComplex.augmentTruncate_inv_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) : HomologicalComplex.Hom.f (CochainComplex.augmentTruncate C).inv 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C 0)

@[simp]

theorem CochainComplex.augmentTruncate_inv_f_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (C : CochainComplex V ℕ) (i : ℕ) : HomologicalComplex.Hom.f (CochainComplex.augmentTruncate C).inv (i + 1) = CategoryTheory.CategoryStruct.id (HomologicalComplex.X C (i + 1))

def CochainComplex.fromSingle₀AsComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] (C : CochainComplex V ℕ) (X : V) (f : (CochainComplex.single₀ V).obj X ⟶ C) : CochainComplex V ℕ

A chain map from a single object cochain complex in degree zero to a cochain complex can be reinterpreted as a cochain complex.

This is the inverse construction of toTruncate.