mathlibdocumentation

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.

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.

Equations
@[simp]
theorem homological_complex.cycles_arrow_d_from_assoc {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) {X' : V} (f' : C.X_next i X') :
(C.cycles i).arrow C.d_from i f' = 0 f'
@[simp]
theorem homological_complex.cycles_arrow_d_from {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :
(C.cycles i).arrow C.d_from i = 0
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.next i = none) :
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.prev j = none) :
theorem homological_complex.boundaries_le_cycles {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :
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.

@[simp]
theorem homological_complex.boundaries_to_cycles_arrow_assoc {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) {X' : V} (f' : C.X i X') :
(C.cycles i).arrow f' = (C.boundaries i).arrow f'
@[simp]
theorem homological_complex.boundaries_to_cycles_arrow {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) (i : ι) :
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.

Computing the cycles is functorial.

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 {ι : 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
@[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.

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
@[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
@[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