feat(CategoryTheory/Preadditive/AdditiveFunctor): finite products in a quotient preadditive category (#41067)

Prove that, if `F : C ⥤ D` is an additive essentially surjective functor between preadditive categories and `C` has finite products, then `D` also has finite products. Use this to shorten the proof that the localization of an abelian category by a Serre class has finite products (in `CategoryTheory/Abelian/SerreClass/Localization`).

Co-authored-by: morel <sophie.morel@ens-lyon.fr>

Author: smorel394

Mathlib/CategoryTheory/Abelian/SerreClass/Localization.lean

@@ -5,10 +5,9 @@ Authors: Joël Riou
 -/
 module
 
+public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 public import Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
 public import Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
-public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
-public import Mathlib.CategoryTheory.Limits.ExactFunctor
 
 /-!
 # Localization with respect to a Serre class
@@ -29,7 +28,7 @@ universe v'' v' v u'' u' u
 
 namespace CategoryTheory
 
-open Limits ZeroObject
+open Limits
 
 namespace ObjectProperty
 
@@ -139,9 +138,6 @@ lemma isZero_obj_iff (X : C) :
   rintro ⟨Y, h⟩
   simpa using h.2
 
-lemma hasZeroObject : HasZeroObject D :=
-  ⟨L.obj 0, by simpa [isZero_obj_iff L P] using P.prop_zero⟩
-
 lemma map_eq_zero_iff {X Y : C} (f : X ⟶ Y) :
     L.map f = 0 ↔ P (Abelian.image f) := by
   rw [← L.map_zero, MorphismProperty.map_eq_iff_precomp L P.isoModSerre]
@@ -381,17 +377,9 @@ lemma hasCoequalizers : HasCoequalizers D :=
     Preadditive.hasCoequalizer_of_hasCokernel _ _
   hasCoequalizers_of_hasColimit_parallelPair _
 
-lemma hasBinaryProducts : HasBinaryProducts D :=
-  have := Localization.essSurj L P.isoModSerre
-  have (X Y : D) : HasBinaryProduct X Y :=
-    hasLimit_of_iso (show Limits.pair _ _ ≅ _ from
-      mapPairIso (L.objObjPreimageIso X) (L.objObjPreimageIso Y))
-  hasBinaryProducts_of_hasLimit_pair D
-
 lemma hasFiniteProducts : HasFiniteProducts D :=
-  have := hasZeroObject L P
-  have := hasBinaryProducts L P
-  hasFiniteProducts_of_has_binary_and_terminal
+  have := Localization.essSurj L P.isoModSerre
+  L.hasFiniteProducts_of_additive_of_essSurj
 
 lemma isNormalMonoCategory : IsNormalMonoCategory D where
   normalMonoOfMono f hf := by
@@ -438,6 +426,10 @@ def abelian : Abelian D := by
   have := isNormalEpiCategory L P
   constructor
 
+lemma hasZeroObject : HasZeroObject D :=
+  have := abelian L P
+  Abelian.hasZeroObject
+
 lemma preservesFiniteLimits : PreservesFiniteLimits L := by
   letI := abelian L P
   rw [((Functor.preservesFiniteLimits_tfae L).out 3 2 :)]

Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

@@ -218,6 +218,12 @@ instance (priority := 100) preservesFiniteProductsOfAdditive [Additive F] :
     PreservesFiniteProducts F where
   preserves _ := preservesProductsOfShape_of_preservesBiproductsOfShape F
 
+lemma hasFiniteProducts_of_additive_of_essSurj [HasFiniteProducts C] [Additive F]
+    [EssSurj F] : HasFiniteProducts D :=
+  ⟨fun _ ↦ ⟨fun K ↦ hasLimit_of_iso
+    (F := Discrete.functor (fun i ↦ F.objPreimage (K.obj ⟨i⟩)) ⋙ F)
+      (Discrete.natIso (fun _ ↦ F.objObjPreimageIso _))⟩⟩
+
 theorem additive_of_preservesBinaryBiproducts [HasBinaryBiproducts C] [PreservesZeroMorphisms F]
     [PreservesBinaryBiproducts F] : Additive F where
   map_add {X Y f g} := by