chore(CategoryTheory/Sites): generalise universes and assumptions in …

…`CoverLifting` file (#12798)

Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

@@ -25,6 +25,8 @@ We give the corresonding result for the regular topology as well (see
 -/
 
 
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
 namespace CategoryTheory
 
 open Limits Functor
@@ -95,9 +97,7 @@ instance isContinuous : haveI := F.reflects_precoherent
 
 section SheafEquiv
 
-universe u
-
-variable {C D : Type (u+1)} [LargeCategory C] [LargeCategory D] (F : C ⥤ D)
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (F : C ⥤ D)
   [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies]
   [F.Full] [F.Faithful]
   [Precoherent D]
@@ -109,17 +109,16 @@ functor `F : C ⥤ D` to a precoherent category, which preserves and reflects e
 families, and satisfies `F.EffectivelyEnough`.
 -/
 noncomputable
-def equivalence (A : Type _) [Category.{u+1} A] [HasLimits A] : haveI := F.reflects_precoherent
+def equivalence (A : Type u₃) [Category.{v₃} A] [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
+    haveI := F.reflects_precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A :=
   Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
 
 end SheafEquiv
 
 section RegularExtensive
 
-universe u
-
-variable {C D : Type (u+1)} [LargeCategory C] [LargeCategory D] (F : C ⥤ D)
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (F : C ⥤ D)
   [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis]
   [F.Full] [F.Faithful]
   [FinitaryExtensive D] [Preregular D]
@@ -133,7 +132,8 @@ functor `F : C ⥤ D` to an extensive preregular category, which preserves and
 epimorphisms and satisfies `F.EffectivelyEnough`.
 -/
 noncomputable
-def equivalence' (A : Type _) [Category.{u+1} A] [HasLimits A] :
+def equivalence' (A : Type u₃) [Category.{v₃} A]
+    [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
     haveI := F.reflects_precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A :=
   Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
@@ -199,9 +199,7 @@ instance isContinuous : haveI := F.reflects_preregular
 
 section SheafEquiv
 
-universe u
-
-variable {C D : Type (u+1)} [LargeCategory C] [LargeCategory D] (F : C ⥤ D)
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (F : C ⥤ D)
   [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis]
   [F.Full] [F.Faithful]
   [Preregular D]
@@ -213,7 +211,8 @@ functor `F : C ⥤ D` to a preregular category, which preserves and reflects ef
 epimorphisms and satisfies `F.EffectivelyEnough`.
 -/
 noncomputable
-def equivalence (A : Type _) [Category.{u+1} A] [HasLimits A] : haveI := F.reflects_preregular
+def equivalence (A : Type u₃) [Category.{v₃} A] [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
+    haveI := F.reflects_preregular
     Sheaf (regularTopology C) A ≌ Sheaf (regularTopology D) A :=
   Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
 

Mathlib/CategoryTheory/Sites/CoverLifting.lean

@@ -42,7 +42,7 @@ small colimits.
 -/
 
 
-universe w v v₁ v₂ v₃ u u₁ u₂ u₃
+universe w' w v v₁ v₂ v₃ u u₁ u₂ u₃
 
 noncomputable section
 
@@ -113,9 +113,8 @@ In `glued_limit_cone`, we verify these obtained sections are indeed compatible,
 A `X ⟶ 𝒢(U)`. The remaining work is to verify that this is indeed the amalgamation and is unique.
 -/
 
-
-variable {C D : Type u} [Category.{v} C] [Category.{v} D] (G : C ⥤ D)
-variable {A : Type w} [Category.{max u v} A] [HasLimits A]
+variable {C D : Type*} [Category C] [Category D] (G : C ⥤ D)
+variable {A : Type w} [Category.{w'} A] [∀ X, HasLimitsOfShape (StructuredArrow X G.op) A]
 variable {J : GrothendieckTopology C} {K : GrothendieckTopology D}
   [G.IsCocontinuous J K]
 
@@ -125,10 +124,6 @@ variable {G}
 variable (ℱ : Sheaf J A)
 variable {X : A} {U : D} (S : Sieve U) (hS : S ∈ K U)
 
-instance (X : Dᵒᵖ) : HasLimitsOfShape (StructuredArrow X G.op) A :=
-  haveI := Limits.hasLimitsOfSizeShrink.{v, max u v, max u v, max u v} A
-  HasLimitsOfSize.has_limits_of_shape _
-
 variable (x : S.arrows.FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)))
 variable (hx : x.Compatible)
 

Mathlib/CategoryTheory/Sites/DenseSubsite.lean

@@ -521,10 +521,11 @@ namespace CategoryTheory.Functor.IsCoverDense
 
 open CategoryTheory
 
-variable {C D : Type u} [Category.{v} C] [Category.{v} D]
+universe w'
+variable {C D : Type*} [Category C] [Category D]
 variable (G : C ⥤ D) [Full G] [Faithful G]
 variable (J : GrothendieckTopology C) (K : GrothendieckTopology D)
-variable {A : Type w} [Category.{max u v} A] [Limits.HasLimits A]
+variable {A : Type w} [Category.{w'} A] [∀ X, Limits.HasLimitsOfShape (StructuredArrow X G.op) A]
 variable [G.IsCoverDense K] [G.IsContinuous J K] [G.IsCocontinuous J K]
 
 instance (Y : Sheaf J A) : IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y) := by

Mathlib/Condensed/Equivalence.lean

@@ -63,7 +63,8 @@ instance : Stonean.toCompHaus.EffectivelyEnough where
 /-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `CompHaus`
     (i.e. condensed sets). -/
 noncomputable
-def equivalence (A : Type*) [Category.{u+1} A] [HasLimits A] :
+def equivalence (A : Type*) [Category A]
+    [∀ X, HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A] :
     Sheaf (coherentTopology Stonean) A ≌ Condensed.{u} A :=
   coherentTopology.equivalence' Stonean.toCompHaus A
 
@@ -93,7 +94,8 @@ instance : Stonean.toProfinite.EffectivelyEnough where
 
 /-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `Profinite`. -/
 noncomputable
-def equivalence (A : Type*) [Category.{u+1} A] [HasLimits A] :
+def equivalence (A : Type*) [Category A]
+    [∀ X, HasLimitsOfShape (StructuredArrow X Stonean.toProfinite.op) A] :
     Sheaf (coherentTopology Stonean) A ≌ Sheaf (coherentTopology Profinite) A :=
   coherentTopology.equivalence' Stonean.toProfinite A
 
@@ -124,19 +126,24 @@ instance : profiniteToCompHaus.EffectivelyEnough where
 /-- The equivalence from coherent sheaves on `Profinite` to coherent sheaves on `CompHaus`
     (i.e. condensed sets). -/
 noncomputable
-def equivalence (A : Type*) [Category.{u+1} A] [HasLimits A] :
+def equivalence (A : Type*) [Category A]
+    [∀ X, HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A] :
     Sheaf (coherentTopology Profinite) A ≌ Condensed.{u} A :=
   coherentTopology.equivalence' profiniteToCompHaus A
 
 end ProfiniteCompHaus
 
-variable {A : Type*} [Category.{u+1} A] [HasLimits A] (X : Condensed.{u} A)
+variable {A : Type*} [Category A] (X : Condensed.{u} A)
 
-lemma isSheafProfinite : Presheaf.IsSheaf (coherentTopology Profinite)
+lemma isSheafProfinite
+    [∀ Y, HasLimitsOfShape (StructuredArrow Y profiniteToCompHaus.{u}.op) A] :
+    Presheaf.IsSheaf (coherentTopology Profinite)
     (profiniteToCompHaus.op ⋙ X.val) :=
   ((ProfiniteCompHaus.equivalence A).inverse.obj X).cond
 
-lemma isSheafStonean : Presheaf.IsSheaf (coherentTopology Stonean)
+lemma isSheafStonean
+    [∀ Y, HasLimitsOfShape (StructuredArrow Y Stonean.toCompHaus.{u}.op) A] :
+    Presheaf.IsSheaf (coherentTopology Stonean)
     (Stonean.toCompHaus.op ⋙ X.val) :=
   ((StoneanCompHaus.equivalence A).inverse.obj X).cond
 

Mathlib/Condensed/Explicit.lean

@@ -113,6 +113,8 @@ namespace Condensed
 variable {A : Type (u+2)} [Category.{u+1} A] (G : A ⥤ Type (u+1)) [HasLimits A] [PreservesLimits G]
     [G.ReflectsIsomorphisms]
 
+instance : HasLimitsOfSize.{u, u+1} A := hasLimitsOfSizeShrink.{u, u+1, u+1, u+1} _
+
 /-- The condensed set associated to a finite-product-preserving presheaf on `Stonean`. -/
 noncomputable def ofSheafStonean (F : Stonean.{u}ᵒᵖ ⥤ A) [PreservesFiniteProducts F] :
     Condensed A :=