# mathlibdocumentation

algebra.homology.homology

# (Co)homology groups for complexes

We setup that part of the theory of homology groups which works in any category with kernels and images.

We define the homology groups themselves, and show that they induce maps on kernels.

Under the additional assumption that our category has equalizers and functorial images, we construct induced morphisms on images and functorial induced morphisms in homology.

## Chains and cochains

Throughout we work with complexes graded by an arbitrary [add_comm_group β], with a differential with grading b : β. Thus we're simultaneously doing homology and cohomology groups (and in future, e.g., enabling computing homologies for successive pages of spectral sequences).

At the end of the file we set up abbreviations cohomology and graded_cohomology, so that when you're working with a C : cochain_complex V, you can write C.cohomology i rather than the confusing C.homology i.

def homological_complex.kernel_map {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :

The map induced by a chain map between the kernels of the differentials.

Equations
@[simp]
theorem homological_complex.kernel_map_condition_assoc {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) {X' : V} (f' : C'.X i X') :
f' = f.f i f'

@[simp]
theorem homological_complex.kernel_map_condition {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :
= f.f i

@[simp]
theorem homological_complex.kernel_map_id {V : Type u} {β : Type} {b : β} (C : b) (i : β) :

@[simp]
theorem homological_complex.kernel_map_comp {V : Type u} {β : Type} {b : β} {C C' C'' : b} (f : C C') (g : C' C'') (i : β) :

def homological_complex.kernel_functor {V : Type u} {β : Type} {b : β}  :

The kernels of the differentials of a complex form a β-graded object.

Equations
def homological_complex.image_map {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :

A morphism of complexes induces a morphism on the images of the differentials in every degree.

@[simp]
theorem homological_complex.image_map_ι {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :
= f.f (i + b)

def homological_complex.image_to_kernel_map {V : Type u} {β : Type} {b : β} (C : b) (i : β) :

The connecting morphism from the image of d i to the kernel of d (i ± 1).

Equations
• = (C.d (i + b)) _
@[simp]
theorem homological_complex.image_to_kernel_map_condition {V : Type u} {β : Type} {b : β} (C : b) (i : β) :

@[simp]
theorem homological_complex.image_to_kernel_map_condition_assoc {V : Type u} {β : Type} {b : β} (C : b) (i : β) {X' : V} (f' : C.X (i + b) X') :

theorem homological_complex.image_to_kernel_map_comp_kernel_map_assoc {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) {X' : V} (f' : category_theory.limits.kernel (C'.d (i + b)) X') :
(i + b) f' = f'

theorem homological_complex.image_to_kernel_map_comp_kernel_map {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :
(i + b) =

def homological_complex.homology_group {V : Type u} {β : Type} {b : β}  :
β → → V

The i-th homology group of the complex C.

Equations
def homological_complex.homology_map {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :

A chain map induces a morphism in homology at every degree.

Equations
@[simp]
theorem homological_complex.homology_map_condition {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) :
= (i - b + b)

@[simp]
theorem homological_complex.homology_map_condition_assoc {V : Type u} {β : Type} {b : β} {C C' : b} (f : C C') (i : β) {X' : V} (f' : X') :
= (i - b + b) f'

@[simp]
theorem homological_complex.homology_map_id {V : Type u} {β : Type} {b : β} (C : b) (i : β) :

@[simp]
theorem homological_complex.homology_map_comp {V : Type u} {β : Type} {b : β} {C C' C'' : b} (f : C C') (g : C' C'') (i : β) :

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

The i-th homology functor from β graded complexes to V.

Equations
@[simp]
theorem homological_complex.homology_obj (V : Type u) {β : Type} {b : β} (i : β) (C : b) :

@[simp]
theorem homological_complex.homology_map_2 (V : Type u) {β : Type} {b : β} (i : β) (C C' : b) (f : C C') :

The homology functor from β graded complexes to β graded objects in V.

Equations
@[simp]
theorem homological_complex.graded_homology_obj (V : Type u) {β : Type} {b : β} (C : b) (i : β) :

@[simp]
theorem homological_complex.graded_homology_map (V : Type u) {β : Type} {b : β} (C C' : b) (f : C C') (i : β) :

We now set up abbreviations so that you can write C.cohomology i or (graded_cohomology V).map f, etc., when C is a cochain complex.

The i-th cohomology group of the cochain complex C.

def cochain_complex.cohomology_map {V : Type u} {C C' : cochain_complex V} (f : C C') (i : ) :

A chain map induces a morphism in cohomology at every degree.

The i-th homology functor from cohain complexes to V.

The cohomology functor from cochain complexes to ℤ-graded objects in V.