feat(category_theory): functors preserving exactness are left and rig…

…ht exact (#15900)

This is the inverse statement to #14581.

src/category_theory/abelian/exact.lean

@@ -7,6 +7,7 @@ import category_theory.abelian.opposite
 import category_theory.limits.constructions.finite_products_of_binary_products
 import category_theory.limits.preserves.shapes.zero
 import category_theory.limits.preserves.shapes.kernels
+import category_theory.preadditive.left_exact
 import category_theory.adjunction.limits
 import algebra.homology.exact
 import tactic.tfae
@@ -28,8 +29,8 @@ true in more general settings.
   sequences.
 * `X ⟶ Y ⟶ Z ⟶ 0` is exact if and only if the second map is a cokernel of the first, and
   `0 ⟶ X ⟶ Y ⟶ Z` is exact if and only if the first map is a kernel of the second.
-* An exact functor preserves exactness, more specifically, if `F` preserves finite colimits and
-  limits, then `exact f g` implies `exact (F.map f) (F.map g)`
+* An exact functor preserves exactness, more specifically, `F` preserves finite colimits and
+  finite limits, if and only if `exact f g` implies `exact (F.map f) (F.map g)`.
 -/
 
 universes v₁ v₂ u₁ u₂
@@ -330,10 +331,16 @@ namespace functor
 open limits abelian
 
 variables {A : Type u₁} {B : Type u₂} [category.{v₁} A] [category.{v₂} B]
-variables [has_zero_object A] [has_zero_morphisms A] [has_images A] [has_equalizers A]
-variables [has_cokernels A] [abelian B]
-variables (L : A ⥤ B) [preserves_finite_limits L] [preserves_finite_colimits L]
+variables [abelian A] [abelian B]
+variables (L : A ⥤ B)
 
+section
+
+variables [preserves_finite_limits L] [preserves_finite_colimits L]
+
+/-- A functor preserving finite limits and finite colimits preserves exactness. The converse
+result is also true, see `functor.preserves_finite_limits_of_map_exact` and
+`functor.preserves_finite_colimits_of_map_exact`. -/
 lemma map_exact {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (e1 : exact f g) :
   exact (L.map f) (L.map g) :=
 begin
@@ -343,6 +350,93 @@ begin
   rw [fork.ι_of_ι, cofork.π_of_π, ← L.map_comp, kernel_comp_cokernel _ _ e1, L.map_zero]
 end
 
+end
+
+section
+
+variables (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, exact f g → exact (L.map f) (L.map g))
+include h
+
+open_locale zero_object
+
+/-- A functor which preserves exactness preserves zero morphisms. -/
+lemma preserves_zero_morphisms_of_map_exact : L.preserves_zero_morphisms :=
+begin
+  replace h := (h (exact_of_zero (𝟙 0) (𝟙 0))).w,
+  rw [L.map_id, category.comp_id] at h,
+  exact preserves_zero_morphisms_of_map_zero_object (id_zero_equiv_iso_zero _ h),
+end
+
+/-- A functor which preserves exactness preserves monomorphisms. -/
+lemma preserves_monomorphisms_of_map_exact : L.preserves_monomorphisms :=
+{ preserves := λ X Y f hf,
+  begin
+    letI := preserves_zero_morphisms_of_map_exact L h,
+    apply ((tfae_mono (L.obj 0) (L.map f)).out 2 0).mp,
+    rw ←L.map_zero,
+    exact h (((tfae_mono 0 f).out 0 2).mp hf)
+  end }
+
+/-- A functor which preserves exactness preserves epimorphisms. -/
+lemma preserves_epimorphisms_of_map_exact : L.preserves_epimorphisms :=
+{ preserves := λ X Y f hf,
+  begin
+    letI := preserves_zero_morphisms_of_map_exact L h,
+    apply ((tfae_epi (L.obj 0) (L.map f)).out 2 0).mp,
+    rw ←L.map_zero,
+    exact h (((tfae_epi 0 f).out 0 2).mp hf)
+  end }
+
+/-- A functor which preserves exactness preserves kernels. -/
+def preserves_kernels_of_map_exact (X Y : A) (f : X ⟶ Y) :
+  preserves_limit (parallel_pair f 0) L :=
+{ preserves := λ c ic,
+  begin
+    letI := preserves_zero_morphisms_of_map_exact L h,
+    letI := preserves_monomorphisms_of_map_exact L h,
+    letI := mono_of_is_limit_fork ic,
+    have hf := (is_limit_map_cone_fork_equiv' L (kernel_fork.condition c)).symm
+      (is_limit_of_exact_of_mono (L.map (fork.ι c)) (L.map f)
+        (h (exact_of_is_kernel (fork.ι c) f (kernel_fork.condition c)
+          (ic.of_iso_limit (iso_of_ι _))))),
+    exact hf.of_iso_limit ((cones.functoriality _ L).map_iso (iso_of_ι _).symm),
+  end }
+
+/-- A functor which preserves exactness preserves zero cokernels. -/
+def preserves_cokernels_of_map_exact (X Y : A) (f : X ⟶ Y) :
+  preserves_colimit (parallel_pair f 0) L :=
+{ preserves := λ c ic,
+  begin
+    letI := preserves_zero_morphisms_of_map_exact L h,
+    letI := preserves_epimorphisms_of_map_exact L h,
+    letI := epi_of_is_colimit_cofork ic,
+    have hf := (is_colimit_map_cocone_cofork_equiv' L (cokernel_cofork.condition c)).symm
+      (is_colimit_of_exact_of_epi (L.map f) (L.map (cofork.π c))
+        (h (exact_of_is_cokernel f (cofork.π c) (cokernel_cofork.condition c)
+          (ic.of_iso_colimit (iso_of_π _))))),
+    exact hf.of_iso_colimit ((cocones.functoriality _ L).map_iso (iso_of_π _).symm),
+  end }
+
+/-- A functor which preserves exactness is left exact, i.e. preserves finite limits.
+This is part of the inverse implication to `functor.map_exact`. -/
+def preserves_finite_limits_of_map_exact : limits.preserves_finite_limits L :=
+begin
+  letI := preserves_zero_morphisms_of_map_exact L h,
+  letI := preserves_kernels_of_map_exact L h,
+  apply preserves_finite_limits_of_preserves_kernels,
+end
+
+/-- A functor which preserves exactness is right exact, i.e. preserves finite colimits.
+This is part of the inverse implication to `functor.map_exact`. -/
+def preserves_finite_colimits_of_map_exact : limits.preserves_finite_colimits L :=
+begin
+  letI := preserves_zero_morphisms_of_map_exact L h,
+  letI := preserves_cokernels_of_map_exact L h,
+  apply preserves_finite_colimits_of_preserves_cokernels,
+end
+
+end
+
 end functor
 
 end category_theory