refactor(topology/sheaf_condition): remove redundant constructions (#…

…17378)

The constructions used to prove `is_sheaf_iff_is_sheaf_equalizer_products` in *sites.lean* is redundant because the equivalence can now be achieved via `is_sheaf` (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff.

The author @justus-springer of the constructions has previously [approved the removal](#11706 (comment)) in #11706.

The universe levels in *equalizer_products.lean* are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions.

- [x] depends on: #17361 



Co-authored-by: erd1 <the.erd.one@gmail.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/category_theory/sites/cover_preserving.lean

@@ -163,7 +163,7 @@ begin
 end
 
 lemma compatible_preserving_of_downwards_closed (F : C ⥤ D) [full F] [faithful F]
-  (hF : ∀ {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F :=
+  (hF : Π {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F :=
 begin
   constructor,
   introv hx he,

src/topology/sheaves/forget.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.limits.preserves.shapes.products
-import topology.sheaves.sheaf_condition.sites
+import topology.sheaves.sheaf_condition.equalizer_products
 
 /-!
 # Checking the sheaf condition on the underlying presheaf of types.
@@ -54,7 +54,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 (F ⋙ G) U :=
+  diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U :=
 begin
   fapply nat_iso.of_components,
   rintro ⟨j⟩,
@@ -82,7 +82,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 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
@@ -168,7 +168,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 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

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.opens_le_cover
+import topology.sheaves.sheaf_condition.pairwise_intersections
 
 /-!
 # functors between categories of sheaves

src/topology/sheaves/limits.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import topology.sheaves.sheaf_condition.sites
+import topology.sheaves.sheaf
 import category_theory.sites.limits
 import category_theory.adjunction
 import category_theory.limits.functor_category

src/topology/sheaves/operations.lean

@@ -9,7 +9,6 @@ import algebra.category.Ring.filtered_colimits
 import algebra.category.Group.limits
 import ring_theory.localization.basic
 import topology.sheaves.sheafify
-import topology.sheaves.sheaf_condition.sites
 
 /-!
 

src/topology/sheaves/sheaf.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import topology.sheaves.sheaf_condition.equalizer_products
+import topology.sheaves.presheaf
 import category_theory.full_subcategory
 import category_theory.limits.unit
 import category_theory.sites.sheaf
@@ -44,8 +44,6 @@ variables {X : Top.{w}} (F : presheaf C X) {ι : Type v} (U : ι → opens X)
 
 namespace presheaf
 
-open sheaf_condition_equalizer_products
-
 /--
 The sheaf condition has several different equivalent formulations.
 The official definition chosen here is in terms of grothendieck topologies so that the results on
@@ -64,11 +62,13 @@ The equivalent formulations of the sheaf condition on `presheaf C X` are as foll
   See `Top.presheaf.is_sheaf_iff_is_sheaf_equalizer_products`.
 
 3. `Top.presheaf.is_sheaf_opens_le_cover`:
-  Each `F(U)` is the (inverse) limit of all `F(V)` with `V ⊆ U`.
+  For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
+  `F(V₁) ⟶ F(V₂)` for every pair of open sets `V₁ ⊇ V₂` that are contained in some `Uᵢ`.
   See `Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover`.
 
 4. `Top.presheaf.is_sheaf_pairwise_intersections`:
-  For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of all `F(Uᵢ)` and all `F(Uᵢ ∩ Uⱼ)`.
+  For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
+  from `F(Uᵢ)` and `F(Uⱼ)` to `F(Uᵢ ∩ Uⱼ)` for each pair `(i, j)`.
   See `Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections`.
 
 The following requires `C` to be concrete and complete, and `forget C` to reflect isomorphisms and