mathlib documentation

algebra.homology.homology

The homology of a complex #

Given C : homological_complex V c, we have C.cycles i and C.boundaries i, both defined as subobjects of C.X i.

We show these are functorial with respect to chain maps, as C.cycles_map f i and C.boundaries_map f i.

As a consequence we construct homology_functor i : homological_complex V c ⥤ V, computing the i-th homology.

The underlying object of C.cycles i is isomorphic to kernel (C.d i j), for any j such that rel i j.

Equations

Computing the cycles is functorial.

The morphism between cycles induced by a chain map.

@[simp]
theorem cycles_map_arrow {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_zero_object V] [category_theory.limits.has_kernels V] {C₁ C₂ : homological_complex V c} (f : C₁ C₂) (i : ι) :
cycles_map f i (C₂.cycles i).arrow = (C₁.cycles i).arrow f.f i
@[simp]
theorem cycles_map_comp {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_zero_object V] [category_theory.limits.has_kernels V] {C₁ C₂ C₃ : homological_complex V c} (f : C₁ C₂) (g : C₂ C₃) (i : ι) :

Cycles as a functor.

Equations

Computing the boundaries is functorial.

The morphism between boundaries induced by a chain map.

The boundaries_to_cycles morphisms are natural.