# Documentation

Mathlib.Algebra.Homology.Augment

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

@[simp]
theorem ChainComplex.truncate_obj_X {V : Type u} (C : ) (i : ) :
HomologicalComplex.X (ChainComplex.truncate.obj C) i = HomologicalComplex.X C (i + 1)
@[simp]
theorem ChainComplex.truncate_obj_d {V : Type u} (C : ) (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} :
∀ {X Y : } (f : X Y) (i : ), HomologicalComplex.Hom.f (ChainComplex.truncate.map f) i = HomologicalComplex.Hom.f f (i + 1)

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

Instances For
def ChainComplex.truncateTo {V : Type u} (C : ) :
ChainComplex.truncate.obj C ().obj ()

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.

Instances For
def ChainComplex.augment {V : Type u} (C : ) {X : V} (f : ) (w : ) :

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

Instances For
@[simp]
theorem ChainComplex.augment_X_zero {V : Type u} (C : ) {X : V} (f : ) (w : ) :
= X
@[simp]
theorem ChainComplex.augment_X_succ {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
@[simp]
theorem ChainComplex.augment_d_one_zero {V : Type u} (C : ) {X : V} (f : ) (w : ) :
@[simp]
theorem ChainComplex.augment_d_succ_succ {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) (j : ) :
HomologicalComplex.d () (i + 1) (j + 1) =
def ChainComplex.truncateAugment {V : Type u} (C : ) {X : V} (f : ) (w : ) :
ChainComplex.truncate.obj () C

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

Instances For
@[simp]
theorem ChainComplex.truncateAugment_hom_f {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
@[simp]
theorem ChainComplex.truncateAugment_inv_f {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
@[simp]
def ChainComplex.augmentTruncate {V : Type u} (C : ) :
ChainComplex.augment (ChainComplex.truncate.obj C) () (_ : 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.

Instances For
@[simp]
@[simp]
theorem ChainComplex.augmentTruncate_hom_f_succ {V : Type u} (C : ) (i : ) :
@[simp]
@[simp]
theorem ChainComplex.augmentTruncate_inv_f_succ {V : Type u} (C : ) (i : ) :
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.

Instances For
@[simp]
theorem CochainComplex.truncate_obj_d {V : Type u} (C : ) (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} (C : ) (i : ) :
HomologicalComplex.X (CochainComplex.truncate.obj C) i = HomologicalComplex.X C (i + 1)
@[simp]
theorem CochainComplex.truncate_map_f {V : Type u} :
∀ {X Y : } (f : X Y) (i : ), HomologicalComplex.Hom.f (CochainComplex.truncate.map f) i = HomologicalComplex.Hom.f f (i + 1)

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

Instances For
def CochainComplex.toTruncate {V : Type u} (C : ) :
().obj () 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.

Instances For
def CochainComplex.augment {V : Type u} (C : ) {X : V} (f : ) (w : ) :

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

Instances For
@[simp]
theorem CochainComplex.augment_X_zero {V : Type u} (C : ) {X : V} (f : ) (w : ) :
= X
@[simp]
theorem CochainComplex.augment_X_succ {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
@[simp]
theorem CochainComplex.augment_d_zero_one {V : Type u} (C : ) {X : V} (f : ) (w : ) :
= f
@[simp]
theorem CochainComplex.augment_d_succ_succ {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) (j : ) :
HomologicalComplex.d () (i + 1) (j + 1) =
def CochainComplex.truncateAugment {V : Type u} (C : ) {X : V} (f : ) (w : ) :
CochainComplex.truncate.obj () C

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

Instances For
@[simp]
theorem CochainComplex.truncateAugment_hom_f {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
@[simp]
theorem CochainComplex.truncateAugment_inv_f {V : Type u} (C : ) {X : V} (f : ) (w : ) (i : ) :
= CategoryTheory.CategoryStruct.id (HomologicalComplex.X (CochainComplex.truncate.obj ()) i)
@[simp]
def CochainComplex.augmentTruncate {V : Type u} (C : ) :
CochainComplex.augment (CochainComplex.truncate.obj C) () (_ : CategoryTheory.CategoryStruct.comp () (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.

Instances For
@[simp]
@[simp]
@[simp]
@[simp]
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.

Instances For