mathlib documentation

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) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] :
β → 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 .)

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

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} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} (C : homological_complex V b) (i : β) :
C.d i C.d (i + b) = 0

@[simp]
theorem homological_complex.comm_at {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {β : Type} [add_comm_group β] {b : β} {C D : homological_complex V 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.

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