refactor(topology/sheaves/sheaf_condition): Generalize unique gluing …

…API (#9002)

Previously, the sheaf condition in terms of unique gluings has been defined only for type-valued presheaves. This PR generalizes this to arbitrary concrete categories, whose forgetful functor preserves limits and reflects isomorphisms (e.g. algebraic categories like `CommRing`). As a side effect, this solves a TODO in `structure_sheaf.lean`.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebraic_geometry/structure_sheaf.lean

@@ -7,7 +7,6 @@ import algebraic_geometry.prime_spectrum
 import algebra.category.CommRing.colimits
 import algebra.category.CommRing.limits
 import topology.sheaves.local_predicate
-import topology.sheaves.forget
 import ring_theory.localization
 import ring_theory.subring
 
@@ -756,10 +755,7 @@ begin
   -- 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),
-
-  -- TODO: Add a version of `eq_of_locally_eq` for sheaves valued in representably concrete
-  -- categories. This will allow us to write `(structure_sheaf R).eq_of_locally_eq` here.
-  apply (structure_sheaf_in_Type R).eq_of_locally_eq'
+  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/topology/sheaves/local_predicate.lean

@@ -271,7 +271,7 @@ begin
   obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV,
   { -- Decompose everything into its constituent parts:
     dsimp,
-    simp only [stalk_to_fiber, colimit.ι_desc_apply] at h,
+    simp only [stalk_to_fiber, types.colimit.ι_desc_apply] at h,
     specialize w (unop U) (unop V) fU hU fV hV h,
     rcases w with ⟨W, iU, iV, w⟩,
     -- and put it back together again in the correct order.

src/topology/sheaves/sheaf_condition/equalizer_products.lean

@@ -8,6 +8,7 @@ import category_theory.limits.punit
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.equalizers
 import category_theory.full_subcategory
+import tactic.elementwise
 
 /-!
 # The sheaf condition in terms of an equalizer of products
@@ -67,9 +68,11 @@ are given by the restriction maps from `U j` to `U i ⊓ U j`.
 def res : F.obj (op (supr U)) ⟶ pi_opens F U :=
 pi.lift (λ i : ι, F.map (topological_space.opens.le_supr U i).op)
 
-@[simp] lemma res_π (i : ι) : res F U ≫ limit.π _ i = F.map (opens.le_supr U i).op :=
+@[simp, elementwise]
+lemma res_π (i : ι) : res F U ≫ limit.π _ i = F.map (opens.le_supr U i).op :=
 by rw [res, limit.lift_π, fan.mk_π_app]
 
+@[elementwise]
 lemma w : res F U ≫ left_res F U = res F U ≫ right_res F U :=
 begin
   dsimp [res, left_res, right_res],