diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
index b96f54ec72e3b3..5aaabd4f0aca18 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.
+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] :
+    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.
+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] :
+    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..2cffda5728fe34 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
@@ -1,32 +1,73 @@
 /-
 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 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]
+
+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