mathlib3 documentation

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.

source
@[reducible]
noncomputable def homological_complex.cycles {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_kernels V] (i : ι) :
category_theory.subobject (C.X i)

The cycles at index i, as a subobject.

source
theorem homological_complex.cycles_eq_kernel_subobject {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_kernels V] {i j : ι} (r : c.rel i j) :
C.cycles i = category_theory.limits.kernel_subobject (C.d i j)
source
noncomputable def homological_complex.cycles_iso_kernel {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_kernels V] {i j : ι} (r : c.rel i j) :
↑(C.cycles i) ≅ category_theory.limits.kernel (C.d 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
source
theorem homological_complex.cycles_eq_top {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_kernels V] {i : ι} (h : ¬c.rel i (c.next i)) :
C.cycles i = ⊤
source
@[reducible]
noncomputable def homological_complex.boundaries {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_images V] (C : homological_complex V c) (j : ι) :
category_theory.subobject (C.X j)

The boundaries at index i, as a subobject.

source
theorem homological_complex.boundaries_eq_image_subobject {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_images V] [category_theory.limits.has_equalizers V] {i j : ι} (r : c.rel i j) :
C.boundaries j = category_theory.limits.image_subobject (C.d i j)
source
noncomputable def homological_complex.boundaries_iso_image {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_images V] [category_theory.limits.has_equalizers V] {i j : ι} (r : c.rel i j) :
↑(C.boundaries j) ≅ category_theory.limits.image (C.d 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
source
theorem homological_complex.boundaries_eq_bot {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} (C : homological_complex V c) [category_theory.limits.has_images V] [category_theory.limits.has_zero_object V] {j : ι} (h : ¬c.rel (c.prev j) j) :
C.boundaries j = ⊥
source
theorem homological_complex.boundaries_le_cycles {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] (C : homological_complex V c) (i : ι) :
C.boundaries i ≤ C.cycles i
source
@[reducible]
noncomputable def homological_complex.boundaries_to_cycles {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] (C : homological_complex V c) (i : ι) :
↑(C.boundaries i) ⟶ ↑(C.cycles i)

The canonical map from boundaries i to cycles i.

source
@[simp]
theorem homological_complex.image_to_kernel_as_boundaries_to_cycles {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] (C : homological_complex V c) (i : ι) (h : C.boundaries i ≤ C.cycles i) :
(C.boundaries i).of_le (C.cycles i) h = C.boundaries_to_cycles i

Prefer boundaries_to_cycles.

source
@[reducible]
noncomputable def homological_complex.homology {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : homological_complex V c) (i : ι) :
V

The homology of a complex at index i.

source
noncomputable def homological_complex.homology_iso {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : homological_complex V 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
source
noncomputable def chain_complex.homology_zero_iso {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : chain_complex V ℕ) [category_theory.epi (category_theory.limits.factor_thru_image (C.d 1 0))] :
homological_complex.homology C 0 ≅ category_theory.limits.cokernel (C.d 1 0)

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

Equations
source
noncomputable def cochain_complex.homology_zero_iso {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_zero_object V] [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : cochain_complex V ℕ) :
homological_complex.homology C 0 ≅ category_theory.limits.kernel (C.d 0 1)

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

Equations
source
noncomputable def chain_complex.homology_succ_iso {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : chain_complex V ℕ) (n : ℕ) :
homological_complex.homology C (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
source
noncomputable def cochain_complex.homology_succ_iso {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_kernels V] [category_theory.limits.has_images V] [category_theory.limits.has_cokernels V] (C : cochain_complex V ℕ) (n : ℕ) :
homological_complex.homology C (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.

source
@[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_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.

source
@[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_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'
source
@[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_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)
source
@[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_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
source
@[simp]
theorem cycles_map_id {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_kernels V] {C₁ : homological_complex V c} (i : ι) :
cycles_map (𝟙 C₁) i = 𝟙 ↑(C₁.cycles i)
source
@[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_kernels V] {C₁ C₂ C₃ : homological_complex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) :
cycles_map (f ≫ g) i = cycles_map f i ≫ cycles_map g i
source
@[simp]
theorem cycles_functor_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_kernels V] (i : ι) (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂) :
(cycles_functor V c i).map f = cycles_map f i
source
noncomputable def cycles_functor {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_kernels V] (i : ι) :
homological_complex V c ⥤ V

Cycles as a functor.

Equations
Instances for cycles_functor
source
@[simp]
theorem cycles_functor_obj {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_kernels V] (i : ι) (C : homological_complex V c) :
(cycles_functor V c i).obj C = ↑(C.cycles i)

Computing the boundaries is functorial.

source
@[reducible]
noncomputable def boundaries_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_images V] [category_theory.limits.has_image_maps V] {C₁ C₂ : homological_complex V c} (f : C₁ ⟶ C₂) (i : ι) :
↑(C₁.boundaries i) ⟶ ↑(C₂.boundaries i)

The morphism between boundaries induced by a chain map.

source
noncomputable def boundaries_functor {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] (i : ι) :
homological_complex V c ⥤ V

Boundaries as a functor.

Equations
Instances for boundaries_functor
source
@[simp]
theorem boundaries_functor_obj {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] (i : ι) (C : homological_complex V c) :
(boundaries_functor V c i).obj C = ↑(C.boundaries i)
source
@[simp]
theorem boundaries_functor_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_images V] [category_theory.limits.has_image_maps V] (i : ι) (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂) :
(boundaries_functor V c i).map f = category_theory.limits.image_subobject_map (homological_complex.hom.sq_to f i)

The boundaries_to_cycles morphisms are natural.

source
@[simp]
theorem boundaries_to_cycles_naturality_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_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] {C₁ C₂ : homological_complex V c} (f : C₁ ⟶ C₂) (i : ι) {X' : V} (f' : ↑(C₂.cycles i) ⟶ X') :
boundaries_map f i ≫ C₂.boundaries_to_cycles i ≫ f' = C₁.boundaries_to_cycles i ≫ cycles_map f i ≫ f'
source
@[simp]
theorem boundaries_to_cycles_naturality {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {c : complex_shape ι} [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] {C₁ C₂ : homological_complex V c} (f : C₁ ⟶ C₂) (i : ι) :
boundaries_map f i ≫ C₂.boundaries_to_cycles i = C₁.boundaries_to_cycles i ≫ cycles_map f i
source
@[simp]
theorem boundaries_to_cycles_nat_trans_app {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] (i : ι) (C : homological_complex V c) :
(boundaries_to_cycles_nat_trans V c i).app C = C.boundaries_to_cycles i
source
noncomputable def boundaries_to_cycles_nat_trans {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] (i : ι) :
boundaries_functor V c i ⟶ cycles_functor V c i

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

Equations
source
noncomputable def homology_functor {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] (i : ι) :
homological_complex V c ⥤ V

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

Equations
Instances for homology_functor
source
@[simp]
theorem homology_functor_obj {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] (i : ι) (C : homological_complex V c) :
(homology_functor V c i).obj C = C.homology i
source
@[simp]
theorem homology_functor_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_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] (i : ι) (C₁ C₂ : homological_complex V c) (f : C₁ ⟶ C₂) :
(homology_functor V c i).map f = homology.map _ _ (homological_complex.hom.sq_to f i) (homological_complex.hom.sq_from f i) _
source
@[simp]
theorem graded_homology_functor_obj {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] (C : homological_complex V c) (i : ι) :
(graded_homology_functor V c).obj C i = C.homology i
source
noncomputable def graded_homology_functor {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (c : complex_shape ι) [category_theory.limits.has_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] :
homological_complex V c ⥤ category_theory.graded_object ι V

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

Equations
source
@[simp]
theorem graded_homology_functor_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_equalizers V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] [category_theory.limits.has_cokernels V] (C C' : homological_complex V c) (f : C ⟶ C') (i : ι) :
(graded_homology_functor V c).map f i = (homology_functor V c i).map f