feat(AlgebraicGeometry): constructor for IsColimit (Cofan.mk S f) (#22541)

Also generalizes some universe assumptions in `Mathlib.AlgebraicGeometry.Limits`.

Author: chrisflav

Mathlib/AlgebraicGeometry/Limits.lean

@@ -27,10 +27,12 @@ We construct various limits and colimits in the category of schemes.
 suppress_compilation
 
 
-universe u
+universe u v
 
 open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
 
+attribute [local instance] Opposite.small
+
 namespace AlgebraicGeometry
 
 /-- `Spec ℤ` is the terminal object in the category of schemes. -/
@@ -137,7 +139,6 @@ section Coproduct
 
 variable {ι : Type u} (f : ι → Scheme.{u})
 
-
 /-- (Implementation Detail) The glue data associated to a disjoint union. -/
 @[simps]
 noncomputable
@@ -203,31 +204,28 @@ instance : CreatesColimit (Discrete.functor f) Scheme.forgetToLocallyRingedSpace
     have := (IsColimit.precomposeHomEquiv F _).symm (toLocallyRingedSpaceCoproductCofanIsColimit f)
     (colimit.isoColimitCocone ⟨_, this⟩).symm
 
-noncomputable
-instance : CreatesColimitsOfShape (Discrete ι) Scheme.forgetToLocallyRingedSpace := by
-  constructor
-  intro K
-  exact createsColimitOfIsoDiagram _ (Discrete.natIsoFunctor (F := K)).symm
+variable {σ : Type v} (g : σ → Scheme.{u})
 
-instance : PreservesColimitsOfShape (Discrete ι) Scheme.forgetToTop.{u} :=
-  inferInstanceAs (PreservesColimitsOfShape (Discrete ι) (Scheme.forgetToLocallyRingedSpace ⋙
+noncomputable
+instance [Small.{u} σ] :
+    CreatesColimitsOfShape (Discrete σ) Scheme.forgetToLocallyRingedSpace.{u} := by
+  choose σ' eq using Small.equiv_small.{u} (α := σ)
+  let e : Discrete σ ≌ Discrete σ' := Discrete.equivalence eq.some
+  let _ : CreatesColimitsOfShape (Discrete σ') Scheme.forgetToLocallyRingedSpace := by
+    constructor
+    intro K
+    exact createsColimitOfIsoDiagram _ (Discrete.natIsoFunctor (F := K)).symm
+  apply CategoryTheory.createsColimitsOfShapeOfEquiv e.symm
+
+instance [Small.{u} σ] : PreservesColimitsOfShape (Discrete σ) Scheme.forgetToTop.{u} :=
+  inferInstanceAs (PreservesColimitsOfShape (Discrete σ) (Scheme.forgetToLocallyRingedSpace ⋙
       LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat))
 
-instance : HasCoproducts.{u} Scheme.{u} :=
-  fun _ ↦ ⟨fun _ ↦ hasColimit_of_created _ Scheme.forgetToLocallyRingedSpace⟩
-
-instance : HasCoproducts.{0} Scheme.{u} := has_smallest_coproducts_of_hasCoproducts
+instance [Small.{u} σ] : HasColimitsOfShape (Discrete σ) Scheme.{u} :=
+  ⟨fun _ ↦ hasColimit_of_created _ Scheme.forgetToLocallyRingedSpace⟩
 
-noncomputable
-instance {ι : Type} : PreservesColimitsOfShape (Discrete ι) Scheme.forgetToTop.{u} :=
-  preservesColimitsOfShape_of_equiv
-    (Discrete.equivalence Equiv.ulift : Discrete (ULift.{u} ι) ≌ _) _
-
-noncomputable
-instance {ι : Type} :
-    PreservesColimitsOfShape (Discrete ι) Scheme.forgetToLocallyRingedSpace.{u} :=
-  preservesColimitsOfShape_of_equiv
-    (Discrete.equivalence Equiv.ulift : Discrete (ULift.{u} ι) ≌ _) _
+instance [UnivLE.{v, u}] : HasCoproducts.{v} Scheme.{u} :=
+  fun _ ↦ ⟨fun _ ↦ hasColimit_of_created _ Scheme.forgetToLocallyRingedSpace⟩
 
 /-- (Implementation Detail) Coproduct of schemes is isomorphic to the disjoint union. -/
 noncomputable
@@ -256,6 +254,12 @@ instance (i) : IsOpenImmersion (Sigma.ι f i) := by
   rw [← ι_sigmaIsoGlued_inv]
   infer_instance
 
+instance [Small.{u} σ] (i) : IsOpenImmersion (Sigma.ι g i) := by
+  obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)
+  obtain ⟨i, rfl⟩ := e.symm.surjective i
+  rw [← Sigma.ι_reindex_hom e.symm g i]
+  infer_instance
+
 lemma sigmaι_eq_iff (i j : ι) (x y) :
     (Sigma.ι f i).base x = (Sigma.ι f j).base y ↔
       (Sigma.mk i x : Σ i, f i) = Sigma.mk j y := by
@@ -283,23 +287,28 @@ lemma disjoint_opensRange_sigmaι (i j : ι) (h : i ≠ j) :
   obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy
   cases h rfl
 
-lemma exists_sigmaι_eq (x : (∐ f :)) : ∃ i y, (Sigma.ι f i).base y = x := by
-  obtain ⟨i, y, e⟩ := (disjointGlueData f).ι_jointly_surjective ((sigmaIsoGlued f).hom.base x)
-  refine ⟨i, y, (sigmaIsoGlued f).hom.isOpenEmbedding.injective ?_⟩
-  rwa [← Scheme.comp_base_apply, ι_sigmaIsoGlued_hom]
+lemma exists_sigmaι_eq [Small.{u} σ] (x : (∐ g :)) : ∃ i y, (Sigma.ι g i).base y = x := by
+  obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)
+  let x' : (∐ g ∘ e.symm :) := (Sigma.reindex e.symm g).inv.base x
+  obtain ⟨i, y, h⟩ := (disjointGlueData <| g ∘ e.symm).ι_jointly_surjective
+    ((sigmaIsoGlued <| g ∘ e.symm).hom.base <| x')
+  refine ⟨e.symm i, y, (Sigma.reindex e.symm g).inv.isOpenEmbedding.injective ?_⟩
+  apply (sigmaIsoGlued _).hom.isOpenEmbedding.injective
+  rwa [← Scheme.comp_base_apply, ← Scheme.comp_base_apply, ← Scheme.comp_base_apply,
+    Sigma.ι_reindex_inv_assoc, ι_sigmaIsoGlued_hom]
 
 lemma iSup_opensRange_sigmaι : ⨆ i, (Sigma.ι f i).opensRange = ⊤ :=
   eq_top_iff.mpr fun x ↦ by simpa using exists_sigmaι_eq f x
 
 /-- The open cover of the coproduct. -/
 @[simps obj map]
 noncomputable
-def sigmaOpenCover : (∐ f).OpenCover where
-  J := ι
-  obj := f
-  map := Sigma.ι f
-  f x := (exists_sigmaι_eq f x).choose
-  covers x := (exists_sigmaι_eq f x).choose_spec
+def sigmaOpenCover [Small.{u} σ] : (∐ g).OpenCover where
+  J := σ
+  obj := g
+  map := Sigma.ι g
+  f x := (exists_sigmaι_eq g x).choose
+  covers x := (exists_sigmaι_eq g x).choose_spec
 
 /-- The underlying topological space of the coproduct is homeomorphic to the disjoint union. -/
 noncomputable
@@ -318,8 +327,8 @@ lemma sigmaMk_mk (i) (x : f i) :
   exact ι_comp_sigmaComparison Scheme.forgetToTop _ _
 
 open scoped Function in
-lemma isOpenImmersion_sigmaDesc
-    {X : Scheme} (α : ∀ i, f i ⟶ X) [∀ i, IsOpenImmersion (α i)]
+private lemma isOpenImmersion_sigmaDesc_aux
+    {X : Scheme.{u}} (α : ∀ i, f i ⟶ X) [∀ i, IsOpenImmersion (α i)]
     (hα : Pairwise (Disjoint on (Set.range <| α · |>.base))) :
     IsOpenImmersion (Sigma.desc α) := by
   rw [IsOpenImmersion.iff_stalk_iso]
@@ -346,6 +355,38 @@ lemma isOpenImmersion_sigmaDesc
     · simp [← Scheme.comp_base_apply]
     · simp [← Scheme.stalkMap_comp, Scheme.stalkMap_congr_hom _ _ (Sigma.ι_desc _ _)]
 
+open scoped Function in
+lemma isOpenImmersion_sigmaDesc [Small.{u} σ]
+    {X : Scheme.{u}} (α : ∀ i, g i ⟶ X) [∀ i, IsOpenImmersion (α i)]
+    (hα : Pairwise (Disjoint on (Set.range <| α · |>.base))) :
+    IsOpenImmersion (Sigma.desc α) := by
+  obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)
+  convert IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)
+  · refine Sigma.hom_ext _ _ fun i ↦ ?_
+    obtain ⟨i, rfl⟩ := e.symm.surjective i
+    simp
+  · apply isOpenImmersion_sigmaDesc_aux
+    intro i j hij
+    exact hα (fun h ↦ hij (e.symm.injective h))
+
+open scoped Function in
+/-- `S` is the disjoint union of `Xᵢ` if the `Xᵢ` are covering, pairwise disjoint open subschemes
+of `S`. -/
+lemma nonempty_isColimit_cofanMk_of [Small.{u} σ]
+    {X : σ → Scheme.{u}} {S : Scheme.{u}} (f : ∀ i, X i ⟶ S) [∀ i, IsOpenImmersion (f i)]
+    (hcov : ⨆ i, (f i).opensRange = ⊤) (hdisj : Pairwise (Disjoint on (f · |>.opensRange))) :
+    Nonempty (IsColimit <| Cofan.mk S f) := by
+  have : IsOpenImmersion (Sigma.desc f) := by
+    refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)
+    simpa [Function.onFun_apply, disjoint_iff, Opens.ext_iff] using hdisj hij
+  simp only [← Cofan.isColimit_iff_isIso_sigmaDesc (Cofan.mk S f), cofan_mk_inj, Cofan.mk_pt]
+  apply isIso_of_isOpenImmersion_of_opensRange_eq_top
+  rw [eq_top_iff]
+  intro x hx
+  have : x ∈ ⨆ i, (f i).opensRange := by rwa [hcov]
+  obtain ⟨i, y, rfl⟩ := by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this
+  use Sigma.ι X i |>.base y
+  simp [← Scheme.comp_base_apply]
 
 variable (X Y : Scheme.{u})
 
@@ -371,7 +412,7 @@ lemma isCompl_range_inl_inr :
     IsCompl (Set.range (coprod.inl : X ⟶ X ⨿ Y).base)
       (Set.range (coprod.inr : Y ⟶ X ⨿ Y).base) :=
   ((TopCat.binaryCofan_isColimit_iff _).mp
-    ⟨mapIsColimitOfPreservesOfIsColimit Scheme.forgetToTop _ _ (coprodIsCoprod X Y)⟩).2.2
+    ⟨mapIsColimitOfPreservesOfIsColimit Scheme.forgetToTop.{u} _ _ (coprodIsCoprod X Y)⟩).2.2
 
 lemma isCompl_opensRange_inl_inr :
     IsCompl (coprod.inl : X ⟶ X ⨿ Y).opensRange (coprod.inr : Y ⟶ X ⨿ Y).opensRange := by
@@ -421,6 +462,26 @@ def coprodOpenCover.{w} : (X ⨿ Y).OpenCover where
     · simp only [Sum.elim_inr, coprodMk_inr, exists_apply_eq_apply]
   map_prop x := x.rec (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)
 
+/-- If `X` and `Y` are open disjoint and covering open subschemes of `S`,
+`S` is the disjoint union of `X` and `Y`. -/
+lemma nonempty_isColimit_binaryCofanMk_of_isCompl {X Y S : Scheme.{u}}
+    (f : X ⟶ S) (g : Y ⟶ S) [IsOpenImmersion f] [IsOpenImmersion g]
+    (hf : IsCompl f.opensRange g.opensRange) :
+    Nonempty (IsColimit <| BinaryCofan.mk f g) := by
+  let c' : Cofan fun j ↦ (WalkingPair.casesOn j X Y : Scheme.{u}) :=
+    .mk S fun j ↦ WalkingPair.casesOn j f g
+  let i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl _) (by rintro (b|b) <;> rfl)
+  refine ⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩
+  let fi (j : WalkingPair) : WalkingPair.casesOn j X Y ⟶ S := WalkingPair.casesOn j f g
+  convert nonempty_isColimit_cofanMk_of fi _ _
+  · intro i
+    cases i <;> (simp [fi]; infer_instance)
+  · simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2
+  · intro i j hij
+    match i, j with
+    | .left, .right => simpa [fi] using hf.1
+    | .right, .left => simpa [fi] using hf.1.symm
+
 variable (R S : Type u) [CommRing R] [CommRing S]
 
 /-- The map `Spec R ⨿ Spec S ⟶ Spec (R × S)`.
@@ -484,7 +545,7 @@ instance : IsIso (coprodSpec R S) := by
   · ext x; exact coprodSpec_apply R S x
   · infer_instance
 
-instance (R S : CommRingCatᵒᵖ) : IsIso (coprodComparison Scheme.Spec R S) := by
+instance (R S : CommRingCat.{u}ᵒᵖ) : IsIso (coprodComparison Scheme.Spec R S) := by
   obtain ⟨R⟩ := R; obtain ⟨S⟩ := S
   have : coprodComparison Scheme.Spec (.op R) (.op S) ≫ (Spec.map
     ((limit.isoLimitCone ⟨_, CommRingCat.prodFanIsLimit R S⟩).inv ≫
@@ -501,22 +562,22 @@ instance (R S : CommRingCatᵒᵖ) : IsIso (coprodComparison Scheme.Spec R S) :=
   rw [(IsIso.eq_comp_inv _).mpr this]
   infer_instance
 
-instance : PreservesColimitsOfShape (Discrete WalkingPair) Scheme.Spec :=
+instance : PreservesColimitsOfShape (Discrete WalkingPair) Scheme.Spec.{u} :=
   ⟨fun {_} ↦
-    have (X Y : CommRingCatᵒᵖ) := PreservesColimitPair.of_iso_coprod_comparison Scheme.Spec X Y
+    have (X Y : CommRingCat.{u}ᵒᵖ) := PreservesColimitPair.of_iso_coprod_comparison Scheme.Spec X Y
     preservesColimit_of_iso_diagram _ (diagramIsoPair _).symm⟩
 
-instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec := by
+instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec.{u} := by
   have : IsEmpty (Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ)) :=
     @Function.isEmpty _ _ spec_punit_isEmpty (Scheme.Spec.mapIso
       (initialIsoIsInitial (initialOpOfTerminal CommRingCat.punitIsTerminal))).hom.base
   have := preservesInitial_of_iso Scheme.Spec (asIso (initial.to _))
   exact preservesColimitsOfShape_pempty_of_preservesInitial _
 
-instance {J} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec :=
+instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec.{u} :=
   preservesFiniteCoproductsOfPreservesBinaryAndInitial _ _
 
-instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec :=
+instance {J : Type*} [Finite J] : PreservesColimitsOfShape (Discrete J) Scheme.Spec.{u} :=
   letI := (nonempty_fintype J).some
   preservesColimitsOfShape_of_equiv (Discrete.equivalence (Fintype.equivFin _).symm) _
 
@@ -545,7 +606,7 @@ instance (i) (R : ι → Type _) [∀ i, CommRing (R i)] :
     · exact Function.surjective_eval _
   exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)
 
-instance (R : ι → CommRingCat) : IsOpenImmersion (sigmaSpec R) := by
+instance (R : ι → CommRingCat.{u}) : IsOpenImmersion (sigmaSpec R) := by
   classical
   apply isOpenImmersion_sigmaDesc
   intro ix iy h
@@ -556,7 +617,7 @@ instance (R : ι → CommRingCat) : IsOpenImmersion (sigmaSpec R) := by
       (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
   simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this
 
-instance [Finite ι] (R : ι → CommRingCat) : IsIso (sigmaSpec R) := by
+instance [Finite ι] (R : ι → CommRingCat.{u}) : IsIso (sigmaSpec R) := by
   have : sigmaSpec R =
       (colimit.isoColimitCocone ⟨_,
         (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves

Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

@@ -58,12 +58,8 @@ instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion f]
     [IsPreimmersion g] : IsPreimmersion (f ≫ g) :=
   MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance
 
-instance (priority := 900) {X Y} (f : X ⟶ Y) [IsPreimmersion f] : Mono f := by
-  refine (Scheme.forgetToLocallyRingedSpace ⋙
-    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
-  apply SheafedSpace.mono_of_base_injective_of_stalk_epi
-  · exact f.isEmbedding.injective
-  · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)
+instance (priority := 900) {X Y} (f : X ⟶ Y) [IsPreimmersion f] : Mono f :=
+  SurjectiveOnStalks.mono_of_injective f.isEmbedding.injective
 
 theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
     [IsPreimmersion (f ≫ g)] : IsPreimmersion f where

Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

@@ -89,6 +89,14 @@ instance stableUnderBaseChange :
   intros R S T _ _ _ _ _ H
   exact H.baseChange
 
+variable {f} in
+lemma mono_of_injective [SurjectiveOnStalks f] (hf : Function.Injective f.base) : Mono f := by
+  refine (Scheme.forgetToLocallyRingedSpace ⋙
+    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
+  apply SheafedSpace.mono_of_base_injective_of_stalk_epi
+  · exact hf
+  · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)
+
 /-- If `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of
 `X × Y` (cartesian product as topological spaces) with the induced topology. -/
 lemma isEmbedding_pullback {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) [SurjectiveOnStalks g] :

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -673,6 +673,13 @@ instance {Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsOpenImmersion f]
 
 end IsOpenImmersion
 
+lemma isIso_of_isOpenImmersion_of_opensRange_eq_top {X Y : Scheme.{u}} (f : X ⟶ Y)
+    [IsOpenImmersion f] (hf : f.opensRange = ⊤) : IsIso f := by
+  rw [isIso_iff_isOpenImmersion]
+  refine ⟨inferInstance, ?_⟩
+  rw [TopCat.epi_iff_surjective, ← Set.range_eq_univ]
+  exact TopologicalSpace.Opens.ext_iff.mp hf
+
 section MorphismProperty
 
 instance isOpenImmersion_isStableUnderComposition :

Mathlib/Data/Opposite.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Reid Barton, Simon Hudon, Kenny Lau
 -/
 import Mathlib.Logic.Equiv.Defs
+import Mathlib.Logic.Small.Defs
 
 /-!
 # Opposites
@@ -110,4 +111,10 @@ so you don't need to use `induction x using Opposite.rec'`. -/
 @[simp, induction_eliminator]
 protected def rec' {F : αᵒᵖ → Sort v} (h : ∀ X, F (op X)) : ∀ X, F X := fun X => h (unop X)
 
+/-- If `X` is `u`-small, also `Xᵒᵖ` is `u`-small.
+Note: This is not an instance, because it tends to mislead typeclass search. -/
+lemma small {X : Type v} [Small.{u} X] : Small.{u} Xᵒᵖ := by
+  obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)
+  exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩
+
 end Opposite

Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

@@ -24,10 +24,12 @@ universe w' w v u
 
 open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
 
+attribute [local instance] Opposite.small
+
 namespace SheafedSpace
 
 variable {C : Type u} [Category.{v} C]
-variable {J : Type w} [Category.{w'} J] [UnivLE.{w, v}] (F : J ⥤ SheafedSpace.{_, _, v} C)
+variable {J : Type w} [Category.{w'} J] [Small.{v} J] (F : J ⥤ SheafedSpace.{_, _, v} C)
 
 theorem isColimit_exists_rep [HasLimitsOfShape Jᵒᵖ C] {c : Cocone F} (hc : IsColimit c) (x : c.pt) :
     ∃ (i : J) (y : F.obj i), (c.ι.app i).base y = x :=
@@ -51,7 +53,7 @@ namespace LocallyRingedSpace
 
 section HasCoproducts
 
-variable {ι : Type v} [UnivLE.{v, u}] (F : Discrete ι ⥤ LocallyRingedSpace.{u})
+variable {ι : Type v} [Small.{u} ι] (F : Discrete ι ⥤ LocallyRingedSpace.{u})
 
 /-- The explicit coproduct for `F : discrete ι ⥤ LocallyRingedSpace`. -/
 noncomputable def coproduct : LocallyRingedSpace where
@@ -102,11 +104,10 @@ noncomputable def coproductCofanIsColimit : IsColimit (coproductCofan F) where
       (IsColimit.uniq _ (forgetToSheafedSpace.mapCocone s) f.toShHom fun j =>
         congr_arg LocallyRingedSpace.Hom.toShHom (h j))
 
-instance : HasCoproducts.{v} LocallyRingedSpace.{u} := fun _ =>
+instance : HasColimitsOfShape (Discrete ι) LocallyRingedSpace.{u} :=
   ⟨fun F => ⟨⟨⟨_, coproductCofanIsColimit F⟩⟩⟩⟩
 
-noncomputable instance (J : Type v) :
-    PreservesColimitsOfShape (Discrete.{v} J) forgetToSheafedSpace.{u} :=
+noncomputable instance : PreservesColimitsOfShape (Discrete.{v} ι) forgetToSheafedSpace.{u} :=
   ⟨fun {G} =>
     preservesColimit_of_preserves_colimit_cocone (coproductCofanIsColimit G)
       ((colimit.isColimit (C := SheafedSpace.{u+1, u, u} CommRingCat.{u}) _).ofIsoColimit

Mathlib/Geometry/RingedSpace/SheafedSpace.lean

@@ -194,7 +194,7 @@ theorem Γ_map {X Y : (SheafedSpace C)ᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.
 theorem Γ_map_op {X Y : SheafedSpace C} (f : X ⟶ Y) : Γ.map f.op = f.c.app (op ⊤) :=
   rfl
 
-noncomputable instance (J : Type w) [Category.{w'} J] [UnivLE.{w, v}] [HasLimitsOfShape Jᵒᵖ C] :
+noncomputable instance (J : Type w) [Category.{w'} J] [Small.{v} J] [HasLimitsOfShape Jᵒᵖ C] :
     CreatesColimitsOfShape J (forgetToPresheafedSpace : SheafedSpace.{_, _, v} C ⥤ _) :=
   ⟨fun {K} =>
     createsColimitOfFullyFaithfulOfIso
@@ -205,13 +205,13 @@ noncomputable instance (J : Type w) [Category.{w'} J] [UnivLE.{w, v}] [HasLimits
 noncomputable instance [HasLimits C] :
     CreatesColimits (forgetToPresheafedSpace : SheafedSpace C ⥤ _) where
 
-instance (J : Type w) [Category.{w'} J] [UnivLE.{w, v}] [HasLimitsOfShape Jᵒᵖ C] :
+instance (J : Type w) [Category.{w'} J] [Small.{v} J] [HasLimitsOfShape Jᵒᵖ C] :
     HasColimitsOfShape J (SheafedSpace.{_, _, v} C) :=
   hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape forgetToPresheafedSpace
 
 instance [HasLimits C] : HasColimits.{v} (SheafedSpace C) where
 
-instance (J : Type w) [Category.{w'} J] [UnivLE.{w, v}] [HasLimitsOfShape Jᵒᵖ C] :
+instance (J : Type w) [Category.{w'} J] [Small.{v} J] [HasLimitsOfShape Jᵒᵖ C] :
     PreservesColimitsOfShape J (forget.{_, _, v} C) :=
   Limits.comp_preservesColimitsOfShape forgetToPresheafedSpace (PresheafedSpace.forget C)