feat(topology/sheaves/sheaf_condition/opens_le_cover): generalize uni…

…verse (#16214)

+ Generalize universe levels in the sheaf condition `opens_le_cover` on topological spaces and its equivalence with the sheaf condition on sites, allowing three different universe parameters as in `Top.{w}`, `C : Type u` and `category.{v} C`. To be used in #15934.

+ Generalize universes for the sheaf condition `pairwise_intersection` on topological spaces. This sheaf condition also doesn't require any assumption on the category `C`, and its equivalence with `opens_le_cover` could also have universe levels at maximal generality; however, the proof `is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections` breaks due to the `small_category` restriction on [category_theory.functor.initial.is_limit_whisker_equiv](https://leanprover-community.github.io/mathlib_docs/category_theory/limits/final.html#category_theory.functor.initial.is_limit_whisker_equiv), which will take more work to fix, so we do not generalize the equivalence at this time.

+ Generalize universes for `Top.presheaf.pushforward`; pullback is not generalized because it would need `has_colimits_of_size`. `Top.sheaf.pushforward` is not yet generalized.

+ Fixate the universe level of [Top.presheaf](https://leanprover-community.github.io/mathlib_docs/topology/sheaves/presheaf.html#Top.presheaf) to be the same as [Top.sheaf](https://leanprover-community.github.io/mathlib_docs/topology/sheaves/sheaf.html#Top.sheaf).

src/algebraic_geometry/locally_ringed_space.lean

@@ -132,7 +132,7 @@ forget_to_SheafedSpace ⋙ SheafedSpace.forget _
 @[simp] lemma comp_val {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).val = f.val ≫ g.val := rfl
 
-@[simp] lemma comp_val_c {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
+@[simp] lemma comp_val_c {X Y Z : LocallyRingedSpace.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).val.c = g.val.c ≫ (presheaf.pushforward _ g.val.base).map f.val.c := rfl
 
 lemma comp_val_c_app {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (opens Z)ᵒᵖ) :

src/topology/sheaves/presheaf.lean

@@ -38,7 +38,7 @@ namespace Top
 
 /-- The category of `C`-valued presheaves on a (bundled) topological space `X`. -/
 @[derive category, nolint has_nonempty_instance]
-def presheaf (X : Top.{w}) := (opens X)ᵒᵖ ⥤ C
+def presheaf (X : Top.{w}) : Type (max u v w) := (opens X)ᵒᵖ ⥤ C
 
 variables {C}
 
@@ -222,16 +222,16 @@ variable (C)
 /--
 The pushforward functor.
 -/
-def pushforward {X Y : Top.{v}} (f : X ⟶ Y) : X.presheaf C ⥤ Y.presheaf C :=
+def pushforward {X Y : Top.{w}} (f : X ⟶ Y) : X.presheaf C ⥤ Y.presheaf C :=
 { obj := pushforward_obj f,
   map := @pushforward_map _ _ X Y f }
 
 @[simp]
-lemma pushforward_map_app' {X Y : Top.{v}} (f : X ⟶ Y)
+lemma pushforward_map_app' {X Y : Top.{w}} (f : X ⟶ Y)
   {ℱ 𝒢 : X.presheaf C} (α : ℱ ⟶ 𝒢) {U : (opens Y)ᵒᵖ} :
   ((pushforward C f).map α).app U = α.app (op $ (opens.map f).obj U.unop) := rfl
 
-lemma id_pushforward {X : Top.{v}} : pushforward C (𝟙 X) = 𝟭 (X.presheaf C) :=
+lemma id_pushforward {X : Top.{w}} : pushforward C (𝟙 X) = 𝟭 (X.presheaf C) :=
 begin
   apply category_theory.functor.ext,
   { intros,

src/topology/sheaves/sheaf_condition/opens_le_cover.lean

@@ -25,7 +25,7 @@ or equivalently whether we're looking at the first or second object in an equali
 * This is the definition Lurie uses in [Spectral Algebraic Geometry][LurieSAG].
 -/
 
-universes v u
+universes w v u
 
 noncomputable theory
 
@@ -38,7 +38,7 @@ open topological_space.opens
 namespace Top
 
 variables {C : Type u} [category.{v} C]
-variables {X : Top.{v}} (F : presheaf C X) {ι : Type v} (U : ι → opens X)
+variables {X : Top.{w}} (F : presheaf C X) {ι : Type w} (U : ι → opens X)
 
 namespace presheaf
 
@@ -48,7 +48,7 @@ namespace sheaf_condition
 The category of open sets contained in some element of the cover.
 -/
 @[derive category]
-def opens_le_cover : Type v := full_subcategory (λ (V : opens X), ∃ i, V ≤ U i)
+def opens_le_cover : Type w := full_subcategory (λ (V : opens X), ∃ i, V ≤ U i)
 
 instance [inhabited ι] : inhabited (opens_le_cover U) :=
 ⟨⟨⊥, default, bot_le⟩⟩
@@ -93,7 +93,7 @@ A presheaf is a sheaf if `F` sends the cone `(opens_le_cover_cocone U).op` to a
 mapping down to any `V` which is contained in some `U i`.)
 -/
 def is_sheaf_opens_le_cover : Prop :=
-∀ ⦃ι : Type v⦄ (U : ι → opens X), nonempty (is_limit (F.map_cone (opens_le_cover_cocone U).op))
+∀ ⦃ι : Type w⦄ (U : ι → opens X), nonempty (is_limit (F.map_cone (opens_le_cover_cocone U).op))
 
 namespace sheaf_condition
 
@@ -215,7 +215,7 @@ in terms of a limit diagram over all `{ V : opens X // ∃ i, V ≤ U i }`
 is equivalent to the reformulation
 in terms of a limit diagram over `U i` and `U i ⊓ U j`.
 -/
-lemma is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections (F : presheaf C X) :
+lemma is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections {X : Top.{v}} (F : presheaf C X) :
   F.is_sheaf_opens_le_cover ↔ F.is_sheaf_pairwise_intersections :=
 forall₂_congr $ λ ι U, equiv.nonempty_congr $
   calc is_limit (F.map_cone (opens_le_cover_cocone U).op)

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -33,7 +33,7 @@ We express this in two equivalent ways, as
 
 noncomputable theory
 
-universes v u
+universes w v u
 
 open topological_space
 open Top
@@ -43,10 +43,11 @@ open category_theory.limits
 
 namespace Top.presheaf
 
-variables {X : Top.{v}}
-
 variables {C : Type u} [category.{v} C]
 
+section
+variables {X : Top.{w}}
+
 /--
 An alternative formulation of the sheaf condition
 (which we prove equivalent to the usual one below as
@@ -56,7 +57,7 @@ A presheaf is a sheaf if `F` sends the cone `(pairwise.cocone U).op` to a limit
 (Recall `pairwise.cocone U` has cone point `supr U`, mapping down to the `U i` and the `U i ⊓ U j`.)
 -/
 def is_sheaf_pairwise_intersections (F : presheaf C X) : Prop :=
-∀ ⦃ι : Type v⦄ (U : ι → opens X), nonempty (is_limit (F.map_cone (pairwise.cocone U).op))
+∀ ⦃ι : Type w⦄ (U : ι → opens X), nonempty (is_limit (F.map_cone (pairwise.cocone U).op))
 
 /--
 An alternative formulation of the sheaf condition
@@ -68,14 +69,16 @@ A presheaf is a sheaf if `F` preserves the limit of `pairwise.diagram U`.
 `U i ⊓ U j` mapping into the open sets `U i`. This diagram has limit `supr U`.)
 -/
 def is_sheaf_preserves_limit_pairwise_intersections (F : presheaf C X) : Prop :=
-∀ ⦃ι : Type v⦄ (U : ι → opens X), nonempty (preserves_limit (pairwise.diagram U).op F)
+∀ ⦃ι : Type w⦄ (U : ι → opens X), nonempty (preserves_limit (pairwise.diagram U).op F)
+
+end
 
 /-!
 The remainder of this file shows that these conditions are equivalent
 to the usual sheaf condition.
 -/
 
-variables [has_products.{v} C]
+variables {X : Top.{v}} [has_products.{v} C]
 
 namespace sheaf_condition_pairwise_intersections