feat(algebra/homology/exact): lemmas about exactness (#4106)

These are a few lemmas on the way to showing how `exact` changes under isomorphisms applied to the objects. It's not everthing one might want; I'm salvaging this from an old branch and unlikely to do more in the near future, but hopefully this is mergeable progress as is.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/homology/exact.lean

@@ -11,6 +11,11 @@ import algebra.homology.image_to_kernel_map
 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.
 
+(We say epimorphism rather than isomorphism because, at least for preadditive categories,
+this is exactly equivalent to the homology at `i` vanishing.
+In an abelian category, this is the same as asking for it to be an isomorphism,
+because the inclusion map is always a monomorphism.)
+
 # 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`.
@@ -43,6 +48,20 @@ class exact {A B C : V} (f : A ⟶ B) (g : B ⟶ C) : Prop :=
 
 attribute [instance] exact.epi
 
+lemma exact.w_assoc {A B C D : V} {f : A ⟶ B} {g : B ⟶ C} [exact f g] {h : C ⟶ D} :
+  f ≫ g ≫ h = 0 :=
+by rw [←category.assoc, @exact.w _ _ _ _ _ _ _ _ _ f g, has_zero_morphisms.zero_comp]
+
+instance exact_comp_iso {A B C C' : V} (f : A ⟶ B) (g : B ⟶ C) (h : C ≅ C') [exact f g] :
+  exact f (g ≫ h.hom) :=
+{ w := exact.w_assoc,
+  epi := by { simp only [image_to_kernel_map_comp_iso], apply epi_comp, } }
+
+instance exact_iso_comp {A A' B C : V} (h : A' ≅ A) (f : A ⟶ B) (g : B ⟶ C) [exact f g] :
+  exact (h.hom ≫ f) g :=
+{ w := by rw [category.assoc, @exact.w _ _ _ _ _ _ _ _ _ f g, has_zero_morphisms.comp_zero],
+  epi := by { simp only [image_to_kernel_map_iso_comp], apply epi_comp, } }
+
 section
 variables [has_cokernels V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C)
 
@@ -60,4 +79,19 @@ by rw [←kernel.lift_ι _ _ hι, ←cokernel.π_desc _ _ hπ, category.assoc, k
 comp_eq_zero_of_exact f g (kernel_fork.condition s) (cokernel_cofork.condition t)
 
 end
+
+section
+local attribute [instance] has_zero_object.has_zero
+
+lemma exact_of_zero [has_zero_object V] {A C : V} (f : A ⟶ 0) (g : 0 ⟶ C) : exact f g :=
+begin
+  obtain rfl : f = 0 := by ext,
+  obtain rfl : g = 0 := by ext,
+  fsplit,
+  { simp, },
+  { exact image_to_kernel_map_epi_of_zero_of_mono 0, },
+end
+
+end
+
 end category_theory

src/algebra/homology/image_to_kernel_map.lean

@@ -53,6 +53,20 @@ lemma image_to_kernel_map_zero_right {w} :
   image_to_kernel_map f (0 : B ⟶ C) w = image.ι f ≫ inv (kernel.ι (0 : B ⟶ C)) :=
 by { ext, simp }
 
+@[simp]
+lemma image_to_kernel_map_comp_iso {D : V} (h : C ⟶ D) [is_iso h] (w) :
+  image_to_kernel_map f (g ≫ h) w =
+  image_to_kernel_map f g ((cancel_mono h).mp (by simpa using w : (f ≫ g) ≫ h = 0 ≫ h)) ≫
+    (kernel_comp_is_iso g h).inv :=
+by { ext, simp, }
+
+@[simp]
+lemma image_to_kernel_map_iso_comp {Z : V} (h : Z ⟶ A) [is_iso h] (w) :
+  image_to_kernel_map (h ≫ f) g w =
+  image.pre_comp h f ≫
+    image_to_kernel_map f g ((cancel_epi h).mp (by simpa using w : h ≫ f ≫ g = h ≫ 0)) :=
+by { ext, simp, }
+
 local attribute [instance] has_zero_object.has_zero
 
 /--

src/category_theory/limits/shapes/images.lean

@@ -317,6 +317,11 @@ image.lift
   m := image.ι g,
   e := f ≫ factor_thru_image g }
 
+@[simp, reassoc]
+lemma image.factor_thru_image_pre_comp [has_image g] [has_image (f ≫ g)] :
+  factor_thru_image (f ≫ g) ≫ image.pre_comp f g = f ≫ factor_thru_image g :=
+by simp [image.pre_comp]
+
 /--
 The two step comparison map
   `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h`
@@ -333,6 +338,21 @@ begin
   simp [image.pre_comp, image.eq_to_hom],
 end
 
+variables [has_equalizers C]
+
+/--
+`image.pre_comp f g` is an isomorphism when `f` is an isomorphism
+(we need `C` to have equalizers to prove this).
+-/
+instance image.is_iso_precomp_iso (f : X ≅ Y) [has_image g] [has_image (f.hom ≫ g)] :
+  is_iso (image.pre_comp f.hom g) :=
+{ inv := image.lift
+  { I := image (f.hom ≫ g),
+    m := image.ι (f.hom ≫ g),
+    e := f.inv ≫ factor_thru_image (f.hom ≫ g) },
+  hom_inv_id' := by { ext, simp [image.pre_comp], },
+  inv_hom_id' := by { ext, simp [image.pre_comp], }, }
+
 -- Note that in general we don't have the other comparison map you might expect
 -- `image f ⟶ image (f ≫ g)`.
 

src/category_theory/limits/shapes/kernels.lean

@@ -143,6 +143,8 @@ abbreviation kernel : C := equalizer f 0
 /-- The map from `kernel f` into the source of `f`. -/
 abbreviation kernel.ι : kernel f ⟶ X := equalizer.ι f 0
 
+@[simp] lemma equalizer_as_kernel : equalizer.ι f 0 = kernel.ι f := rfl
+
 @[simp, reassoc] lemma kernel.condition : kernel.ι f ≫ f = 0 :=
 kernel_fork.condition _
 
@@ -216,42 +218,44 @@ lemma kernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (kernel.ι f)) → false
 /--
 When `g` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.
 -/
-@[simps]
 def kernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] :
   kernel (f ≫ g) ≅ kernel f :=
 { hom := kernel.lift _ (kernel.ι _) (by { rw [←cancel_mono g], simp, }),
   inv := kernel.lift _ (kernel.ι _) (by simp), }
 
+@[simp]
 lemma kernel_comp_is_iso_hom_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] :
   (kernel_comp_is_iso f g).hom ≫ kernel.ι f = kernel.ι (f ≫ g) :=
-by simp
+by simp [kernel_comp_is_iso]
 
+@[simp]
 lemma kernel_comp_is_iso_inv_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [has_kernel f] [is_iso g] :
   (kernel_comp_is_iso f g).inv ≫ kernel.ι (f ≫ g) = kernel.ι f :=
-by simp
+by simp [kernel_comp_is_iso]
 
 /--
 When `f` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `g`.
 -/
-@[simps]
 def kernel_is_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] :
   kernel (f ≫ g) ≅ kernel g :=
 { hom := kernel.lift _ (kernel.ι _ ≫ f) (by simp),
   inv := kernel.lift _ (kernel.ι _ ≫ inv f) (by simp), }
 
+@[simp]
 lemma kernel_is_iso_comp_hom_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] :
   (kernel_is_iso_comp f g).hom ≫ kernel.ι g = kernel.ι (f ≫ g) ≫ f :=
-by simp
+by simp [kernel_is_iso_comp]
 
+@[simp]
 lemma kernel_is_iso_comp_inv_comp_kernel_ι {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_kernel (f ≫ g)] [is_iso f] [has_kernel g] :
   (kernel_is_iso_comp f g).inv ≫ kernel.ι (f ≫ g) = kernel.ι g ≫ (inv f) :=
-by simp
+by simp [kernel_is_iso_comp]
 
 end
 
@@ -396,6 +400,8 @@ abbreviation cokernel : C := coequalizer f 0
 /-- The map from the target of `f` to `cokernel f`. -/
 abbreviation cokernel.π : Y ⟶ cokernel f := coequalizer.π f 0
 
+@[simp] lemma coequalizer_as_cokernel : coequalizer.π f 0 = cokernel.π f := rfl
+
 @[simp, reassoc] lemma cokernel.condition : f ≫ cokernel.π f = 0 :=
 cokernel_cofork.condition _
 
@@ -471,43 +477,44 @@ lemma cokernel_not_iso_of_nonzero (w : f ≠ 0) : (is_iso (cokernel.π f)) → f
 /--
 When `g` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `f`.
 -/
-@[simps]
 def cokernel_comp_is_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] :
   cokernel (f ≫ g) ≅ cokernel f :=
 { hom := cokernel.desc _ (inv g ≫ cokernel.π f) (by simp),
   inv := cokernel.desc _ (g ≫ cokernel.π (f ≫ g)) (by rw [←category.assoc, cokernel.condition]), }
 
+@[simp]
 lemma cokernel_π_comp_cokernel_comp_is_iso_hom {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] :
   cokernel.π (f ≫ g) ≫ (cokernel_comp_is_iso f g).hom = inv g ≫ cokernel.π f :=
-by simp
+by simp [cokernel_comp_is_iso]
 
+@[simp]
 lemma cokernel_π_comp_cokernel_comp_is_iso_inv {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [has_cokernel f] [is_iso g] :
   cokernel.π f ≫ (cokernel_comp_is_iso f g).inv = g ≫ cokernel.π (f ≫ g) :=
-by simp
+by simp [cokernel_comp_is_iso]
 
 /--
 When `f` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.
 -/
-@[simps]
 def cokernel_is_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] :
   cokernel (f ≫ g) ≅ cokernel g :=
 { hom := cokernel.desc _ (cokernel.π g) (by simp),
   inv := cokernel.desc _ (cokernel.π (f ≫ g)) (by { rw [←cancel_epi f, ←category.assoc], simp, }), }
 
-
+@[simp]
 lemma cokernel_π_comp_cokernel_is_iso_comp_hom {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] :
   cokernel.π (f ≫ g) ≫ (cokernel_is_iso_comp f g).hom = cokernel.π g :=
-by simp
+by simp [cokernel_is_iso_comp]
 
+@[simp]
 lemma cokernel_π_comp_cokernel_is_iso_comp_inv {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
   [has_cokernel (f ≫ g)] [is_iso f] [has_cokernel g] :
   cokernel.π g ≫ (cokernel_is_iso_comp f g).inv = cokernel.π (f ≫ g) :=
-by simp
+by simp [cokernel_is_iso_comp]
 
 end