chore(topology/sheaf_condition): is_sheaf_iff_pairwise_intersections …

…without products (#17181)

+ Generalize universes in *category_theory/limits/final* in order to generalize universe in `is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections`, from which we deduce `is_sheaf_iff_is_sheaf_pairwise_intersection` in full generality; the original version of this lemma with a `has_products` assumption now has `'` appended to its name, and will be removed in a future refactor.

+ As applications, we remove `has_products` from the definition of the pushforward functor in *topology/sheaves/functors* (and generalize universes there), and from skyscraper sheaves.

src/category_theory/limits/final.lean

@@ -57,7 +57,7 @@ Dualise condition 3 above and the implications 2 ⇒ 3 and 3 ⇒ 1 to initial fu
 
 noncomputable theory
 
-universes v u
+universes v v₁ v₂ v₃ u₁ u₂ u₃
 
 namespace category_theory
 
@@ -66,8 +66,10 @@ namespace functor
 open opposite
 open category_theory.limits
 
-variables {C : Type v} [small_category C]
-variables {D : Type v} [small_category D]
+section arbitrary_universe
+
+variables {C : Type u₁} [category.{v₁} C]
+variables {D : Type u₂} [category.{v₂} D]
 
 /--
 A functor `F : C ⥤ D` is final if for every `d : D`, the comma category of morphisms `d ⟶ F.obj c`
@@ -137,7 +139,7 @@ variables (F : C ⥤ D) [final F]
 
 instance (d : D) : nonempty (structured_arrow d F) := is_connected.is_nonempty
 
-variables {E : Type u} [category.{v} E] (G : D ⥤ E)
+variables {E : Type u₃} [category.{v₃} E] (G : D ⥤ E)
 
 /--
 When `F : C ⥤ D` is cofinal, we denote by `lift F d` an arbitrary choice of object in `C` such that
@@ -320,9 +322,15 @@ https://stacks.math.columbia.edu/tag/04E7
 -/
 def colimit_iso' [has_colimit (F ⋙ G)] : colimit (F ⋙ G) ≅ colimit G := as_iso (colimit.pre G F)
 
-
 end
 
+end final
+end arbitrary_universe
+
+namespace final
+
+variables {C : Type v} [category.{v} C] {D : Type v} [category.{v} D] (F : C ⥤ D) [final F]
+
 /--
 If the universal morphism `colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d))`
 is an isomorphism (as it always is when `F` is cofinal),
@@ -381,11 +389,11 @@ end final
 
 namespace initial
 
-variables (F : C ⥤ D) [initial F]
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D] (F : C ⥤ D) [initial F]
 
 instance (d : D) : nonempty (costructured_arrow F d) := is_connected.is_nonempty
 
-variables {E : Type u} [category.{v} E] (G : D ⥤ E)
+variables {E : Type u₃} [category.{v₃} E] (G : D ⥤ E)
 
 /--
 When `F : C ⥤ D` is initial, we denote by `lift F d` an arbitrary choice of object in `C` such that

src/topology/sheaves/functors.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
 
-import topology.sheaves.sheaf_condition.pairwise_intersections
+import topology.sheaves.sheaf_condition.opens_le_cover
 
 /-!
 # functors between categories of sheaves
@@ -19,15 +19,15 @@ TODO: pullback for presheaves and sheaves
 
 noncomputable theory
 
-universes v u u₁
+universes w v u
 
 open category_theory
 open category_theory.limits
 open topological_space
 
-variables {C : Type u₁} [category.{v} C]
-variables {X Y : Top.{v}} (f : X ⟶ Y)
-variables ⦃ι : Type v⦄ {U : ι → opens Y}
+variables {C : Type u} [category.{v} C]
+variables {X Y : Top.{w}} (f : X ⟶ Y)
+variables ⦃ι : Type w⦄ {U : ι → opens Y}
 
 namespace Top
 namespace presheaf.sheaf_condition_pairwise_intersections
@@ -66,8 +66,6 @@ namespace sheaf
 
 open presheaf
 
-variables [has_products.{v} C]
-
 /--
 The pushforward of a sheaf (by a continuous map) is a sheaf.
 -/

src/topology/sheaves/sheaf_condition/opens_le_cover.lean

@@ -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 {X : Top.{v}} (F : presheaf C X) :
+lemma is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections :
   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)
@@ -315,6 +315,15 @@ begin
     rw ← (is_limit_opens_le_equiv_generate₂ F S hS).nonempty_congr, apply h },
 end
 
+/--
+The sheaf condition in terms of an equalizer diagram is equivalent
+to the reformulation in terms of a limit diagram over `U i` and `U i ⊓ U j`.
+-/
+lemma is_sheaf_iff_is_sheaf_pairwise_intersections :
+  F.is_sheaf ↔ F.is_sheaf_pairwise_intersections :=
+by rw [is_sheaf_iff_is_sheaf_opens_le_cover,
+  is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections]
+
 end
 
 end presheaf

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -362,16 +362,17 @@ is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U)).symm Q)
   hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], },
   inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, }
 
-
 end sheaf_condition_pairwise_intersections
 
 open sheaf_condition_pairwise_intersections
 
 /--
 The sheaf condition in terms of an equalizer diagram is equivalent
 to the reformulation in terms of a limit diagram over `U i` and `U i ⊓ U j`.
+A more general version `is_sheaf_iff_is_sheaf_pairwise_intersections` without
+the `has_products` assumption is available in a later file.
 -/
-lemma is_sheaf_iff_is_sheaf_pairwise_intersections (F : presheaf C X) :
+lemma is_sheaf_iff_is_sheaf_pairwise_intersections' (F : presheaf C X) :
   F.is_sheaf ↔ F.is_sheaf_pairwise_intersections :=
 (is_sheaf_iff_is_sheaf_equalizer_products F).trans $
 iff.intro (λ h ι U, ⟨is_limit_map_cone_of_is_limit_sheaf_condition_fork F U (h U).some⟩)
@@ -385,7 +386,7 @@ consisting of the `U i` and `U i ⊓ U j`.
 lemma is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections (F : presheaf C X) :
   F.is_sheaf ↔ F.is_sheaf_preserves_limit_pairwise_intersections :=
 begin
-  rw is_sheaf_iff_is_sheaf_pairwise_intersections,
+  rw is_sheaf_iff_is_sheaf_pairwise_intersections',
   split,
   { intros h ι U,
     exact ⟨preserves_limit_of_preserves_limit_cone (pairwise.cocone_is_colimit U).op (h U).some⟩ },
@@ -436,7 +437,7 @@ begin
       exacts [⟨⟨walking_pair.left⟩, h⟩, ⟨⟨walking_pair.right⟩, h⟩] },
     { rintro ⟨⟨_ | _⟩, h⟩,
       exacts [or.inl h, or.inr h] } },
-  refine (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 ι).some.lift
+  refine (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 ι).some.lift
     ⟨s.X, { app := _, naturality' := _ }⟩ ≫ F.1.map (eq_to_hom hι).op,
   { apply opposite.rec,
     rintro ((_|_)|(_|_)),
@@ -459,15 +460,15 @@ lemma inter_union_pullback_cone_lift_left :
 begin
   dsimp,
   erw [category.assoc, ←F.1.map_comp],
-  exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 _).some.fac _
+  exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 _).some.fac _
     (op $ pairwise.single (ulift.up walking_pair.left))
 end
 
 lemma inter_union_pullback_cone_lift_right :
   inter_union_pullback_cone_lift F U V s ≫ F.1.map (hom_of_le le_sup_right).op = s.snd :=
 begin
   erw [category.assoc, ←F.1.map_comp],
-  exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 _).some.fac _
+  exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 _).some.fac _
     (op $ pairwise.single (ulift.up walking_pair.right))
 end
 
@@ -491,7 +492,7 @@ begin
   { apply inter_union_pullback_cone_lift_right },
   { intros m h₁ h₂,
     rw ← cancel_mono (F.1.map (eq_to_hom hι.symm).op),
-    apply (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 ι).some.hom_ext,
+    apply (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 ι).some.hom_ext,
     apply opposite.rec,
     rintro ((_|_)|(_|_)); rw [category.assoc, category.assoc],
     { erw ← F.1.map_comp,

src/topology/sheaves/skyscraper.lean

@@ -211,7 +211,7 @@ def skyscraper_presheaf_stalk_of_not_specializes_is_terminal
   [has_colimits C] {y : X} (h : ¬p₀ ⤳ y) : is_terminal ((skyscraper_presheaf p₀ A).stalk y) :=
 is_terminal.of_iso terminal_is_terminal $ (skyscraper_presheaf_stalk_of_not_specializes _ _ h).symm
 
-lemma skyscraper_presheaf_is_sheaf [has_products.{u} C] : (skyscraper_presheaf p₀ A).is_sheaf :=
+lemma skyscraper_presheaf_is_sheaf : (skyscraper_presheaf p₀ A).is_sheaf :=
 by classical; exact (presheaf.is_sheaf_iso_iff
   (eq_to_iso $ skyscraper_presheaf_eq_pushforward p₀ A)).mpr
   (sheaf.pushforward_sheaf_of_sheaf _ (presheaf.is_sheaf_on_punit_of_is_terminal _
@@ -221,15 +221,15 @@ by classical; exact (presheaf.is_sheaf_iso_iff
 The skyscraper presheaf supported at `p₀` with value `A` is the sheaf that assigns `A` to all opens
 `U` that contain `p₀` and assigns `*` otherwise.
 -/
-def skyscraper_sheaf [has_products.{u} C] : sheaf C X :=
+def skyscraper_sheaf : sheaf C X :=
 ⟨skyscraper_presheaf p₀ A, skyscraper_presheaf_is_sheaf _ _⟩
 
 /--
 Taking skyscraper sheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
 sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
 `p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
 -/
-def skyscraper_sheaf_functor [has_products.{u} C] : C ⥤ sheaf C X :=
+def skyscraper_sheaf_functor : C ⥤ sheaf C X :=
 { obj := λ c, skyscraper_sheaf p₀ c,
   map := λ a b f, Sheaf.hom.mk $ (skyscraper_presheaf_functor p₀).map f,
   map_id' := λ c, Sheaf.hom.ext _ _ $ (skyscraper_presheaf_functor p₀).map_id _,
@@ -363,7 +363,7 @@ instance [has_colimits C] : is_left_adjoint (presheaf.stalk_functor C p₀) :=
 /--
 Taking stalks of a sheaf is the left adjoint functor to `skyscraper_sheaf_functor`
 -/
-def stalk_skyscraper_sheaf_adjunction [has_colimits C] [has_products.{u} C] :
+def stalk_skyscraper_sheaf_adjunction [has_colimits C] :
   sheaf.forget C X ⋙ presheaf.stalk_functor _ p₀ ⊣ skyscraper_sheaf_functor p₀ :=
 { hom_equiv := λ 𝓕 c,
   ⟨λ f, ⟨to_skyscraper_presheaf p₀ f⟩, λ g, from_stalk p₀ g.1, from_stalk_to_skyscraper p₀,
@@ -377,8 +377,7 @@ def stalk_skyscraper_sheaf_adjunction [has_colimits C] [has_products.{u} C] :
     by { ext1, exact (skyscraper_presheaf_stalk_adjunction p₀).hom_equiv_unit },
   hom_equiv_counit' := λ 𝓐 c f, (skyscraper_presheaf_stalk_adjunction p₀).hom_equiv_counit }
 
-instance [has_colimits C] [has_products.{u} C] :
-  is_right_adjoint (skyscraper_sheaf_functor p₀ : C ⥤ sheaf C X) :=
+instance [has_colimits C] : is_right_adjoint (skyscraper_sheaf_functor p₀ : C ⥤ sheaf C X) :=
 ⟨_, stalk_skyscraper_sheaf_adjunction _⟩
 
 end