/
homology.lean
197 lines (146 loc) · 6.55 KB
/
homology.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Markus Himmel
-/
import algebra.homology.chain_complex
import algebra.homology.image_to_kernel_map
/-!
# (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`.
-/
universes v u
noncomputable theory
open category_theory
open category_theory.limits
variables {V : Type u} [category.{v} V] [has_zero_morphisms V]
variables {β : Type} [add_comm_group β] {b : β}
namespace homological_complex
section has_kernels
variable [has_kernels V]
/-- The map induced by a chain map between the kernels of the differentials. -/
def kernel_map {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
kernel (C.d i) ⟶ kernel (C'.d i) :=
kernel.lift _ (kernel.ι _ ≫ f.f i)
begin
rw [category.assoc, ←comm_at f, ←category.assoc, kernel.condition, zero_comp],
end
@[simp, reassoc]
lemma kernel_map_condition {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
kernel_map f i ≫ kernel.ι (C'.d i) = kernel.ι (C.d i) ≫ f.f i :=
by simp [kernel_map]
@[simp]
lemma kernel_map_id (C : homological_complex V b) (i : β) :
kernel_map (𝟙 C) i = 𝟙 _ :=
(cancel_mono (kernel.ι (C.d i))).1 $ by simp
@[simp]
lemma kernel_map_comp {C C' C'' : homological_complex V b} (f : C ⟶ C')
(g : C' ⟶ C'') (i : β) :
kernel_map (f ≫ g) i = kernel_map f i ≫ kernel_map g i :=
(cancel_mono (kernel.ι (C''.d i))).1 $ by simp
/-- The kernels of the differentials of a complex form a `β`-graded object. -/
def kernel_functor : homological_complex V b ⥤ graded_object β V :=
{ obj := λ C i, kernel (C.d i),
map := λ X Y f i, kernel_map f i }
end has_kernels
section has_image_maps
variables [has_images V] [has_image_maps V]
/-- A morphism of complexes induces a morphism on the images of the differentials in every
degree. -/
abbreviation image_map {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
image (C.d i) ⟶ image (C'.d i) :=
image.map (arrow.hom_mk' (comm_at f i).symm)
@[simp]
lemma image_map_ι {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
image_map f i ≫ image.ι (C'.d i) = image.ι (C.d i) ≫ f.f (i + b) :=
image.map_hom_mk'_ι (comm_at f i).symm
end has_image_maps
variables [has_images V] [has_equalizers V]
/--
The connecting morphism from the image of `d i` to the kernel of `d (i ± 1)`.
-/
def image_to_kernel_map (C : homological_complex V b) (i : β) :
image (C.d i) ⟶ kernel (C.d (i+b)) :=
category_theory.image_to_kernel_map (C.d i) (C.d (i+b)) (by simp)
@[simp, reassoc]
lemma image_to_kernel_map_condition (C : homological_complex V b) (i : β) :
image_to_kernel_map C i ≫ kernel.ι (C.d (i + b)) = image.ι (C.d i) :=
by simp [image_to_kernel_map]
@[reassoc]
lemma image_to_kernel_map_comp_kernel_map [has_image_maps V]
{C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
image_to_kernel_map C i ≫ kernel_map f (i + b) = image_map f i ≫ image_to_kernel_map C' i :=
by { ext, simp }
variables [has_cokernels V]
/-- The `i`-th homology group of the complex `C`. -/
def homology_group (i : β) (C : homological_complex V b) : V :=
cokernel (image_to_kernel_map C (i-b))
variables [has_image_maps V]
/-- A chain map induces a morphism in homology at every degree. -/
def homology_map {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
C.homology_group i ⟶ C'.homology_group i :=
cokernel.desc _ (kernel_map f (i - b + b) ≫ cokernel.π _) $
by simp [image_to_kernel_map_comp_kernel_map_assoc]
@[simp, reassoc]
lemma homology_map_condition {C C' : homological_complex V b} (f : C ⟶ C') (i : β) :
cokernel.π (image_to_kernel_map C (i - b)) ≫ homology_map f i =
kernel_map f (i - b + b) ≫ cokernel.π _ :=
by simp [homology_map]
@[simp]
lemma homology_map_id (C : homological_complex V b) (i : β) :
homology_map (𝟙 C) i = 𝟙 (C.homology_group i) :=
begin
ext,
simp only [homology_map_condition, kernel_map_id, category.id_comp],
erw [category.comp_id]
end
@[simp]
lemma homology_map_comp {C C' C'' : homological_complex V b} (f : C ⟶ C') (g : C' ⟶ C'') (i : β) :
homology_map (f ≫ g) i = homology_map f i ≫ homology_map g i :=
by { ext, simp }
variables (V)
/-- The `i`-th homology functor from `β` graded complexes to `V`. -/
@[simps]
def homology (i : β) : homological_complex V b ⥤ V :=
{ obj := λ C, C.homology_group i,
map := λ C C' f, homology_map f i, }
/-- The homology functor from `β` graded complexes to `β` graded objects in `V`. -/
@[simps]
def graded_homology : homological_complex V b ⥤ graded_object β V :=
{ obj := λ C i, C.homology_group i,
map := λ C C' f i, homology_map f i }
end homological_complex
/-!
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.
-/
namespace cochain_complex
variables [has_images V] [has_equalizers V] [has_cokernels V]
/-- The `i`-th cohomology group of the cochain complex `C`. -/
abbreviation cohomology_group (C : cochain_complex V) (i : ℤ) : V :=
C.homology_group i
variables [has_image_maps V]
/-- A chain map induces a morphism in cohomology at every degree. -/
abbreviation cohomology_map {C C' : cochain_complex V} (f : C ⟶ C') (i : ℤ) :
C.cohomology_group i ⟶ C'.cohomology_group i :=
homological_complex.homology_map f i
variables (V)
/-- The `i`-th homology functor from cohain complexes to `V`. -/
abbreviation cohomology (i : ℤ) : cochain_complex V ⥤ V :=
homological_complex.homology V i
/-- The cohomology functor from cochain complexes to `ℤ`-graded objects in `V`. -/
abbreviation graded_cohomology : cochain_complex V ⥤ graded_object ℤ V :=
homological_complex.graded_homology V
end cochain_complex