From f4039f4f1f1e363a778031614c57722e037e4a08 Mon Sep 17 00:00:00 2001
From: Paul Reichert <preichert@noreply.codeberg.org>
Date: Fri, 1 Nov 2024 10:47:24 +0100
Subject: [PATCH 01/46] working state

---
 .../Abelian/GrothendieckAxioms.lean           | 39 ++++++++++++++++---
 .../Adjunction/AdjointFunctorTheorems.lean    | 12 ++++++
 2 files changed, 46 insertions(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 84eda8c006ac29..10ce033f959c05 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -7,6 +7,13 @@ Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
+import Mathlib.CategoryTheory.Limits.Final
+import Mathlib.CategoryTheory.Limits.FinallySmall
+import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
+import Mathlib.CategoryTheory.Abelian.Subobject
+import Mathlib.CategoryTheory.Subobject.WellPowered
+import Mathlib.CategoryTheory.Abelian.Opposite
 
 /-!
 
@@ -20,10 +27,15 @@ basic facts about them.
 - `AB4` -- an abelian category satisfies `AB4` provided that coproducts are exact.
 - `AB5` -- an abelian category satisfies `AB5` provided that filtered colimits are exact.
 - The duals of the above definitions, called `AB4Star` and `AB5Star`.
+- `GrothendieckCategory` -- an abelian category satisfies `GrothendieckCategory` provided that
+it has `AB5` and a separator.
 
 ## Theorems
 
 - The implication from `AB5` to `AB4` is established in `AB4.ofAB5`.
+- Relevant implications of `GrothendieckCategory` are established in
+`GrothendieckCategory.wellPowered`, `GrothendieckCategory.hasLimits` and
+`GrothendieckCategory.hasColimits`.
 
 ## Remarks
 
@@ -33,10 +45,9 @@ comments of the linked Stacks page.
 Exactness as the preservation of short exact sequences is introduced in
 `CategoryTheory.Abelian.Exact`.
 
-## Projects
-
-- Add additional axioms, especially define Grothendieck categories.
-- Prove that `AB5` implies `AB4`.
+We do not require `Abelian` in the definition of `AB4` and `AB5` because these classes represent
+individual axioms. A non-abelian category with `AB5` is not an AB5 category in the sense of the
+literature.
 
 ## References
 * [Stacks: Grothendieck's AB conditions](https://stacks.math.columbia.edu/tag/079A)
@@ -97,6 +108,24 @@ class AB5Star [HasCofilteredLimits C] where
 
 attribute [instance] AB5Star.preservesFiniteColimits
 
+section GrothendieckCategory
+
+/--
+An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
+separator (see `HasSeparator`).
+-/
+class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
+
+variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [h : GrothendieckCategory C]
+
+instance GrothendieckCategory.wellPowered : WellPowered C := HasSeparator.wellPowered
+
+instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
+
+instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
+
+end GrothendieckCategory
+
 noncomputable section
 
 open CoproductsFromFiniteFiltered
@@ -117,7 +146,7 @@ instance preservesFiniteLimitsLiftToFinset : PreservesFiniteLimits (liftToFinset
     preservesFiniteLimitsOfNatIso (liftToFinsetEvaluationIso  I).symm
 
 /-- A category with finite biproducts and finite limits is AB4 if it is AB5. -/
-def AB4.ofAB5 [HasFiniteCoproducts C] [HasFilteredColimits C] [AB5 C] : AB4 C where
+def AB4.ofAB5 [HasFilteredColimits C] [AB5 C] : AB4 C where
   preservesFiniteLimits J :=
     letI : PreservesFiniteLimits (liftToFinset C J ⋙ colim) :=
       compPreservesFiniteLimits _ _
diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
index 6d42354bbaaa34..77dacdde43b108 100644
--- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
+++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -135,6 +135,18 @@ theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered C
       hasLimitsOfShape_iff_isLeftAdjoint_const.2
         (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) }
 
+theorem hasLimits_of_hasColimits_of_hasSeparator [HasColimits C] [HasSeparator C]
+    [WellPowered Cᵒᵖ] : HasLimits C := by
+  obtain ⟨G, hG⟩ : HasSeparator C := inferInstance
+  exact hasLimits_of_hasColimits_of_isSeparating hG
+
+theorem hasColimits_of_hasLimits_of_hasCoseparator [HasLimits C] [HasCoseparator C]
+    [WellPowered C] : HasColimits C := by
+  suffices HasLimits Cᵒᵖ from hasColimits_of_hasLimits_op
+  have : WellPowered Cᵒᵖᵒᵖ := wellPowered_of_equiv (opOpEquivalence C).symm
+  have : HasSeparator Cᵒᵖ := HasCoseparator.hasSeparator_op
+  exact hasLimits_of_hasColimits_of_hasSeparator
+
 end Limits
 
 end CategoryTheory

From cb6065b92e496b8962fec4e2bd7a0b96cc25bbbb Mon Sep 17 00:00:00 2001
From: Paul Reichert <preichert@noreply.codeberg.org>
Date: Fri, 1 Nov 2024 11:07:32 +0100
Subject: [PATCH 02/46] organize imports

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 10ce033f959c05..dbeead6f89472d 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -4,16 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
 -/
 
+import Mathlib.CategoryTheory.Abelian.Subobject
+import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
-import Mathlib.CategoryTheory.Limits.Final
-import Mathlib.CategoryTheory.Limits.FinallySmall
-import Mathlib.CategoryTheory.Generator
-import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
-import Mathlib.CategoryTheory.Abelian.Subobject
-import Mathlib.CategoryTheory.Subobject.WellPowered
-import Mathlib.CategoryTheory.Abelian.Opposite
 
 /-!
 

From 7a12b7b2f2de38e6bc1287205f4783a67deba33f Mon Sep 17 00:00:00 2001
From: Paul Reichert <preichert@noreply.codeberg.org>
Date: Fri, 1 Nov 2024 11:28:19 +0100
Subject: [PATCH 03/46] add documentation

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean |  2 +-
 .../Adjunction/AdjointFunctorTheorems.lean             | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index dbeead6f89472d..098e99e017391d 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -111,7 +111,7 @@ separator (see `HasSeparator`).
 -/
 class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
 
-variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [h : GrothendieckCategory C]
+variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]
 
 instance GrothendieckCategory.wellPowered : WellPowered C := HasSeparator.wellPowered
 
diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
index 77dacdde43b108..ba1a361373a47b 100644
--- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
+++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -29,9 +29,11 @@ This file also proves the special adjoint functor theorem, in the form:
 * If `G : D ⥤ C` preserves limits and `D` is complete, well-powered and has a small coseparating
   set, then `G` has a left adjoint: `isRightAdjointOfPreservesLimitsOfIsCoseparating`
 
-Finally, we prove the following corollary of the special adjoint functor theorem:
+Finally, we prove the following corollaries of the special adjoint functor theorem:
 * If `C` is complete, well-powered and has a small coseparating set, then it is cocomplete:
-  `hasColimits_of_hasLimits_of_isCoseparating`
+  `hasColimits_of_hasLimits_of_isCoseparating`, `hasColimits_of_hasLimits_of_hasCoseparator`
+* If `C` is cocomplete, co-well-powered and has a small separating set, then it is complete:
+  `hasLimits_of_hasColimits_of_isSeparating`, `hasLimits_of_hasColimits_of_hasSeparator`
 
 -/
 
@@ -135,11 +137,15 @@ theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered C
       hasLimitsOfShape_iff_isLeftAdjoint_const.2
         (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) }
 
+/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
+    has a separator, then it is complete. -/
 theorem hasLimits_of_hasColimits_of_hasSeparator [HasColimits C] [HasSeparator C]
     [WellPowered Cᵒᵖ] : HasLimits C := by
   obtain ⟨G, hG⟩ : HasSeparator C := inferInstance
   exact hasLimits_of_hasColimits_of_isSeparating hG
 
+/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
+    has a coseparator, then it is cocomplete. -/
 theorem hasColimits_of_hasLimits_of_hasCoseparator [HasLimits C] [HasCoseparator C]
     [WellPowered C] : HasColimits C := by
   suffices HasLimits Cᵒᵖ from hasColimits_of_hasLimits_op

From 0a7bd9a8784aeaf962a6cac7052a68806ff4ec63 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 11:31:04 +0100
Subject: [PATCH 04/46] factor grothendieck categories out into a new file

---
 .../Abelian/GrothendieckAxioms.lean           | 25 ---------
 .../Abelian/GrothendieckCategory.lean         | 56 +++++++++++++++++++
 2 files changed, 56 insertions(+), 25 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 098e99e017391d..07b08dc0788bb4 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
 -/
 
-import Mathlib.CategoryTheory.Abelian.Subobject
-import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
@@ -22,15 +20,10 @@ basic facts about them.
 - `AB4` -- an abelian category satisfies `AB4` provided that coproducts are exact.
 - `AB5` -- an abelian category satisfies `AB5` provided that filtered colimits are exact.
 - The duals of the above definitions, called `AB4Star` and `AB5Star`.
-- `GrothendieckCategory` -- an abelian category satisfies `GrothendieckCategory` provided that
-it has `AB5` and a separator.
 
 ## Theorems
 
 - The implication from `AB5` to `AB4` is established in `AB4.ofAB5`.
-- Relevant implications of `GrothendieckCategory` are established in
-`GrothendieckCategory.wellPowered`, `GrothendieckCategory.hasLimits` and
-`GrothendieckCategory.hasColimits`.
 
 ## Remarks
 
@@ -103,24 +96,6 @@ class AB5Star [HasCofilteredLimits C] where
 
 attribute [instance] AB5Star.preservesFiniteColimits
 
-section GrothendieckCategory
-
-/--
-An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
-separator (see `HasSeparator`).
--/
-class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
-
-variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]
-
-instance GrothendieckCategory.wellPowered : WellPowered C := HasSeparator.wellPowered
-
-instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
-
-instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
-
-end GrothendieckCategory
-
 noncomputable section
 
 open CoproductsFromFiniteFiltered
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
new file mode 100644
index 00000000000000..e3922c20fcc100
--- /dev/null
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2024 Paul Reichert. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+
+import Mathlib.CategoryTheory.Abelian.Basic
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
+import Mathlib.CategoryTheory.Limits.Filtered
+
+/-!
+
+# Grothendieck categories
+
+This file defines Grothendieck categories and proves basic facts about them.
+
+## Definitions
+
+A `GrothendieckCategory` is an abelian category provided that it has `AB5` and a separator.
+
+## Theorems
+
+Relevant implications of `GrothendieckCategory` are established in
+`GrothendieckCategory.wellPowered`, `GrothendieckCategory.hasLimits` and
+`GrothendieckCategory.hasColimits`.
+
+## References
+
+* [Stacks: Grothendieck's AB conditions](https://stacks.math.columbia.edu/tag/079A)
+
+-/
+
+namespace CategoryTheory
+
+open Limits
+
+universe u v
+variable (C : Type u) [Category.{v} C]
+
+/--
+An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
+separator (see `HasSeparator`).
+-/
+class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
+
+section Instances
+
+variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]
+
+instance GrothendieckCategory.wellPowered : WellPowered C := HasSeparator.wellPowered
+instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
+instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
+
+end Instances
+
+end CategoryTheory

From f6f00469705e02f4f597ab397661e72c20c833af Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 11:48:21 +0100
Subject: [PATCH 05/46] move unrelated changes to datokrat/GrothendieckAxioms

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 07b08dc0788bb4..ea2fb89f5295e6 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -33,10 +33,6 @@ comments of the linked Stacks page.
 Exactness as the preservation of short exact sequences is introduced in
 `CategoryTheory.Abelian.Exact`.
 
-We do not require `Abelian` in the definition of `AB4` and `AB5` because these classes represent
-individual axioms. A non-abelian category with `AB5` is not an AB5 category in the sense of the
-literature.
-
 ## References
 * [Stacks: Grothendieck's AB conditions](https://stacks.math.columbia.edu/tag/079A)
 
@@ -116,7 +112,7 @@ instance preservesFiniteLimitsLiftToFinset : PreservesFiniteLimits (liftToFinset
     preservesFiniteLimitsOfNatIso (liftToFinsetEvaluationIso  I).symm
 
 /-- A category with finite biproducts and finite limits is AB4 if it is AB5. -/
-def AB4.ofAB5 [HasFilteredColimits C] [AB5 C] : AB4 C where
+def AB4.ofAB5 [HasFiniteCoproducts C] [HasFilteredColimits C] [AB5 C] : AB4 C where
   preservesFiniteLimits J :=
     letI : PreservesFiniteLimits (liftToFinset C J ⋙ colim) :=
       compPreservesFiniteLimits _ _

From c827ad827287e023edd9bbf8f3bd97c7d0b7330d Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 11:55:16 +0100
Subject: [PATCH 06/46] fix imports

---
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index e3922c20fcc100..15f5483e9c52b8 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 
-import Mathlib.CategoryTheory.Abelian.Basic
+import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
-import Mathlib.CategoryTheory.Limits.Filtered
+import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 
 /-!
 

From e403d96f56ce18d60b381bec153fdb5ce033870c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 12:05:23 +0100
Subject: [PATCH 07/46] simplify

---
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean    | 6 ++----
 .../CategoryTheory/Adjunction/AdjointFunctorTheorems.lean   | 6 ++----
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 15f5483e9c52b8..2b6335f1613751 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -20,9 +20,8 @@ A `GrothendieckCategory` is an abelian category provided that it has `AB5` and a
 
 ## Theorems
 
-Relevant implications of `GrothendieckCategory` are established in
-`GrothendieckCategory.wellPowered`, `GrothendieckCategory.hasLimits` and
-`GrothendieckCategory.hasColimits`.
+Relevant implications of `GrothendieckCategory` are established in `GrothendieckCategory.hasLimits`
+and `GrothendieckCategory.hasColimits`.
 
 ## References
 
@@ -47,7 +46,6 @@ section Instances
 
 variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]
 
-instance GrothendieckCategory.wellPowered : WellPowered C := HasSeparator.wellPowered
 instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
 instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
 
diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
index ba1a361373a47b..d9e59933f1a1b2 100644
--- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
+++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -140,9 +140,8 @@ theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered C
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a separator, then it is complete. -/
 theorem hasLimits_of_hasColimits_of_hasSeparator [HasColimits C] [HasSeparator C]
-    [WellPowered Cᵒᵖ] : HasLimits C := by
-  obtain ⟨G, hG⟩ : HasSeparator C := inferInstance
-  exact hasLimits_of_hasColimits_of_isSeparating hG
+    [WellPowered Cᵒᵖ] : HasLimits C :=
+  hasLimits_of_hasColimits_of_isSeparating <| isSeparator_separator C
 
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a coseparator, then it is cocomplete. -/
@@ -150,7 +149,6 @@ theorem hasColimits_of_hasLimits_of_hasCoseparator [HasLimits C] [HasCoseparator
     [WellPowered C] : HasColimits C := by
   suffices HasLimits Cᵒᵖ from hasColimits_of_hasLimits_op
   have : WellPowered Cᵒᵖᵒᵖ := wellPowered_of_equiv (opOpEquivalence C).symm
-  have : HasSeparator Cᵒᵖ := HasCoseparator.hasSeparator_op
   exact hasLimits_of_hasColimits_of_hasSeparator
 
 end Limits

From 6e51dcc7e65f05fd24d8eb37eaa120c416779edd Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 12:15:03 +0100
Subject: [PATCH 08/46] straighten lemma

---
 .../CategoryTheory/Adjunction/AdjointFunctorTheorems.lean   | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
index d9e59933f1a1b2..b4b03bb6b7eb76 100644
--- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
+++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -146,10 +146,8 @@ theorem hasLimits_of_hasColimits_of_hasSeparator [HasColimits C] [HasSeparator C
 /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
     has a coseparator, then it is cocomplete. -/
 theorem hasColimits_of_hasLimits_of_hasCoseparator [HasLimits C] [HasCoseparator C]
-    [WellPowered C] : HasColimits C := by
-  suffices HasLimits Cᵒᵖ from hasColimits_of_hasLimits_op
-  have : WellPowered Cᵒᵖᵒᵖ := wellPowered_of_equiv (opOpEquivalence C).symm
-  exact hasLimits_of_hasColimits_of_hasSeparator
+    [WellPowered C] : HasColimits C :=
+  hasColimits_of_hasLimits_of_isCoseparating <| isCoseparator_coseparator C
 
 end Limits
 

From bf2bc29a1ad291a4996770601fb6d4214699d475 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 10 Nov 2024 12:25:53 +0100
Subject: [PATCH 09/46] oops, forgot to update Mathlib.lean

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index a64b2959225052..294ebe08061705 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1487,6 +1487,7 @@ import Mathlib.CategoryTheory.Abelian.Ext
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.Generator
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
 import Mathlib.CategoryTheory.Abelian.Images
 import Mathlib.CategoryTheory.Abelian.Injective
 import Mathlib.CategoryTheory.Abelian.InjectiveResolution

From 4e47dc038a73507ce21813b48dcdddba95dd96c0 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 16 Nov 2024 11:23:02 +0100
Subject: [PATCH 10/46] stacks attributes

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean   | 4 ++++
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean | 1 +
 2 files changed, 5 insertions(+)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index eb2338dde029a1..8df02262d5d4ec 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -56,6 +56,7 @@ attribute [local instance] hasCoproducts_of_finite_and_filtered
 A category `C` which has coproducts is said to have `AB4` provided that
 coproducts are exact.
 -/
+@[stacks 079B]
 class AB4 [HasCoproducts C] where
   /-- Exactness of coproducts stated as `colim : (Discrete α ⥤ C) ⥤ C` preserving limits. -/
   preservesFiniteLimits (α : Type v) :
@@ -65,6 +66,7 @@ attribute [instance] AB4.preservesFiniteLimits
 
 /-- A category `C` which has products is said to have `AB4Star` (in literature `AB4*`)
 provided that products are exact. -/
+@[stacks 079B]
 class AB4Star [HasProducts C] where
   /-- Exactness of products stated as `lim : (Discrete α ⥤ C) ⥤ C` preserving colimits. -/
   preservesFiniteColimits (α : Type v) :
@@ -76,6 +78,7 @@ attribute [instance] AB4Star.preservesFiniteColimits
 A category `C` which has filtered colimits is said to have `AB5` provided that
 filtered colimits are exact.
 -/
+@[stacks 079B]
 class AB5 [HasFilteredColimits C] where
   /-- Exactness of filtered colimits stated as `colim : (J ⥤ C) ⥤ C` on filtered `J`
   preserving limits. -/
@@ -88,6 +91,7 @@ attribute [instance] AB5.preservesFiniteLimits
 A category `C` which has cofiltered limits is said to have `AB5Star` (in literature `AB5*`)
 provided that cofiltered limits are exact.
 -/
+@[stacks 079B]
 class AB5Star [HasCofilteredLimits C] where
   /-- Exactness of cofiltered limits stated as `lim : (J ⥤ C) ⥤ C` on cofiltered `J`
   preserving colimits. -/
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 2b6335f1613751..ca9c1aff8c7c6a 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -40,6 +40,7 @@ variable (C : Type u) [Category.{v} C]
 An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
 separator (see `HasSeparator`).
 -/
+@[stacks 079B]
 class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
 
 section Instances

From 3166f62b0257cc70698e56dc8c5076e419e75b54 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 18 Nov 2024 20:54:36 +0100
Subject: [PATCH 11/46] make preconditions of GrothendieckCategory fields

---
 .../CategoryTheory/Abelian/GrothendieckCategory.lean  | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index ca9c1aff8c7c6a..49ef1eb87cc6c2 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -41,11 +41,18 @@ An abelian category `C` is called a Grothendieck category provided that it has `
 separator (see `HasSeparator`).
 -/
 @[stacks 079B]
-class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where
+class GrothendieckCategory [Abelian C] where
+  -- necessary for AB5
+  hasFilteredColimits : HasFilteredColimits C := by infer_instance
+  ab5 : AB5 C := by infer_instance
+  hasSeparator : HasSeparator C := by infer_instance
+
+attribute [instance] GrothendieckCategory.hasSeparator GrothendieckCategory.hasFilteredColimits
+  GrothendieckCategory.ab5
 
 section Instances
 
-variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]
+variable [Abelian C] [GrothendieckCategory C]
 
 instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
 instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator

From c79a86128c593396a89be0c4c56bbccb75fbdef7 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 7 Dec 2024 21:36:18 +0100
Subject: [PATCH 12/46] new definition, ugly proof

---
 .../Abelian/GrothendieckCategory.lean         | 75 ++++++++++++++++++-
 Mathlib/CategoryTheory/Generator.lean         | 30 ++++++++
 2 files changed, 104 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 49ef1eb87cc6c2..5ae485c9e1906b 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -7,6 +7,8 @@ Authors: Paul Reichert
 import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
+import Mathlib.CategoryTheory.Adjunction.Opposites
+import Mathlib.CategoryTheory.Limits.HasLimits
 
 /-!
 
@@ -33,7 +35,7 @@ namespace CategoryTheory
 
 open Limits
 
-universe u v
+universe w v u
 variable (C : Type u) [Category.{v} C]
 
 /--
@@ -59,4 +61,75 @@ instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimit
 
 end Instances
 
+class IsGrothendieckAbelian : Prop where
+  locallySmall : LocallySmall.{w} C := by infer_instance
+  hasFilteredColimitsOfSize : HasFilteredColimitsOfSize.{w, w} C := by infer_instance
+  ab5OfSize : AB5OfSize.{w, w} C := by infer_instance
+  hasSeparator : HasSeparator C := by infer_instance
+
+attribute [instance] IsGrothendieckAbelian.locallySmall
+  IsGrothendieckAbelian.hasFilteredColimitsOfSize IsGrothendieckAbelian.ab5OfSize
+  IsGrothendieckAbelian.hasSeparator
+
+instance bla₁ (C : Type u) [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{w} C] :
+    HasFilteredColimitsOfSize.{w, w} (ShrinkHoms C) := by
+  refine ⟨fun _ _ _ => ?_⟩
+  exact Adjunction.hasColimitsOfShape_of_equivalence (ShrinkHoms.equivalence C).inverse
+
+universe v' u' v₁ u₁ v₂ u₂ in
+theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
+    (D : Type u₂) [Category.{v₂} D] (F : C ⥤ D) :
+    F ⋙ Functor.const J = Functor.const J ⋙ (whiskeringRight J C D).obj F := by
+  apply Functor.ext
+  · intro X Y f
+    simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj,
+    whiskeringRight_obj_map]
+    apply NatTrans.ext
+    ext x
+    simp only [Functor.const_obj_obj, Functor.const_map_app, NatTrans.comp_app, Functor.comp_obj,
+      eqToHom_app, eqToHom_refl, whiskerRight_app, Category.comp_id, Category.id_comp]
+  · intro X
+    simp only [Functor.comp_obj, whiskeringRight_obj_obj]
+    apply Functor.ext
+    · intro A B g
+      simp only [Functor.const_obj_obj, Functor.const_obj_map, Functor.comp_obj, eqToHom_refl,
+        Functor.comp_map, Functor.map_id, Category.comp_id]
+    · simp only [Functor.const_obj_obj, Functor.comp_obj]
+      intros ; trivial
+
+universe v' u' v₁ u₁ v₂ u₂ in
+theorem blub (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C] (D : Type u₂)
+    [Category.{v₂} D] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (F : C ≌ D) :
+    have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence F.inverse
+    HasExactColimitsOfShape J D := by
+  have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence F.inverse
+  refine ⟨⟨?_⟩⟩
+  intro I instI finI
+  refine ⟨?_⟩
+  intro K
+  let this : (J ⥤ D) ⥤ D := F.congrRight.inverse ⋙ (colim : (J ⥤ C) ⥤ C) ⋙ F.functor
+  refine preservesLimit_of_natIso K (?_ : this ≅ colim)
+  unfold this
+  refine Adjunction.natIsoOfRightAdjointNatIso ?_ CategoryTheory.Limits.colimConstAdj (Iso.refl _)
+  have : Functor.const J ≅ F.inverse ⋙ Functor.const J ⋙ F.congrRight.functor := by
+    rw [← Functor.assoc, comp_const, Equivalence.congrRight_functor, Functor.assoc]
+    change Functor.const J ⋙ 𝟭 _ ≅ _
+    apply isoWhiskerLeft
+    rw [whiskeringRight_obj_comp]
+    exact (whiskeringRight J D D).mapIso F.counitIso.symm
+  apply Adjunction.ofNatIsoRight _ this.symm
+  conv => lhs ; rw [← Functor.assoc]
+  refine Adjunction.comp ?_ F.toAdjunction
+  refine Adjunction.comp F.congrRight.symm.toAdjunction ?_
+  exact CategoryTheory.Limits.colimConstAdj
+
+instance IsGrothendieckAbelian.shrinkHoms (C : Type u) [Category.{v} C] [Abelian C]
+    [IsGrothendieckAbelian.{w} C] : IsGrothendieckAbelian.{w, w} (ShrinkHoms C) := by
+  refine ⟨inferInstance, inferInstance, ?_, ?_⟩
+  · refine ⟨?_⟩
+    intro J instJ filteredJ
+    apply blub J C
+    apply ShrinkHoms.equivalence
+  · exact HasSeparator.of_equivalence <| ShrinkHoms.equivalence C
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index 0e0311c2253f2f..afa09ce5456011 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -351,6 +351,28 @@ def IsDetector (G : C) : Prop :=
 def IsCodetector (G : C) : Prop :=
   IsCodetecting ({G} : Set C)
 
+
+section Equivalence
+
+def IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (α : C ≌ D) :
+    IsSeparator (α.functor.obj G) := by
+  intro d₁ d₂ f g hD
+  suffices h : α.inverse.map f = α.inverse.map g by
+    have h := congrArg α.functor.map h
+    simp only [Equivalence.fun_inv_map, Functor.comp_obj, Functor.id_obj,
+      NatIso.cancel_natIso_hom_left] at h
+    have h := congrArg (· ≫ α.counit.app d₂) h
+    simpa using h
+  apply hC
+  intro _ hG' hh
+  cases hG'
+  have := hD (α.functor.obj G) rfl (Adjunction.homEquiv α.toAdjunction G d₁ |>.symm hh)
+  have := congrArg (Adjunction.homEquiv α.toAdjunction G d₂) this
+  simp only [Adjunction.homEquiv_apply, Functor.map_comp, Adjunction.homEquiv_symm_apply] at this
+  simpa
+
+end Equivalence
+
 section Dual
 
 theorem isSeparator_op_iff (G : C) : IsSeparator (op G) ↔ IsCoseparator G := by
@@ -704,6 +726,14 @@ instance HasSeparator.wellPowered [HasPullbacks C] [Balanced C] [HasSeparator C]
 
 end Instances
 
+section Equivalence
+
+theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
+  ⟨α.functor.obj (separator C),
+   isSeparator_separator C |>.isSeparator_obj_of_equivalence α⟩
+
+end Equivalence
+
 section Dual
 
 @[simp]

From 78c210a966ad5d121b0dedf20bafc39fd5cb5182 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 7 Dec 2024 23:02:44 +0100
Subject: [PATCH 13/46] equivalence lemma for IsGrothendieckAbelian

---
 .../Abelian/GrothendieckCategory.lean         | 70 +++++++++----------
 Mathlib/CategoryTheory/Generator.lean         |  2 +-
 2 files changed, 34 insertions(+), 38 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 5ae485c9e1906b..3ae30ddb9e3b6a 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -35,32 +35,18 @@ namespace CategoryTheory
 
 open Limits
 
-universe w v u
-variable (C : Type u) [Category.{v} C]
+universe w v u w₂ v₂ u₂
+variable (C : Type u) [Category.{v} C] (D : Type u₂) [Category.{v₂} D]
 
 /--
-An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
-separator (see `HasSeparator`).
+In the literature, an abelian category `C` is called a Grothendieck category provided that it has
+`AB5` and a separator (see `HasSeparator`).
+
+`IsGrothendieckAbelian C` is defined such that it holds if and only if `C` is equivalent to a
+Grothendieck category -- more concretely, if and only if `ShrinkHoms.{w} C` is a Grothendieck
+category.
 -/
 @[stacks 079B]
-class GrothendieckCategory [Abelian C] where
-  -- necessary for AB5
-  hasFilteredColimits : HasFilteredColimits C := by infer_instance
-  ab5 : AB5 C := by infer_instance
-  hasSeparator : HasSeparator C := by infer_instance
-
-attribute [instance] GrothendieckCategory.hasSeparator GrothendieckCategory.hasFilteredColimits
-  GrothendieckCategory.ab5
-
-section Instances
-
-variable [Abelian C] [GrothendieckCategory C]
-
-instance GrothendieckCategory.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
-instance GrothendieckCategory.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
-
-end Instances
-
 class IsGrothendieckAbelian : Prop where
   locallySmall : LocallySmall.{w} C := by infer_instance
   hasFilteredColimitsOfSize : HasFilteredColimitsOfSize.{w, w} C := by infer_instance
@@ -71,12 +57,7 @@ attribute [instance] IsGrothendieckAbelian.locallySmall
   IsGrothendieckAbelian.hasFilteredColimitsOfSize IsGrothendieckAbelian.ab5OfSize
   IsGrothendieckAbelian.hasSeparator
 
-instance bla₁ (C : Type u) [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{w} C] :
-    HasFilteredColimitsOfSize.{w, w} (ShrinkHoms C) := by
-  refine ⟨fun _ _ _ => ?_⟩
-  exact Adjunction.hasColimitsOfShape_of_equivalence (ShrinkHoms.equivalence C).inverse
-
-universe v' u' v₁ u₁ v₂ u₂ in
+universe v' u' v₁ u₁ in
 theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
     (D : Type u₂) [Category.{v₂} D] (F : C ⥤ D) :
     F ⋙ Functor.const J = Functor.const J ⋙ (whiskeringRight J C D).obj F := by
@@ -97,7 +78,7 @@ theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v
     · simp only [Functor.const_obj_obj, Functor.comp_obj]
       intros ; trivial
 
-universe v' u' v₁ u₁ v₂ u₂ in
+universe v' u' v₁ u₁ in
 theorem blub (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C] (D : Type u₂)
     [Category.{v₂} D] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (F : C ≌ D) :
     have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence F.inverse
@@ -123,13 +104,28 @@ theorem blub (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
   refine Adjunction.comp F.congrRight.symm.toAdjunction ?_
   exact CategoryTheory.Limits.colimConstAdj
 
-instance IsGrothendieckAbelian.shrinkHoms (C : Type u) [Category.{v} C] [Abelian C]
-    [IsGrothendieckAbelian.{w} C] : IsGrothendieckAbelian.{w, w} (ShrinkHoms C) := by
-  refine ⟨inferInstance, inferInstance, ?_, ?_⟩
-  · refine ⟨?_⟩
-    intro J instJ filteredJ
-    apply blub J C
-    apply ShrinkHoms.equivalence
-  · exact HasSeparator.of_equivalence <| ShrinkHoms.equivalence C
+variable {C} {D} in
+theorem IsGrothendieckAbelian.of_equivalence
+    [IsGrothendieckAbelian.{w} C] (α : C ≌ D) : IsGrothendieckAbelian.{w} D := by
+  have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
+    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
+  refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
+  · exact locallySmall_of_faithful α.inverse
+  · refine ⟨fun _ _ _ => ?_⟩
+    exact blub _ C D α
+  · exact HasSeparator.of_equivalence α
+
+instance IsGrothendieckAbelian.shrinkHoms [IsGrothendieckAbelian.{w} C] :
+    IsGrothendieckAbelian.{w, w} (ShrinkHoms C) :=
+  IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C
+
+section Instances
+
+variable [Abelian C] [IsGrothendieckAbelian C]
+
+instance IsGrothendieckAbelian.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
+instance IsGrothendieckAbelian.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
+
+end Instances
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index afa09ce5456011..dd6c754873705f 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -354,7 +354,7 @@ def IsCodetector (G : C) : Prop :=
 
 section Equivalence
 
-def IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (α : C ≌ D) :
+theorem IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (α : C ≌ D) :
     IsSeparator (α.functor.obj G) := by
   intro d₁ d₂ f g hD
   suffices h : α.inverse.map f = α.inverse.map g by

From b3c765a297d7d5f39e248651d28d92226d50d5b0 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Dec 2024 00:30:56 +0100
Subject: [PATCH 14/46] snapshot

---
 .../Abelian/GrothendieckAxioms.lean           | 33 +++++++++++
 .../Abelian/GrothendieckCategory.lean         | 49 +---------------
 Mathlib/CategoryTheory/Functor/Currying.lean  |  4 ++
 Mathlib/CategoryTheory/Limits/HasLimits.lean  | 58 +++++++++++++++++++
 4 files changed, 96 insertions(+), 48 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 2ca0dc8ec89e92..01933cb4edc5ff 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -5,6 +5,7 @@ Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
 -/
 import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
+import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Shapes.Countable
@@ -88,6 +89,38 @@ lemma hasExactColimitsOfShape_of_equiv {J J' : Type*} [Category J] [Category J']
   haveI : HasColimitsOfShape J' C := hasColimitsOfShape_of_equivalence e
   ⟨preservesFiniteLimits_of_natIso (Functor.Final.colimIso e.functor)⟩
 
+variable {C} in
+lemma hasExactColimitsOfShape_obj_of_equiv (J : Type*) {D : Type*} [Category J] [Category D]
+    (e : C ≌ D) [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
+    have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
+    HasExactColimitsOfShape J D := by
+  have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
+  refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
+  refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)
+  apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
+  exact isoWhiskerLeft (_ ⋙ colim) e.unitIso.symm ≪≫ (preservesColimitNatIso e.inverse).symm
+
+universe v₁ u₁ v₂ u₂ in
+theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
+    (D : Type u₂) [Category.{v₂} D] (F : C ⥤ D) :
+    F ⋙ Functor.const J = Functor.const J ⋙ (whiskeringRight J C D).obj F := by
+  apply Functor.ext
+  · intro X Y f
+    simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj,
+    whiskeringRight_obj_map]
+    apply NatTrans.ext
+    ext x
+    simp only [Functor.const_obj_obj, Functor.const_map_app, NatTrans.comp_app, Functor.comp_obj,
+      eqToHom_app, eqToHom_refl, whiskerRight_app, Category.comp_id, Category.id_comp]
+  · intro X
+    simp only [Functor.comp_obj, whiskeringRight_obj_obj]
+    apply Functor.ext
+    · intro A B g
+      simp only [Functor.const_obj_obj, Functor.const_obj_map, Functor.comp_obj, eqToHom_refl,
+        Functor.comp_map, Functor.map_id, Category.comp_id]
+    · simp only [Functor.const_obj_obj, Functor.comp_obj]
+      intros ; trivial
+
 /--
 Transport a `HasExactLimitsOfShape` along an equivalence of the shape.
 
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 3ae30ddb9e3b6a..300b06b9d56943 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -57,53 +57,6 @@ attribute [instance] IsGrothendieckAbelian.locallySmall
   IsGrothendieckAbelian.hasFilteredColimitsOfSize IsGrothendieckAbelian.ab5OfSize
   IsGrothendieckAbelian.hasSeparator
 
-universe v' u' v₁ u₁ in
-theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
-    (D : Type u₂) [Category.{v₂} D] (F : C ⥤ D) :
-    F ⋙ Functor.const J = Functor.const J ⋙ (whiskeringRight J C D).obj F := by
-  apply Functor.ext
-  · intro X Y f
-    simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj,
-    whiskeringRight_obj_map]
-    apply NatTrans.ext
-    ext x
-    simp only [Functor.const_obj_obj, Functor.const_map_app, NatTrans.comp_app, Functor.comp_obj,
-      eqToHom_app, eqToHom_refl, whiskerRight_app, Category.comp_id, Category.id_comp]
-  · intro X
-    simp only [Functor.comp_obj, whiskeringRight_obj_obj]
-    apply Functor.ext
-    · intro A B g
-      simp only [Functor.const_obj_obj, Functor.const_obj_map, Functor.comp_obj, eqToHom_refl,
-        Functor.comp_map, Functor.map_id, Category.comp_id]
-    · simp only [Functor.const_obj_obj, Functor.comp_obj]
-      intros ; trivial
-
-universe v' u' v₁ u₁ in
-theorem blub (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C] (D : Type u₂)
-    [Category.{v₂} D] [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (F : C ≌ D) :
-    have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence F.inverse
-    HasExactColimitsOfShape J D := by
-  have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence F.inverse
-  refine ⟨⟨?_⟩⟩
-  intro I instI finI
-  refine ⟨?_⟩
-  intro K
-  let this : (J ⥤ D) ⥤ D := F.congrRight.inverse ⋙ (colim : (J ⥤ C) ⥤ C) ⋙ F.functor
-  refine preservesLimit_of_natIso K (?_ : this ≅ colim)
-  unfold this
-  refine Adjunction.natIsoOfRightAdjointNatIso ?_ CategoryTheory.Limits.colimConstAdj (Iso.refl _)
-  have : Functor.const J ≅ F.inverse ⋙ Functor.const J ⋙ F.congrRight.functor := by
-    rw [← Functor.assoc, comp_const, Equivalence.congrRight_functor, Functor.assoc]
-    change Functor.const J ⋙ 𝟭 _ ≅ _
-    apply isoWhiskerLeft
-    rw [whiskeringRight_obj_comp]
-    exact (whiskeringRight J D D).mapIso F.counitIso.symm
-  apply Adjunction.ofNatIsoRight _ this.symm
-  conv => lhs ; rw [← Functor.assoc]
-  refine Adjunction.comp ?_ F.toAdjunction
-  refine Adjunction.comp F.congrRight.symm.toAdjunction ?_
-  exact CategoryTheory.Limits.colimConstAdj
-
 variable {C} {D} in
 theorem IsGrothendieckAbelian.of_equivalence
     [IsGrothendieckAbelian.{w} C] (α : C ≌ D) : IsGrothendieckAbelian.{w} D := by
@@ -112,7 +65,7 @@ theorem IsGrothendieckAbelian.of_equivalence
   refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
   · exact locallySmall_of_faithful α.inverse
   · refine ⟨fun _ _ _ => ?_⟩
-    exact blub _ C D α
+    exact hasExactColimitsOfShape_obj_of_equiv _ α
   · exact HasSeparator.of_equivalence α
 
 instance IsGrothendieckAbelian.shrinkHoms [IsGrothendieckAbelian.{w} C] :
diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
index 5c8021e9a84c08..59b0c5f8c42191 100644
--- a/Mathlib/CategoryTheory/Functor/Currying.lean
+++ b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -109,6 +109,10 @@ def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E
   uncurry ⋙
     whiskeringRight _ _ _ ⋙ (whiskeringLeft _ _ _).obj (prodFunctorToFunctorProd _ _ _) ⋙ curry
 
+@[simps!]
+def whiskeringLeft₂ : (B ⥤ C ⥤ D) ⥤ (D ⥤ E) ⥤ B ⥤ C ⥤ E :=
+  (whiskeringLeft _ _ _ |>.flip) ⋙ (whiskeringLeft _ _ _ |>.flip) |>.flip
+
 namespace Functor
 
 variable {B C D E}
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index febff5598358dc..013092aef4aedb 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.EssentiallySmall
 import Mathlib.Logic.Equiv.Basic
+import Mathlib.CategoryTheory.Functor.Currying
 
 /-!
 # Existence of limits and colimits
@@ -923,6 +924,31 @@ to `G` applied to the colimit of `F`.
 def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
   colimit.desc (F ⋙ G) (G.mapCocone (colimit.cocone F))
 
+def colimit.post_nat {F₁ F₂ : J ⥤ C} [HasColimit F₁] [HasColimit F₂] (f : F₁ ⟶ F₂) (G : C ⥤ D)
+    [HasColimit (F₁ ⋙ G)] [HasColimit (F₂ ⋙ G)] :
+    colimMap (whiskerRight f G) ≫ colimit.post F₂ G = colimit.post F₁ G ≫ G.map (colimMap f) := by
+  simp only [colimMap, post]
+  ext j
+  simp only [IsColimit.map]
+  simp only [isColimit_desc, ι_desc_assoc, comp_obj, Cocones.precompose_obj_pt, cocone_x,
+    Cocones.precompose_obj_ι, NatTrans.comp_app, const_obj_obj, whiskerRight_app, cocone_ι, assoc,
+    ι_desc, mapCocone_pt, mapCocone_ι_app]
+  simp only [← Functor.map_comp]
+  simp only [ι_desc, Cocones.precompose_obj_pt, cocone_x, Cocones.precompose_obj_ι,
+    NatTrans.comp_app, const_obj_obj, cocone_ι]
+
+def colimit.post_nat' (F : J ⥤ C) [HasColimit F] {G₁ G₂ : C ⥤ D} [HasColimit (F ⋙ G₁)]
+    [HasColimit (F ⋙ G₂)] (g : G₁ ⟶ G₂) :
+    have : HasColimit (((whiskeringRight J C D).obj G₁).obj F) :=
+      inferInstanceAs <| HasColimit <| F ⋙ G₁
+    have : HasColimit (((whiskeringRight J C D).obj G₂).obj F) :=
+      inferInstanceAs <| HasColimit <| F ⋙ G₂
+    colimMap (((whiskeringRight J C D).map g).app F) ≫ colimit.post F G₂ =
+      colimit.post F G₁ ≫ g.app (colimit F) := by
+  simp only [whiskeringRight_obj_obj, post]
+  ext j
+  simp [IsColimit.map]
+
 @[reassoc (attr := simp)]
 theorem colimit.ι_post (j : J) :
     colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) := by
@@ -988,6 +1014,38 @@ def colim : (J ⥤ C) ⥤ C where
   obj F := colimit F
   map α := colimMap α
 
+-- variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] in
+-- def colim.post' :
+--     (whiskeringLeft₂' _ _ _ _ |>.obj (whiskeringRight J C D) |>.obj colim)
+--     ⟶ (colim ⋙ evaluation C D |>.flip) where
+--   app := colim.post J
+--   naturality G₁ G₂ g := colim_post_nat' J G₁ G₂ g
+
+variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] in
+def colim.post :
+    (whiskeringLeft₂ _ _ _ _ |>.obj (whiskeringRight J C D) |>.obj colim)
+    ⟶ (colim ⋙ evaluation C D |>.flip) where
+  app G := by
+    refine ⟨?_, ?_⟩
+    · exact fun F => colimit.post F G
+    · exact fun F₁ F₂ α => colimit.post_nat α G
+  naturality G₁ G₂ g := by ext ; apply colimit.post_nat'
+
+variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] {E : Type*} [Category E]
+  [HasColimitsOfShape J E] in
+@[reassoc]
+theorem colim.post_comp (G : C ⥤ D) (H : D ⥤ E) :
+    whiskerLeft ((whiskeringRight J C D).obj G) (post J |>.app H)
+    ≫ whiskerRight (post J |>.app G) H = (post J |>.app (G ⋙ H)) := by
+  ext F
+  simp only [comp_obj, whiskeringRight_obj_obj, colim_obj, post, NatTrans.comp_app, whiskerLeft_app,
+    whiskerRight_app, colimit.post_post]
+
+variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] {E : Type*} [Category E]
+  [HasColimitsOfShape J E] in
+theorem colim.post_id : (colim.post J |>.app (𝟭 _)) = NatTrans.id (colim : (J ⥤ C) ⥤ C) := by
+  ext F ; exact colimit.desc_cocone
+
 end
 
 variable {G : J ⥤ C} (α : F ⟶ G)

From 02ddcdf799186167bc8bc7c3f1e8d4e71a1b5440 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Dec 2024 00:34:50 +0100
Subject: [PATCH 15/46] cleanup

---
 Mathlib/CategoryTheory/Functor/Currying.lean |  4 --
 Mathlib/CategoryTheory/Limits/HasLimits.lean | 58 --------------------
 2 files changed, 62 deletions(-)

diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
index 59b0c5f8c42191..5c8021e9a84c08 100644
--- a/Mathlib/CategoryTheory/Functor/Currying.lean
+++ b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -109,10 +109,6 @@ def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E
   uncurry ⋙
     whiskeringRight _ _ _ ⋙ (whiskeringLeft _ _ _).obj (prodFunctorToFunctorProd _ _ _) ⋙ curry
 
-@[simps!]
-def whiskeringLeft₂ : (B ⥤ C ⥤ D) ⥤ (D ⥤ E) ⥤ B ⥤ C ⥤ E :=
-  (whiskeringLeft _ _ _ |>.flip) ⋙ (whiskeringLeft _ _ _ |>.flip) |>.flip
-
 namespace Functor
 
 variable {B C D E}
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index 013092aef4aedb..febff5598358dc 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -7,7 +7,6 @@ import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.EssentiallySmall
 import Mathlib.Logic.Equiv.Basic
-import Mathlib.CategoryTheory.Functor.Currying
 
 /-!
 # Existence of limits and colimits
@@ -924,31 +923,6 @@ to `G` applied to the colimit of `F`.
 def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
   colimit.desc (F ⋙ G) (G.mapCocone (colimit.cocone F))
 
-def colimit.post_nat {F₁ F₂ : J ⥤ C} [HasColimit F₁] [HasColimit F₂] (f : F₁ ⟶ F₂) (G : C ⥤ D)
-    [HasColimit (F₁ ⋙ G)] [HasColimit (F₂ ⋙ G)] :
-    colimMap (whiskerRight f G) ≫ colimit.post F₂ G = colimit.post F₁ G ≫ G.map (colimMap f) := by
-  simp only [colimMap, post]
-  ext j
-  simp only [IsColimit.map]
-  simp only [isColimit_desc, ι_desc_assoc, comp_obj, Cocones.precompose_obj_pt, cocone_x,
-    Cocones.precompose_obj_ι, NatTrans.comp_app, const_obj_obj, whiskerRight_app, cocone_ι, assoc,
-    ι_desc, mapCocone_pt, mapCocone_ι_app]
-  simp only [← Functor.map_comp]
-  simp only [ι_desc, Cocones.precompose_obj_pt, cocone_x, Cocones.precompose_obj_ι,
-    NatTrans.comp_app, const_obj_obj, cocone_ι]
-
-def colimit.post_nat' (F : J ⥤ C) [HasColimit F] {G₁ G₂ : C ⥤ D} [HasColimit (F ⋙ G₁)]
-    [HasColimit (F ⋙ G₂)] (g : G₁ ⟶ G₂) :
-    have : HasColimit (((whiskeringRight J C D).obj G₁).obj F) :=
-      inferInstanceAs <| HasColimit <| F ⋙ G₁
-    have : HasColimit (((whiskeringRight J C D).obj G₂).obj F) :=
-      inferInstanceAs <| HasColimit <| F ⋙ G₂
-    colimMap (((whiskeringRight J C D).map g).app F) ≫ colimit.post F G₂ =
-      colimit.post F G₁ ≫ g.app (colimit F) := by
-  simp only [whiskeringRight_obj_obj, post]
-  ext j
-  simp [IsColimit.map]
-
 @[reassoc (attr := simp)]
 theorem colimit.ι_post (j : J) :
     colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) := by
@@ -1014,38 +988,6 @@ def colim : (J ⥤ C) ⥤ C where
   obj F := colimit F
   map α := colimMap α
 
--- variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] in
--- def colim.post' :
---     (whiskeringLeft₂' _ _ _ _ |>.obj (whiskeringRight J C D) |>.obj colim)
---     ⟶ (colim ⋙ evaluation C D |>.flip) where
---   app := colim.post J
---   naturality G₁ G₂ g := colim_post_nat' J G₁ G₂ g
-
-variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] in
-def colim.post :
-    (whiskeringLeft₂ _ _ _ _ |>.obj (whiskeringRight J C D) |>.obj colim)
-    ⟶ (colim ⋙ evaluation C D |>.flip) where
-  app G := by
-    refine ⟨?_, ?_⟩
-    · exact fun F => colimit.post F G
-    · exact fun F₁ F₂ α => colimit.post_nat α G
-  naturality G₁ G₂ g := by ext ; apply colimit.post_nat'
-
-variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] {E : Type*} [Category E]
-  [HasColimitsOfShape J E] in
-@[reassoc]
-theorem colim.post_comp (G : C ⥤ D) (H : D ⥤ E) :
-    whiskerLeft ((whiskeringRight J C D).obj G) (post J |>.app H)
-    ≫ whiskerRight (post J |>.app G) H = (post J |>.app (G ⋙ H)) := by
-  ext F
-  simp only [comp_obj, whiskeringRight_obj_obj, colim_obj, post, NatTrans.comp_app, whiskerLeft_app,
-    whiskerRight_app, colimit.post_post]
-
-variable (J) {D : Type*} [Category D] [HasColimitsOfShape J D] {E : Type*} [Category E]
-  [HasColimitsOfShape J E] in
-theorem colim.post_id : (colim.post J |>.app (𝟭 _)) = NatTrans.id (colim : (J ⥤ C) ⥤ C) := by
-  ext F ; exact colimit.desc_cocone
-
 end
 
 variable {G : J ⥤ C} (α : F ⟶ G)

From f735ee956803d8e1d9a71fffc4489edf914f415e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Dec 2024 00:45:54 +0100
Subject: [PATCH 16/46] cleanup

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean | 1 -
 Mathlib/CategoryTheory/Generator.lean                  | 8 +++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 01933cb4edc5ff..fc33999a6c21a9 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -5,7 +5,6 @@ Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
 -/
 import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
-import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.Constructions.Filtered
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Shapes.Countable
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index dd6c754873705f..dcb82f653071c7 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -354,8 +354,10 @@ def IsCodetector (G : C) : Prop :=
 
 section Equivalence
 
-theorem IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (α : C ≌ D) :
-    IsSeparator (α.functor.obj G) := by
+theorem IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (F : C ⥤ D)
+    [F.IsEquivalence] :
+    IsSeparator (F.obj G) := by
+  let α := F.asEquivalence
   intro d₁ d₂ f g hD
   suffices h : α.inverse.map f = α.inverse.map g by
     have h := congrArg α.functor.map h
@@ -730,7 +732,7 @@ section Equivalence
 
 theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
   ⟨α.functor.obj (separator C),
-   isSeparator_separator C |>.isSeparator_obj_of_equivalence α⟩
+   isSeparator_separator C |>.isSeparator_obj_of_equivalence α.functor⟩
 
 end Equivalence
 

From 86fadf3e76fc137006184e8066d24c728d08bc92 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Dec 2024 00:47:31 +0100
Subject: [PATCH 17/46] more cleanup

---
 Mathlib/CategoryTheory/Generator.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index dcb82f653071c7..1c33c205c400e7 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -731,8 +731,7 @@ end Instances
 section Equivalence
 
 theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
-  ⟨α.functor.obj (separator C),
-   isSeparator_separator C |>.isSeparator_obj_of_equivalence α.functor⟩
+  ⟨α.functor.obj (separator C), isSeparator_separator C |>.isSeparator_obj_of_equivalence α.functor⟩
 
 end Equivalence
 

From 102bc3ea2bda678edba4bc05d3fcee2f2ae7d9aa Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Dec 2024 02:19:13 +0100
Subject: [PATCH 18/46] have -> haveI

---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index fc33999a6c21a9..2f89c1da23f8e0 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -91,9 +91,9 @@ lemma hasExactColimitsOfShape_of_equiv {J J' : Type*} [Category J] [Category J']
 variable {C} in
 lemma hasExactColimitsOfShape_obj_of_equiv (J : Type*) {D : Type*} [Category J] [Category D]
     (e : C ≌ D) [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
-    have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
+    haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
     HasExactColimitsOfShape J D := by
-  have : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
+  haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
   refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
   refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)
   apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

From 383fd4403b612a8a6cbd1f393f64adf926b89852 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 14 Dec 2024 07:07:36 +0100
Subject: [PATCH 19/46] wip

---
 .../Abelian/GrothendieckAxioms.lean           | 21 ------
 .../Abelian/GrothendieckCategory.lean         | 73 ++++++++++++++++++-
 2 files changed, 69 insertions(+), 25 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
index 2f89c1da23f8e0..62330313eb9da4 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
@@ -99,27 +99,6 @@ lemma hasExactColimitsOfShape_obj_of_equiv (J : Type*) {D : Type*} [Category J]
   apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
   exact isoWhiskerLeft (_ ⋙ colim) e.unitIso.symm ≪≫ (preservesColimitNatIso e.inverse).symm
 
-universe v₁ u₁ v₂ u₂ in
-theorem comp_const (J : Type u') [Category.{v'} J] (C : Type u₁) [Category.{v₁} C]
-    (D : Type u₂) [Category.{v₂} D] (F : C ⥤ D) :
-    F ⋙ Functor.const J = Functor.const J ⋙ (whiskeringRight J C D).obj F := by
-  apply Functor.ext
-  · intro X Y f
-    simp only [Functor.comp_obj, Functor.comp_map, whiskeringRight_obj_obj,
-    whiskeringRight_obj_map]
-    apply NatTrans.ext
-    ext x
-    simp only [Functor.const_obj_obj, Functor.const_map_app, NatTrans.comp_app, Functor.comp_obj,
-      eqToHom_app, eqToHom_refl, whiskerRight_app, Category.comp_id, Category.id_comp]
-  · intro X
-    simp only [Functor.comp_obj, whiskeringRight_obj_obj]
-    apply Functor.ext
-    · intro A B g
-      simp only [Functor.const_obj_obj, Functor.const_obj_map, Functor.comp_obj, eqToHom_refl,
-        Functor.comp_map, Functor.map_id, Category.comp_id]
-    · simp only [Functor.const_obj_obj, Functor.comp_obj]
-      intros ; trivial
-
 /--
 Transport a `HasExactLimitsOfShape` along an equivalence of the shape.
 
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 300b06b9d56943..76165fe5a2adb3 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 
-import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
+import Mathlib.CategoryTheory.Abelian.Subobject
+import Mathlib.CategoryTheory.Abelian.Transfer
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.HasLimits
@@ -72,12 +73,76 @@ instance IsGrothendieckAbelian.shrinkHoms [IsGrothendieckAbelian.{w} C] :
     IsGrothendieckAbelian.{w, w} (ShrinkHoms C) :=
   IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C
 
+noncomputable instance ShrinkHoms.homGroups [Preadditive C] (P Q : ShrinkHoms C) : AddCommGroup (P ⟶ Q) where
+  add f g := (equivShrink _ |>.symm) f + (equivShrink _ |>.symm) g |> equivShrink _
+  zero := 0 |> equivShrink _
+  nsmul n f := magnify f |> AddMonoid.nsmul n |> shrink
+  zsmul z f := magnify f |> SubNegMonoid.zsmul z |> shrink
+  neg f := - magnify f |> shrink
+  zero_add f := by
+    unfold HAdd.hAdd instHAdd OfNat.ofNat Zero.toOfNat0 Zero.zero HasZeroMorphisms.zero
+      Preadditive.preadditiveHasZeroMorphisms inferInstance NegZeroClass.toZero
+      SubNegZeroMonoid.toNegZeroClass AddMonoid.toZero SubNegMonoid.toAddMonoid
+      SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid
+      SubtractionMonoid.toSubNegMonoid SubtractionCommMonoid.toSubtractionMonoid
+      AddCommGroup.toDivisionAddCommMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup
+      Preadditive.homGroup
+    dsimp
+    simp only [Equiv.symm_apply_apply]
+    conv =>
+      lhs
+      apply congrArg
+      simp_rw [zero_add (equivShrink _ |>.symm f)]
+    erw [zero_add (equivShrink _ |>.symm f)]
+  add_zero := sorry
+  neg_add_cancel := sorry
+  nsmul_zero := sorry
+  nsmul_succ := sorry
+  zsmul_zero' := sorry
+  zsmul_neg' := sorry
+  zsmul_succ' := sorry
+  add_comm f g := congrArg _ <| add_comm _ _
+  add_assoc f g h := by
+    unfold HAdd.hAdd instHAdd
+    simp only [Equiv.symm_apply_apply]
+    exact congrArg _ <| add_assoc _ _ _
+where
+  shrink := equivShrink _
+  magnify := equivShrink _ |>.symm
+
+instance ShrinkHoms.preadditive [Preadditive C] : Preadditive (ShrinkHoms C) where
+  homGroup P Q := by
+    addCommGroup
+
+instance ShrinkHoms.abelian [Abelian C] : Abelian (ShrinkHoms C) :=
+  abelianOfEquivalence (ShrinkHoms.equivalence C |>.inverse)
+
+
 section Instances
 
-variable [Abelian C] [IsGrothendieckAbelian C]
+variable [Abelian C] [IsGrothendieckAbelian.{w} C]
+
+-- instance IsGrothendieckAbelian.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
+-- instance IsGrothendieckAbelian.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
+
+instance IsGrothendieckAbelian.hasColimitsOfSize' : HasColimitsOfSize.{w, w} C :=
+  has_colimits_of_finite_and_filtered
+
+instance IsGrothendieckAbelian.hasLimitsOfSize' : HasLimitsOfSize.{w, w} C := by
+  --have : Abelian (ShrinkHoms C) := sorry
+  have : HasColimits.{w, u} (ShrinkHoms C) := IsGrothendieckAbelian.hasColimitsOfSize' _
+  have : HasLimits.{w, u} (ShrinkHoms C) := hasLimits_of_hasColimits_of_hasSeparator
+
+  done
+
+-- instance IsGrothendieckAbelian.hasColimitsOfSize : HasColimitsOfSize.{w, w} (ShrinkHoms C) := by
+--   have : HasColimitsOfSize.{w, w} C := has_colimits_of_finite_and_filtered
+--   exact Adjunction.has_colimits_of_equivalence (ShrinkHoms.equivalence C |>.inverse)
 
-instance IsGrothendieckAbelian.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
-instance IsGrothendieckAbelian.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
+instance IsGrothendieckAbelian.hasLimitsOfSize : HasLimitsOfSize.{w, w} (ShrinkHoms C) := by
+  -- hasLimits_of_hasColimits_of_hasSeparator
+  have : HasLimitsOfSize.{w, w} C := hasLimits_of_hasColimits_of_hasSeparator
+  apply Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.inverse)
 
 end Instances
 

From 82d82f7129bd6edaa69ecc738388c6c67399ce90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Dec 2024 20:26:46 +0100
Subject: [PATCH 20/46] feat(CategoryTheory/Sites): categories of sites have a
 separator

---
 Mathlib.lean                                |   1 +
 Mathlib/CategoryTheory/Sites/Generator.lean | 149 ++++++++++++++++++++
 2 files changed, 150 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Sites/Generator.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 87d14e789d6f0d..351802a9644c3b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2110,6 +2110,7 @@ import Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
 import Mathlib.CategoryTheory.Sites.EpiMono
 import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Equivalence
+import Mathlib.CategoryTheory.Sites.Generator
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
diff --git a/Mathlib/CategoryTheory/Sites/Generator.lean b/Mathlib/CategoryTheory/Sites/Generator.lean
new file mode 100644
index 00000000000000..a468148b1db4ed
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/Generator.lean
@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.Limits.Shapes.Products
+import Mathlib.CategoryTheory.Sites.Sheafification
+import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.CategoryTheory.Generator
+
+/-!
+# Generators in the category of sheaves
+
+In this file, we show that if `J : GrothendieckTopology C` and `A` is a preadditive
+category which has a separator (and suitable coproducts), then `Sheaf J A` has a separator.
+
+-/
+
+universe w v' v u' u
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+-- to be moved
+open Classical in
+lemma IsSeparating.isSeparator_coproduct {C : Type u} [Category.{v} C]
+    {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S)) [HasCoproduct S]
+    [HasZeroMorphisms C] :
+    IsSeparator (∐ S) := by
+  intro X Y f g h
+  refine hS _ _ ?_
+  rintro _ ⟨i, rfl⟩ α
+  let β : ∐ S ⟶ X := Sigma.desc
+    (fun j ↦ if hij : i = j then eqToHom (by rw [hij]) ≫ α else 0)
+  have hβ : Sigma.ι S i ≫ β = α := by simp [β]
+  simp only [← hβ, Category.assoc, h (∐ S) (by simp) β]
+
+namespace Presheaf
+
+variable {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
+  [∀ (ι : Type v), HasCoproductsOfShape ι A]
+
+/-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
+`Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`. -/
+@[simps]
+noncomputable def freeYoneda (X : C) (M : A) : Cᵒᵖ ⥤ A where
+  obj Y := ∐ (fun (i : (yoneda.obj X).obj Y) ↦ M)
+  map f := Sigma.map' ((yoneda.obj X).map f) (fun _ ↦ 𝟙 M)
+
+/-- The bijection `(Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X))`. -/
+noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Cᵒᵖ ⥤ A} :
+    (freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X)) where
+  toFun f := Sigma.ι (fun (i : (yoneda.obj X).obj _) ↦ M) (𝟙 _) ≫ f.app (op X)
+  invFun g :=
+    { app Y := Sigma.desc (fun φ ↦ g ≫ F.map φ.op)
+      naturality _ _ _ := Sigma.hom_ext _ _ (by simp)}
+  left_inv f := by
+    ext Y
+    refine Sigma.hom_ext _ _ (fun φ ↦ ?_)
+    simpa using (Sigma.ι _ (𝟙 _) ≫= f.naturality φ.op).symm
+  right_inv g := by simp
+
+@[reassoc]
+lemma freeYonedaHomEquiv_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A}
+    (α : freeYoneda X M ⟶ F) (f : F ⟶ G) :
+    freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X) := by
+  simp [freeYonedaHomEquiv]
+
+@[reassoc]
+lemma freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M ⟶ F.obj (op X))
+    (f : F ⟶ G) :
+    freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)) := by
+  obtain ⟨β, rfl⟩ := freeYonedaHomEquiv.surjective α
+  apply freeYonedaHomEquiv.injective
+  simp only [Equiv.symm_apply_apply, freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]
+
+variable (C)
+
+lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
+    IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) := by
+  intro F G f g h
+  ext ⟨X⟩
+  refine hS _ _ ?_
+  rintro _ ⟨i, rfl⟩ α
+  apply freeYonedaHomEquiv.symm.injective
+  simpa only [freeYonedaHomEquiv_symm_comp] using
+    h _ ⟨⟨X, i⟩, rfl⟩ (freeYonedaHomEquiv.symm α)
+
+lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
+    [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))]
+    [HasZeroMorphisms A] :
+    IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) :=
+  (isSeparating C hS).isSeparator_coproduct
+
+variable (A) in
+instance hasSeparator [HasSeparator A] [HasZeroMorphisms A]
+    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+    HasSeparator (Cᵒᵖ ⥤ A) where
+  hasSeparator := ⟨_, isSeparator C (S := fun (_ : Unit) ↦ separator A)
+      (by simpa using isSeparator_separator A)⟩
+
+end Presheaf
+
+namespace Sheaf
+
+variable {C : Type u} [Category.{v} C]
+  (J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
+  [∀ (ι : Type v), HasCoproductsOfShape ι A]
+  [HasWeakSheafify J A]
+
+/-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
+sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
+noncomputable def freeYoneda (X : C) (M : A) : Sheaf J A :=
+  (presheafToSheaf J A).obj (Presheaf.freeYoneda X M)
+
+variable {J} in
+/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
+when `F : Sheaf J A`, `X : C` and `M : A`. -/
+noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
+    (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) :=
+  ((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv
+
+lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
+    IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
+  intro F G f g hfg
+  refine (sheafToPresheaf J A).map_injective ((Presheaf.isSeparating C hS) _ _ ?_)
+  rintro _ ⟨⟨X, i⟩, rfl⟩ a
+  dsimp at a
+  apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
+  simpa only [← Adjunction.homEquiv_naturality_right_symm] using
+    hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
+
+lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
+    [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))] [Preadditive A] :
+    IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) :=
+  (isSeparating J hS).isSeparator_coproduct
+
+variable (A) in
+instance hasSeparator [HasSeparator A] [Preadditive A]
+    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+    HasSeparator (Sheaf J A) where
+  hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
+      (by simpa using isSeparator_separator A)⟩
+
+end Sheaf
+
+end CategoryTheory

From ea2d7aee6539e6c9ac051b866934b5f40ed97582 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Dec 2024 21:51:09 +0100
Subject: [PATCH 21/46] cleaning up

---
 Mathlib.lean                                  | 10 +--
 .../ModuleCat/Presheaf/Generator.lean         |  2 +-
 .../Adjunction/AdjointFunctorTheorems.lean    |  2 +-
 .../Generator.lean => Generator/Abelian.lean} |  0
 .../{Generator.lean => Generator/Basic.lean}  |  0
 .../CategoryTheory/Generator/Coproduct.lean   | 45 ++++++++++++
 .../Preadditive.lean}                         |  2 +-
 .../Presheaf.lean}                            | 69 ++-----------------
 Mathlib/CategoryTheory/Generator/Sheaf.lean   | 68 ++++++++++++++++++
 9 files changed, 127 insertions(+), 71 deletions(-)
 rename Mathlib/CategoryTheory/{Abelian/Generator.lean => Generator/Abelian.lean} (100%)
 rename Mathlib/CategoryTheory/{Generator.lean => Generator/Basic.lean} (100%)
 create mode 100644 Mathlib/CategoryTheory/Generator/Coproduct.lean
 rename Mathlib/CategoryTheory/{Preadditive/Generator.lean => Generator/Preadditive.lean} (98%)
 rename Mathlib/CategoryTheory/{Sites/Generator.lean => Generator/Presheaf.lean} (51%)
 create mode 100644 Mathlib/CategoryTheory/Generator/Sheaf.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 351802a9644c3b..f408c5ed1a5d4f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1571,7 +1571,6 @@ import Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
 import Mathlib.CategoryTheory.Abelian.Exact
 import Mathlib.CategoryTheory.Abelian.Ext
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
-import Mathlib.CategoryTheory.Abelian.Generator
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
@@ -1759,7 +1758,12 @@ import Mathlib.CategoryTheory.Galois.GaloisObjects
 import Mathlib.CategoryTheory.Galois.IsFundamentalgroup
 import Mathlib.CategoryTheory.Galois.Prorepresentability
 import Mathlib.CategoryTheory.Galois.Topology
-import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Generator.Abelian
+import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Generator.Coproduct
+import Mathlib.CategoryTheory.Generator.Preadditive
+import Mathlib.CategoryTheory.Generator.Presheaf
+import Mathlib.CategoryTheory.Generator.Sheaf
 import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject
 import Mathlib.CategoryTheory.GradedObject.Associator
@@ -2034,7 +2038,6 @@ import Mathlib.CategoryTheory.Preadditive.Biproducts
 import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
 import Mathlib.CategoryTheory.Preadditive.EndoFunctor
 import Mathlib.CategoryTheory.Preadditive.FunctorCategory
-import Mathlib.CategoryTheory.Preadditive.Generator
 import Mathlib.CategoryTheory.Preadditive.HomOrthogonal
 import Mathlib.CategoryTheory.Preadditive.Injective
 import Mathlib.CategoryTheory.Preadditive.InjectiveResolution
@@ -2110,7 +2113,6 @@ import Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
 import Mathlib.CategoryTheory.Sites.EpiMono
 import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Equivalence
-import Mathlib.CategoryTheory.Sites.Generator
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
index 4cc999ebf5e900..0cea495d593055 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
@@ -8,7 +8,7 @@ import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
 import Mathlib.Algebra.Homology.ShortComplex.Exact
 import Mathlib.CategoryTheory.Elements
-import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Generator.Basic
 
 /-!
 # Generators for the category of presheaves of modules
diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
index 6d42354bbaaa34..374d018cb15082 100644
--- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
+++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Small
-import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Generator.Basic
 import Mathlib.CategoryTheory.Limits.ConeCategory
 import Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
 import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
diff --git a/Mathlib/CategoryTheory/Abelian/Generator.lean b/Mathlib/CategoryTheory/Generator/Abelian.lean
similarity index 100%
rename from Mathlib/CategoryTheory/Abelian/Generator.lean
rename to Mathlib/CategoryTheory/Generator/Abelian.lean
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator/Basic.lean
similarity index 100%
rename from Mathlib/CategoryTheory/Generator.lean
rename to Mathlib/CategoryTheory/Generator/Basic.lean
diff --git a/Mathlib/CategoryTheory/Generator/Coproduct.lean b/Mathlib/CategoryTheory/Generator/Coproduct.lean
new file mode 100644
index 00000000000000..8ac6f0302b0a1a
--- /dev/null
+++ b/Mathlib/CategoryTheory/Generator/Coproduct.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.Products
+
+/-!
+# The coproduct of a separating family of objects is separating
+
+-/
+
+universe w v u
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type u} [Category.{v} C] [HasZeroMorphisms C]
+
+namespace IsSeparating
+
+open Classical in
+lemma isSeparator_of_isColimit_cofan
+    {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S))
+    {c : Cofan S} (hc : IsColimit c) :
+    IsSeparator c.pt := by
+  intro X Y f g h
+  refine hS _ _ ?_
+  rintro _ ⟨i, rfl⟩ α
+  let β : c.pt ⟶ X := Cofan.IsColimit.desc hc
+      (fun j ↦ if hij : i = j then eqToHom (by rw [hij]) ≫ α else 0)
+  have hβ : c.inj i ≫ β = α := by simp [β]
+  simp only [← hβ, Category.assoc, h c.pt (by simp) β]
+
+lemma isSeparator_coproduct
+    {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S)) [HasCoproduct S] :
+    IsSeparator (∐ S) :=
+  isSeparator_of_isColimit_cofan hS (colimit.isColimit _)
+
+end IsSeparating
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Preadditive/Generator.lean b/Mathlib/CategoryTheory/Generator/Preadditive.lean
similarity index 98%
rename from Mathlib/CategoryTheory/Preadditive/Generator.lean
rename to Mathlib/CategoryTheory/Generator/Preadditive.lean
index f9a5abbe1b1fb6..7fa4d2290416ce 100644
--- a/Mathlib/CategoryTheory/Preadditive/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator/Preadditive.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Generator.Basic
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 
 /-!
diff --git a/Mathlib/CategoryTheory/Sites/Generator.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean
similarity index 51%
rename from Mathlib/CategoryTheory/Sites/Generator.lean
rename to Mathlib/CategoryTheory/Generator/Presheaf.lean
index a468148b1db4ed..982f7c62a523a0 100644
--- a/Mathlib/CategoryTheory/Sites/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean
@@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 
-import Mathlib.CategoryTheory.Limits.Shapes.Products
-import Mathlib.CategoryTheory.Sites.Sheafification
-import Mathlib.CategoryTheory.Sites.Limits
-import Mathlib.CategoryTheory.Generator
+import Mathlib.CategoryTheory.Generator.Coproduct
+import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 
 /-!
-# Generators in the category of sheaves
+# Generators in the category of presheaves
 
-In this file, we show that if `J : GrothendieckTopology C` and `A` is a preadditive
-category which has a separator (and suitable coproducts), then `Sheaf J A` has a separator.
+In this file, we show that if `A` is a preadditive category that has a separator (and
+suitable coproducts), then the category of presheaves `Cᵒᵖ ⥤ A` also has a separator.
 
 -/
 
@@ -23,20 +21,6 @@ namespace CategoryTheory
 
 open Limits Opposite
 
--- to be moved
-open Classical in
-lemma IsSeparating.isSeparator_coproduct {C : Type u} [Category.{v} C]
-    {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S)) [HasCoproduct S]
-    [HasZeroMorphisms C] :
-    IsSeparator (∐ S) := by
-  intro X Y f g h
-  refine hS _ _ ?_
-  rintro _ ⟨i, rfl⟩ α
-  let β : ∐ S ⟶ X := Sigma.desc
-    (fun j ↦ if hij : i = j then eqToHom (by rw [hij]) ≫ α else 0)
-  have hβ : Sigma.ι S i ≫ β = α := by simp [β]
-  simp only [← hβ, Category.assoc, h (∐ S) (by simp) β]
-
 namespace Presheaf
 
 variable {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
@@ -103,47 +87,4 @@ instance hasSeparator [HasSeparator A] [HasZeroMorphisms A]
 
 end Presheaf
 
-namespace Sheaf
-
-variable {C : Type u} [Category.{v} C]
-  (J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
-  [∀ (ι : Type v), HasCoproductsOfShape ι A]
-  [HasWeakSheafify J A]
-
-/-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
-sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
-noncomputable def freeYoneda (X : C) (M : A) : Sheaf J A :=
-  (presheafToSheaf J A).obj (Presheaf.freeYoneda X M)
-
-variable {J} in
-/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
-when `F : Sheaf J A`, `X : C` and `M : A`. -/
-noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
-    (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) :=
-  ((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv
-
-lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
-    IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
-  intro F G f g hfg
-  refine (sheafToPresheaf J A).map_injective ((Presheaf.isSeparating C hS) _ _ ?_)
-  rintro _ ⟨⟨X, i⟩, rfl⟩ a
-  dsimp at a
-  apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
-  simpa only [← Adjunction.homEquiv_naturality_right_symm] using
-    hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
-
-lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
-    [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))] [Preadditive A] :
-    IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) :=
-  (isSeparating J hS).isSeparator_coproduct
-
-variable (A) in
-instance hasSeparator [HasSeparator A] [Preadditive A]
-    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
-    HasSeparator (Sheaf J A) where
-  hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
-      (by simpa using isSeparator_separator A)⟩
-
-end Sheaf
-
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator/Sheaf.lean b/Mathlib/CategoryTheory/Generator/Sheaf.lean
new file mode 100644
index 00000000000000..d4883858f47881
--- /dev/null
+++ b/Mathlib/CategoryTheory/Generator/Sheaf.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.Generator.Presheaf
+import Mathlib.CategoryTheory.Sites.Sheafification
+import Mathlib.CategoryTheory.Sites.Limits
+
+/-!
+# Generators in the category of sheaves
+
+In this file, we show that if `J : GrothendieckTopology C` and `A` is a preadditive
+category which has a separator (and suitable coproducts), then `Sheaf J A` has a separator.
+
+-/
+
+universe w v' v u' u
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+namespace Sheaf
+
+variable {C : Type u} [Category.{v} C]
+  (J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
+  [∀ (ι : Type v), HasCoproductsOfShape ι A]
+  [HasWeakSheafify J A]
+
+/-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
+sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
+noncomputable def freeYoneda (X : C) (M : A) : Sheaf J A :=
+  (presheafToSheaf J A).obj (Presheaf.freeYoneda X M)
+
+variable {J} in
+/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
+when `F : Sheaf J A`, `X : C` and `M : A`. -/
+noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
+    (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) :=
+  ((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv
+
+lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
+    IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
+  intro F G f g hfg
+  refine (sheafToPresheaf J A).map_injective ((Presheaf.isSeparating C hS) _ _ ?_)
+  rintro _ ⟨⟨X, i⟩, rfl⟩ a
+  dsimp at a
+  apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
+  simpa only [← Adjunction.homEquiv_naturality_right_symm] using
+    hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
+
+lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
+    [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))] [Preadditive A] :
+    IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) :=
+  (isSeparating J hS).isSeparator_coproduct
+
+variable (A) in
+instance hasSeparator [HasSeparator A] [Preadditive A]
+    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+    HasSeparator (Sheaf J A) where
+  hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
+      (by simpa using isSeparator_separator A)⟩
+
+end Sheaf
+
+end CategoryTheory

From a66a6ee03f24f3012b75db88fb9efdde9276dc6f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Dec 2024 21:52:54 +0100
Subject: [PATCH 22/46] fixing imports

---
 Mathlib/CategoryTheory/Generator/Abelian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Generator/Abelian.lean b/Mathlib/CategoryTheory/Generator/Abelian.lean
index 18a35b536d306d..f803ac2bc56451 100644
--- a/Mathlib/CategoryTheory/Generator/Abelian.lean
+++ b/Mathlib/CategoryTheory/Generator/Abelian.lean
@@ -6,7 +6,7 @@ Authors: Markus Himmel
 import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Limits.EssentiallySmall
 import Mathlib.CategoryTheory.Preadditive.Injective
-import Mathlib.CategoryTheory.Preadditive.Generator
+import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Abelian.Opposite
 
 /-!

From 9bd83cdbb52c1498793bb6ee2d451a6226e4a1af Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 22:05:37 +0100
Subject: [PATCH 23/46] has limits and colimits

---
 .../Abelian/GrothendieckCategory.lean         | 103 +++++++-----------
 Mathlib/CategoryTheory/Abelian/Transfer.lean  |  14 +--
 2 files changed, 48 insertions(+), 69 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 76165fe5a2adb3..ad9d6e22e4cfd0 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 
-import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.Transfer
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.HasLimits
+import Mathlib.Logic.Equiv.TransferInstance
 
 /-!
 
@@ -69,80 +70,58 @@ theorem IsGrothendieckAbelian.of_equivalence
     exact hasExactColimitsOfShape_obj_of_equiv _ α
   · exact HasSeparator.of_equivalence α
 
-instance IsGrothendieckAbelian.shrinkHoms [IsGrothendieckAbelian.{w} C] :
+section ShrinkHoms
+
+instance ShrinkHoms.is_grothendieck_abelian [IsGrothendieckAbelian.{w} C] :
     IsGrothendieckAbelian.{w, w} (ShrinkHoms C) :=
   IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C
 
-noncomputable instance ShrinkHoms.homGroups [Preadditive C] (P Q : ShrinkHoms C) : AddCommGroup (P ⟶ Q) where
-  add f g := (equivShrink _ |>.symm) f + (equivShrink _ |>.symm) g |> equivShrink _
-  zero := 0 |> equivShrink _
-  nsmul n f := magnify f |> AddMonoid.nsmul n |> shrink
-  zsmul z f := magnify f |> SubNegMonoid.zsmul z |> shrink
-  neg f := - magnify f |> shrink
-  zero_add f := by
-    unfold HAdd.hAdd instHAdd OfNat.ofNat Zero.toOfNat0 Zero.zero HasZeroMorphisms.zero
-      Preadditive.preadditiveHasZeroMorphisms inferInstance NegZeroClass.toZero
-      SubNegZeroMonoid.toNegZeroClass AddMonoid.toZero SubNegMonoid.toAddMonoid
-      SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid
-      SubtractionMonoid.toSubNegMonoid SubtractionCommMonoid.toSubtractionMonoid
-      AddCommGroup.toDivisionAddCommMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup
-      Preadditive.homGroup
-    dsimp
-    simp only [Equiv.symm_apply_apply]
-    conv =>
-      lhs
-      apply congrArg
-      simp_rw [zero_add (equivShrink _ |>.symm f)]
-    erw [zero_add (equivShrink _ |>.symm f)]
-  add_zero := sorry
-  neg_add_cancel := sorry
-  nsmul_zero := sorry
-  nsmul_succ := sorry
-  zsmul_zero' := sorry
-  zsmul_neg' := sorry
-  zsmul_succ' := sorry
-  add_comm f g := congrArg _ <| add_comm _ _
-  add_assoc f g h := by
-    unfold HAdd.hAdd instHAdd
-    simp only [Equiv.symm_apply_apply]
-    exact congrArg _ <| add_assoc _ _ _
-where
-  shrink := equivShrink _
-  magnify := equivShrink _ |>.symm
-
-instance ShrinkHoms.preadditive [Preadditive C] : Preadditive (ShrinkHoms C) where
-  homGroup P Q := by
-    addCommGroup
-
-instance ShrinkHoms.abelian [Abelian C] : Abelian (ShrinkHoms C) :=
+noncomputable instance ShrinkHoms.preadditive [LocallySmall.{w} C] [Preadditive C] :
+    Preadditive.{w} (ShrinkHoms C) where
+  homGroup P Q := Equiv.addCommGroup (equivShrink _).symm
+  add_comp _ _ _ _ _ _ := by
+    apply congr_arg (equivShrink _)
+    conv => congr <;> congr <;> try apply Equiv.symm_apply_apply
+    apply Preadditive.add_comp
+  comp_add _ _ _ _ _ _ := by
+    apply congr_arg (equivShrink _)
+    conv => congr <;> congr <;> try apply Equiv.symm_apply_apply
+    apply Preadditive.comp_add
+
+-- Alternative? Not sure which is cleaner
+-- noncomputable instance ShrinkHoms.preadditive [Preadditive C] : Preadditive (ShrinkHoms C) := by
+--   refine ⟨fun _ _ => Equiv.addCommGroup (equivShrink _).symm, ?_, ?_⟩
+--   all_goals
+--     intros
+--     apply congr_arg (equivShrink _)
+--     conv => congr <;> congr <;> try apply (equivShrink _).symm_apply_apply
+--     first | apply Preadditive.add_comp | apply Preadditive.comp_add
+
+instance ShrinkHoms.has_limits [LocallySmall.{w} C] {J : Type*} [Category J]
+    [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
+  Adjunction.hasLimitsOfShape_of_equivalence (ShrinkHoms.equivalence C).inverse
+
+instance ShrinkHoms.has_finite_limits [LocallySmall.{w} C] [HasFiniteLimits C] :
+    HasFiniteLimits.{w} (ShrinkHoms C) :=
+  ⟨fun _ => inferInstance⟩
+
+universe w2 in
+noncomputable instance ShrinkHoms.abelian [Abelian C] [LocallySmall.{w} C] :
+    Abelian.{w} (ShrinkHoms C) :=
   abelianOfEquivalence (ShrinkHoms.equivalence C |>.inverse)
 
+end ShrinkHoms
 
 section Instances
 
 variable [Abelian C] [IsGrothendieckAbelian.{w} C]
 
--- instance IsGrothendieckAbelian.hasColimits : HasColimits C := has_colimits_of_finite_and_filtered
--- instance IsGrothendieckAbelian.hasLimits : HasLimits C := hasLimits_of_hasColimits_of_hasSeparator
-
-instance IsGrothendieckAbelian.hasColimitsOfSize' : HasColimitsOfSize.{w, w} C :=
+instance IsGrothendieckAbelian.has_colimits : HasColimitsOfSize.{w, w} C :=
   has_colimits_of_finite_and_filtered
 
-instance IsGrothendieckAbelian.hasLimitsOfSize' : HasLimitsOfSize.{w, w} C := by
-  --have : Abelian (ShrinkHoms C) := sorry
-  have : HasColimits.{w, u} (ShrinkHoms C) := IsGrothendieckAbelian.hasColimitsOfSize' _
+instance IsGrothendieckAbelian.has_limits : HasLimitsOfSize.{w, w} C :=
   have : HasLimits.{w, u} (ShrinkHoms C) := hasLimits_of_hasColimits_of_hasSeparator
-
-  done
-
--- instance IsGrothendieckAbelian.hasColimitsOfSize : HasColimitsOfSize.{w, w} (ShrinkHoms C) := by
---   have : HasColimitsOfSize.{w, w} C := has_colimits_of_finite_and_filtered
---   exact Adjunction.has_colimits_of_equivalence (ShrinkHoms.equivalence C |>.inverse)
-
-instance IsGrothendieckAbelian.hasLimitsOfSize : HasLimitsOfSize.{w, w} (ShrinkHoms C) := by
-  -- hasLimits_of_hasColimits_of_hasSeparator
-  have : HasLimitsOfSize.{w, w} C := hasLimits_of_hasColimits_of_hasSeparator
-  apply Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.inverse)
+  Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.functor)
 
 end Instances
 
diff --git a/Mathlib/CategoryTheory/Abelian/Transfer.lean b/Mathlib/CategoryTheory/Abelian/Transfer.lean
index edda974b2f59c0..a06000d76eed1e 100644
--- a/Mathlib/CategoryTheory/Abelian/Transfer.lean
+++ b/Mathlib/CategoryTheory/Abelian/Transfer.lean
@@ -37,12 +37,12 @@ namespace CategoryTheory
 
 open Limits
 
-universe v u₁ u₂
+universe v₁ v₂ u₁ u₂
 
 namespace AbelianOfAdjunction
 
-variable {C : Type u₁} [Category.{v} C] [Preadditive C]
-variable {D : Type u₂} [Category.{v} D] [Abelian D]
+variable {C : Type u₁} [Category.{v₁} C] [Preadditive C]
+variable {D : Type u₂} [Category.{v₂} D] [Abelian D]
 variable (F : C ⥤ D)
 variable (G : D ⥤ C) [Functor.PreservesZeroMorphisms G]
 
@@ -153,8 +153,8 @@ then `C` is also abelian.
 
 See <https://stacks.math.columbia.edu/tag/03A3>
 -/
-def abelianOfAdjunction {C : Type u₁} [Category.{v} C] [Preadditive C] [HasFiniteProducts C]
-    {D : Type u₂} [Category.{v} D] [Abelian D] (F : C ⥤ D) [Functor.PreservesZeroMorphisms F]
+def abelianOfAdjunction {C : Type u₁} [Category.{v₁} C] [Preadditive C] [HasFiniteProducts C]
+    {D : Type u₂} [Category.{v₂} D] [Abelian D] (F : C ⥤ D) [Functor.PreservesZeroMorphisms F]
     (G : D ⥤ C) [Functor.PreservesZeroMorphisms G] [PreservesFiniteLimits G] (i : F ⋙ G ≅ 𝟭 C)
     (adj : G ⊣ F) : Abelian C := by
   haveI := hasKernels F G i
@@ -169,8 +169,8 @@ def abelianOfAdjunction {C : Type u₁} [Category.{v} C] [Preadditive C] [HasFin
 via a functor that preserves zero morphisms,
 then `C` is also abelian.
 -/
-def abelianOfEquivalence {C : Type u₁} [Category.{v} C] [Preadditive C] [HasFiniteProducts C]
-    {D : Type u₂} [Category.{v} D] [Abelian D] (F : C ⥤ D) [Functor.PreservesZeroMorphisms F]
+def abelianOfEquivalence {C : Type u₁} [Category.{v₁} C] [Preadditive C] [HasFiniteProducts C]
+    {D : Type u₂} [Category.{v₂} D] [Abelian D] (F : C ⥤ D) [Functor.PreservesZeroMorphisms F]
     [F.IsEquivalence] : Abelian C :=
   abelianOfAdjunction F F.inv F.asEquivalence.unitIso.symm F.asEquivalence.symm.toAdjunction
 

From 83457ae02491b3577800b4f63b69dbb7d0db9044 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Dec 2024 22:08:34 +0100
Subject: [PATCH 24/46] better docstring

---
 Mathlib/CategoryTheory/Generator/Coproduct.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/CategoryTheory/Generator/Coproduct.lean b/Mathlib/CategoryTheory/Generator/Coproduct.lean
index 8ac6f0302b0a1a..07d7acae8c4d9b 100644
--- a/Mathlib/CategoryTheory/Generator/Coproduct.lean
+++ b/Mathlib/CategoryTheory/Generator/Coproduct.lean
@@ -10,6 +10,9 @@ import Mathlib.CategoryTheory.Limits.Shapes.Products
 /-!
 # The coproduct of a separating family of objects is separating
 
+If a family of objects `S : ι → C` in a category with zero morphisms
+is separating, then the coproduct of `S` is a separator in `C`.
+
 -/
 
 universe w v u

From ff4fee0f4f256e576618f06856b492b5942191f5 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 22:27:00 +0100
Subject: [PATCH 25/46] Has(Co)LimitsOfShape adjustments

---
 .../Abelian/GrothendieckAxioms/Basic.lean     | 31 +++++++++++------
 .../Abelian/GrothendieckCategory.lean         |  2 +-
 Mathlib/CategoryTheory/Generator.lean         | 34 ++++++++-----------
 3 files changed, 37 insertions(+), 30 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
index 2a675bd0a19b97..d16d729ecc2eef 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -123,16 +123,16 @@ Transport a `HasExactColimitsOfShape` along an equivalence of the shape.
 Note: When `C` has finite limits, this lemma holds with the equivalence replaced by a final
 functor, see `hasExactColimitsOfShape_of_final` below.
 -/
-lemma hasExactColimitsOfShape_of_equiv {J J' : Type*} [Category J] [Category J'] (e : J ≌ J')
-    [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
+lemma HasExactColimitsOfShape.of_domain_equivalence {J J' : Type*} [Category J] [Category J']
+    (e : J ≌ J') [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
     haveI : HasColimitsOfShape J' C := hasColimitsOfShape_of_equivalence e
     HasExactColimitsOfShape J' C :=
   haveI : HasColimitsOfShape J' C := hasColimitsOfShape_of_equivalence e
   ⟨preservesFiniteLimits_of_natIso (Functor.Final.colimIso e.functor)⟩
 
 variable {C} in
-lemma hasExactColimitsOfShape_obj_of_equiv (J : Type*) {D : Type*} [Category J] [Category D]
-    (e : C ≌ D) [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
+lemma HasExactColimitsOfShape.of_codomain_equivalence (J : Type*) [Category J] {D : Type*}
+    [Category D] (e : C ≌ D) [HasColimitsOfShape J C] [HasExactColimitsOfShape J C] :
     haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
     HasExactColimitsOfShape J D := by
   haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
@@ -147,13 +147,24 @@ Transport a `HasExactLimitsOfShape` along an equivalence of the shape.
 Note: When `C` has finite colimits, this lemma holds with the equivalence replaced by a initial
 functor, see `hasExactLimitsOfShape_of_initial` below.
 -/
-lemma hasExactLimitsOfShape_of_equiv {J J' : Type*} [Category J] [Category J'] (e : J ≌ J')
-    [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
+lemma HasExactLimitsOfShape.of_domain_equivalence {J J' : Type*} [Category J] [Category J']
+    (e : J ≌ J') [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
     haveI : HasLimitsOfShape J' C := hasLimitsOfShape_of_equivalence e
     HasExactLimitsOfShape J' C :=
   haveI : HasLimitsOfShape J' C := hasLimitsOfShape_of_equivalence e
   ⟨preservesFiniteColimits_of_natIso (Functor.Initial.limIso e.functor)⟩
 
+variable {C} in
+lemma HasExactLimitsOfShape.of_codomain_equivalence (J : Type*) [Category J] {D : Type*}
+    [Category D] (e : C ≌ D) [HasLimitsOfShape J C] [HasExactLimitsOfShape J C] :
+    haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
+    HasExactLimitsOfShape J D := by
+  haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
+  refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
+  refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)
+  apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
+  exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm
+
 /--
 A category `C` which has coproducts is said to have `AB4` of size `w` provided that
 coproducts of size `w` are exact.
@@ -175,7 +186,7 @@ lemma AB4OfSize_shrink [HasCoproducts.{max w w'} C] [AB4OfSize.{max w w'} C] :
     haveI : HasCoproducts.{w} C := hasCoproducts_shrink.{w, w'}
     AB4OfSize.{w} C :=
   haveI := hasCoproducts_shrink.{w, w'} (C := C)
-  ⟨fun J ↦ hasExactColimitsOfShape_of_equiv C
+  ⟨fun J ↦ HasExactColimitsOfShape.of_domain_equivalence C
     (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩
 
 instance (priority := 100) [HasCoproducts.{w} C] [AB4OfSize.{w} C] :
@@ -198,7 +209,7 @@ lemma AB4StarOfSize_shrink [HasProducts.{max w w'} C] [AB4StarOfSize.{max w w'}
     haveI : HasProducts.{w} C := hasProducts_shrink.{w, w'}
     AB4StarOfSize.{w} C :=
   haveI := hasProducts_shrink.{w, w'} (C := C)
-  ⟨fun J ↦ hasExactLimitsOfShape_of_equiv C
+  ⟨fun J ↦ HasExactLimitsOfShape.of_domain_equivalence C
     (Discrete.equivalence Equiv.ulift : Discrete (ULift.{w'} J) ≌ _)⟩
 
 instance (priority := 100) [HasProducts.{w} C] [AB4StarOfSize.{w} C] :
@@ -256,7 +267,7 @@ lemma AB5OfSize_of_univLE [HasFilteredColimitsOfSize.{w₂, w₂'} C] [UnivLE.{w
   intro J _ _
   haveI := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
     Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
-  exact hasExactColimitsOfShape_of_equiv _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
+  exact HasExactColimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
     Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
 
 lemma AB5OfSize_shrink [HasFilteredColimitsOfSize.{max w w₂, max w' w₂'} C]
@@ -290,7 +301,7 @@ lemma AB5StarOfSize_of_univLE [HasCofilteredLimitsOfSize.{w₂, w₂'} C] [UnivL
   intro J _ _
   haveI := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
     Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
-  exact hasExactLimitsOfShape_of_equiv _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
+  exact HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
     Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
 
 lemma AB5StarOfSize_shrink [HasCofilteredLimitsOfSize.{max w w₂, max w' w₂'} C]
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index ad9d6e22e4cfd0..e2928a41c46162 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -67,7 +67,7 @@ theorem IsGrothendieckAbelian.of_equivalence
   refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
   · exact locallySmall_of_faithful α.inverse
   · refine ⟨fun _ _ _ => ?_⟩
-    exact hasExactColimitsOfShape_obj_of_equiv _ α
+    exact HasExactColimitsOfShape.of_codomain_equivalence _ α
   · exact HasSeparator.of_equivalence α
 
 section ShrinkHoms
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index 1c33c205c400e7..1dd0f45fc20611 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -80,6 +80,18 @@ def IsDetecting (𝒢 : Set C) : Prop :=
 def IsCodetecting (𝒢 : Set C) : Prop :=
   ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h) → IsIso f
 
+section Equivalence
+
+lemma IsSeparating.of_equivalence
+    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (e : C ≌ D) :
+    IsSeparating (e.functor.obj '' 𝒢) := fun X Y f g H =>
+  e.inverse.map_injective (h _ _ (fun Z hZ h => by
+    obtain ⟨h', rfl⟩ := (e.toAdjunction.homEquiv _ _).surjective h
+    simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
+      H (e.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))
+
+end Equivalence
+
 section Dual
 
 theorem isSeparating_op_iff (𝒢 : Set C) : IsSeparating 𝒢.op ↔ IsCoseparating 𝒢 := by
@@ -354,24 +366,8 @@ def IsCodetector (G : C) : Prop :=
 
 section Equivalence
 
-theorem IsSeparator.isSeparator_obj_of_equivalence {G : C} (hC : IsSeparator G) (F : C ⥤ D)
-    [F.IsEquivalence] :
-    IsSeparator (F.obj G) := by
-  let α := F.asEquivalence
-  intro d₁ d₂ f g hD
-  suffices h : α.inverse.map f = α.inverse.map g by
-    have h := congrArg α.functor.map h
-    simp only [Equivalence.fun_inv_map, Functor.comp_obj, Functor.id_obj,
-      NatIso.cancel_natIso_hom_left] at h
-    have h := congrArg (· ≫ α.counit.app d₂) h
-    simpa using h
-  apply hC
-  intro _ hG' hh
-  cases hG'
-  have := hD (α.functor.obj G) rfl (Adjunction.homEquiv α.toAdjunction G d₁ |>.symm hh)
-  have := congrArg (Adjunction.homEquiv α.toAdjunction G d₂) this
-  simp only [Adjunction.homEquiv_apply, Functor.map_comp, Adjunction.homEquiv_symm_apply] at this
-  simpa
+theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (F : C ⥤ D) [F.IsEquivalence] :
+    IsSeparator (F.obj G) := by simpa using IsSeparating.of_equivalence h (F.asEquivalence)
 
 end Equivalence
 
@@ -731,7 +727,7 @@ end Instances
 section Equivalence
 
 theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
-  ⟨α.functor.obj (separator C), isSeparator_separator C |>.isSeparator_obj_of_equivalence α.functor⟩
+  ⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α.functor⟩
 
 end Equivalence
 

From 1844a75b081001d7609eab8c73942f55957f59b2 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 22:28:37 +0100
Subject: [PATCH 26/46] fix Mathlib.lean

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 23d2655db7be28..f10e24235b851e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1575,7 +1575,6 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
->>>>>>> origin/master
 import Mathlib.CategoryTheory.Abelian.Images
 import Mathlib.CategoryTheory.Abelian.Injective
 import Mathlib.CategoryTheory.Abelian.InjectiveResolution

From 6dbbef0d7b9bf086461aad37fb6d6101b5007f20 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 23:04:26 +0100
Subject: [PATCH 27/46] make IsSeparating.of_equivalence more convenient and
 dualize

---
 Mathlib/CategoryTheory/Generator.lean | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index 1dd0f45fc20611..6bb724682c8b11 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -83,12 +83,21 @@ def IsCodetecting (𝒢 : Set C) : Prop :=
 section Equivalence
 
 lemma IsSeparating.of_equivalence
-    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (e : C ≌ D) :
-    IsSeparating (e.functor.obj '' 𝒢) := fun X Y f g H =>
-  e.inverse.map_injective (h _ _ (fun Z hZ h => by
-    obtain ⟨h', rfl⟩ := (e.toAdjunction.homEquiv _ _).surjective h
+    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (F : C ⥤ D) [F.IsEquivalence] :
+    IsSeparating (F.obj '' 𝒢) := fun X Y f g H =>
+  F.asEquivalence.inverse.map_injective (h _ _ (fun Z hZ h => by
+    obtain ⟨h', rfl⟩ := (F.asEquivalence.toAdjunction.homEquiv _ _).surjective h
     simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
-      H (e.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))
+      H (F.obj Z) (Set.mem_image_of_mem _ hZ) h']))
+
+lemma IsCoseparating.of_equivalence
+    {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (F : C ⥤ D) [F.IsEquivalence] :
+    IsCoseparating (F.obj '' 𝒢) := fun X Y f g H =>
+  F.asEquivalence.inverse.map_injective (h _ _ (fun Z hZ h => by
+    have h' := (F.asEquivalence.symm.toAdjunction.homEquiv _ _) h
+    obtain ⟨h', rfl⟩ := (F.asEquivalence.symm.toAdjunction.homEquiv _ _).symm.surjective h
+    simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp,
+      Equivalence.symm_functor, H (F.obj Z) (Set.mem_image_of_mem _ hZ) h']))
 
 end Equivalence
 
@@ -367,7 +376,10 @@ def IsCodetector (G : C) : Prop :=
 section Equivalence
 
 theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (F : C ⥤ D) [F.IsEquivalence] :
-    IsSeparator (F.obj G) := by simpa using IsSeparating.of_equivalence h (F.asEquivalence)
+    IsSeparator (F.obj G) := by simpa using IsSeparating.of_equivalence h F
+
+theorem IsCoseparator.of_equivalence {G : C} (h : IsCoseparator G) (F : C ⥤ D) [F.IsEquivalence] :
+    IsCoseparator (F.obj G) := by simpa using IsCoseparating.of_equivalence h F
 
 end Equivalence
 

From 239174e3e4d5fb2cdfcfe8b267b3c88ab53c40e6 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 23:07:28 +0100
Subject: [PATCH 28/46] add HasCoseparator.of_equivalence and extend docstring

---
 Mathlib/CategoryTheory/Generator.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index 6bb724682c8b11..74b348d073ea97 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -26,6 +26,7 @@ There are, of course, also the dual notions of coseparating and codetecting sets
 We
 * define predicates `IsSeparating`, `IsCoseparating`, `IsDetecting` and `IsCodetecting` on
   sets of objects;
+* show that equivalences of categories preserves these notions;
 * show that separating and coseparating are dual notions;
 * show that detecting and codetecting are dual notions;
 * show that if `C` has equalizers, then detecting implies separating;
@@ -741,6 +742,9 @@ section Equivalence
 theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
   ⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α.functor⟩
 
+theorem HasCoseparator.of_equivalence [HasCoseparator C] (α : C ≌ D) : HasCoseparator D :=
+  ⟨α.functor.obj (coseparator C), isCoseparator_coseparator C |>.of_equivalence α.functor⟩
+
 end Equivalence
 
 section Dual

From 488c80314cf1f944b9f8c4b9e6763e14a1fd9099 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 15 Dec 2024 23:59:44 +0100
Subject: [PATCH 29/46] process some remarks and fix linter error

---
 .../Abelian/GrothendieckCategory.lean         | 47 ++---------------
 Mathlib/CategoryTheory/Abelian/Transfer.lean  | 51 ++++++++++++++++++-
 Mathlib/CategoryTheory/EssentiallySmall.lean  |  4 ++
 Mathlib/CategoryTheory/Generator.lean         | 33 ++++++------
 4 files changed, 74 insertions(+), 61 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index e2928a41c46162..2ca7d0afbe14b1 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -10,7 +10,6 @@ import Mathlib.CategoryTheory.Abelian.Transfer
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.HasLimits
-import Mathlib.Logic.Equiv.TransferInstance
 
 /-!
 
@@ -44,12 +43,12 @@ variable (C : Type u) [Category.{v} C] (D : Type u₂) [Category.{v₂} D]
 In the literature, an abelian category `C` is called a Grothendieck category provided that it has
 `AB5` and a separator (see `HasSeparator`).
 
-`IsGrothendieckAbelian C` is defined such that it holds if and only if `C` is equivalent to a
+`IsGrothendieckAbelian.{w} C` is defined such that it holds if and only if `C` is equivalent to a
 Grothendieck category -- more concretely, if and only if `ShrinkHoms.{w} C` is a Grothendieck
 category.
 -/
 @[stacks 079B]
-class IsGrothendieckAbelian : Prop where
+class IsGrothendieckAbelian [Abelian C] : Prop where
   locallySmall : LocallySmall.{w} C := by infer_instance
   hasFilteredColimitsOfSize : HasFilteredColimitsOfSize.{w, w} C := by infer_instance
   ab5OfSize : AB5OfSize.{w, w} C := by infer_instance
@@ -60,7 +59,7 @@ attribute [instance] IsGrothendieckAbelian.locallySmall
   IsGrothendieckAbelian.hasSeparator
 
 variable {C} {D} in
-theorem IsGrothendieckAbelian.of_equivalence
+theorem IsGrothendieckAbelian.of_equivalence [Abelian C] [Abelian D]
     [IsGrothendieckAbelian.{w} C] (α : C ≌ D) : IsGrothendieckAbelian.{w} D := by
   have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
     ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
@@ -70,48 +69,10 @@ theorem IsGrothendieckAbelian.of_equivalence
     exact HasExactColimitsOfShape.of_codomain_equivalence _ α
   · exact HasSeparator.of_equivalence α
 
-section ShrinkHoms
-
-instance ShrinkHoms.is_grothendieck_abelian [IsGrothendieckAbelian.{w} C] :
+instance ShrinkHoms.isGrothendieckAbelian [Abelian C] [IsGrothendieckAbelian.{w} C] :
     IsGrothendieckAbelian.{w, w} (ShrinkHoms C) :=
   IsGrothendieckAbelian.of_equivalence <| ShrinkHoms.equivalence C
 
-noncomputable instance ShrinkHoms.preadditive [LocallySmall.{w} C] [Preadditive C] :
-    Preadditive.{w} (ShrinkHoms C) where
-  homGroup P Q := Equiv.addCommGroup (equivShrink _).symm
-  add_comp _ _ _ _ _ _ := by
-    apply congr_arg (equivShrink _)
-    conv => congr <;> congr <;> try apply Equiv.symm_apply_apply
-    apply Preadditive.add_comp
-  comp_add _ _ _ _ _ _ := by
-    apply congr_arg (equivShrink _)
-    conv => congr <;> congr <;> try apply Equiv.symm_apply_apply
-    apply Preadditive.comp_add
-
--- Alternative? Not sure which is cleaner
--- noncomputable instance ShrinkHoms.preadditive [Preadditive C] : Preadditive (ShrinkHoms C) := by
---   refine ⟨fun _ _ => Equiv.addCommGroup (equivShrink _).symm, ?_, ?_⟩
---   all_goals
---     intros
---     apply congr_arg (equivShrink _)
---     conv => congr <;> congr <;> try apply (equivShrink _).symm_apply_apply
---     first | apply Preadditive.add_comp | apply Preadditive.comp_add
-
-instance ShrinkHoms.has_limits [LocallySmall.{w} C] {J : Type*} [Category J]
-    [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
-  Adjunction.hasLimitsOfShape_of_equivalence (ShrinkHoms.equivalence C).inverse
-
-instance ShrinkHoms.has_finite_limits [LocallySmall.{w} C] [HasFiniteLimits C] :
-    HasFiniteLimits.{w} (ShrinkHoms C) :=
-  ⟨fun _ => inferInstance⟩
-
-universe w2 in
-noncomputable instance ShrinkHoms.abelian [Abelian C] [LocallySmall.{w} C] :
-    Abelian.{w} (ShrinkHoms C) :=
-  abelianOfEquivalence (ShrinkHoms.equivalence C |>.inverse)
-
-end ShrinkHoms
-
 section Instances
 
 variable [Abelian C] [IsGrothendieckAbelian.{w} C]
diff --git a/Mathlib/CategoryTheory/Abelian/Transfer.lean b/Mathlib/CategoryTheory/Abelian/Transfer.lean
index a06000d76eed1e..8072e2624418c2 100644
--- a/Mathlib/CategoryTheory/Abelian/Transfer.lean
+++ b/Mathlib/CategoryTheory/Abelian/Transfer.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.CategoryTheory.Abelian.Basic
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
 import Mathlib.CategoryTheory.Adjunction.Limits
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
+import Mathlib.Logic.Equiv.TransferInstance
 
 /-!
 # Transferring "abelian-ness" across a functor
@@ -174,4 +176,51 @@ def abelianOfEquivalence {C : Type u₁} [Category.{v₁} C] [Preadditive C] [Ha
     [F.IsEquivalence] : Abelian C :=
   abelianOfAdjunction F F.inv F.asEquivalence.unitIso.symm F.asEquivalence.symm.toAdjunction
 
+namespace ShrinkHoms
+
+universe w
+
+variable (C : Type*) [Category C] [LocallySmall.{w} C] [Preadditive C]
+
+noncomputable instance homGroup (P Q : ShrinkHoms C) : AddCommGroup (P ⟶ Q : Type w) :=
+  Equiv.addCommGroup (equivShrink _).symm
+
+lemma functor_map_add {P Q : C} (f g : P ⟶ Q) :
+    (functor C).map (f + g) =
+      (functor C).map f + (functor C).map g :=
+  map_add (equivShrink.{w} (P ⟶ Q)).symm.addEquiv.symm f g
+
+lemma inverse_map_add {P Q : ShrinkHoms C} (f g : P ⟶ Q) :
+    (inverse C).map (f + g) =
+      (inverse C).map f + (ShrinkHoms.inverse C).map g :=
+  map_add (equivShrink.{w} (P.fromShrinkHoms ⟶ Q.fromShrinkHoms)).symm.addEquiv f g
+
+noncomputable instance preadditive [Preadditive C] :
+    Preadditive.{w} (ShrinkHoms C) where
+  homGroup P Q := Equiv.addCommGroup (equivShrink _).symm
+  add_comp _ _ _ _ _ _ := by
+    apply (inverse C).map_injective
+    simp only [inverse_map_add, Functor.map_comp, Preadditive.add_comp]
+  comp_add _ _ _ _ _ _ := by
+    apply (inverse C).map_injective
+    simp only [inverse_map_add, Functor.map_comp, Preadditive.comp_add]
+
+instance : (inverse C).Additive where
+  map_add := by apply inverse_map_add
+
+instance : (functor C).Additive where
+  map_add := by apply functor_map_add
+
+instance hasLimits [LocallySmall.{w} C] {J : Type*} [Category J]
+    [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
+  Adjunction.hasLimitsOfShape_of_equivalence (inverse C)
+
+instance hasFiniteLimits [LocallySmall.{w} C] [HasFiniteLimits C] :
+    HasFiniteLimits.{w} (ShrinkHoms C) := ⟨fun _ => inferInstance⟩
+
+noncomputable instance abelian [Abelian C] [LocallySmall.{w} C] :
+    Abelian.{w} (ShrinkHoms C) := abelianOfEquivalence (inverse C)
+
+end ShrinkHoms
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
index 70c065ab24e7b5..56e79934d2ba99 100644
--- a/Mathlib/CategoryTheory/EssentiallySmall.lean
+++ b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -174,6 +174,9 @@ noncomputable def equivalence : C ≌ ShrinkHoms C where
   unitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)
   counitIso := NatIso.ofComponents (fun _ ↦ Iso.refl _)
 
+instance : (functor C).IsEquivalence := (equivalence C).isEquivalence_functor
+instance : (inverse C).IsEquivalence := (equivalence C).isEquivalence_inverse
+
 end ShrinkHoms
 
 namespace Shrink
@@ -240,4 +243,5 @@ theorem essentiallySmall_iff_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThi
 
 instance [Small.{w} C] : Small.{w} (Discrete C) := small_map discreteEquiv
 
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean
index 74b348d073ea97..78a17790ce9fb0 100644
--- a/Mathlib/CategoryTheory/Generator.lean
+++ b/Mathlib/CategoryTheory/Generator.lean
@@ -84,21 +84,20 @@ def IsCodetecting (𝒢 : Set C) : Prop :=
 section Equivalence
 
 lemma IsSeparating.of_equivalence
-    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (F : C ⥤ D) [F.IsEquivalence] :
-    IsSeparating (F.obj '' 𝒢) := fun X Y f g H =>
-  F.asEquivalence.inverse.map_injective (h _ _ (fun Z hZ h => by
-    obtain ⟨h', rfl⟩ := (F.asEquivalence.toAdjunction.homEquiv _ _).surjective h
+    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) :
+    IsSeparating (α.functor.obj '' 𝒢) := fun X Y f g H =>
+  α.inverse.map_injective (h _ _ (fun Z hZ h => by
+    obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h
     simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
-      H (F.obj Z) (Set.mem_image_of_mem _ hZ) h']))
+      H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))
 
 lemma IsCoseparating.of_equivalence
-    {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (F : C ⥤ D) [F.IsEquivalence] :
-    IsCoseparating (F.obj '' 𝒢) := fun X Y f g H =>
-  F.asEquivalence.inverse.map_injective (h _ _ (fun Z hZ h => by
-    have h' := (F.asEquivalence.symm.toAdjunction.homEquiv _ _) h
-    obtain ⟨h', rfl⟩ := (F.asEquivalence.symm.toAdjunction.homEquiv _ _).symm.surjective h
+    {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) :
+    IsCoseparating (α.functor.obj '' 𝒢) := fun X Y f g H =>
+  α.inverse.map_injective (h _ _ (fun Z hZ h => by
+    obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h
     simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp,
-      Equivalence.symm_functor, H (F.obj Z) (Set.mem_image_of_mem _ hZ) h']))
+      Equivalence.symm_functor, H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))
 
 end Equivalence
 
@@ -376,11 +375,11 @@ def IsCodetector (G : C) : Prop :=
 
 section Equivalence
 
-theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (F : C ⥤ D) [F.IsEquivalence] :
-    IsSeparator (F.obj G) := by simpa using IsSeparating.of_equivalence h F
+theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (α : C ≌ D) :
+    IsSeparator (α.functor.obj G) := by simpa using IsSeparating.of_equivalence h α
 
-theorem IsCoseparator.of_equivalence {G : C} (h : IsCoseparator G) (F : C ⥤ D) [F.IsEquivalence] :
-    IsCoseparator (F.obj G) := by simpa using IsCoseparating.of_equivalence h F
+theorem IsCoseparator.of_equivalence {G : C} (h : IsCoseparator G) (α : C ≌ D) :
+    IsCoseparator (α.functor.obj G) := by simpa using IsCoseparating.of_equivalence h α
 
 end Equivalence
 
@@ -740,10 +739,10 @@ end Instances
 section Equivalence
 
 theorem HasSeparator.of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
-  ⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α.functor⟩
+  ⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α⟩
 
 theorem HasCoseparator.of_equivalence [HasCoseparator C] (α : C ≌ D) : HasCoseparator D :=
-  ⟨α.functor.obj (coseparator C), isCoseparator_coseparator C |>.of_equivalence α.functor⟩
+  ⟨α.functor.obj (coseparator C), isCoseparator_coseparator C |>.of_equivalence α⟩
 
 end Equivalence
 

From 0a58d78503c08f258bef43cbfbbe2cb64396be95 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 00:03:43 +0100
Subject: [PATCH 30/46] use camel case

---
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 2ca7d0afbe14b1..ac8481ee991708 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -77,10 +77,10 @@ section Instances
 
 variable [Abelian C] [IsGrothendieckAbelian.{w} C]
 
-instance IsGrothendieckAbelian.has_colimits : HasColimitsOfSize.{w, w} C :=
+instance IsGrothendieckAbelian.hasColimits : HasColimitsOfSize.{w, w} C :=
   has_colimits_of_finite_and_filtered
 
-instance IsGrothendieckAbelian.has_limits : HasLimitsOfSize.{w, w} C :=
+instance IsGrothendieckAbelian.hasLimits : HasLimitsOfSize.{w, w} C :=
   have : HasLimits.{w, u} (ShrinkHoms C) := hasLimits_of_hasColimits_of_hasSeparator
   Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.functor)
 

From de7aa907ae0285ff4fb1069c50854012195624a1 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 00:08:24 +0100
Subject: [PATCH 31/46] remove empty line

---
 Mathlib/CategoryTheory/EssentiallySmall.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
index 56e79934d2ba99..f041cca1723b94 100644
--- a/Mathlib/CategoryTheory/EssentiallySmall.lean
+++ b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -243,5 +243,4 @@ theorem essentiallySmall_iff_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThi
 
 instance [Small.{w} C] : Small.{w} (Discrete C) := small_map discreteEquiv
 
-
 end CategoryTheory

From 96793268950ad17a8bfa37125e094ac1a54a55fa Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 00:41:27 +0100
Subject: [PATCH 32/46] remove unused import

---
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index ac8481ee991708..1913952f29a233 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -8,7 +8,6 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.Transfer
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
-import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Limits.HasLimits
 
 /-!

From 1bccbf1640f1da46d64bd6f7205925d7feb26a56 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 01:02:58 +0100
Subject: [PATCH 33/46] feat(CategoryTheory/Sites): categories of sheaves are
 Grothendieck abelian

---
 Mathlib.lean                                  |   1 +
 .../Sites/GrothendieckAbelian.lean            | 157 ++++++++++++++++++
 2 files changed, 158 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d00e5f67301d1c..7f112a83ccd379 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2115,6 +2115,7 @@ import Mathlib.CategoryTheory.Sites.EpiMono
 import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.CategoryTheory.Sites.Grothendieck
+import Mathlib.CategoryTheory.Sites.GrothendieckAbelian
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
 import Mathlib.CategoryTheory.Sites.LeftExact
diff --git a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
new file mode 100644
index 00000000000000..c7f556892b8da2
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
+import Mathlib.CategoryTheory.Generator.Sheaf
+import Mathlib.CategoryTheory.Sites.Abelian
+
+/-!
+# Categories of sheaves are Grothendieck abelian
+
+If `J` is a Grothendieck topology on a small category `C : Type v`,
+and `A : Type u` (with `Category.{v} A`) is a Grothendieck abelian category,
+then `Sheaf J A` is a Grothendieck abelian category.
+
+-/
+
+universe v'' v' v u'' u' u
+
+namespace CategoryTheory
+
+open Limits
+
+-- this should be moved
+namespace Adjunction
+
+variable {C : Type u} {D : Type u'} [Category.{v} C] [Category.{v'} D]
+  {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
+  {K : Type u''} [Category.{v''} K]
+  [G.Faithful] [G.Full]
+
+namespace colimIso
+
+variable {P : K ⥤ D} (c : Cocone (P ⋙ G)) (hc : IsColimit c)
+
+/-- A cocone for `P : K ⥤ D` deduced from a cocone for `P ⋙ G` when `adj : F ⊣ G`
+is an adjunction such that `G : D ⥤ C` is fully faithful. -/
+@[simps pt]
+noncomputable def cocone : Cocone P where
+  pt := F.obj c.pt
+  ι :=
+    { app k := G.preimage (c.ι.app k ≫ adj.unit.app _)
+      naturality k k' f := by
+        apply G.map_injective
+        have := c.w f
+        dsimp at this
+        simp [reassoc_of% this]}
+
+@[simp]
+lemma map_cocone_ι_app (k : K) :
+    G.map ((cocone adj c).ι.app k) = c.ι.app k ≫ adj.unit.app _ := by
+  simp [cocone]
+
+namespace isColimitCocone
+
+variable {c}
+
+/-- Auxiliary definition for `Adjunction.isColimitCocone`. -/
+noncomputable def desc (s : Cocone P) : F.obj c.pt ⟶ s.pt :=
+  (adj.homEquiv _ _).symm (hc.desc (G.mapCocone s))
+
+@[reassoc]
+lemma fac (s : Cocone P) (k : K) :
+    (cocone adj c).ι.app k ≫ isColimitCocone.desc adj hc s = s.ι.app k :=
+  G.map_injective (by simp [desc, homEquiv_counit])
+
+include hc in
+lemma uniq {s : Cocone P} {f g : F.obj c.pt ⟶ s.pt}
+    (h : ∀ (k : K), (cocone adj c).ι.app k ≫ f = (cocone adj c).ι.app k ≫ g) : f = g :=
+  (adj.homEquiv _ _).injective
+    (hc.hom_ext (fun k ↦ by simpa [homEquiv_unit] using G.congr_map (h k)))
+
+end isColimitCocone
+
+/-- Given an adjunction `adj : F ⊣ G` such that `G : D ⥤ C` is fully faithful,
+this is a construction of a colimit cocone for `P : K ⥤ D` from a colimit
+cocone for `P ⋙ G`. -/
+noncomputable def isColimitCocone : IsColimit (cocone adj c) where
+  desc s := isColimitCocone.desc adj hc s
+  fac s k := isColimitCocone.fac adj hc s k
+  uniq s m hm := isColimitCocone.uniq adj hc (fun _ ↦ by rw [isColimitCocone.fac, hm])
+
+end colimIso
+
+variable [HasColimitsOfShape K C] [HasColimitsOfShape K D]
+
+/-- If `adj : F ⊣ G` is an adjuncton such that `G` is fully faithful, this is the
+isomorphism between the colimit of `P : K ⥤ D` and the image by `F` of
+the colimit of `P ⋙ G`. -/
+noncomputable def colimIsoObj (P : K ⥤ D) : colimit P ≅ F.obj (colimit (P ⋙ G)) :=
+  IsColimit.coconePointUniqueUpToIso (colimit.isColimit P)
+      (colimIso.isColimitCocone adj _ (colimit.isColimit (P ⋙ G)))
+
+@[reassoc]
+lemma ι_colimIsoObj_hom (P : K ⥤ D) (k : K) :
+    colimit.ι P k ≫ (colimIsoObj adj P).hom =
+      (colimIso.cocone adj (colimit.cocone (P ⋙ G))).ι.app k :=
+  IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _
+
+variable (K)
+
+/-- If `adj : F ⊣ G` is an adjuncton such that `G` is fully faithful, this is the
+natural isomorphism between the colimit of `P : K ⥤ D` and the image by `F` of
+the colimit of `P ⋙ G`. -/
+noncomputable def colimIso : colim (J := K) (C := D) ≅
+    (whiskeringRight _ _ _).obj G ⋙ colim (J := K) (C := C) ⋙ F :=
+  NatIso.ofComponents adj.colimIsoObj (fun {P Q} f ↦ by
+    dsimp
+    ext k
+    rw [ι_colimMap_assoc, ι_colimIsoObj_hom, ι_colimIsoObj_hom_assoc]
+    apply G.map_injective
+    simp)
+
+include adj in
+lemma hasExactColimitsOfShape [HasExactColimitsOfShape K C] [Abelian D]
+    [F.PreservesMonomorphisms] :
+    HasExactColimitsOfShape K D := by
+  suffices (colim (J := K) (C := D)).PreservesMonomorphisms by
+    apply hasExactColimitsOfShape_of_preservesMono
+  have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
+  apply Functor.preservesMonomorphisms.of_iso (adj.colimIso K).symm
+
+end Adjunction
+
+namespace Sheaf
+
+-- part of this should to moved to Abelian.GrothendieckAxioms.Sheaf
+
+instance hasExactColimitsOfShape
+    {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+    (A : Type u') [Category.{v'} A] [Abelian A]
+    (K : Type u'') [Category.{v''} K] [HasSheafify J A] [HasColimitsOfShape K A]
+    [HasExactColimitsOfShape K A] :
+    HasExactColimitsOfShape K (Sheaf J A) :=
+  (sheafificationAdjunction J A).hasExactColimitsOfShape K
+
+instance hasFilteredColimitsOfSize {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+    (A : Type u') [Category.{v'} A] [HasSheafify J A]
+    [HasFilteredColimitsOfSize.{v'', u''} A] :
+    HasFilteredColimitsOfSize.{v'', u''} (Sheaf J A) where
+  HasColimitsOfShape K := by infer_instance
+
+instance ab5ofSize {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
+    (A : Type u') [Category.{v'} A] [Abelian A] [HasSheafify J A]
+    [HasFilteredColimitsOfSize.{v'', u''} A] [AB5OfSize.{v'', u''} A] :
+    AB5OfSize.{v'', u''} (Sheaf J A) where
+  ofShape K _ _ := by infer_instance
+
+instance {C : Type v} [SmallCategory C] (J : GrothendieckTopology C) (A : Type u)
+    [Category.{v} A] [Abelian A] [IsGrothendieckAbelian.{v} A]
+    [HasSheafify J A] : IsGrothendieckAbelian.{v} (Sheaf J A) where
+
+end Sheaf
+
+end CategoryTheory

From 2882f8216a2e6bfd878c00811c872ee17b69ef24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 01:07:19 +0100
Subject: [PATCH 34/46] typo

---
 Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
index c7f556892b8da2..384718a214a567 100644
--- a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
+++ b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
@@ -126,7 +126,7 @@ end Adjunction
 
 namespace Sheaf
 
--- part of this should to moved to Abelian.GrothendieckAxioms.Sheaf
+-- part of this should be moved to Abelian.GrothendieckAxioms.Sheaf
 
 instance hasExactColimitsOfShape
     {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)

From 79ea57dff61c5afb90f0b88b5d2fc89447a7eed8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 01:07:30 +0100
Subject: [PATCH 35/46] wip

---
 Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
index 384718a214a567..f92024fd857391 100644
--- a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
+++ b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
@@ -126,7 +126,7 @@ end Adjunction
 
 namespace Sheaf
 
--- part of this should be moved to Abelian.GrothendieckAxioms.Sheaf
+-- this should be moved to Abelian.GrothendieckAxioms.Sheaf
 
 instance hasExactColimitsOfShape
     {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)

From 8d7caabaf952b9741bd01d8115b274220b6220eb Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 16:26:47 +0100
Subject: [PATCH 36/46] extend docstrings, process remarks

---
 .../Abelian/GrothendieckAxioms/Basic.lean     |  5 ++-
 .../Abelian/GrothendieckCategory.lean         | 34 ++++++++++++++-----
 Mathlib/CategoryTheory/Abelian/Transfer.lean  | 28 ++++++++++-----
 3 files changed, 49 insertions(+), 18 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
index d16d729ecc2eef..b96f54ec72e3b3 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -18,7 +18,7 @@ basic facts about them.
 
 ## Definitions
 
-- `HasExactColimitsOfShape J` -- colimits of shape `J` are exact.
+- `HasExactColimitsOfShape J C` -- colimits of shape `J` in `C` are exact.
 - The dual of the above definitions, called `HasExactLimitsOfShape`.
 - `AB4` -- coproducts are exact (this is formulated in terms of `HasExactColimitsOfShape`).
 - `AB5` -- filtered colimits are exact (this is formulated in terms of `HasExactColimitsOfShape`).
@@ -26,6 +26,9 @@ basic facts about them.
 ## Theorems
 
 - The implication from `AB5` to `AB4` is established in `AB4.ofAB5`.
+- That `HasExactColimitsOfShape J C` is invariant under equivalences in both parameters is shown
+in `HasExactColimitsOfShape.of_domain_equivalence` and
+`HasExactColimitsOfShape.of_codomain_equivalence`.
 
 ## Remarks
 
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 1913952f29a233..89834bd495c6e1 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -18,12 +18,22 @@ This file defines Grothendieck categories and proves basic facts about them.
 
 ## Definitions
 
-A `GrothendieckCategory` is an abelian category provided that it has `AB5` and a separator.
+A Grothendieck category according to the Stacks project is an abelian category provided that it
+has `AB5` and a separator. However, this definition is not invariant under equivalences of
+categories. Therefore, if `C` is an abelian category, the class `IsGrothendieckAbelian.{w} C` has a
+weaker definition that is also satisfied for categories that are merely equivalent to a
+Grothendieck category in the former strict sense.
 
 ## Theorems
 
-Relevant implications of `GrothendieckCategory` are established in `GrothendieckCategory.hasLimits`
-and `GrothendieckCategory.hasColimits`.
+The invariance under equivalences of categories is established in
+`IsGrothendieckAbelian.of_equivalence`.
+
+Conversely, `ShrinkHoms.isGrothendieckAbelian C` shows that `C` satisfies the strict definition
+of a Grothendieck category after shrinking its hom sets.
+
+Relevant implications of `IsGrothendieckAbelian` are established in
+`IsGrothendieckAbelian.hasLimits` and `IsGrothendieckAbelian.hasColimits`.
 
 ## References
 
@@ -39,12 +49,18 @@ universe w v u w₂ v₂ u₂
 variable (C : Type u) [Category.{v} C] (D : Type u₂) [Category.{v₂} D]
 
 /--
-In the literature, an abelian category `C` is called a Grothendieck category provided that it has
-`AB5` and a separator (see `HasSeparator`).
-
-`IsGrothendieckAbelian.{w} C` is defined such that it holds if and only if `C` is equivalent to a
-Grothendieck category -- more concretely, if and only if `ShrinkHoms.{w} C` is a Grothendieck
-category.
+If `C` is an abelian category, we shall say that it satisfies `IsGrothendieckAbelian.{w} C`
+if it is locally small (relative to `w`), has exact filtered colimits of size `w` (AB5) and has a
+separator.
+If `[Category.{v} C]` and `w = v`, this means that `C` satisfies `AB5` and has a separator;
+general results about Grothendieck abelian categories can be
+reduced to this case using the instance `ShrinkHoms.isGrothendieckAbelian` below.
+
+The introduction of the auxiliary universe `w` shall be needed for certain
+applications to categories of sheaves. That the present definition still preserves essential
+properties of Grothendieck categories is ensured by `IsGrothendieckAbelian.of_equivalence`,
+which shows that every instance for `C` implies an instance for `ShrinkHoms C` with hom sets in
+`Type w`.
 -/
 @[stacks 079B]
 class IsGrothendieckAbelian [Abelian C] : Prop where
diff --git a/Mathlib/CategoryTheory/Abelian/Transfer.lean b/Mathlib/CategoryTheory/Abelian/Transfer.lean
index 8072e2624418c2..fb1ec2c96a5072 100644
--- a/Mathlib/CategoryTheory/Abelian/Transfer.lean
+++ b/Mathlib/CategoryTheory/Abelian/Transfer.lean
@@ -18,6 +18,9 @@ we have `F : C ⥤ D` `G : D ⥤ C` (both preserving zero morphisms),
 and further we have `adj : G ⊣ F` and `i : F ⋙ G ≅ 𝟭 C`,
 then `C` is also abelian.
 
+A particular example is the transfer of `Abelian` instances from a category `C` to `ShrinkHoms C`;
+see `ShrinkHoms.abelian`. In this case, we also transfer the `Preadditive` structure.
+
 See <https://stacks.math.columbia.edu/tag/03A3>
 
 ## Notes
@@ -180,24 +183,30 @@ namespace ShrinkHoms
 
 universe w
 
-variable (C : Type*) [Category C] [LocallySmall.{w} C] [Preadditive C]
+variable {C : Type*} [Category C] [LocallySmall.{w} C]
+
+section Preadditive
+
+variable [Preadditive C]
 
 noncomputable instance homGroup (P Q : ShrinkHoms C) : AddCommGroup (P ⟶ Q : Type w) :=
   Equiv.addCommGroup (equivShrink _).symm
 
 lemma functor_map_add {P Q : C} (f g : P ⟶ Q) :
     (functor C).map (f + g) =
-      (functor C).map f + (functor C).map g :=
-  map_add (equivShrink.{w} (P ⟶ Q)).symm.addEquiv.symm f g
+      (functor C).map f + (functor C).map g := by
+  exact map_add (equivShrink.{w} (P ⟶ Q)).symm.addEquiv.symm f g
 
 lemma inverse_map_add {P Q : ShrinkHoms C} (f g : P ⟶ Q) :
     (inverse C).map (f + g) =
       (inverse C).map f + (ShrinkHoms.inverse C).map g :=
   map_add (equivShrink.{w} (P.fromShrinkHoms ⟶ Q.fromShrinkHoms)).symm.addEquiv f g
 
-noncomputable instance preadditive [Preadditive C] :
+variable (C)
+
+noncomputable instance preadditive :
     Preadditive.{w} (ShrinkHoms C) where
-  homGroup P Q := Equiv.addCommGroup (equivShrink _).symm
+  homGroup := homGroup
   add_comp _ _ _ _ _ _ := by
     apply (inverse C).map_injective
     simp only [inverse_map_add, Functor.map_comp, Preadditive.add_comp]
@@ -211,14 +220,17 @@ instance : (inverse C).Additive where
 instance : (functor C).Additive where
   map_add := by apply functor_map_add
 
-instance hasLimits [LocallySmall.{w} C] {J : Type*} [Category J]
+instance hasLimits (J : Type*) [Category J]
     [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
   Adjunction.hasLimitsOfShape_of_equivalence (inverse C)
 
-instance hasFiniteLimits [LocallySmall.{w} C] [HasFiniteLimits C] :
+instance hasFiniteLimits [HasFiniteLimits C] :
     HasFiniteLimits.{w} (ShrinkHoms C) := ⟨fun _ => inferInstance⟩
 
-noncomputable instance abelian [Abelian C] [LocallySmall.{w} C] :
+end Preadditive
+
+variable (C) in
+noncomputable instance abelian [Abelian C] :
     Abelian.{w} (ShrinkHoms C) := abelianOfEquivalence (inverse C)
 
 end ShrinkHoms

From 8bd714f30e1b335533bfc39548d1c722490f9d8c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 16:34:06 +0100
Subject: [PATCH 37/46] clarify docstring

---
 Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
index 89834bd495c6e1..3fbacaecba6e9d 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory.lean
@@ -29,8 +29,9 @@ Grothendieck category in the former strict sense.
 The invariance under equivalences of categories is established in
 `IsGrothendieckAbelian.of_equivalence`.
 
-Conversely, `ShrinkHoms.isGrothendieckAbelian C` shows that `C` satisfies the strict definition
-of a Grothendieck category after shrinking its hom sets.
+In particular, `ShrinkHoms.isGrothendieckAbelian C` shows that `ShrinkHoms C` satisfies our
+definition of a Grothendieck category after shrinking its hom sets, which coincides with the strict
+definition in this case.
 
 Relevant implications of `IsGrothendieckAbelian` are established in
 `IsGrothendieckAbelian.hasLimits` and `IsGrothendieckAbelian.hasColimits`.

From 9df44212d9951be492be9b34bf330528f5d757eb Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 16 Dec 2024 16:51:02 +0100
Subject: [PATCH 38/46] hasLimitsOfShape

---
 Mathlib/CategoryTheory/Abelian/Transfer.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/Transfer.lean b/Mathlib/CategoryTheory/Abelian/Transfer.lean
index fb1ec2c96a5072..0c4a50ffe85f5f 100644
--- a/Mathlib/CategoryTheory/Abelian/Transfer.lean
+++ b/Mathlib/CategoryTheory/Abelian/Transfer.lean
@@ -220,7 +220,7 @@ instance : (inverse C).Additive where
 instance : (functor C).Additive where
   map_add := by apply functor_map_add
 
-instance hasLimits (J : Type*) [Category J]
+instance hasLimitsOfShape (J : Type*) [Category J]
     [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
   Adjunction.hasLimitsOfShape_of_equivalence (inverse C)
 

From 2dd740608a009163df1dde8b1e846f5da5f9156f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 18:52:05 +0100
Subject: [PATCH 39/46] fix

---
 Mathlib/CategoryTheory/Generator/Presheaf.lean | 5 ++---
 Mathlib/CategoryTheory/Generator/Sheaf.lean    | 9 +++------
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean
index 982f7c62a523a0..ac8049ed8adfdf 100644
--- a/Mathlib/CategoryTheory/Generator/Presheaf.lean
+++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean
@@ -24,7 +24,7 @@ open Limits Opposite
 namespace Presheaf
 
 variable {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
-  [∀ (ι : Type v), HasCoproductsOfShape ι A]
+  [HasCoproducts.{v} A]
 
 /-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
 `Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`. -/
@@ -79,8 +79,7 @@ lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
   (isSeparating C hS).isSeparator_coproduct
 
 variable (A) in
-instance hasSeparator [HasSeparator A] [HasZeroMorphisms A]
-    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+instance hasSeparator [HasSeparator A] [HasZeroMorphisms A] [HasCoproducts.{u} A] :
     HasSeparator (Cᵒᵖ ⥤ A) where
   hasSeparator := ⟨_, isSeparator C (S := fun (_ : Unit) ↦ separator A)
       (by simpa using isSeparator_separator A)⟩
diff --git a/Mathlib/CategoryTheory/Generator/Sheaf.lean b/Mathlib/CategoryTheory/Generator/Sheaf.lean
index d4883858f47881..5539908fff9819 100644
--- a/Mathlib/CategoryTheory/Generator/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Generator/Sheaf.lean
@@ -26,8 +26,7 @@ namespace Sheaf
 
 variable {C : Type u} [Category.{v} C]
   (J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
-  [∀ (ι : Type v), HasCoproductsOfShape ι A]
-  [HasWeakSheafify J A]
+  [HasCoproducts.{v} A] [HasWeakSheafify J A]
 
 /-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
 sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
@@ -44,9 +43,8 @@ noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
 lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
     IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
   intro F G f g hfg
-  refine (sheafToPresheaf J A).map_injective ((Presheaf.isSeparating C hS) _ _ ?_)
+  refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)
   rintro _ ⟨⟨X, i⟩, rfl⟩ a
-  dsimp at a
   apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
   simpa only [← Adjunction.homEquiv_naturality_right_symm] using
     hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
@@ -57,8 +55,7 @@ lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
   (isSeparating J hS).isSeparator_coproduct
 
 variable (A) in
-instance hasSeparator [HasSeparator A] [Preadditive A]
-    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+instance hasSeparator [HasSeparator A] [Preadditive A] [HasCoproducts.{u} A] :
     HasSeparator (Sheaf J A) where
   hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
       (by simpa using isSeparator_separator A)⟩

From 9414d3bdbf470aa76f208d20ece8261e9335ff29 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 18:55:44 +0100
Subject: [PATCH 40/46] fix

---
 Mathlib/CategoryTheory/Generator/Presheaf.lean | 5 ++---
 Mathlib/CategoryTheory/Generator/Sheaf.lean    | 9 +++------
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean
index 982f7c62a523a0..ac8049ed8adfdf 100644
--- a/Mathlib/CategoryTheory/Generator/Presheaf.lean
+++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean
@@ -24,7 +24,7 @@ open Limits Opposite
 namespace Presheaf
 
 variable {C : Type u} [Category.{v} C] {A : Type u'} [Category.{v'} A]
-  [∀ (ι : Type v), HasCoproductsOfShape ι A]
+  [HasCoproducts.{v} A]
 
 /-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
 `Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`. -/
@@ -79,8 +79,7 @@ lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
   (isSeparating C hS).isSeparator_coproduct
 
 variable (A) in
-instance hasSeparator [HasSeparator A] [HasZeroMorphisms A]
-    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+instance hasSeparator [HasSeparator A] [HasZeroMorphisms A] [HasCoproducts.{u} A] :
     HasSeparator (Cᵒᵖ ⥤ A) where
   hasSeparator := ⟨_, isSeparator C (S := fun (_ : Unit) ↦ separator A)
       (by simpa using isSeparator_separator A)⟩
diff --git a/Mathlib/CategoryTheory/Generator/Sheaf.lean b/Mathlib/CategoryTheory/Generator/Sheaf.lean
index d4883858f47881..5539908fff9819 100644
--- a/Mathlib/CategoryTheory/Generator/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Generator/Sheaf.lean
@@ -26,8 +26,7 @@ namespace Sheaf
 
 variable {C : Type u} [Category.{v} C]
   (J : GrothendieckTopology C) {A : Type u'} [Category.{v'} A]
-  [∀ (ι : Type v), HasCoproductsOfShape ι A]
-  [HasWeakSheafify J A]
+  [HasCoproducts.{v} A] [HasWeakSheafify J A]
 
 /-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
 sheaf to the presheaf `Presheaf.freeYoneda X M`. -/
@@ -44,9 +43,8 @@ noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} :
 lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
     IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by
   intro F G f g hfg
-  refine (sheafToPresheaf J A).map_injective ((Presheaf.isSeparating C hS) _ _ ?_)
+  refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)
   rintro _ ⟨⟨X, i⟩, rfl⟩ a
-  dsimp at a
   apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
   simpa only [← Adjunction.homEquiv_naturality_right_symm] using
     hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)
@@ -57,8 +55,7 @@ lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S))
   (isSeparating J hS).isSeparator_coproduct
 
 variable (A) in
-instance hasSeparator [HasSeparator A] [Preadditive A]
-    [∀ (ι : Type u), HasCoproductsOfShape ι A] :
+instance hasSeparator [HasSeparator A] [Preadditive A] [HasCoproducts.{u} A] :
     HasSeparator (Sheaf J A) where
   hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A)
       (by simpa using isSeparator_separator A)⟩

From 6a04477d1b5df0f4882ced6f5554c835bf983e1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 19:01:13 +0100
Subject: [PATCH 41/46] fix docstring

---
 Mathlib/CategoryTheory/Generator/Presheaf.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean
index ac8049ed8adfdf..d12ab50d4882a9 100644
--- a/Mathlib/CategoryTheory/Generator/Presheaf.lean
+++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean
@@ -10,8 +10,9 @@ import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 /-!
 # Generators in the category of presheaves
 
-In this file, we show that if `A` is a preadditive category that has a separator (and
-suitable coproducts), then the category of presheaves `Cᵒᵖ ⥤ A` also has a separator.
+In this file, we show that if `A` is a category with zero morphisms that
+has a separator (and suitable coproducts), then the category of
+presheaves `Cᵒᵖ ⥤ A` also has a separator.
 
 -/
 

From 17c90c0dfd9ccb9dbb929e6a31380d189a3c0fa6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 16 Dec 2024 19:17:33 +0100
Subject: [PATCH 42/46] fix

---
 Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
index f92024fd857391..78faa85009d9d5 100644
--- a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
+++ b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
-import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
 import Mathlib.CategoryTheory.Generator.Sheaf
 import Mathlib.CategoryTheory.Sites.Abelian
 

From fe42daf1b945703c06df8f6cfcbb56bc77aad066 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 25 Dec 2024 02:23:47 +0100
Subject: [PATCH 43/46] cleaning up

---
 Mathlib.lean                                  |   1 -
 .../Abelian/GrothendieckAxioms/Basic.lean     |  43 ++++-
 .../Abelian/GrothendieckAxioms/Sheaf.lean     |  63 +++++--
 .../Sites/GrothendieckAbelian.lean            | 157 ------------------
 4 files changed, 93 insertions(+), 171 deletions(-)
 delete mode 100644 Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 9ab63d411c4f27..25b6753d6ca64d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2142,7 +2142,6 @@ import Mathlib.CategoryTheory.Sites.EpiMono
 import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.CategoryTheory.Sites.Grothendieck
-import Mathlib.CategoryTheory.Sites.GrothendieckAbelian
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
 import Mathlib.CategoryTheory.Sites.LeftExact
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
index b96f54ec72e3b3..b6f2e1e9944f99 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -53,7 +53,7 @@ open Limits
 
 attribute [instance] comp_preservesFiniteLimits comp_preservesFiniteColimits
 
-universe w w' w₂ w₂' v v' u u'
+universe w w' w₂ w₂' v v' v'' u u' u''
 
 variable (C : Type u) [Category.{v} C]
 
@@ -168,6 +168,47 @@ lemma HasExactLimitsOfShape.of_codomain_equivalence (J : Type*) [Category J] {D
   apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
   exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm
 
+namespace Adjunction
+
+variable {C} {D : Type u''} [Category.{v''} D] {F : C ⥤ D} {G : D ⥤ C}
+
+/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective. If `D` has
+finite limits and `F` commutes to them, then if `C` has exact colimits of shape `J`,
+then `D` also has exact colimits of shape `J`. -/
+lemma hasExactColimitsOfShape (adj : F ⊣ G) [G.Full] [G.Faithful]
+    (J : Type u') [Category.{v'} J] [HasColimitsOfShape J C] [HasColimitsOfShape J D]
+    [HasExactColimitsOfShape J C] [HasFiniteLimits D] [PreservesFiniteLimits F] :
+    HasExactColimitsOfShape J D where
+  preservesFiniteLimits := ⟨fun K _ _ ↦ ⟨fun {H} ↦ by
+    have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
+    have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
+    let e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
+      isoWhiskerLeft _ (preservesColimitNatIso F) ≪≫ (Functor.associator _ _ _).symm ≪≫
+        isoWhiskerRight (whiskeringRightObjCompIso G F) _ ≪≫
+        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) _ ≪≫
+        isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ colim.leftUnitor
+    exact preservesLimit_of_natIso _ e⟩⟩
+
+/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective. If `C` has
+finite colimits and `G` commutes to them, then if `D` has exact limits of shape `J`,
+then `C` also has exact limits of shape `J`. -/
+lemma hasExactLimitsOfShape (adj : F ⊣ G) [F.Full] [F.Faithful]
+    (J : Type u') [Category.{v'} J] [HasLimitsOfShape J C] [HasLimitsOfShape J D]
+    [HasExactLimitsOfShape J D] [HasFiniteColimits C] [PreservesFiniteColimits G] :
+    HasExactLimitsOfShape J C where
+  preservesFiniteColimits:= ⟨fun K _ _ ↦ ⟨fun {H} ↦ by
+    have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
+    have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
+    let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
+      isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
+        (Functor.associator _ _ _).symm ≪≫
+        isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
+        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
+        isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ lim.leftUnitor
+    exact preservesColimit_of_natIso _ e⟩⟩
+
+end Adjunction
+
 /--
 A category `C` which has coproducts is said to have `AB4` of size `w` provided that
 coproducts of size `w` are exact.
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
index 7696bed4e68af6..472a33b21b56e8 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
@@ -1,32 +1,71 @@
 /-
 Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dagur Asgeirsson
+Authors: Dagur Asgeirsson, Joël Riou
 -/
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
-import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
+import Mathlib.CategoryTheory.Generator.Sheaf
+import Mathlib.CategoryTheory.Sites.Abelian
+
 /-!
 
 # AB axioms in sheaf categories
 
-This file proves that, when the relevant limits and colimits and sheafification exist, exactness of
-limits and colimits carries over from `A` to categories of `A`-valued sheaves.
+If `J` is a Grothendieck topology on a small category `C : Type v`,
+and `A : Type u₁` (with `Category.{v} A`) is a Grothendieck abelian category,
+then `Sheaf J A` is a Grothendieck abelian category.
+
 -/
 
+universe v v₁ v₂ u u₁ u₂
+
 namespace CategoryTheory
 
 open Limits
 
-variable {A C J : Type*} [Category A] [Category C] [Category J]
+namespace Sheaf
+
+variable {C : Type u} {A : Type u₁} {K : Type u₂}
+  [Category.{v} C] [Category.{v₁} A] [Category.{v₂} K]
+  (J : GrothendieckTopology C)
+
+section
+
+/- The two instances in this section shall apply in very rare situations, as it assumes
+that the forget functor from sheaves to presheaves commutes with certain colimits. -/
+
+variable [HasWeakSheafify J A]
+
+instance [HasFiniteLimits A] [HasColimitsOfShape K A] [HasExactColimitsOfShape K A]
+    [PreservesColimitsOfShape K (sheafToPresheaf J A)] : HasExactColimitsOfShape K (Sheaf J A) :=
+  HasExactColimitsOfShape.domain_of_functor K (sheafToPresheaf J A)
+
+instance [HasFiniteColimits A] [HasLimitsOfShape K A] [HasExactLimitsOfShape K A]
+    [PreservesFiniteColimits (sheafToPresheaf J A)] : HasExactLimitsOfShape K (Sheaf J A) :=
+  HasExactLimitsOfShape.domain_of_functor K (sheafToPresheaf J A)
+
+end
+
+instance hasFilteredColimitsOfSize
+    [HasSheafify J A] [HasFilteredColimitsOfSize.{v₂, u₂} A] :
+    HasFilteredColimitsOfSize.{v₂, u₂} (Sheaf J A) where
+  HasColimitsOfShape K := by infer_instance
+
+instance hasExactColimitsOfShape [HasFiniteLimits A] [HasSheafify J A]
+    [HasColimitsOfShape K A] [HasExactColimitsOfShape K A] :
+    HasExactColimitsOfShape K (Sheaf J A) :=
+  (sheafificationAdjunction J A).hasExactColimitsOfShape K
 
-variable (K : GrothendieckTopology C) [HasWeakSheafify K A]
+instance ab5ofSize [HasFiniteLimits A] [HasSheafify J A]
+    [HasFilteredColimitsOfSize.{v₂, u₂} A] [AB5OfSize.{v₂, u₂} A] :
+    AB5OfSize.{v₂, u₂} (Sheaf J A) where
+  ofShape K _ _ := by infer_instance
 
-instance [HasFiniteLimits A] [HasColimitsOfShape J A] [HasExactColimitsOfShape J A]
-    [PreservesColimitsOfShape J (sheafToPresheaf K A)] : HasExactColimitsOfShape J (Sheaf K A) :=
-  HasExactColimitsOfShape.domain_of_functor J (sheafToPresheaf K A)
+instance {C : Type v} [SmallCategory.{v} C] (J : GrothendieckTopology C)
+    (A : Type u₁) [Category.{v} A] [Abelian A] [IsGrothendieckAbelian.{v} A]
+    [HasSheafify J A] : IsGrothendieckAbelian.{v} (Sheaf J A) where
 
-instance [HasFiniteColimits A] [HasLimitsOfShape J A] [HasExactLimitsOfShape J A]
-    [PreservesFiniteColimits (sheafToPresheaf K A)] : HasExactLimitsOfShape J (Sheaf K A) :=
-  HasExactLimitsOfShape.domain_of_functor J (sheafToPresheaf K A)
+end Sheaf
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean b/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
deleted file mode 100644
index 78faa85009d9d5..00000000000000
--- a/Mathlib/CategoryTheory/Sites/GrothendieckAbelian.lean
+++ /dev/null
@@ -1,157 +0,0 @@
-/-
-Copyright (c) 2024 Joël Riou. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joël Riou
--/
-import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
-import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
-import Mathlib.CategoryTheory.Generator.Sheaf
-import Mathlib.CategoryTheory.Sites.Abelian
-
-/-!
-# Categories of sheaves are Grothendieck abelian
-
-If `J` is a Grothendieck topology on a small category `C : Type v`,
-and `A : Type u` (with `Category.{v} A`) is a Grothendieck abelian category,
-then `Sheaf J A` is a Grothendieck abelian category.
-
--/
-
-universe v'' v' v u'' u' u
-
-namespace CategoryTheory
-
-open Limits
-
--- this should be moved
-namespace Adjunction
-
-variable {C : Type u} {D : Type u'} [Category.{v} C] [Category.{v'} D]
-  {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
-  {K : Type u''} [Category.{v''} K]
-  [G.Faithful] [G.Full]
-
-namespace colimIso
-
-variable {P : K ⥤ D} (c : Cocone (P ⋙ G)) (hc : IsColimit c)
-
-/-- A cocone for `P : K ⥤ D` deduced from a cocone for `P ⋙ G` when `adj : F ⊣ G`
-is an adjunction such that `G : D ⥤ C` is fully faithful. -/
-@[simps pt]
-noncomputable def cocone : Cocone P where
-  pt := F.obj c.pt
-  ι :=
-    { app k := G.preimage (c.ι.app k ≫ adj.unit.app _)
-      naturality k k' f := by
-        apply G.map_injective
-        have := c.w f
-        dsimp at this
-        simp [reassoc_of% this]}
-
-@[simp]
-lemma map_cocone_ι_app (k : K) :
-    G.map ((cocone adj c).ι.app k) = c.ι.app k ≫ adj.unit.app _ := by
-  simp [cocone]
-
-namespace isColimitCocone
-
-variable {c}
-
-/-- Auxiliary definition for `Adjunction.isColimitCocone`. -/
-noncomputable def desc (s : Cocone P) : F.obj c.pt ⟶ s.pt :=
-  (adj.homEquiv _ _).symm (hc.desc (G.mapCocone s))
-
-@[reassoc]
-lemma fac (s : Cocone P) (k : K) :
-    (cocone adj c).ι.app k ≫ isColimitCocone.desc adj hc s = s.ι.app k :=
-  G.map_injective (by simp [desc, homEquiv_counit])
-
-include hc in
-lemma uniq {s : Cocone P} {f g : F.obj c.pt ⟶ s.pt}
-    (h : ∀ (k : K), (cocone adj c).ι.app k ≫ f = (cocone adj c).ι.app k ≫ g) : f = g :=
-  (adj.homEquiv _ _).injective
-    (hc.hom_ext (fun k ↦ by simpa [homEquiv_unit] using G.congr_map (h k)))
-
-end isColimitCocone
-
-/-- Given an adjunction `adj : F ⊣ G` such that `G : D ⥤ C` is fully faithful,
-this is a construction of a colimit cocone for `P : K ⥤ D` from a colimit
-cocone for `P ⋙ G`. -/
-noncomputable def isColimitCocone : IsColimit (cocone adj c) where
-  desc s := isColimitCocone.desc adj hc s
-  fac s k := isColimitCocone.fac adj hc s k
-  uniq s m hm := isColimitCocone.uniq adj hc (fun _ ↦ by rw [isColimitCocone.fac, hm])
-
-end colimIso
-
-variable [HasColimitsOfShape K C] [HasColimitsOfShape K D]
-
-/-- If `adj : F ⊣ G` is an adjuncton such that `G` is fully faithful, this is the
-isomorphism between the colimit of `P : K ⥤ D` and the image by `F` of
-the colimit of `P ⋙ G`. -/
-noncomputable def colimIsoObj (P : K ⥤ D) : colimit P ≅ F.obj (colimit (P ⋙ G)) :=
-  IsColimit.coconePointUniqueUpToIso (colimit.isColimit P)
-      (colimIso.isColimitCocone adj _ (colimit.isColimit (P ⋙ G)))
-
-@[reassoc]
-lemma ι_colimIsoObj_hom (P : K ⥤ D) (k : K) :
-    colimit.ι P k ≫ (colimIsoObj adj P).hom =
-      (colimIso.cocone adj (colimit.cocone (P ⋙ G))).ι.app k :=
-  IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _
-
-variable (K)
-
-/-- If `adj : F ⊣ G` is an adjuncton such that `G` is fully faithful, this is the
-natural isomorphism between the colimit of `P : K ⥤ D` and the image by `F` of
-the colimit of `P ⋙ G`. -/
-noncomputable def colimIso : colim (J := K) (C := D) ≅
-    (whiskeringRight _ _ _).obj G ⋙ colim (J := K) (C := C) ⋙ F :=
-  NatIso.ofComponents adj.colimIsoObj (fun {P Q} f ↦ by
-    dsimp
-    ext k
-    rw [ι_colimMap_assoc, ι_colimIsoObj_hom, ι_colimIsoObj_hom_assoc]
-    apply G.map_injective
-    simp)
-
-include adj in
-lemma hasExactColimitsOfShape [HasExactColimitsOfShape K C] [Abelian D]
-    [F.PreservesMonomorphisms] :
-    HasExactColimitsOfShape K D := by
-  suffices (colim (J := K) (C := D)).PreservesMonomorphisms by
-    apply hasExactColimitsOfShape_of_preservesMono
-  have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
-  apply Functor.preservesMonomorphisms.of_iso (adj.colimIso K).symm
-
-end Adjunction
-
-namespace Sheaf
-
--- this should be moved to Abelian.GrothendieckAxioms.Sheaf
-
-instance hasExactColimitsOfShape
-    {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
-    (A : Type u') [Category.{v'} A] [Abelian A]
-    (K : Type u'') [Category.{v''} K] [HasSheafify J A] [HasColimitsOfShape K A]
-    [HasExactColimitsOfShape K A] :
-    HasExactColimitsOfShape K (Sheaf J A) :=
-  (sheafificationAdjunction J A).hasExactColimitsOfShape K
-
-instance hasFilteredColimitsOfSize {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
-    (A : Type u') [Category.{v'} A] [HasSheafify J A]
-    [HasFilteredColimitsOfSize.{v'', u''} A] :
-    HasFilteredColimitsOfSize.{v'', u''} (Sheaf J A) where
-  HasColimitsOfShape K := by infer_instance
-
-instance ab5ofSize {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
-    (A : Type u') [Category.{v'} A] [Abelian A] [HasSheafify J A]
-    [HasFilteredColimitsOfSize.{v'', u''} A] [AB5OfSize.{v'', u''} A] :
-    AB5OfSize.{v'', u''} (Sheaf J A) where
-  ofShape K _ _ := by infer_instance
-
-instance {C : Type v} [SmallCategory C] (J : GrothendieckTopology C) (A : Type u)
-    [Category.{v} A] [Abelian A] [IsGrothendieckAbelian.{v} A]
-    [HasSheafify J A] : IsGrothendieckAbelian.{v} (Sheaf J A) where
-
-end Sheaf
-
-end CategoryTheory

From 5542e4086ab55dd36e2ae8412b56eb8cf5416870 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 25 Dec 2024 02:26:31 +0100
Subject: [PATCH 44/46] better docstring

---
 .../Abelian/GrothendieckAxioms/Basic.lean            | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
index b6f2e1e9944f99..5aaabd4f0aca18 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -172,9 +172,9 @@ namespace Adjunction
 
 variable {C} {D : Type u''} [Category.{v''} D] {F : C ⥤ D} {G : D ⥤ C}
 
-/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective. If `D` has
-finite limits and `F` commutes to them, then if `C` has exact colimits of shape `J`,
-then `D` also has exact colimits of shape `J`. -/
+/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective.
+Assume that `D` has finite limits and `F` commutes to them.
+If `C` has exact colimits of shape `J`, then `D` also has exact colimits of shape `J`. -/
 lemma hasExactColimitsOfShape (adj : F ⊣ G) [G.Full] [G.Faithful]
     (J : Type u') [Category.{v'} J] [HasColimitsOfShape J C] [HasColimitsOfShape J D]
     [HasExactColimitsOfShape J C] [HasFiniteLimits D] [PreservesFiniteLimits F] :
@@ -189,9 +189,9 @@ lemma hasExactColimitsOfShape (adj : F ⊣ G) [G.Full] [G.Faithful]
         isoWhiskerRight wiskeringRightObjIdIso _ ≪≫ colim.leftUnitor
     exact preservesLimit_of_natIso _ e⟩⟩
 
-/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective. If `C` has
-finite colimits and `G` commutes to them, then if `D` has exact limits of shape `J`,
-then `C` also has exact limits of shape `J`. -/
+/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective.
+Assume that `C` has finite colimits and `G` commutes to them.
+If `D` has exact limits of shape `J`, then `C` also has exact limits of shape `J`. -/
 lemma hasExactLimitsOfShape (adj : F ⊣ G) [F.Full] [F.Faithful]
     (J : Type u') [Category.{v'} J] [HasLimitsOfShape J C] [HasLimitsOfShape J D]
     [HasExactLimitsOfShape J D] [HasFiniteColimits C] [PreservesFiniteColimits G] :

From 325c854edf83a5fbd74c8a6834e51e969ba4a80f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Thu, 26 Dec 2024 17:14:40 +0100
Subject: [PATCH 45/46] Update
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 .../CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean    | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
index 472a33b21b56e8..ec80f81cec3bf7 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
@@ -32,8 +32,10 @@ variable {C : Type u} {A : Type u₁} {K : Type u₂}
 
 section
 
-/- The two instances in this section shall apply in very rare situations, as it assumes
-that the forget functor from sheaves to presheaves commutes with certain colimits. -/
+/- The two instances in this section apply in very rare situations, as they assume
+that the forgetful functor from sheaves to presheaves commutes with certain colimits.
+This does apply for sheaves for the extensive topology --- condensed modules over a 
+ring are examples of such sheaves.  -/
 
 variable [HasWeakSheafify J A]
 

From 4b0a487c95f63e0f19b2a5c0f650ccd46aa2e521 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Thu, 26 Dec 2024 20:50:34 +0100
Subject: [PATCH 46/46] Update
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
index ec80f81cec3bf7..2cffda5728fe34 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
@@ -34,7 +34,7 @@ section
 
 /- The two instances in this section apply in very rare situations, as they assume
 that the forgetful functor from sheaves to presheaves commutes with certain colimits.
-This does apply for sheaves for the extensive topology --- condensed modules over a 
+This does apply for sheaves for the extensive topology --- condensed modules over a
 ring are examples of such sheaves.  -/
 
 variable [HasWeakSheafify J A]