feat(algebra/homology): the cohomology functor (leanprover-community#…

…2374)

This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on leanprover-community#2373.

In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial.

In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular.

A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

src/algebra/homology/homology.lean

@@ -8,16 +8,16 @@ import category_theory.limits.shapes.images
 import category_theory.limits.shapes.kernels
 
 /-!
-# Non-functorial cohomology groups for cochain complexes
+# Cohomology groups for cochain complexes
 
 We setup that part of the theory of cohomology groups which works in
 any category with kernels and images.
 
-We define the cohomology groups themselves, and while we can show that
-chain maps induce maps on the kernels, at this level of generality
-chain maps do not induce maps on the images, and so not on the cohomology groups.
+We define the cohomology 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 cohomology.
 
-We'll do this with stronger assumptions, later.
 -/
 
 universes v u
@@ -30,6 +30,8 @@ open category_theory.limits
 variables {V : Type u} [𝒱 : category.{v} V] [has_zero_morphisms.{v} V]
 include 𝒱
 
+section
+
 variable [has_kernels.{v} V]
 /-- The map induced by a chain map between the kernels of the differentials. -/
 def kernel_map {C C' : cochain_complex V} (f : C ⟶ C') (i : ℤ) :
@@ -39,10 +41,10 @@ begin
   rw [category.assoc, ←comm_at f, ←category.assoc, kernel.condition, has_zero_morphisms.zero_comp],
 end
 
-@[simp]
+@[simp, reassoc]
 lemma kernel_map_condition {C C' : cochain_complex V} (f : C ⟶ C') (i : ℤ) :
   kernel_map f i ≫ kernel.ι (C'.d i) = kernel.ι (C.d i) ≫ f.f i :=
-by erw [limit.lift_π, fork.of_ι_app_zero]
+by simp [kernel_map]
 
 @[simp]
 lemma kernel_map_id (C : cochain_complex.{v} V) (i : ℤ) :
@@ -53,83 +55,92 @@ lemma kernel_map_id (C : cochain_complex.{v} V) (i : ℤ) :
 lemma kernel_map_comp {C C' C'' : cochain_complex.{v} V} (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 rw [kernel_map_condition, category.assoc, kernel_map_condition,
-    ←category.assoc, kernel_map_condition, category.assoc, differential_object.comp_f,
-    graded_object.comp_apply]
+(cancel_mono (kernel.ι (C''.d i))).1 $ by simp
 
--- TODO: Actually, this is a functor `cochain_complex V ⥤ cochain_complex V`, but to state this
--- properly we will need `has_shift` on `differential_object` first.
 /-- The kernels of the differentials of a cochain complex form a ℤ-graded object. -/
 def kernel_functor : cochain_complex.{v} V ⥤ graded_object ℤ V :=
 { obj := λ C i, kernel (C.d i),
   map := λ X Y f i, kernel_map f i }
 
+end
+
+section
+variables [has_images.{v} V] [has_image_maps.{v} V]
+
+/-- A morphism of cochain complexes induces a morphism on the images of the differentials in every
+    degree. -/
+abbreviation image_map {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+  image (C.d i) ⟶ image (C'.d i) :=
+image.map (arrow.hom_mk' (cochain_complex.comm_at f i).symm)
+
+@[simp]
+lemma image_map_ι {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+  image_map f i ≫ image.ι (C'.d i) = image.ι (C.d i) ≫ f.f (i + 1) :=
+image.map_hom_mk'_ι (cochain_complex.comm_at f i).symm
+
+end
+
 /-!
 At this point we assume that we have all images, and all equalizers.
 We need to assume all equalizers, not just kernels, so that
 `factor_thru_image` is an epimorphism.
 -/
-variables [has_images.{v} V] [has_equalizers.{v} V]
+variables [has_kernels.{v} V] [has_images.{v} V] [has_equalizers.{v} V]
 
 /--
 The connecting morphism from the image of `d i` to the kernel of `d (i+1)`.
 -/
 def image_to_kernel_map (C : cochain_complex V) (i : ℤ) :
   image (C.d i) ⟶ kernel (C.d (i+1)) :=
-kernel.lift _ (image.ι (C.d i))
-begin
-  rw ←cancel_epi (factor_thru_image (C.d i)),
-  rw [has_zero_morphisms.comp_zero, image.fac_assoc, d_squared],
-end
+kernel.lift _ (image.ι (C.d i)) $ (cancel_epi (factor_thru_image (C.d i))).1 $ by simp
+
+@[simp, reassoc]
+lemma image_to_kernel_map_condition (C : cochain_complex V) (i : ℤ) :
+  image_to_kernel_map C i ≫ kernel.ι (C.d (i + 1)) = image.ι (C.d i) :=
+by simp [image_to_kernel_map]
 
--- TODO (a good project!):
--- At this level of generality, it's just not true that a chain map
--- induces maps on boundaries
---
--- Let's add these later, with appropriate (but hopefully fairly minimal)
--- assumptions: perhaps that the category is regular?
--- I think in that case we can compute `image` as the regular coimage,
--- i.e. the coequalizer of the kernel pair,
--- and that image has the appropriate mapping property.
-
--- def image_map {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
---   image (C.d i) ⟶ image (C'.d i) :=
--- sorry
-
--- -- I'm not certain what the minimal assumptions required to prove the following
--- -- lemma are:
--- lemma induced_maps_commute {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
--- image_to_kernel_map C i ≫ kernel_map f (i+1) =
---   image_map f i ≫ image_to_kernel_map C' i :=
--- sorry
+@[reassoc]
+lemma induced_maps_commute [has_image_maps.{v} V] {C C' : cochain_complex.{v} V} (f : C ⟶ C')
+  (i : ℤ) :
+  image_to_kernel_map C i ≫ kernel_map f (i + 1) = image_map f i ≫ image_to_kernel_map C' i :=
+by { ext, simp }
 
 variables [has_cokernels.{v} V]
 
 /-- The `i`-th cohomology group of the cochain complex `C`. -/
 def cohomology (C : cochain_complex V) (i : ℤ) : V :=
 cokernel (image_to_kernel_map C (i-1))
 
--- TODO:
-
--- As noted above, as we don't get induced maps on boundaries with this generality,
--- we can't assemble the cohomology groups into a functor. Hopefully, however,
--- the commented out code below will work
--- (with whatever added assumptions are needed above.)
-
--- def cohomology_map {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
---   C.cohomology i ⟶ C'.cohomology i :=
--- cokernel.desc _ (kernel_map f (i-1) ≫ cokernel.π _)
--- begin
---   rw [←category.assoc, induced_maps_commute, category.assoc, cokernel.condition],
---   erw [has_zero_morphisms.comp_zero],
--- end
-
--- /-- The cohomology functor from chain complexes to `ℤ` graded objects in `V`. -/
--- def cohomology_functor : cochain_complex.{v} V ⥤ graded_object ℤ V :=
--- { obj := λ C i, cohomology C i,
---   map := λ C C' f i, cohomology_map f i,
---   map_id' := sorry,
---   map_comp' := sorry, }
+variables [has_image_maps.{v} V]
+
+/-- A morphism of cochain complexes induces a morphism in cohomology at every degree. -/
+def cohomology_map {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+  C.cohomology i ⟶ C'.cohomology i :=
+cokernel.desc _ (kernel_map f (i - 1 + 1) ≫ cokernel.π _) $ by simp [induced_maps_commute_assoc]
+
+@[simp, reassoc]
+lemma cohomology_map_condition {C C' : cochain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+  cokernel.π (image_to_kernel_map C (i - 1)) ≫ cohomology_map f i =
+    kernel_map f (i - 1 + 1) ≫ cokernel.π _ :=
+by simp [cohomology_map]
+
+@[simp]
+lemma cohomology_map_id (C : cochain_complex.{v} V) (i : ℤ) :
+  cohomology_map (𝟙 C) i = 𝟙 (cohomology C i) :=
+begin
+  ext,
+  simp only [cohomology_map_condition, kernel_map_id, category.id_comp],
+  erw [category.comp_id]
+end
+
+@[simp]
+lemma cohomology_map_comp {C C' C'' : cochain_complex.{v} V} (f : C ⟶ C') (g : C' ⟶ C'') (i : ℤ) :
+  cohomology_map (f ≫ g) i = cohomology_map f i ≫ cohomology_map g i :=
+by { ext, simp }
+
+/-- The cohomology functor from cochain complexes to `ℤ` graded objects in `V`. -/
+def cohomology_functor : cochain_complex.{v} V ⥤ graded_object ℤ V :=
+{ obj := λ C i, cohomology C i,
+  map := λ C C' f i, cohomology_map f i }
 
 end cochain_complex