feat(category_theory/abelian/*): functors that preserve finite limits…

… and colimits preserve exactness (#14581)

If $F$ is a functor between two abelian categories which preserves limits and colimits, then it preserves exactness.

src/category_theory/abelian/basic.lean

@@ -8,6 +8,7 @@ import category_theory.limits.constructions.pullbacks
 import category_theory.limits.shapes.biproducts
 import category_theory.limits.shapes.images
 import category_theory.limits.constructions.limits_of_products_and_equalizers
+import category_theory.limits.constructions.epi_mono
 import category_theory.abelian.non_preadditive
 
 /-!

src/category_theory/abelian/exact.lean

@@ -28,7 +28,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)`
 -/
 
 universes v₁ v₂ u₁ u₂
@@ -324,4 +325,24 @@ end
 
 end functor
 
+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]
+
+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
+  let hcoker := is_colimit_of_has_cokernel_of_preserves_colimit L f,
+  let hker := is_limit_of_has_kernel_of_preserves_limit L g,
+  refine (exact_iff' _ _ hker hcoker).2 ⟨by simp [← L.map_comp, e1.1], _⟩,
+  rw [fork.ι_of_ι, cofork.π_of_π, ← L.map_comp, kernel_comp_cokernel _ _ e1, L.map_zero]
+end
+
+end functor
+
 end category_theory

src/category_theory/limits/preserves/shapes/images.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import category_theory.limits.shapes.images
+import category_theory.limits.constructions.epi_mono
+
+/-!
+# Preserving images
+
+In this file, we show that if a functor preserves span and cospan, then it preserves images.
+-/
+
+
+noncomputable theory
+
+namespace category_theory
+
+namespace preserves_image
+
+open category_theory
+open category_theory.limits
+
+universes u₁ u₂ v₁ v₂
+
+variables {A : Type u₁} {B : Type u₂} [category.{v₁} A] [category.{v₂} B]
+variables [has_equalizers A] [has_images A]
+variables [strong_epi_category B] [has_images B]
+variables (L : A ⥤ B)
+variables [Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), preserves_limit (cospan f g) L]
+variables [Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), preserves_colimit (span f g) L]
+
+/--
+If a functor preserves span and cospan, then it preserves images.
+-/
+@[simps] def iso {X Y : A} (f : X ⟶ Y) : image (L.map f) ≅ L.obj (image f) :=
+let aux1 : strong_epi_mono_factorisation (L.map f) :=
+{ I := L.obj (limits.image f),
+  m := L.map $ limits.image.ι _,
+  m_mono := preserves_mono_of_preserves_limit _ _,
+  e := L.map $ factor_thru_image _,
+  e_strong_epi := @@strong_epi_of_epi _ _ _ $ preserves_epi_of_preserves_colimit L _,
+  fac' := by rw [←L.map_comp, limits.image.fac] } in
+is_image.iso_ext (image.is_image (L.map f)) aux1.to_mono_is_image
+
+@[reassoc] lemma factor_thru_image_comp_hom {X Y : A} (f : X ⟶ Y) :
+  factor_thru_image (L.map f) ≫ (iso L f).hom =
+  L.map (factor_thru_image f) :=
+by simp
+
+@[reassoc] lemma hom_comp_map_image_ι {X Y : A} (f : X ⟶ Y) :
+  (iso L f).hom ≫ L.map (image.ι f) = image.ι (L.map f) :=
+by simp
+
+@[reassoc] lemma inv_comp_image_ι_map {X Y : A} (f : X ⟶ Y) :
+  (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f) :=
+by simp
+
+end preserves_image
+
+end category_theory

src/category_theory/limits/shapes/images.lean

@@ -289,6 +289,10 @@ lemma image.lift_fac (F' : mono_factorisation f) : image.lift F' ≫ F'.m = imag
 @[simp, reassoc]
 lemma image.fac_lift (F' : mono_factorisation f) : factor_thru_image f ≫ image.lift F' = F'.e :=
 (image.is_image f).fac_lift F'
+@[simp]
+lemma image.is_image_lift (F : mono_factorisation f) :
+  (image.is_image f).lift F = image.lift F :=
+rfl
 
 @[simp, reassoc]
 lemma is_image.lift_ι {F : mono_factorisation f} (hF : is_image F) :