# mathlibdocumentation

algebra.homology.chain_complex

# Chain complexes

We define a chain complex in V as a differential ℤ-graded object in V.

This is fancy language for the obvious definition, and it seems we can use it straightforwardly:

example (C : chain_complex V) : C.X 5 ⟶ C.X 6 := C.d 5

def homological_complex (V : Type u) {β : Type}  :
β → Type (max v u)

A homological_complex V b for b : β is a (co)chain complex graded by β, with differential in grading b.

(We use the somewhat cumbersome homological_complex to avoid the name conflict with ℂ.)

def chain_complex (V : Type u)  :
Type (max v u)

A chain complex in V is "just" a differential ℤ-graded object in V, with differential graded -1.

def cochain_complex (V : Type u)  :
Type (max v u)

A cochain complex in V is "just" a differential ℤ-graded object in V, with differential graded +1.

@[simp]
theorem homological_complex.d_squared {V : Type u} {β : Type} {b : β} (C : b) (i : β) :
C.d i C.d (i + b) = 0

@[simp]
theorem homological_complex.comm_at {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) (i : β) :
C.d i f.f (i + b) = f.f i D.d i

A convenience lemma for morphisms of cochain complexes, picking out one component of the commutation relation.

@[simp]
theorem homological_complex.comm {V : Type u} {β : Type} {b : β} {C D : b} (f : C D) :
C.d = f.f D.d

def homological_complex.forget (V : Type u) {β : Type} {b : β} :

The forgetful functor from cochain complexes to graded objects, forgetting the differential.

@[instance]
def homological_complex.inhabited {β : Type} {b : β} :

Equations