From e112ddd0b71f14b6fed31b482f72499079471859 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 11 Mar 2023 13:48:29 +0000
Subject: [PATCH] feat: port CategoryTheory.Preadditive.AdditiveFunctor (#2779)

---
 Mathlib.lean                                  |   1 +
 .../Preadditive/AdditiveFunctor.lean          | 333 ++++++++++++++++++
 2 files changed, 334 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 83ed586fe9c10..0034b165add0a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -375,6 +375,7 @@ import Mathlib.CategoryTheory.PEmpty
 import Mathlib.CategoryTheory.PUnit
 import Mathlib.CategoryTheory.PathCategory
 import Mathlib.CategoryTheory.Pi.Basic
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 import Mathlib.CategoryTheory.Preadditive.Basic
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 import Mathlib.CategoryTheory.Preadditive.FunctorCategory
diff --git a/Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean b/Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
new file mode 100644
index 0000000000000..43b2d4e8560be
--- /dev/null
+++ b/Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
@@ -0,0 +1,333 @@
+/-
+Copyright (c) 2021 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz, Scott Morrison
+
+! This file was ported from Lean 3 source module category_theory.preadditive.additive_functor
+! leanprover-community/mathlib commit ee89acdf96a0b45afe3eea493bceb2a80a0f2efa
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Limits.ExactFunctor
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
+import Mathlib.CategoryTheory.Preadditive.Biproducts
+import Mathlib.CategoryTheory.Preadditive.FunctorCategory
+
+/-!
+# Additive Functors
+
+A functor between two preadditive categories is called *additive*
+provided that the induced map on hom types is a morphism of abelian
+groups.
+
+An additive functor between preadditive categories creates and preserves biproducts.
+Conversely, if `F : C ⥤ D` is a functor between preadditive categories, where `C` has binary
+biproducts, and if `F` preserves binary biproducts, then `F` is additive.
+
+We also define the category of bundled additive functors.
+
+# Implementation details
+
+`Functor.Additive` is a `Prop`-valued class, defined by saying that for every two objects `X` and
+`Y`, the map `F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)` is a morphism of abelian groups.
+
+-/
+
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+/-- A functor `F` is additive provided `F.map` is an additive homomorphism. -/
+class Functor.Additive {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]
+  (F : C ⥤ D) : Prop where
+  /-- the addition of two morphisms is mapped to the sum of their images -/
+  map_add : ∀ {X Y : C} {f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g := by aesop_cat
+#align category_theory.functor.additive CategoryTheory.Functor.Additive
+
+section Preadditive
+
+namespace Functor
+
+section
+
+variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D] (F : C ⥤ D)
+  [Functor.Additive F]
+
+@[simp]
+theorem map_add {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g :=
+  Functor.Additive.map_add
+#align category_theory.functor.map_add CategoryTheory.Functor.map_add
+
+-- porting note: it was originally @[simps (config := { fullyApplied := false })]
+/-- `F.map_add_hom` is an additive homomorphism whose underlying function is `F.map`. -/
+@[simps!]
+def mapAddHom {X Y : C} : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y) :=
+  AddMonoidHom.mk' (fun f => F.map f) fun _ _ => F.map_add
+#align category_theory.functor.map_add_hom CategoryTheory.Functor.mapAddHom
+
+theorem coe_mapAddHom {X Y : C} : ⇑(F.mapAddHom : (X ⟶ Y) →+ _) = F.map :=
+  rfl
+#align category_theory.functor.coe_map_add_hom CategoryTheory.Functor.coe_mapAddHom
+
+instance (priority := 100) preservesZeroMorphisms_of_additive : PreservesZeroMorphisms F
+    where map_zero _ _ := F.mapAddHom.map_zero
+#align category_theory.functor.preserves_zero_morphisms_of_additive CategoryTheory.Functor.preservesZeroMorphisms_of_additive
+
+instance : Additive (𝟭 C) where
+
+instance {E : Type _} [Category E] [Preadditive E] (G : D ⥤ E) [Functor.Additive G] :
+    Additive (F ⋙ G) where
+
+@[simp]
+theorem map_neg {X Y : C} {f : X ⟶ Y} : F.map (-f) = -F.map f :=
+  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_neg _
+#align category_theory.functor.map_neg CategoryTheory.Functor.map_neg
+
+@[simp]
+theorem map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=
+  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_sub _ _
+#align category_theory.functor.map_sub CategoryTheory.Functor.map_sub
+
+theorem map_nsmul {X Y : C} {f : X ⟶ Y} {n : ℕ} : F.map (n • f) = n • F.map f :=
+  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_nsmul _ _
+#align category_theory.functor.map_nsmul CategoryTheory.Functor.map_nsmul
+
+-- You can alternatively just use `Functor.map_smul` here, with an explicit `(r : ℤ)` argument.
+theorem map_zsmul {X Y : C} {f : X ⟶ Y} {r : ℤ} : F.map (r • f) = r • F.map f :=
+  (F.mapAddHom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_zsmul _ _
+#align category_theory.functor.map_zsmul CategoryTheory.Functor.map_zsmul
+
+open BigOperators
+
+@[simp]
+theorem map_sum {X Y : C} {α : Type _} (f : α → (X ⟶ Y)) (s : Finset α) :
+    F.map (∑ a in s, f a) = ∑ a in s, F.map (f a) :=
+  (F.mapAddHom : (X ⟶ Y) →+ _).map_sum f s
+#align category_theory.functor.map_sum CategoryTheory.Functor.map_sum
+
+end
+
+section InducedCategory
+
+variable {C : Type _} {D : Type _} [Category D] [Preadditive D] (F : C → D)
+
+instance inducedFunctor_additive : Functor.Additive (inducedFunctor F) where
+#align category_theory.functor.induced_functor_additive CategoryTheory.Functor.inducedFunctor_additive
+
+end InducedCategory
+
+instance fullSubcategoryInclusion_additive {C : Type _} [Category C] [Preadditive C]
+    (Z : C → Prop) : (fullSubcategoryInclusion Z).Additive where
+#align category_theory.functor.full_subcategory_inclusion_additive CategoryTheory.Functor.fullSubcategoryInclusion_additive
+
+section
+
+-- To talk about preservation of biproducts we need to specify universes explicitly.
+noncomputable section
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] [Preadditive C]
+  [Preadditive D] (F : C ⥤ D)
+
+open CategoryTheory.Limits
+
+open CategoryTheory.Preadditive
+
+instance (priority := 100) preservesFiniteBiproductsOfAdditive [Additive F] :
+    PreservesFiniteBiproducts F where
+  preserves :=
+    { preserves :=
+      { preserves := fun hb =>
+          isBilimitOfTotal _ (by
+            simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]
+            erw [← F.map_sum, ← F.map_id, IsBilimit.total hb])} }
+#align category_theory.functor.preserves_finite_biproducts_of_additive CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive
+
+theorem additive_of_preservesBinaryBiproducts [HasBinaryBiproducts C] [PreservesZeroMorphisms F]
+    [PreservesBinaryBiproducts F] : Additive F where
+  map_add {X Y f g} := by
+    rw [biprod.add_eq_lift_id_desc,  F.map_comp, ← biprod.lift_mapBiprod,
+      ←  biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
+      biprod.add_eq_lift_id_desc]
+#align category_theory.functor.additive_of_preserves_binary_biproducts CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
+
+end
+
+end
+
+end Functor
+
+namespace Equivalence
+
+variable {C D : Type _} [Category C] [Category D] [Preadditive C] [Preadditive D]
+
+instance inverse_additive (e : C ≌ D) [e.functor.Additive] : e.inverse.Additive where
+  map_add {f g} := e.functor.map_injective (by simp)
+#align category_theory.equivalence.inverse_additive CategoryTheory.Equivalence.inverse_additive
+
+end Equivalence
+
+section
+
+variable (C D : Type _) [Category C] [Category D] [Preadditive C] [Preadditive D]
+
+-- porting note: removed @[nolint has_nonempty_instance]
+/-- Bundled additive functors. -/
+def AdditiveFunctor :=
+  FullSubcategory fun F : C ⥤ D => F.Additive
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor CategoryTheory.AdditiveFunctor
+
+instance : Category (AdditiveFunctor C D) :=
+  FullSubcategory.category _
+
+/-- the category of additive functors is denoted `C ⥤+ D` -/
+infixr:26 " ⥤+ " => AdditiveFunctor
+
+instance : Preadditive (C ⥤+ D) :=
+  Preadditive.inducedCategory _
+
+/-- An additive functor is in particular a functor. -/
+def AdditiveFunctor.forget : (C ⥤+ D) ⥤ C ⥤ D :=
+  fullSubcategoryInclusion _
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.forget CategoryTheory.AdditiveFunctor.forget
+
+instance : Full (AdditiveFunctor.forget C D) :=
+  FullSubcategory.full _
+
+variable {C D}
+
+/-- Turn an additive functor into an object of the category `AdditiveFunctor C D`. -/
+def AdditiveFunctor.of (F : C ⥤ D) [F.Additive] : C ⥤+ D :=
+  ⟨F, inferInstance⟩
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of CategoryTheory.AdditiveFunctor.of
+
+@[simp]
+theorem AdditiveFunctor.of_fst (F : C ⥤ D) [F.Additive] : (AdditiveFunctor.of F).1 = F :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_fst CategoryTheory.AdditiveFunctor.of_fst
+
+@[simp]
+theorem AdditiveFunctor.forget_obj (F : C ⥤+ D) : (AdditiveFunctor.forget C D).obj F = F.1 :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.forget_obj CategoryTheory.AdditiveFunctor.forget_obj
+
+theorem AdditiveFunctor.forget_obj_of (F : C ⥤ D) [F.Additive] :
+    (AdditiveFunctor.forget C D).obj (AdditiveFunctor.of F) = F :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.forget_obj_of CategoryTheory.AdditiveFunctor.forget_obj_of
+
+@[simp]
+theorem AdditiveFunctor.forget_map (F G : C ⥤+ D) (α : F ⟶ G) :
+    (AdditiveFunctor.forget C D).map α = α :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.forget_map CategoryTheory.AdditiveFunctor.forget_map
+
+instance : Functor.Additive (AdditiveFunctor.forget C D) where map_add := rfl
+
+instance (F : C ⥤+ D) : Functor.Additive F.1 :=
+  F.2
+
+end
+
+section Exact
+
+open CategoryTheory.Limits
+
+variable (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Category.{v₂} D] [Preadditive C]
+
+variable [Preadditive D] [HasZeroObject C] [HasZeroObject D] [HasBinaryBiproducts C]
+
+section
+
+attribute [local instance] preservesBinaryBiproductsOfPreservesBinaryProducts
+
+attribute [local instance] preservesBinaryBiproductsOfPreservesBinaryCoproducts
+
+/-- Turn a left exact functor into an additive functor. -/
+def AdditiveFunctor.ofLeftExact : (C ⥤ₗ D) ⥤ C ⥤+ D :=
+  FullSubcategory.map fun F ⟨_⟩ =>
+    Functor.additive_of_preservesBinaryBiproducts F
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_left_exact CategoryTheory.AdditiveFunctor.ofLeftExact
+
+instance : Full (AdditiveFunctor.ofLeftExact C D) := FullSubcategory.full_map _
+instance : Faithful (AdditiveFunctor.ofLeftExact C D) := FullSubcategory.faithful_map _
+
+/-- Turn a right exact functor into an additive functor. -/
+def AdditiveFunctor.ofRightExact : (C ⥤ᵣ D) ⥤ C ⥤+ D :=
+  FullSubcategory.map fun F ⟨_⟩ =>
+    Functor.additive_of_preservesBinaryBiproducts F
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_right_exact CategoryTheory.AdditiveFunctor.ofRightExact
+
+instance : Full (AdditiveFunctor.ofRightExact C D) := FullSubcategory.full_map _
+instance : Faithful (AdditiveFunctor.ofRightExact C D) := FullSubcategory.faithful_map _
+
+/-- Turn an exact functor into an additive functor. -/
+def AdditiveFunctor.ofExact : (C ⥤ₑ D) ⥤ C ⥤+ D :=
+  FullSubcategory.map fun F ⟨⟨_⟩, _⟩ =>
+    Functor.additive_of_preservesBinaryBiproducts F
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_exact CategoryTheory.AdditiveFunctor.ofExact
+
+instance : Full (AdditiveFunctor.ofExact C D) := FullSubcategory.full_map _
+instance : Faithful (AdditiveFunctor.ofExact C D) := FullSubcategory.faithful_map _
+
+end
+
+variable {C D}
+
+@[simp]
+theorem AdditiveFunctor.ofLeftExact_obj_fst (F : C ⥤ₗ D) :
+    ((AdditiveFunctor.ofLeftExact C D).obj F).obj = F.obj :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_left_exact_obj_fst CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst
+
+@[simp]
+theorem AdditiveFunctor.ofRightExact_obj_fst (F : C ⥤ᵣ D) :
+    ((AdditiveFunctor.ofRightExact C D).obj F).obj = F.obj :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_right_exact_obj_fst CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst
+
+@[simp]
+theorem AdditiveFunctor.ofExact_obj_fst (F : C ⥤ₑ D) :
+    ((AdditiveFunctor.ofExact C D).obj F).obj = F.obj :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.AdditiveFunctor.of_exact_obj_fst CategoryTheory.AdditiveFunctor.ofExact_obj_fst
+
+@[simp]
+theorem AdditiveFunctor.ofLeftExact_map {F G : C ⥤ₗ D} (α : F ⟶ G) :
+    (AdditiveFunctor.ofLeftExact C D).map α = α :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.Additive_Functor.of_left_exact_map CategoryTheory.AdditiveFunctor.ofLeftExact_map
+
+@[simp]
+theorem AdditiveFunctor.ofRightExact_map {F G : C ⥤ᵣ D} (α : F ⟶ G) :
+    (AdditiveFunctor.ofRightExact C D).map α = α :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.Additive_Functor.of_right_exact_map CategoryTheory.AdditiveFunctor.ofRightExact_map
+
+@[simp]
+theorem AdditiveFunctor.ofExact_map {F G : C ⥤ₑ D} (α : F ⟶ G) :
+    (AdditiveFunctor.ofExact C D).map α = α :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align category_theory.Additive_Functor.of_exact_map CategoryTheory.AdditiveFunctor.ofExact_map
+
+end Exact
+
+end Preadditive
+
+end CategoryTheory