feat(algebra/homology, category_theory/abelian, algebra/category/Module): exactness (#3784)

We define what it means for two maps `f` and `g` to be exact and show that for R-modules, this is the case if and only if `range f = ker g`.

Author: TwoFX

src/algebra/category/Module/abelian.lean

@@ -5,10 +5,12 @@ Authors: Markus Himmel
 -/
 import algebra.category.Module.kernels
 import algebra.category.Module.limits
-import category_theory.abelian.basic
+import category_theory.abelian.exact
 
 /-!
 # The category of left R-modules is abelian.
+
+Additionally, two linear maps are exact in the categorical sense iff `range f = ker g`.
 -/
 
 open category_theory
@@ -72,4 +74,16 @@ instance : abelian (Module R) :=
   normal_mono := λ X Y, normal_mono,
   normal_epi := λ X Y, normal_epi }
 
+variables {O : Module R} (g : N ⟶ O)
+
+open linear_map
+local attribute [instance] preadditive.has_equalizers_of_has_kernels
+
+theorem exact_iff : exact f g ↔ f.range = g.ker :=
+begin
+  rw abelian.exact_iff' f g (kernel_is_limit _) (cokernel_is_colimit _),
+  exact ⟨λ h, le_antisymm (range_le_ker_iff.2 h.1) (ker_le_range_iff.2 h.2),
+    λ h, ⟨range_le_ker_iff.1 $ le_of_eq h, ker_le_range_iff.1 $ le_of_eq h.symm⟩⟩
+end
+
 end Module

src/algebra/homology/exact.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import algebra.homology.image_to_kernel_map
+
+/-!
+# Exact sequences
+
+In a category with zero morphisms, images, and equalizers we say that `f : A ⟶ B` and `g : B ⟶ C`
+are exact if `f ≫ g = 0` and the natural map `image f ⟶ kernel g` is an epimorphism.
+
+# Main results
+* Suppose that cokernels exist and that `f` and `g` are exact. If `s` is any kernel fork over `g`
+  and `t` is any cokernel cofork over `f`, then `fork.ι s ≫ cofork.π t = 0`.
+
+See also `category_theory/abelian/exact.lean` for results that only hold in abelian categories.
+
+# Future work
+* Short exact sequences, split exact sequences, the splitting lemma (maybe only for abelian
+  categories?)
+* Two adjacent maps in a chain complex are exact iff the homology vanishes
+* Composing with isomorphisms retains exactness, and similar constructions
+
+-/
+
+universes v u
+
+open category_theory
+open category_theory.limits
+
+variables {V : Type u} [category.{v} V] [has_zero_morphisms V]
+variables [has_kernels V] [has_equalizers V] [has_images V]
+
+namespace category_theory
+
+/-- Two morphisms `f : A ⟶ B`, `g : B ⟶ C` are called exact if `f ≫ g = 0` and the natural map
+    `image f ⟶ kernel g` is an epimorphism. -/
+class exact {A B C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop :=
+(w : f ≫ g = 0)
+(epi : epi (image_to_kernel_map f g w))
+
+attribute [instance] exact.epi
+
+section
+variables [has_cokernels V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C)
+
+@[simp, reassoc] lemma kernel_comp_cokernel [exact f g] : kernel.ι g ≫ cokernel.π f = 0 :=
+zero_of_epi_comp (image_to_kernel_map f g exact.w) $ zero_of_epi_comp (factor_thru_image f) $
+  by simp
+
+lemma comp_eq_zero_of_exact [exact f g] {X Y : V} {ι : X ⟶ B} (hι : ι ≫ g = 0) {π : B ⟶ Y}
+  (hπ : f ≫ π = 0) : ι ≫ π = 0 :=
+by rw [←kernel.lift_ι _ _ hι, ←cokernel.π_desc _ _ hπ, category.assoc, kernel_comp_cokernel_assoc,
+  has_zero_morphisms.zero_comp, has_zero_morphisms.comp_zero]
+
+@[simp, reassoc] lemma fork_ι_comp_cofork_π [exact f g] (s : kernel_fork g)
+  (t : cokernel_cofork f) : fork.ι s ≫ cofork.π t = 0 :=
+comp_eq_zero_of_exact f g (kernel_fork.condition s) (cokernel_cofork.condition t)
+
+end
+end category_theory

src/algebra/homology/homology.lean

@@ -103,7 +103,7 @@ 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, category_theory.image_to_kernel_map]
+by simp [image_to_kernel_map]
 
 @[reassoc]
 lemma image_to_kernel_map_comp_kernel_map [has_image_maps V]

src/algebra/homology/image_to_kernel_map.lean

@@ -34,33 +34,24 @@ 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] [has_equalizers V]
+variables [has_images V] [has_equalizers V] [has_kernels V]
 variables {A B C : V} (f : A ⟶ B) (g : B ⟶ C)
 
 /--
 The morphism from `image f` to `kernel g` when `f ≫ g = 0`.
 -/
-def image_to_kernel_map (w : f ≫ g = 0) :
+abbreviation image_to_kernel_map (w : f ≫ g = 0) :
   image f ⟶ kernel g :=
 kernel.lift g (image.ι f) $ (cancel_epi (factor_thru_image f)).1 $ by simp [w]
 
-instance image_to_kernel_map_mono {w : f ≫ g = 0} : mono (image_to_kernel_map f g w) :=
-begin
-  dsimp [image_to_kernel_map],
-  apply_instance,
-end
-
 @[simp]
 lemma image_to_kernel_map_zero_left [has_zero_object V] {w} :
   image_to_kernel_map (0 : A ⟶ B) g w = 0 :=
-by simp [image_to_kernel_map]
+by { delta image_to_kernel_map, simp }
 
 lemma image_to_kernel_map_zero_right {w} :
   image_to_kernel_map f (0 : B ⟶ C) w = image.ι f ≫ inv (kernel.ι (0 : B ⟶ C)) :=
-begin
-  ext,
-  simp [image_to_kernel_map],
-end
+by { ext, simp }
 
 local attribute [instance] has_zero_object.has_zero
 

src/category_theory/abelian/basic.lean

@@ -52,12 +52,12 @@ working with has natively.
 
 ## Implementation notes
 
-The typeclass `abelian` does not extend `non_preadditive_abelian`, 
-to avoid having to deal with comparing the two `has_zero_morphisms` instances 
-(one from `preadditive` in `abelian`, and the other a field of `non_preadditive_abelian`). 
-As a consequence, at the beginning of this file we trivially build 
-a `non_preadditive_abelian` instance from an `abelian` instance, 
-and use this to restate a number of theorems, 
+The typeclass `abelian` does not extend `non_preadditive_abelian`,
+to avoid having to deal with comparing the two `has_zero_morphisms` instances
+(one from `preadditive` in `abelian`, and the other a field of `non_preadditive_abelian`).
+As a consequence, at the beginning of this file we trivially build
+a `non_preadditive_abelian` instance from an `abelian` instance,
+and use this to restate a number of theorems,
 in each case just reusing the proof from `non_preadditive_abelian.lean`.
 
 We don't show this yet, but abelian categories are finitely complete and finitely cocomplete.
@@ -128,7 +128,8 @@ section to_non_preadditive_abelian
 
 local attribute [instance] has_finite_biproducts
 
-@[priority 100] instance non_preadditive_abelian : non_preadditive_abelian C := { ..‹abelian C› }
+/-- Every abelian category is, in particular, `non_preadditive_abelian`. -/
+def non_preadditive_abelian : non_preadditive_abelian C := { ..‹abelian C› }
 
 end to_non_preadditive_abelian
 
@@ -152,83 +153,92 @@ is_iso_of_mono_of_strong_epi _
 end mono_epi_iso
 
 section factor
+local attribute [instance] non_preadditive_abelian
 
 variables {P Q : C} (f : P ⟶ Q)
 
+namespace images
+
 /-- The kernel of the cokernel of `f` is called the image of `f`. -/
 protected abbreviation image : C := kernel (cokernel.π f)
 
 /-- The inclusion of the image into the codomain. -/
-protected abbreviation image.ι : abelian.image f ⟶ Q :=
+protected abbreviation image.ι : images.image f ⟶ Q :=
 kernel.ι (cokernel.π f)
 
 /-- There is a canonical epimorphism `p : P ⟶ image f` for every `f`. -/
-protected abbreviation factor_thru_image : P ⟶ abelian.image f :=
+protected abbreviation factor_thru_image : P ⟶ images.image f :=
 kernel.lift (cokernel.π f) f $ cokernel.condition f
 
 /-- `f` factors through its image via the canonical morphism `p`. -/
 @[simp, reassoc] protected lemma image.fac :
-  abelian.factor_thru_image f ≫ image.ι f = f :=
+  images.factor_thru_image f ≫ image.ι f = f :=
 kernel.lift_ι _ _ _
 
 /-- The map `p : P ⟶ image f` is an epimorphism -/
-instance : epi (abelian.factor_thru_image f) :=
+instance : epi (images.factor_thru_image f) :=
 show epi (non_preadditive_abelian.factor_thru_image f), by apply_instance
 
-instance mono_factor_thru_image [mono f] : mono (abelian.factor_thru_image f) :=
+instance mono_factor_thru_image [mono f] : mono (images.factor_thru_image f) :=
 mono_of_mono_fac $ image.fac f
 
-instance is_iso_factor_thru_image [mono f] : is_iso (abelian.factor_thru_image f) :=
+instance is_iso_factor_thru_image [mono f] : is_iso (images.factor_thru_image f) :=
 is_iso_of_mono_of_epi _
 
 /-- Factoring through the image is a strong epi-mono factorisation. -/
 @[simps] def image_strong_epi_mono_factorisation : strong_epi_mono_factorisation f :=
-{ I := abelian.image f,
+{ I := images.image f,
   m := image.ι f,
   m_mono := by apply_instance,
-  e := abelian.factor_thru_image f,
+  e := images.factor_thru_image f,
   e_strong_epi := strong_epi_of_epi _ }
 
+end images
+
+namespace coimages
+
 /-- The cokernel of the kernel of `f` is called the coimage of `f`. -/
 protected abbreviation coimage : C := cokernel (kernel.ι f)
 
 /-- The projection onto the coimage. -/
-protected abbreviation coimage.π : P ⟶ abelian.coimage f :=
+protected abbreviation coimage.π : P ⟶ coimages.coimage f :=
 cokernel.π (kernel.ι f)
 
 /-- There is a canonical monomorphism `i : coimage f ⟶ Q`. -/
-protected abbreviation factor_thru_coimage : abelian.coimage f ⟶ Q :=
+protected abbreviation factor_thru_coimage : coimages.coimage f ⟶ Q :=
 cokernel.desc (kernel.ι f) f $ kernel.condition f
 
 /-- `f` factors through its coimage via the canonical morphism `p`. -/
-protected lemma coimage.fac : coimage.π f ≫ abelian.factor_thru_coimage f = f :=
+protected lemma coimage.fac : coimage.π f ≫ coimages.factor_thru_coimage f = f :=
 cokernel.π_desc _ _ _
 
 /-- The canonical morphism `i : coimage f ⟶ Q` is a monomorphism -/
-instance : mono (abelian.factor_thru_coimage f) :=
+instance : mono (coimages.factor_thru_coimage f) :=
 show mono (non_preadditive_abelian.factor_thru_coimage f), by apply_instance
 
-instance epi_factor_thru_coimage [epi f] : epi (abelian.factor_thru_coimage f) :=
+instance epi_factor_thru_coimage [epi f] : epi (coimages.factor_thru_coimage f) :=
 epi_of_epi_fac $ coimage.fac f
 
-instance is_iso_factor_thru_coimage [epi f] : is_iso (abelian.factor_thru_coimage f) :=
+instance is_iso_factor_thru_coimage [epi f] : is_iso (coimages.factor_thru_coimage f) :=
 is_iso_of_mono_of_epi _
 
 /-- Factoring through the coimage is a strong epi-mono factorisation. -/
 @[simps] def coimage_strong_epi_mono_factorisation : strong_epi_mono_factorisation f :=
-{ I := abelian.coimage f,
-  m := abelian.factor_thru_coimage f,
+{ I := coimages.coimage f,
+  m := coimages.factor_thru_coimage f,
   m_mono := by apply_instance,
   e := coimage.π f,
   e_strong_epi := strong_epi_of_epi _ }
 
+end coimages
+
 end factor
 
 section has_strong_epi_mono_factorisations
 
 /-- An abelian category has strong epi-mono factorisations. -/
 @[priority 100] instance : has_strong_epi_mono_factorisations C :=
-⟨λ X Y f, image_strong_epi_mono_factorisation f⟩
+⟨λ X Y f, images.image_strong_epi_mono_factorisation f⟩
 
 /- In particular, this means that it has well-behaved images. -/
 example : has_images C := by apply_instance
@@ -239,22 +249,26 @@ end has_strong_epi_mono_factorisations
 section images
 variables {X Y : C} (f : X ⟶ Y)
 
-lemma image_eq_image : limits.image f = abelian.image f := rfl
+lemma image_eq_image : limits.image f = images.image f := rfl
 
 /-- There is a canonical isomorphism between the coimage and the image of a morphism. -/
-abbreviation coimage_iso_image : abelian.coimage f ≅ abelian.image f :=
-is_image.iso_ext (coimage_strong_epi_mono_factorisation f).to_mono_is_image
-  (image_strong_epi_mono_factorisation f).to_mono_is_image
+abbreviation coimage_iso_image : coimages.coimage f ≅ images.image f :=
+is_image.iso_ext (coimages.coimage_strong_epi_mono_factorisation f).to_mono_is_image
+  (images.image_strong_epi_mono_factorisation f).to_mono_is_image
 
-lemma full_image_factorisation : coimage.π f ≫ (coimage_iso_image f).hom ≫ image.ι f = f :=
-by rw [limits.is_image.iso_ext_hom, ←image_strong_epi_mono_factorisation_to_mono_factorisation_m,
-    is_image.lift_fac, coimage_strong_epi_mono_factorisation_to_mono_factorisation_m, coimage.fac]
+lemma full_image_factorisation : coimages.coimage.π f ≫ (coimage_iso_image f).hom ≫
+  images.image.ι f = f :=
+by rw [limits.is_image.iso_ext_hom,
+  ←images.image_strong_epi_mono_factorisation_to_mono_factorisation_m, is_image.lift_fac,
+  coimages.coimage_strong_epi_mono_factorisation_to_mono_factorisation_m, coimages.coimage.fac]
 
 end images
 
 section cokernel_of_kernel
 variables {X Y : C} {f : X ⟶ Y}
 
+local attribute [instance] non_preadditive_abelian
+
 /-- In an abelian category, an epi is the cokernel of its kernel. More precisely:
     If `f` is an epimorphism and `s` is some limit kernel cone on `f`, then `f` is a cokernel
     of `fork.ι s`. -/

src/category_theory/abelian/exact.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.abelian.basic
+import algebra.homology.exact
+
+/-!
+# Exact sequences in abelian categories
+
+We prove that in an abelian category, `(f, g)` is exact if and only if `f ≫ g = 0` and
+`kernel.ι g ≫ cokernel.π f = 0`.
+
+-/
+
+universes v u
+
+open category_theory
+open category_theory.limits
+open category_theory.preadditive
+
+variables {C : Type u} [category.{v} C] [abelian C]
+
+namespace category_theory.abelian
+variables {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
+
+local attribute [instance] has_equalizers_of_has_kernels
+
+theorem exact_iff : exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0 :=
+begin
+  split,
+  { introI h,
+    exact ⟨h.1, kernel_comp_cokernel f g⟩ },
+  { refine λ h, ⟨h.1, _⟩,
+    suffices hl :
+      is_limit (kernel_fork.of_ι (image.ι f) ((epi_iff_cancel_zero (factor_thru_image f)).1
+        (by apply_instance) _ (image.ι f ≫ g) (by simp [h.1]))),
+    { have : image_to_kernel_map f g h.1 =
+        (is_limit.cone_point_unique_up_to_iso hl (limit.is_limit _)).hom,
+      { ext, simp },
+      rw this,
+      apply_instance },
+    refine is_limit.of_ι _ _ _ _ _,
+    { refine λ W u hu, kernel.lift (cokernel.π f) u _,
+      rw [←kernel.lift_ι g u hu, category.assoc, h.2, has_zero_morphisms.comp_zero] },
+    { exact λ _ _ _, kernel.lift_ι _ _ _ },
+    { tidy } }
+end
+
+theorem exact_iff' {cg : kernel_fork g} (hg : is_limit cg)
+  {cf : cokernel_cofork f} (hf : is_colimit cf) : exact f g ↔ f ≫ g = 0 ∧ cg.ι ≫ cf.π = 0 :=
+begin
+  split,
+  { introI h,
+    exact ⟨h.1, fork_ι_comp_cofork_π f g cg cf⟩ },
+  { rw exact_iff,
+    refine λ h, ⟨h.1, _⟩,
+    apply zero_of_epi_comp (is_limit.cone_point_unique_up_to_iso hg (limit.is_limit _)).hom,
+    apply zero_of_comp_mono (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _) hf).hom,
+    simp [h.2] }
+end
+
+end category_theory.abelian