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.

@[reducible]

The cycles at index i, as a subobject.

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

Equations
@[reducible]

The boundaries at index i, as a subobject.

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

Equations
@[reducible]

The canonical map from boundaries i to cycles i.

Computing the cycles is functorial.

@[reducible]
noncomputable def cycles_map {ι : 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 : ι) :
(C₁.cycles i) (C₂.cycles i)

The morphism between cycles induced by a chain map.

@[simp]
theorem cycles_map_arrow_assoc {ι : 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 : ι) {X' : V} (f' : C₂.X i X') :
cycles_map f i (C₂.cycles i).arrow f' = (C₁.cycles i).arrow f.f i f'
@[simp]
theorem cycles_map_arrow_apply {ι : 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 : ι) [I : category_theory.concrete_category V] (x : (C₁.cycles i)) :
((C₂.cycles i).arrow) ((cycles_map f i) x) = (f.f i) (((C₁.cycles i).arrow) x)
@[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
Instances for cycles_functor

Computing the boundaries is functorial.

@[reducible]

The morphism between boundaries induced by a chain map.

The boundaries_to_cycles morphisms are natural.

The homology functor from ι-indexed complexes to ι-graded objects in V.

Equations