# mathlib3documentation

algebra.homology.homology

# The homology of a complex #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
noncomputable def homological_complex.cycles {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :

The cycles at index i, as a subobject.

theorem homological_complex.cycles_eq_kernel_subobject {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i j : ι} (r : c.rel i j) :
C.cycles i =
noncomputable def homological_complex.cycles_iso_kernel {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i j : ι} (r : c.rel i j) :

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

Equations
theorem homological_complex.cycles_eq_top {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i : ι} (h : ¬c.rel i (c.next i)) :
@[reducible]
noncomputable def homological_complex.boundaries {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (j : ι) :

The boundaries at index i, as a subobject.

theorem homological_complex.boundaries_eq_image_subobject {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i j : ι} (r : c.rel i j) :
noncomputable def homological_complex.boundaries_iso_image {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i j : ι} (r : c.rel i j) :

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

Equations
theorem homological_complex.boundaries_eq_bot {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {j : ι} (h : ¬c.rel (c.prev j) j) :
theorem homological_complex.boundaries_le_cycles {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :
@[reducible]
noncomputable def homological_complex.boundaries_to_cycles {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :

The canonical map from boundaries i to cycles i.

@[simp]
theorem homological_complex.image_to_kernel_as_boundaries_to_cycles {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) (h : C.boundaries i C.cycles i) :
(C.boundaries i).of_le (C.cycles i) h =

Prefer boundaries_to_cycles.

@[reducible]
noncomputable def homological_complex.homology {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :
V

The homology of a complex at index i.

noncomputable def homological_complex.homology_iso {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) {i j k : ι} (hij : c.rel i j) (hjk : c.rel j k) :
C.homology j homology (C.d i j) (C.d j k) _

The jth homology of a homological complex (as kernel of 'the differential from Cⱼ' modulo the image of 'the differential to Cⱼ') is isomorphic to the kernel of d : Cⱼ → Cₖ modulo the image of d : Cᵢ → Cⱼ when rel i j and rel j k.

Equations

The 0th homology of a chain complex is isomorphic to the cokernel of d : C₁ ⟶ C₀.

Equations

The 0th cohomology of a cochain complex is isomorphic to the kernel of d : C₀ → C₁.

Equations
noncomputable def chain_complex.homology_succ_iso {V : Type u} (C : ) (n : ) :
(n + 1) homology (C.d (n + 2) (n + 1)) (C.d (n + 1) n) _

The n + 1th homology of a chain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ modulo the image of d : Cₙ₊₂ → Cₙ₊₁.

Equations
noncomputable def cochain_complex.homology_succ_iso {V : Type u} (C : ) (n : ) :
(n + 1) homology (C.d n (n + 1)) (C.d (n + 1) (n + 2)) _

The n + 1th cohomology of a cochain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ₊₂ modulo the image of d : Cₙ → Cₙ₊₁.

Equations

Computing the cycles is functorial.

@[reducible]
noncomputable def cycles_map {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : 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} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) {X' : V} (f' : C₂.X i X') :
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} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) (x : (C₁.cycles i)) :
((C₂.cycles i).arrow) ( i) x) = (f.f i) (((C₁.cycles i).arrow) x)
@[simp]
theorem cycles_map_arrow {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) :
i (C₂.cycles i).arrow = (C₁.cycles i).arrow f.f i
@[simp]
theorem cycles_map_id {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ : c} (i : ι) :
cycles_map (𝟙 C₁) i = 𝟙 (C₁.cycles i)
@[simp]
theorem cycles_map_comp {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ C₃ : c} (f : C₁ C₂) (g : C₂ C₃) (i : ι) :
cycles_map (f g) i = i i
@[simp]
theorem cycles_functor_map {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C₁ C₂ : c) (f : C₁ C₂) :
c i).map f = i
noncomputable def cycles_functor {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :
V

Cycles as a functor.

Equations
Instances for cycles_functor
@[simp]
theorem cycles_functor_obj {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
c i).obj C = (C.cycles i)

Computing the boundaries is functorial.

@[reducible]
noncomputable def boundaries_map {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) :
(C₁.boundaries i) (C₂.boundaries i)

The morphism between boundaries induced by a chain map.

noncomputable def boundaries_functor {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :
V

Boundaries as a functor.

Equations
Instances for boundaries_functor
@[simp]
theorem boundaries_functor_obj {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
i).obj C = (C.boundaries i)
@[simp]
theorem boundaries_functor_map {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C₁ C₂ : c) (f : C₁ C₂) :

The boundaries_to_cycles morphisms are natural.

@[simp]
theorem boundaries_to_cycles_naturality_assoc {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) {X' : V} (f' : (C₂.cycles i) X') :
f' = i f'
@[simp]
theorem boundaries_to_cycles_naturality {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (f : C₁ C₂) (i : ι) :
= i
@[simp]
theorem boundaries_to_cycles_nat_trans_app {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
.app C =
noncomputable def boundaries_to_cycles_nat_trans {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :
i i

The natural transformation from the boundaries functor to the cycles functor.

Equations
noncomputable def homology_functor {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :
V

The i-th homology, as a functor to V.

Equations
Instances for homology_functor
@[simp]
theorem homology_functor_obj {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
c i).obj C = C.homology i
@[simp]
theorem homology_functor_map {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C₁ C₂ : c) (f : C₁ C₂) :
c i).map f = _
@[simp]
theorem graded_homology_functor_obj {ι : Type u_1} (V : Type u) (c : complex_shape ι) (C : c) (i : ι) :
.obj C i = C.homology i
noncomputable def graded_homology_functor {ι : Type u_1} (V : Type u) (c : complex_shape ι)  :

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

Equations
@[simp]
theorem graded_homology_functor_map {ι : Type u_1} (V : Type u) (c : complex_shape ι) (C C' : c) (f : C C') (i : ι) :
.map f i = c i).map f