(Co)homology groups for complexes
We setup that part of the theory of homology groups which works in any category with kernels and images.
We define the homology groups themselves, and show that they induce maps on kernels.
Under the additional assumption that our category has equalizers and functorial images, we construct induced morphisms on images and functorial induced morphisms in homology.
Chains and cochains
Throughout we work with complexes graded by an arbitrary [add_comm_group β],
with a differential with grading b : β.
Thus we're simultaneously doing homology and cohomology groups
(and in future, e.g., enabling computing homologies for successive pages of spectral sequences).
At the end of the file we set up abbreviations cohomology and graded_cohomology,
so that when you're working with a C : cochain_complex V, you can write C.cohomology i
rather than the confusing C.homology i.
def
homological_complex.kernel_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
category_theory.limits.kernel (C.d i) ⟶ category_theory.limits.kernel (C'.d i)
The map induced by a chain map between the kernels of the differentials.
Equations
- homological_complex.kernel_map f i = category_theory.limits.kernel.lift (C'.d i) (category_theory.limits.kernel.ι (C.d i) ≫ f.f i) _
@[simp]
theorem
homological_complex.kernel_map_condition
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
homological_complex.kernel_map f i ≫ category_theory.limits.kernel.ι (C'.d i) = category_theory.limits.kernel.ι (C.d i) ≫ f.f i
@[simp]
theorem
homological_complex.kernel_map_condition_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β)
{X' : V}
(f' : C'.X i ⟶ X') :
homological_complex.kernel_map f i ≫ category_theory.limits.kernel.ι (C'.d i) ≫ f' = category_theory.limits.kernel.ι (C.d i) ≫ f.f i ≫ f'
@[simp]
theorem
homological_complex.kernel_map_id
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V]
(C : homological_complex V b)
(i : β) :
homological_complex.kernel_map (𝟙 C) i = 𝟙 (category_theory.limits.kernel (C.d i))
@[simp]
theorem
homological_complex.kernel_map_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V]
{C C' C'' : homological_complex V b}
(f : C ⟶ C')
(g : C' ⟶ C'')
(i : β) :
def
homological_complex.kernel_functor
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_kernels V] :
The kernels of the differentials of a complex form a β-graded object.
Equations
- homological_complex.kernel_functor = {obj := λ (C : homological_complex V b) (i : β), category_theory.limits.kernel (C.d i), map := λ (X Y : homological_complex V b) (f : X ⟶ Y) (i : β), homological_complex.kernel_map f i, map_id' := _, map_comp' := _}
def
homological_complex.image_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
category_theory.limits.image (C.d i) ⟶ category_theory.limits.image (C'.d i)
A morphism of complexes induces a morphism on the images of the differentials in every degree.
@[simp]
theorem
homological_complex.image_map_ι
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
homological_complex.image_map f i ≫ category_theory.limits.image.ι (C'.d i) = category_theory.limits.image.ι (C.d i) ≫ f.f (i + b)
def
homological_complex.image_to_kernel_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
(C : homological_complex V b)
(i : β) :
category_theory.limits.image (C.d i) ⟶ category_theory.limits.kernel (C.d (i + b))
The connecting morphism from the image of d i to the kernel of d (i ± 1).
Equations
- C.image_to_kernel_map i = category_theory.image_to_kernel_map (C.d i) (C.d (i + b)) _
@[simp]
theorem
homological_complex.image_to_kernel_map_condition_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
(C : homological_complex V b)
(i : β)
{X' : V}
(f' : C.X (i + b) ⟶ X') :
C.image_to_kernel_map i ≫ category_theory.limits.kernel.ι (C.d (i + b)) ≫ f' = category_theory.limits.image.ι (C.d i) ≫ f'
@[simp]
theorem
homological_complex.image_to_kernel_map_condition
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
(C : homological_complex V b)
(i : β) :
C.image_to_kernel_map i ≫ category_theory.limits.kernel.ι (C.d (i + b)) = category_theory.limits.image.ι (C.d i)
theorem
homological_complex.image_to_kernel_map_comp_kernel_map_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β)
{X' : V}
(f' : category_theory.limits.kernel (C'.d (i + b)) ⟶ X') :
C.image_to_kernel_map i ≫ homological_complex.kernel_map f (i + b) ≫ f' = homological_complex.image_map f i ≫ C'.image_to_kernel_map i ≫ f'
theorem
homological_complex.image_to_kernel_map_comp_kernel_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
C.image_to_kernel_map i ≫ homological_complex.kernel_map f (i + b) = homological_complex.image_map f i ≫ C'.image_to_kernel_map i
def
homological_complex.homology_group
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V] :
β → homological_complex V b → V
The i-th homology group of the complex C.
Equations
def
homological_complex.homology_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
A chain map induces a morphism in homology at every degree.
Equations
- homological_complex.homology_map f i = category_theory.limits.cokernel.desc (C.image_to_kernel_map (i - b)) (homological_complex.kernel_map f (i - b + b) ≫ category_theory.limits.cokernel.π (C'.image_to_kernel_map (i - b))) _
@[simp]
theorem
homological_complex.homology_map_condition
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β) :
category_theory.limits.cokernel.π (C.image_to_kernel_map (i - b)) ≫ homological_complex.homology_map f i = homological_complex.kernel_map f (i - b + b) ≫ category_theory.limits.cokernel.π (C'.image_to_kernel_map (i - b))
@[simp]
theorem
homological_complex.homology_map_condition_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
{C C' : homological_complex V b}
(f : C ⟶ C')
(i : β)
{X' : V}
(f' : homological_complex.homology_group i C' ⟶ X') :
category_theory.limits.cokernel.π (C.image_to_kernel_map (i - b)) ≫ homological_complex.homology_map f i ≫ f' = homological_complex.kernel_map f (i - b + b) ≫ category_theory.limits.cokernel.π (C'.image_to_kernel_map (i - b)) ≫ f'
@[simp]
theorem
homological_complex.homology_map_id
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
(C : homological_complex V b)
(i : β) :
@[simp]
theorem
homological_complex.homology_map_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
{C C' C'' : homological_complex V b}
(f : C ⟶ C')
(g : C' ⟶ C'')
(i : β) :
@[simp]
theorem
homological_complex.homology_obj
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
(i : β)
(C : homological_complex V b) :
def
homological_complex.homology
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V] :
β → homological_complex V b ⥤ V
The i-th homology functor from β graded complexes to V.
Equations
- homological_complex.homology V i = {obj := λ (C : homological_complex V b), homological_complex.homology_group i C, map := λ (C C' : homological_complex V b) (f : C ⟶ C'), homological_complex.homology_map f i, map_id' := _, map_comp' := _}
@[simp]
theorem
homological_complex.homology_map_2
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
(i : β)
(C C' : homological_complex V b)
(f : C ⟶ C') :
def
homological_complex.graded_homology
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V] :
The homology functor from β graded complexes to β graded objects in V.
Equations
- homological_complex.graded_homology V = {obj := λ (C : homological_complex V b) (i : β), homological_complex.homology_group i C, map := λ (C C' : homological_complex V b) (f : C ⟶ C') (i : β), homological_complex.homology_map f i, map_id' := _, map_comp' := _}
@[simp]
theorem
homological_complex.graded_homology_obj
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
(C : homological_complex V b)
(i : β) :
@[simp]
theorem
homological_complex.graded_homology_map
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{β : Type}
[add_comm_group β]
{b : β}
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
(C C' : homological_complex V b)
(f : C ⟶ C')
(i : β) :
We now set up abbreviations so that you can write C.cohomology i or (graded_cohomology V).map f,
etc., when C is a cochain complex.
def
cochain_complex.cohomology_group
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V] :
cochain_complex V → ℤ → V
The i-th cohomology group of the cochain complex C.
def
cochain_complex.cohomology_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V]
{C C' : cochain_complex V}
(f : C ⟶ C')
(i : ℤ) :
C.cohomology_group i ⟶ C'.cohomology_group i
A chain map induces a morphism in cohomology at every degree.
def
cochain_complex.cohomology
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V] :
ℤ → cochain_complex V ⥤ V
The i-th homology functor from cohain complexes to V.
def
cochain_complex.graded_cohomology
(V : Type u)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_image_maps V] :
The cohomology functor from cochain complexes to ℤ-graded objects in V.