Revert "chore(topology/sheaves/*): universe generalizations (#19153)"

This reverts commit 1336155.

src/algebraic_geometry/morphisms/quasi_compact.lean

@@ -298,7 +298,7 @@ end
 
 /-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then
 `f ^ n * x = 0` for some `n`. -/
-lemma exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact (X : Scheme.{u})
+lemma exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact (X : Scheme)
   {U : opens X.carrier} (hU : is_compact U.1) (x f : X.presheaf.obj (op U))
   (H : x |_ X.basic_open f = 0) :
   ∃ n : ℕ, f ^ n * x = 0 :=
@@ -322,7 +322,7 @@ begin
   use finset.univ.sup n,
   suffices : ∀ (i : s), X.presheaf.map (hom_of_le (h₁ i)).op (f ^ (finset.univ.sup n) * x) = 0,
   { subst e,
-    apply Top.sheaf.eq_of_locally_eq.{(u+1) u} X.sheaf (λ (i : s), (i : opens X.carrier)),
+    apply X.sheaf.eq_of_locally_eq (λ (i : s), (i : opens X.carrier)),
     intro i,
     rw map_zero,
     apply this },

src/algebraic_geometry/morphisms/quasi_separated.lean

@@ -345,7 +345,7 @@ begin
   exact e
 end
 
-lemma exists_eq_pow_mul_of_is_compact_of_is_quasi_separated (X : Scheme.{u})
+lemma exists_eq_pow_mul_of_is_compact_of_is_quasi_separated (X : Scheme)
   (U : opens X.carrier) (hU : is_compact U.1) (hU' : is_quasi_separated U.1)
   (f : X.presheaf.obj (op U)) (x : X.presheaf.obj (op $ X.basic_open f)) :
   ∃ (n : ℕ) (y : X.presheaf.obj (op U)), y |_ X.basic_open f = (f |_ X.basic_open f) ^ n * x :=
@@ -401,7 +401,7 @@ begin
       ((X.presheaf.map (hom_of_le le_sup_left).op f) ^ (finset.univ.sup n + n₂) * y₁) =
         X.presheaf.map (hom_of_le $ inf_le_right).op
           ((X.presheaf.map (hom_of_le le_sup_right).op f) ^ (finset.univ.sup n + n₁) * y₂),
-    { fapply Top.sheaf.eq_of_locally_eq'.{(u+1) u} X.sheaf (λ i : s, i.1.1),
+    { fapply X.sheaf.eq_of_locally_eq' (λ i : s, i.1.1),
       { refine λ i, hom_of_le _, erw hs, exact le_supr _ _ },
       { exact le_of_eq hs },
       { intro i,
@@ -419,7 +419,7 @@ begin
     -- By the sheaf condition, since `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`, it can be glued into
     -- the desired section on `S ∪ U`.
     use (X.sheaf.obj_sup_iso_prod_eq_locus S U.1).inv ⟨⟨_ * _, _ * _⟩, this⟩,
-    refine Top.sheaf.eq_of_locally_eq₂.{(u+1) u} X.sheaf
+    refine X.sheaf.eq_of_locally_eq₂
       (hom_of_le (_ : X.basic_open (X.presheaf.map (hom_of_le le_sup_left).op f) ≤ _))
       (hom_of_le (_ : X.basic_open (X.presheaf.map (hom_of_le le_sup_right).op f) ≤ _)) _ _ _ _ _,
     { rw X.basic_open_res, exact inf_le_right },

src/algebraic_geometry/ringed_space.lean

@@ -76,7 +76,7 @@ begin
   -- Let `g x` denote the inverse of `f` in `U x`.
   choose g hg using λ x : U, is_unit.exists_right_inv (h_unit x),
   -- We claim that these local inverses glue together to a global inverse of `f`.
-  obtain ⟨gl, gl_spec, -⟩ := Top.sheaf.exists_unique_gluing'.{(v+1) v} X.sheaf V U iVU hcover g _,
+  obtain ⟨gl, gl_spec, -⟩ := X.sheaf.exists_unique_gluing' V U iVU hcover g _,
   swap,
   { intros x y,
     apply section_ext X.sheaf (V x ⊓ V y),
@@ -89,7 +89,7 @@ begin
       congr_arg (X.presheaf.germ (⟨z, hzVy⟩ : V y)) (hg y),
       ring_hom.map_one, ring_hom.map_one] },
   apply is_unit_of_mul_eq_one f gl,
-  apply Top.sheaf.eq_of_locally_eq'.{(v+1) v} X.sheaf V U iVU hcover,
+  apply X.sheaf.eq_of_locally_eq' V U iVU hcover,
   intro i,
   rw [ring_hom.map_one, ring_hom.map_mul, gl_spec],
   exact hg i,

src/algebraic_geometry/structure_sheaf.lean

@@ -772,10 +772,10 @@ begin
   rw to_basic_open_mk',
 
   -- Since the structure sheaf is a sheaf, we can show the desired equality locally.
-  -- Annoyingly, `sheaf.eq_of_locally_eq'` requires an open cover indexed by a *type*, so we need to
+  -- Annoyingly, `sheaf.eq_of_locally_eq` requires an open cover indexed by a *type*, so we need to
   -- coerce our finset `t` to a type first.
   let tt := ((t : set (basic_open f)) : Type u),
-  apply Top.sheaf.eq_of_locally_eq'.{(u+1) u} (structure_sheaf R)
+  apply (structure_sheaf R).eq_of_locally_eq'
     (λ i : tt, basic_open (h i)) (basic_open f) (λ i : tt, iDh i),
   { -- This feels a little redundant, since already have `ht_cover` as a hypothesis
     -- Unfortunately, `ht_cover` uses a bounded union over the set `t`, while here we have the

src/category_theory/limits/shapes/types.lean

@@ -51,28 +51,13 @@ local attribute [tidy] tactic.discrete_cases
 /-- A restatement of `types.lift_π_apply` that uses `pi.π` and `pi.lift`. -/
 @[simp]
 lemma pi_lift_π_apply
-  {β : Type v} (f : β → Type max v u) {P : Type max v u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
-  (pi.π f b : (∏ f) → f b) (@pi.lift β _ _ f _ P s x) = s b x :=
-congr_fun (limit.lift_π (fan.mk P s) ⟨b⟩) x
-
-/-- A restatement of `types.lift_π_apply` that uses `pi.π` and `pi.lift`,
-with specialized universes. -/
-@[simp]
-lemma pi_lift_π_apply'
-  {β : Type v} (f : β → Type v) {P : Type v} (s : Π b, P ⟶ f b) (b : β) (x : P) :
+  {β : Type u} (f : β → Type u) {P : Type u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
   (pi.π f b : (∏ f) → f b) (@pi.lift β _ _ f _ P s x) = s b x :=
 congr_fun (limit.lift_π (fan.mk P s) ⟨b⟩) x
 
 /-- A restatement of `types.map_π_apply` that uses `pi.π` and `pi.map`. -/
 @[simp]
-lemma pi_map_π_apply {β : Type v} {f g : β → Type max v u} (α : Π j, f j ⟶ g j) (b : β) (x) :
-  (pi.π g b : (∏ g) → g b) (pi.map α x) = α b ((pi.π f b : (∏ f) → f b) x) :=
-limit.map_π_apply _ _ _
-
-/-- A restatement of `types.map_π_apply` that uses `pi.π` and `pi.map`,
-with specialized universes. -/
-@[simp]
-lemma pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : Π j, f j ⟶ g j) (b : β) (x) :
+lemma pi_map_π_apply {β : Type u} {f g : β → Type u} (α : Π j, f j ⟶ g j) (b : β) (x) :
   (pi.π g b : (∏ g) → g b) (pi.map α x) = α b ((pi.π f b : (∏ f) → f b) x) :=
 limit.map_π_apply _ _ _
 

src/topology/sheaves/forget.lean

@@ -42,13 +42,13 @@ namespace sheaf_condition
 
 open sheaf_condition_equalizer_products
 
-universes v u₁ u₂ w
+universes v u₁ u₂
 
-variables {C : Type u₁} [category.{v} C] [has_limits_of_size.{w w} C]
-variables {D : Type u₂} [category.{v} D] [has_limits_of_size.{w w} D]
-variables (G : C ⥤ D) [preserves_limits_of_size.{w w} G]
-variables {X : Top.{w}} (F : presheaf C X)
-variables {ι : Type w} (U : ι → opens X)
+variables {C : Type u₁} [category.{v} C] [has_limits C]
+variables {D : Type u₂} [category.{v} D] [has_limits D]
+variables (G : C ⥤ D) [preserves_limits G]
+variables {X : Top.{v}} (F : presheaf C X)
+variables {ι : Type v} (U : ι → opens X)
 
 local attribute [reducible] diagram left_res right_res
 
@@ -57,7 +57,7 @@ When `G` preserves limits, the sheaf condition diagram for `F` composed with `G`
 naturally isomorphic to the sheaf condition diagram for `F ⋙ G`.
 -/
 def diagram_comp_preserves_limits :
-  diagram F U ⋙ G ≅ diagram.{w} (F ⋙ G) U :=
+  diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U :=
 begin
   fapply nat_iso.of_components,
   rintro ⟨j⟩,
@@ -85,7 +85,7 @@ When `G` preserves limits, the image under `G` of the sheaf condition fork for `
 is the sheaf condition fork for `F ⋙ G`,
 postcomposed with the inverse of the natural isomorphism `diagram_comp_preserves_limits`.
 -/
-def map_cone_fork : G.map_cone (fork.{w} F U) ≅
+def map_cone_fork : G.map_cone (fork.{v} F U) ≅
   (cones.postcompose (diagram_comp_preserves_limits G F U).inv).obj (fork (F ⋙ G) U) :=
 cones.ext (iso.refl _) (λ j,
 begin
@@ -102,17 +102,16 @@ end)
 
 end sheaf_condition
 
-universes v u₁ u₂ w
+universes v u₁ u₂
 
 open sheaf_condition sheaf_condition_equalizer_products
 
 variables {C : Type u₁} [category.{v} C] {D : Type u₂} [category.{v} D]
 variables (G : C ⥤ D)
 variables [reflects_isomorphisms G]
-variables [has_limits_of_size.{w w} C] [has_limits_of_size.{w w} D]
-  [preserves_limits_of_size.{w w} G]
+variables [has_limits C] [has_limits D] [preserves_limits G]
 
-variables {X : Top.{w}} (F : presheaf C X)
+variables {X : Top.{v}} (F : presheaf C X)
 
 /--
 If `G : C ⥤ D` is a functor which reflects isomorphisms and preserves limits
@@ -172,7 +171,7 @@ begin
       -- image under `G` of the equalizer cone for the sheaf condition diagram.
       let c := fork (F ⋙ G) U,
       obtain ⟨hc⟩ := S U,
-      let d := G.map_cone (equalizer.fork (left_res.{w} F U) (right_res F U)),
+      let d := G.map_cone (equalizer.fork (left_res.{v} F U) (right_res F U)),
       letI := preserves_smallest_limits_of_preserves_limits G,
       have hd : is_limit d := preserves_limit.preserves (limit.is_limit _),
       -- Since both of these are limit cones
@@ -183,8 +182,7 @@ begin
       -- introduced above.
       let d' := (cones.postcompose (diagram_comp_preserves_limits G F U).hom).obj d,
       have hd' : is_limit d' :=
-        (is_limit.postcompose_hom_equiv
-          (diagram_comp_preserves_limits.{v u₁ u₂ w} G F U : _) d).symm hd,
+        (is_limit.postcompose_hom_equiv (diagram_comp_preserves_limits G F U : _) d).symm hd,
       -- Now everything works: we verify that `f` really is a morphism between these cones:
       let f' : c ⟶ d' :=
       fork.mk_hom (G.map f)

src/topology/sheaves/local_predicate.lean

@@ -38,12 +38,12 @@ to the types in the ambient type family.
 We give conditions sufficient to show that this map is injective and/or surjective.
 -/
 
-universes v w
+universe v
 
 noncomputable theory
 
 variables {X : Top.{v}}
-variables (T : X → Type w)
+variables (T : X → Type v)
 
 open topological_space
 open opposite
@@ -69,12 +69,12 @@ variables (X)
 Continuity is a "prelocal" predicate on functions to a fixed topological space `T`.
 -/
 @[simps]
-def continuous_prelocal (T : Top.{w}) : prelocal_predicate (λ x : X, T) :=
+def continuous_prelocal (T : Top.{v}) : prelocal_predicate (λ x : X, T) :=
 { pred := λ U f, continuous f,
   res := λ U V i f h, continuous.comp h (opens.open_embedding_of_le i.le).continuous, }
 
 /-- Satisfying the inhabited linter. -/
-instance inhabited_prelocal_predicate (T : Top.{w}) : inhabited (prelocal_predicate (λ x : X, T)) :=
+instance inhabited_prelocal_predicate (T : Top.{v}) : inhabited (prelocal_predicate (λ x : X, T)) :=
 ⟨continuous_prelocal X T⟩
 
 variables {X}
@@ -150,7 +150,7 @@ lemma prelocal_predicate.sheafify_of {T : X → Type v} {P : prelocal_predicate
 The subpresheaf of dependent functions on `X` satisfying the "pre-local" predicate `P`.
 -/
 @[simps]
-def subpresheaf_to_Types (P : prelocal_predicate T) : presheaf (Type (max v w)) X :=
+def subpresheaf_to_Types (P : prelocal_predicate T) : presheaf (Type v) X :=
 { obj := λ U, { f : Π x : unop U, T x // P.pred f },
   map := λ U V i f, ⟨λ x, f.1 (i.unop x), P.res i.unop f.1 f.2⟩ }.
 
@@ -211,27 +211,22 @@ end subpresheaf_to_Types
 The subsheaf of the sheaf of all dependently typed functions satisfying the local predicate `P`.
 -/
 @[simps]
-def subsheaf_to_Types (P : local_predicate T) : sheaf (Type max v w) X :=
+def subsheaf_to_Types (P : local_predicate T) : sheaf (Type v) X :=
 ⟨subpresheaf_to_Types P.to_prelocal_predicate, subpresheaf_to_Types.is_sheaf P⟩
 
--- TODO There is further universe generalization to do here,
--- but it depends on more difficult universe generalization in `topology.sheaves.stalks`.
--- The aim is to replace `T'` with the more general `T` below.
-variables {T' : X → Type v}
-
 /--
 There is a canonical map from the stalk to the original fiber, given by evaluating sections.
 -/
-def stalk_to_fiber (P : local_predicate T') (x : X) :
-  (subsheaf_to_Types P).presheaf.stalk x ⟶ T' x :=
+def stalk_to_fiber (P : local_predicate T) (x : X) :
+  (subsheaf_to_Types P).presheaf.stalk x ⟶ T x :=
 begin
   refine colimit.desc _
-    { X := T' x, ι := { app := λ U f, _, naturality' := _ } },
+    { X := T x, ι := { app := λ U f, _, naturality' := _ } },
   { exact f.1 ⟨x, (unop U).2⟩, },
   { tidy, }
 end
 
-@[simp] lemma stalk_to_fiber_germ (P : local_predicate T') (U : opens X) (x : U) (f) :
+@[simp] lemma stalk_to_fiber_germ (P : local_predicate T) (U : opens X) (x : U) (f) :
   stalk_to_fiber P x ((subsheaf_to_Types P).presheaf.germ x f) = f.1 x :=
 begin
   dsimp [presheaf.germ, stalk_to_fiber],
@@ -244,8 +239,8 @@ end
 The `stalk_to_fiber` map is surjective at `x` if
 every point in the fiber `T x` has an allowed section passing through it.
 -/
-lemma stalk_to_fiber_surjective (P : local_predicate T') (x : X)
-  (w : ∀ (t : T' x), ∃ (U : open_nhds x) (f : Π y : U.1, T' y) (h : P.pred f), f ⟨x, U.2⟩ = t) :
+lemma stalk_to_fiber_surjective (P : local_predicate T) (x : X)
+  (w : ∀ (t : T x), ∃ (U : open_nhds x) (f : Π y : U.1, T y) (h : P.pred f), f ⟨x, U.2⟩ = t) :
   function.surjective (stalk_to_fiber P x) :=
 λ t,
 begin
@@ -259,16 +254,16 @@ end
 The `stalk_to_fiber` map is injective at `x` if any two allowed sections which agree at `x`
 agree on some neighborhood of `x`.
 -/
-lemma stalk_to_fiber_injective (P : local_predicate T') (x : X)
-  (w : ∀ (U V : open_nhds x) (fU : Π y : U.1, T' y) (hU : P.pred fU)
-    (fV : Π y : V.1, T' y) (hV : P.pred fV) (e : fU ⟨x, U.2⟩ = fV ⟨x, V.2⟩),
+lemma stalk_to_fiber_injective (P : local_predicate T) (x : X)
+  (w : ∀ (U V : open_nhds x) (fU : Π y : U.1, T y) (hU : P.pred fU)
+    (fV : Π y : V.1, T y) (hV : P.pred fV) (e : fU ⟨x, U.2⟩ = fV ⟨x, V.2⟩),
     ∃ (W : open_nhds x) (iU : W ⟶ U) (iV : W ⟶ V), ∀ (w : W.1), fU (iU w : U.1) = fV (iV w : V.1)) :
   function.injective (stalk_to_fiber P x) :=
 λ tU tV h,
 begin
   -- We promise to provide all the ingredients of the proof later:
   let Q :
-    ∃ (W : (open_nhds x)ᵒᵖ) (s : Π w : (unop W).1, T' w) (hW : P.pred s),
+    ∃ (W : (open_nhds x)ᵒᵖ) (s : Π w : (unop W).1, T w) (hW : P.pred s),
       tU = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
       tV = (subsheaf_to_Types P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ := _,
   { choose W s hW e using Q,
@@ -288,9 +283,6 @@ begin
            colimit_sound iV.op (subtype.eq (funext w).symm)⟩, },
 end
 
--- TODO to continue generalizing universes here, we will need to deal with the issue noted
--- at `presheaf_to_Top` (universe generalization for the Yoneda embedding).
-
 /--
 Some repackaging:
 the presheaf of functions satisfying `continuous_prelocal` is just the same thing as

src/topology/sheaves/presheaf.lean

@@ -221,7 +221,7 @@ def pushforward_map {X Y : Top.{w}} (f : X ⟶ Y) {ℱ 𝒢 : X.presheaf C} (α
 
 open category_theory.limits
 section pullback
-variable [has_colimits_of_size.{w w} C]
+variable [has_colimits C]
 noncomputable theory
 
 /--
@@ -231,17 +231,17 @@ This is defined in terms of left Kan extensions, which is just a fancy way of sa
 "take the colimits over the open sets whose preimage contains U".
 -/
 @[simps]
-def pullback_obj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : Y.presheaf C) : X.presheaf C :=
+def pullback_obj {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : Y.presheaf C) : X.presheaf C :=
 (Lan (opens.map f).op).obj ℱ
 
 /-- Pulling back along continuous maps is functorial. -/
-def pullback_map {X Y : Top.{w}} (f : X ⟶ Y) {ℱ 𝒢 : Y.presheaf C} (α : ℱ ⟶ 𝒢) :
+def pullback_map {X Y : Top.{v}} (f : X ⟶ Y) {ℱ 𝒢 : Y.presheaf C} (α : ℱ ⟶ 𝒢) :
   pullback_obj f ℱ ⟶ pullback_obj f 𝒢 :=
 (Lan (opens.map f).op).map α
 
 /-- If `f '' U` is open, then `f⁻¹ℱ U ≅ ℱ (f '' U)`.  -/
 @[simps]
-def pullback_obj_obj_of_image_open {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : Y.presheaf C) (U : opens X)
+def pullback_obj_obj_of_image_open {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : Y.presheaf C) (U : opens X)
   (H : is_open (f '' U)) : (pullback_obj f ℱ).obj (op U) ≅ ℱ.obj (op ⟨_, H⟩) :=
 begin
   let x : costructured_arrow (opens.map f).op (op U) := begin
@@ -263,7 +263,7 @@ begin
 end
 
 namespace pullback
-variables {X Y : Top.{w}} (ℱ : Y.presheaf C)
+variables {X Y : Top.{v}} (ℱ : Y.presheaf C)
 
 /-- The pullback along the identity is isomorphic to the original presheaf. -/
 def id : pullback_obj (𝟙 _) ℱ ≅ ℱ :=
@@ -366,30 +366,30 @@ by simpa [pushforward_to_of_iso, equivalence.to_adjunction]
 
 end iso
 
-variables (C) [has_colimits_of_size.{w w} C]
+variables (C) [has_colimits C]
 
 /-- Pullback a presheaf on `Y` along a continuous map `f : X ⟶ Y`, obtaining a presheaf
 on `X`. -/
 @[simps map_app]
-def pullback {X Y : Top.{w}} (f : X ⟶ Y) : Y.presheaf C ⥤ X.presheaf C := Lan (opens.map f).op
+def pullback {X Y : Top.{v}} (f : X ⟶ Y) : Y.presheaf C ⥤ X.presheaf C := Lan (opens.map f).op
 
 @[simp] lemma pullback_obj_eq_pullback_obj {C} [category C] [has_colimits C] {X Y : Top.{w}}
   (f : X ⟶ Y) (ℱ : Y.presheaf C) : (pullback C f).obj ℱ = pullback_obj f ℱ := rfl
 
 /-- The pullback and pushforward along a continuous map are adjoint to each other. -/
 @[simps unit_app_app counit_app_app]
-def pushforward_pullback_adjunction {X Y : Top.{w}} (f : X ⟶ Y) :
+def pushforward_pullback_adjunction {X Y : Top.{v}} (f : X ⟶ Y) :
   pullback C f ⊣ pushforward C f := Lan.adjunction _ _
 
 /-- Pulling back along a homeomorphism is the same as pushing forward along its inverse. -/
-def pullback_hom_iso_pushforward_inv {X Y : Top.{w}} (H : X ≅ Y) :
+def pullback_hom_iso_pushforward_inv {X Y : Top.{v}} (H : X ≅ Y) :
   pullback C H.hom ≅ pushforward C H.inv :=
 adjunction.left_adjoint_uniq
   (pushforward_pullback_adjunction C H.hom)
   (presheaf_equiv_of_iso C H.symm).to_adjunction
 
 /-- Pulling back along the inverse of a homeomorphism is the same as pushing forward along it. -/
-def pullback_inv_iso_pushforward_hom {X Y : Top.{w}} (H : X ≅ Y) :
+def pullback_inv_iso_pushforward_hom {X Y : Top.{v}} (H : X ≅ Y) :
   pullback C H.inv ≅ pushforward C H.hom :=
 adjunction.left_adjoint_uniq
   (pushforward_pullback_adjunction C H.inv)