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

@[simp]
theorem ChainComplex.truncate_obj_X {V : Type u} (C : ) (i : ) :
(ChainComplex.truncate.obj C).X i = C.X (i + 1)
@[simp]
theorem ChainComplex.truncate_obj_d {V : Type u} (C : ) (i : ) (j : ) :
(ChainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
@[simp]
theorem ChainComplex.truncate_map_f {V : Type u} :
∀ {X Y : } (f : X Y) (i : ), (ChainComplex.truncate.map f).f i = f.f (i + 1)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def ChainComplex.truncateTo {V : Type u} (C : ) :
ChainComplex.truncate.obj C .obj (C.X 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.

Equations
• C.truncateTo = ((ChainComplex.truncate.obj C).toSingle₀Equiv (C.X 0)).symm C.d 1 0,
Instances For
def ChainComplex.augment {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ChainComplex.augment_X_zero {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
(C.augment f w).X 0 = X
@[simp]
theorem ChainComplex.augment_X_succ {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
(C.augment f w).X (i + 1) = C.X i
@[simp]
theorem ChainComplex.augment_d_one_zero {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
(C.augment f w).d 1 0 = f
@[simp]
theorem ChainComplex.augment_d_succ_succ {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) (j : ) :
(C.augment f w).d (i + 1) (j + 1) = C.d i j
def ChainComplex.truncateAugment {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) :
ChainComplex.truncate.obj (C.augment f w) C

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ChainComplex.truncateAugment_hom_f {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
(C.truncateAugment f w).hom.f i =
@[simp]
theorem ChainComplex.truncateAugment_inv_f {V : Type u} (C : ) {X : V} (f : C.X 0 X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ) :
(C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((ChainComplex.truncate.obj (C.augment f w)).X i)
@[simp]
theorem ChainComplex.chainComplex_d_succ_succ_zero {V : Type u} (C : ) (i : ) :
C.d (i + 2) 0 = 0
def ChainComplex.augmentTruncate {V : Type u} (C : ) :
(ChainComplex.truncate.obj C).augment (C.d 1 0) C

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem ChainComplex.augmentTruncate_hom_f_zero {V : Type u} (C : ) :
C.augmentTruncate.hom.f 0 =
@[simp]
theorem ChainComplex.augmentTruncate_hom_f_succ {V : Type u} (C : ) (i : ) :
C.augmentTruncate.hom.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
@[simp]
theorem ChainComplex.augmentTruncate_inv_f_zero {V : Type u} (C : ) :
C.augmentTruncate.inv.f 0 =
@[simp]
theorem ChainComplex.augmentTruncate_inv_f_succ {V : Type u} (C : ) (i : ) :
C.augmentTruncate.inv.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
def ChainComplex.toSingle₀AsComplex {V : Type u} (C : ) (X : V) (f : C .obj X) :

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.

Equations
• C.toSingle₀AsComplex X f = match (C.toSingle₀Equiv X) f with | f, w => C.augment f w
Instances For
@[simp]
theorem CochainComplex.truncate_obj_d {V : Type u} (C : ) (i : ) (j : ) :
(CochainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
@[simp]
theorem CochainComplex.truncate_obj_X {V : Type u} (C : ) (i : ) :
(CochainComplex.truncate.obj C).X i = C.X (i + 1)
@[simp]
theorem CochainComplex.truncate_map_f {V : Type u} :
∀ {X Y : } (f : X Y) (i : ), (CochainComplex.truncate.map f).f i = f.f (i + 1)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CochainComplex.toTruncate {V : Type u} (C : ) :
.obj (C.X 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.

Equations
• C.toTruncate = ((CochainComplex.truncate.obj C).fromSingle₀Equiv (C.X 0)).symm C.d 0 1,
Instances For
def CochainComplex.augment {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CochainComplex.augment_X_zero {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
(C.augment f w).X 0 = X
@[simp]
theorem CochainComplex.augment_X_succ {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) :
(C.augment f w).X (i + 1) = C.X i
@[simp]
theorem CochainComplex.augment_d_zero_one {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
(C.augment f w).d 0 1 = f
@[simp]
theorem CochainComplex.augment_d_succ_succ {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) (j : ) :
(C.augment f w).d (i + 1) (j + 1) = C.d i j
def CochainComplex.truncateAugment {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) :
CochainComplex.truncate.obj (C.augment f w) C

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CochainComplex.truncateAugment_hom_f {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) :
(C.truncateAugment f w).hom.f i =
@[simp]
theorem CochainComplex.truncateAugment_inv_f {V : Type u} (C : ) {X : V} (f : X C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ) :
(C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((CochainComplex.truncate.obj (C.augment f w)).X i)
@[simp]
theorem CochainComplex.cochainComplex_d_succ_succ_zero {V : Type u} (C : ) (i : ) :
C.d 0 (i + 2) = 0
def CochainComplex.augmentTruncate {V : Type u} (C : ) :
(CochainComplex.truncate.obj C).augment (C.d 0 1) C

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CochainComplex.augmentTruncate_hom_f_zero {V : Type u} (C : ) :
C.augmentTruncate.hom.f 0 =
@[simp]
theorem CochainComplex.augmentTruncate_hom_f_succ {V : Type u} (C : ) (i : ) :
C.augmentTruncate.hom.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
@[simp]
theorem CochainComplex.augmentTruncate_inv_f_zero {V : Type u} (C : ) :
C.augmentTruncate.inv.f 0 =
@[simp]
theorem CochainComplex.augmentTruncate_inv_f_succ {V : Type u} (C : ) (i : ) :
C.augmentTruncate.inv.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
def CochainComplex.fromSingle₀AsComplex {V : Type u} (C : ) (X : V) (f : .obj X C) :

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.

Equations
• C.fromSingle₀AsComplex X f = match (C.fromSingle₀Equiv X) f with | f, w => C.augment f w
Instances For