From f83fe2ffbf66847f84fed742249ce13585209ea3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?=
 <dagurtomas@gmail.com>
Date: Thu, 18 Apr 2024 13:15:24 +0000
Subject: [PATCH] feat(CategoryTheory): more universe polymorphism for limits
 in sheaf categories (#12222)

We prove that sheaf categories have limits and colimits of the same size as the target category. Before, the universe levels were too restrictive. We change the construction of the colimit: it now uses the formal properties of sheafification instead of an explicit construction.
---
 Mathlib/CategoryTheory/Sites/Abelian.lean   | 30 ++------
 Mathlib/CategoryTheory/Sites/LeftExact.lean |  5 +-
 Mathlib/CategoryTheory/Sites/Limits.lean    | 79 ++++++++-------------
 Mathlib/Condensed/Abelian.lean              | 10 +--
 4 files changed, 40 insertions(+), 84 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/Abelian.lean b/Mathlib/CategoryTheory/Sites/Abelian.lean
index 80d7fc0ca41fd..047823e8072fb 100644
--- a/Mathlib/CategoryTheory/Sites/Abelian.lean
+++ b/Mathlib/CategoryTheory/Sites/Abelian.lean
@@ -5,9 +5,8 @@ Authors: Adam Topaz, Jujian Zhang
 -/
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
-import Mathlib.CategoryTheory.Preadditive.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.Transfer
-import Mathlib.CategoryTheory.Sites.LeftExact
+import Mathlib.CategoryTheory.Sites.Limits
 
 #align_import topology.sheaves.abelian from "leanprover-community/mathlib"@"ac3ae212f394f508df43e37aa093722fa9b65d31"
 
@@ -29,33 +28,14 @@ open CategoryTheory.Limits
 
 section Abelian
 
-universe w v u
+universe w' w v u
 
--- Porting note: `C` was `Type (max v u)`, but making it more universe polymorphic
---   solves some problems
 variable {C : Type u} [Category.{v} C]
-variable {D : Type w} [Category.{max v u} D] [Abelian D]
+variable {D : Type w} [Category.{w'} D] [Abelian D]
 variable {J : GrothendieckTopology C}
+variable [HasSheafify J D] [HasFiniteLimits D]
 
--- Porting note: this `Abelian` instance is no longer necessary,
--- maybe because I have made `C` more universe polymorphic
---
--- This needs to be specified manually because of universe level.
---instance : Abelian (Cᵒᵖ ⥤ D) :=
---  @Abelian.functorCategoryAbelian Cᵒᵖ _ D _ _
-
--- This also needs to be specified manually, but I don't know why.
-instance hasFiniteProductsSheaf : HasFiniteProducts (Sheaf J D) where
-  out j := { has_limit := fun F => by infer_instance }
-
--- sheafification assumptions
-variable [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
-variable [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
-variable [ConcreteCategory.{max v u} D] [PreservesLimits (forget D)]
-variable [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
-variable [(forget D).ReflectsIsomorphisms]
-
-instance sheafIsAbelian [HasFiniteLimits D] : Abelian (Sheaf J D) :=
+instance sheafIsAbelian : Abelian (Sheaf J D) :=
   let adj := sheafificationAdjunction J D
   abelianOfAdjunction _ _ (asIso adj.counit) adj
 set_option linter.uppercaseLean3 false in
diff --git a/Mathlib/CategoryTheory/Sites/LeftExact.lean b/Mathlib/CategoryTheory/Sites/LeftExact.lean
index 2cba3b090f6fa..30c91630569a0 100644
--- a/Mathlib/CategoryTheory/Sites/LeftExact.lean
+++ b/Mathlib/CategoryTheory/Sites/LeftExact.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import Mathlib.CategoryTheory.Sites.Limits
-import Mathlib.CategoryTheory.Limits.FunctorCategory
 import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
 import Mathlib.CategoryTheory.Adhesive
-import Mathlib.CategoryTheory.Sites.Sheafification
+import Mathlib.CategoryTheory.Sites.ConcreteSheafification
 
 #align_import category_theory.sites.left_exact from "leanprover-community/mathlib"@"59382264386afdbaf1727e617f5fdda511992eb9"
 
@@ -21,8 +20,6 @@ open CategoryTheory Limits Opposite
 
 universe w' w v u
 
--- Porting note: was `C : Type max v u` which made most instances non automatically applicable
--- it seems to me it is better to declare `C : Type u`: it works better, and it is more general
 variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
 variable {D : Type w} [Category.{max v u} D]
 variable [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
diff --git a/Mathlib/CategoryTheory/Sites/Limits.lean b/Mathlib/CategoryTheory/Sites/Limits.lean
index 893ef4ebe71da..55eaf4f09c07c 100644
--- a/Mathlib/CategoryTheory/Sites/Limits.lean
+++ b/Mathlib/CategoryTheory/Sites/Limits.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import Mathlib.CategoryTheory.Limits.Creates
-import Mathlib.CategoryTheory.Sites.ConcreteSheafification
+import Mathlib.CategoryTheory.Sites.Sheafification
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
 
 #align_import category_theory.sites.limits from "leanprover-community/mathlib"@"95e83ced9542828815f53a1096a4d373c1b08a77"
@@ -38,14 +38,14 @@ open CategoryTheory.Limits
 
 open Opposite
 
-section Limits
-
-universe w v u z z'
+universe w w' v u z z' u₁ u₂
 
 variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
-variable {D : Type w} [Category.{max v u} D]
+variable {D : Type w} [Category.{w'} D]
 variable {K : Type z} [Category.{z'} K]
 
+section Limits
+
 noncomputable section
 
 section
@@ -168,71 +168,47 @@ instance : HasLimitsOfShape K (Sheaf J D) :=
 instance [HasFiniteProducts D] : HasFiniteProducts (Sheaf J D) :=
   ⟨inferInstance⟩
 
+instance [HasFiniteLimits D] : HasFiniteLimits (Sheaf J D) :=
+  ⟨fun _ ↦ inferInstance⟩
+
 end
 
-instance createsLimits [HasLimits D] : CreatesLimits (sheafToPresheaf J D) :=
+instance createsLimits [HasLimitsOfSize.{u₁, u₂} D] :
+    CreatesLimitsOfSize.{u₁, u₂} (sheafToPresheaf J D) :=
   ⟨createsLimitsOfShape⟩
 
-instance [HasLimits D] : HasLimits (Sheaf J D) :=
+instance hasLimitsOfSize [HasLimitsOfSize.{u₁, u₂} D] : HasLimitsOfSize.{u₁, u₂} (Sheaf J D) :=
   hasLimits_of_hasLimits_createsLimits (sheafToPresheaf J D)
 
+variable {D : Type w} [Category.{max v u} D]
+
+example [HasLimits D] : HasLimits (Sheaf J D) := inferInstance
+
 end
 
 end Limits
 
 section Colimits
 
-universe w v u z z'
-
-variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
-variable {D : Type w} [Category.{max v u} D]
-variable {K : Type z} [Category.{z'} K]
-
--- Now we need a handful of instances to obtain sheafification...
-variable [ConcreteCategory.{max v u} D]
-variable [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
-variable [PreservesLimits (forget D)]
-variable [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
-variable [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
-variable [(forget D).ReflectsIsomorphisms]
+variable [HasWeakSheafify J D]
 
 /-- Construct a cocone by sheafifying a cocone point of a cocone `E` of presheaves
 over a functor which factors through sheaves.
 In `isColimitSheafifyCocone`, we show that this is a colimit cocone when `E` is a colimit. -/
-@[simps]
 noncomputable def sheafifyCocone {F : K ⥤ Sheaf J D}
-    (E : Cocone (F ⋙ sheafToPresheaf J D)) : Cocone F where
-  pt := ⟨J.sheafify E.pt, GrothendieckTopology.Plus.isSheaf_plus_plus _ _⟩
-  ι :=
-    { app := fun k => ⟨E.ι.app k ≫ J.toSheafify E.pt⟩
-      naturality := fun i j f => by
-        ext1
-        dsimp
-        erw [Category.comp_id, ← Category.assoc, E.w f] }
+    (E : Cocone (F ⋙ sheafToPresheaf J D)) : Cocone F :=
+  (Cocones.precompose
+    (isoWhiskerLeft F (asIso (sheafificationAdjunction J D).counit).symm).hom).obj
+    ((presheafToSheaf J D).mapCocone E)
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.sheafify_cocone CategoryTheory.Sheaf.sheafifyCocone
 
 /-- If `E` is a colimit cocone of presheaves, over a diagram factoring through sheaves,
 then `sheafifyCocone E` is a colimit cocone. -/
-@[simps]
 noncomputable def isColimitSheafifyCocone {F : K ⥤ Sheaf J D}
-    (E : Cocone (F ⋙ sheafToPresheaf J D)) (hE : IsColimit E) : IsColimit (sheafifyCocone E) where
-  desc S := ⟨J.sheafifyLift (hE.desc ((sheafToPresheaf J D).mapCocone S)) S.pt.2⟩
-  fac := by
-    intro S j
-    ext1
-    dsimp [sheafifyCocone]
-    erw [Category.assoc, J.toSheafify_sheafifyLift, hE.fac]
-    rfl
-  uniq := by
-    intro S m hm
-    ext1
-    apply J.sheafifyLift_unique
-    apply hE.uniq ((sheafToPresheaf J D).mapCocone S)
-    intro j
-    dsimp
-    simp only [← Category.assoc, ← hm] -- Porting note: was `simpa only [...]`
-    rfl
+    (E : Cocone (F ⋙ sheafToPresheaf J D)) (hE : IsColimit E) : IsColimit (sheafifyCocone E) :=
+  (IsColimit.precomposeHomEquiv _ ((presheafToSheaf J D).mapCocone E)).symm
+    (isColimitOfPreserves _ hE)
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf.is_colimit_sheafify_cocone CategoryTheory.Sheaf.isColimitSheafifyCocone
 
@@ -243,9 +219,16 @@ instance [HasColimitsOfShape K D] : HasColimitsOfShape K (Sheaf J D) :=
 instance [HasFiniteCoproducts D] : HasFiniteCoproducts (Sheaf J D) :=
   ⟨inferInstance⟩
 
-instance [HasColimits D] : HasColimits (Sheaf J D) :=
+instance [HasFiniteColimits D] : HasFiniteColimits (Sheaf J D) :=
+  ⟨fun _ ↦ inferInstance⟩
+
+instance [HasColimitsOfSize.{u₁, u₂} D] : HasColimitsOfSize.{u₁, u₂} (Sheaf J D) :=
   ⟨inferInstance⟩
 
+variable {D : Type w} [Category.{max v u} D]
+
+example [HasLimits D] : HasLimits (Sheaf J D) := inferInstance
+
 end Colimits
 
 end Sheaf
diff --git a/Mathlib/Condensed/Abelian.lean b/Mathlib/Condensed/Abelian.lean
index 028df811361f7..80d5b2112e7ba 100644
--- a/Mathlib/Condensed/Abelian.lean
+++ b/Mathlib/Condensed/Abelian.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
 import Mathlib.Algebra.Category.GroupCat.Abelian
-import Mathlib.Algebra.Category.GroupCat.FilteredColimits
 import Mathlib.CategoryTheory.Sites.Abelian
+import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.Condensed.Basic
 
 /-!
@@ -16,7 +16,7 @@ Condensed abelian groups form an abelian category.
 
 universe u
 
-open CategoryTheory Limits
+open CategoryTheory
 
 /--
 The category of condensed abelian groups, defined as sheaves of abelian groups over
@@ -24,8 +24,4 @@ The category of condensed abelian groups, defined as sheaves of abelian groups o
 -/
 abbrev CondensedAb := Condensed.{u} AddCommGroupCat.{u+1}
 
-noncomputable instance CondensedAb.abelian :
-    CategoryTheory.Abelian CondensedAb.{u} :=
-  letI : PreservesLimits (forget AddCommGroupCat.{u+1}) :=
-    AddCommGroupCat.forgetPreservesLimits.{u+1}
-  CategoryTheory.sheafIsAbelian
+noncomputable instance CondensedAb.abelian : Abelian CondensedAb.{u} := sheafIsAbelian