feat(topology/sheaves): alternate formulation of the sheaf condition (#4190)

Currently the sheaf condition is stated as it often is in textbooks, e.g. 
https://stacks.math.columbia.edu/tag/0072. That is, it is about an equalizer of the two maps `∏ F.obj (U i) ⟶ ∏ F.obj (U i) ⊓ (U j)`.

This PR adds an equivalent formulation, saying that `F.obj (supr U)` (with its natural projection maps) is the limit of the diagram consisting of the `F.obj (U i)` and the `F.obj (U i ⊓ U j)`. 

I'd like to add further reformulations in subsequent PRs, in particular the nice one I saw in Lurie's SAG, just saying that `F.obj (supr U)` is the limit over the diagram of all `F.obj V` where `V` is an open subset of *some* `U i`. This version is actually much nicer to formalise, and I'm hoping we can translate over quite a lot of what we've already done about the sheaf condition to that version 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebraic_geometry/sheafed_space.lean

@@ -33,7 +33,7 @@ namespace algebraic_geometry
 
 /-- A `SheafedSpace C` is a topological space equipped with a sheaf of `C`s. -/
 structure SheafedSpace extends PresheafedSpace C :=
-(sheaf_condition : sheaf_condition presheaf)
+(sheaf_condition : presheaf.sheaf_condition)
 
 variables {C}
 
@@ -55,7 +55,7 @@ instance (X : SheafedSpace.{v} C) : topological_space X := X.carrier.str
 /-- The trivial `punit` valued sheaf on any topological space. -/
 noncomputable
 def punit (X : Top) : SheafedSpace (discrete punit) :=
-{ sheaf_condition := sheaf_condition_punit _,
+{ sheaf_condition := presheaf.sheaf_condition_punit _,
   ..@PresheafedSpace.const (discrete punit) _ X punit.star }
 
 noncomputable
@@ -101,6 +101,8 @@ def forget : SheafedSpace C ⥤ Top :=
 
 end
 
+open Top.presheaf
+
 /--
 The restriction of a sheafed space along an open embedding into the space.
 -/
@@ -109,7 +111,7 @@ def restrict {U : Top} (X : SheafedSpace C)
   (f : U ⟶ (X : Top.{v})) (h : open_embedding f) : SheafedSpace C :=
 { sheaf_condition := λ ι 𝒰, is_limit.of_iso_limit
     ((is_limit.postcompose_inv_equiv _ _).inv_fun (X.sheaf_condition _))
-    (sheaf_condition.fork.iso_of_open_embedding h 𝒰).symm,
+    (sheaf_condition_equalizer_products.fork.iso_of_open_embedding h 𝒰).symm,
   ..X.to_PresheafedSpace.restrict f h }
 
 /--

src/algebraic_geometry/structure_sheaf.lean

@@ -307,6 +307,8 @@ nat_iso.of_components
   (λ U, iso.refl _)
   (by tidy)
 
+open Top.presheaf
+
 /--
 The structure sheaf on $Spec R$, valued in `CommRing`.
 

src/category_theory/category/pairwise.lean

@@ -0,0 +1,150 @@
+import topology.sheaves.sheaf
+import category_theory.limits.preserves.basic
+
+/-!
+# The category of "pairwise intersections".
+
+Given `ι : Type v`, we build the diagram category `pairwise ι`
+with objects `single i` and `pair i j`, for `i j : ι`,
+whose only non-identity morphisms are
+`left : single i ⟶ pair i j` and `right : single j ⟶ pair i j`.
+
+We use this later in describing the sheaf condition.
+
+Given any function `U : ι → α`, where `α` is some complete lattice (e.g. `opens X`),
+we produce a functor `pairwise ι ⥤ αᵒᵖ` in the obvious way,
+and show that `supr U` provides a limit cone over this functor.
+-/
+
+noncomputable theory
+
+universes v u
+
+open topological_space
+open Top
+open opposite
+open category_theory
+open category_theory.limits
+
+namespace category_theory
+
+/--
+An inductive type representing either a single term of a type `ι`, or a pair of terms.
+We use this as the objects of a category to describe the sheaf condition.
+-/
+inductive pairwise (ι : Type v)
+| single : ι → pairwise
+| pair : ι → ι → pairwise
+
+variables {ι : Type v}
+
+namespace pairwise
+
+instance pairwise_inhabited [inhabited ι] : inhabited (pairwise ι) := ⟨single (default ι)⟩
+
+/--
+Morphisms in the category `pairwise ι`. The only non-identity morphisms are
+`left i j : single i ⟶ pair i j` and `right i j : single j ⟶ pair i j`.
+-/
+inductive hom : pairwise ι → pairwise ι → Type v
+| id_single : Π i, hom (single i) (single i)
+| id_pair : Π i j, hom (pair i j) (pair i j)
+| left : Π i j, hom (single i) (pair i j)
+| right : Π i j, hom (single j) (pair i j)
+
+open hom
+
+instance hom_inhabited [inhabited ι] : inhabited (hom (single (default ι)) (single (default ι))) :=
+⟨id_single (default ι)⟩
+
+/--
+The identity morphism in `pairwise ι`.
+-/
+def id : Π (o : pairwise ι), hom o o
+| (single i) := id_single i
+| (pair i j) := id_pair i j
+
+/-- Composition of morphisms in `pairwise ι`. -/
+def comp : Π {o₁ o₂ o₃ : pairwise ι} (f : hom o₁ o₂) (g : hom o₂ o₃), hom o₁ o₃
+| _ _ _ (id_single i) g := g
+| _ _ _ (id_pair i j) g := g
+| _ _ _ (left i j) (id_pair _ _) := left i j
+| _ _ _ (right i j) (id_pair _ _) := right i j
+
+section
+local attribute [tidy] tactic.case_bash
+
+instance : category (pairwise ι) :=
+{ hom := hom,
+  id := id,
+  comp := λ X Y Z f g, comp f g, }
+
+end
+
+variables {α : Type v} (U : ι → α)
+
+section
+variables [semilattice_inf α]
+
+/-- Auxilliary definition for `diagram`. -/
+@[simp]
+def diagram_obj : pairwise ι → αᵒᵖ
+| (single i) := op (U i)
+| (pair i j) := op (U i ⊓ U j)
+
+/-- Auxilliary definition for `diagram`. -/
+@[simp]
+def diagram_map : Π {o₁ o₂ : pairwise ι} (f : o₁ ⟶ o₂), diagram_obj U o₁ ⟶ diagram_obj U o₂
+| _ _ (id_single i) := 𝟙 _
+| _ _ (id_pair i j) := 𝟙 _
+| _ _ (left i j) := (hom_of_le inf_le_left).op
+| _ _ (right i j) := (hom_of_le inf_le_right).op
+
+/--
+Given a function `U : ι → α` for `[semilattice_inf α]`, we obtain a functor `pairwise ι ⥤ αᵒᵖ`,
+sending `single i` to `op (U i)` and `pair i j` to `op (U i ⊓ U j)`,
+and the morphisms to the obvious inequalities.
+-/
+@[simps]
+def diagram : pairwise ι ⥤ αᵒᵖ :=
+{ obj := diagram_obj U,
+  map := λ X Y f, diagram_map U f, }
+
+end
+
+section
+-- `complete_lattice` is not really needed, as we only ever use `inf`,
+-- but the appropriate structure has not been defined.
+variables [complete_lattice α]
+
+/-- Auxilliary definition for `cone`. -/
+def cone_π_app : Π (o : pairwise ι), op (supr U) ⟶ diagram_obj U o
+| (single i) := (hom_of_le (le_supr _ _)).op
+| (pair i j) := (hom_of_le inf_le_left ≫ hom_of_le (le_supr U i)).op
+
+/--
+Given a function `U : ι → α` for `[complete_lattice α]`,
+`supr U` provides a cone over `diagram U`.
+-/
+@[simps]
+def cone : cone (diagram U) :=
+{ X := op (supr U),
+  π := { app := cone_π_app U, } }
+
+/--
+Given a function `U : ι → α` for `[complete_lattice α]`,
+`supr U` provides a limit cone over `diagram U`.
+-/
+def cone_is_limit : is_limit (cone U) :=
+{ lift := λ s, op_hom_of_le
+  begin
+    apply complete_lattice.Sup_le,
+    rintros _ ⟨j, rfl⟩,
+    exact le_of_op_hom (s.π.app (single j))
+  end }
+
+end
+
+end pairwise
+
+end category_theory

src/category_theory/opposites.lean

@@ -303,4 +303,14 @@ rfl
 lemma op_equiv_symm_apply (A B : Cᵒᵖ) (f : B.unop ⟶ A.unop) : (op_equiv _ _).symm f = f.op :=
 rfl
 
+universes v
+variables {α : Type v} [preorder α]
+
+/-- Construct a morphism in the opposite of a preorder category from an inequality. -/
+def op_hom_of_le {U V : αᵒᵖ} (h : unop V ≤ unop U) : U ⟶ V :=
+has_hom.hom.op (hom_of_le h)
+
+lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U :=
+le_of_hom (h.unop)
+
 end category_theory

src/topology/sheaves/forget.lean

@@ -34,8 +34,12 @@ open opposite
 
 namespace Top
 
+namespace presheaf
+
 namespace sheaf_condition
 
+open sheaf_condition_equalizer_products
+
 universes v u₁ u₂
 
 variables {C : Type u₁} [category.{v} C] [has_limits C]
@@ -44,15 +48,14 @@ variables (G : C ⥤ D) [preserves_limits G]
 variables {X : Top.{v}} (F : presheaf C X)
 variables {ι : Type v} (U : ι → opens X)
 
-local attribute [reducible] sheaf_condition.diagram
-local attribute [reducible] sheaf_condition.left_res sheaf_condition.right_res
+local attribute [reducible] diagram left_res right_res
 
 /--
 When `G` preserves limits, the sheaf condition diagram for `F` composed with `G` is
 naturally isomorphic to the sheaf condition diagram for `F ⋙ G`.
 -/
 def diagram_comp_preserves_limits :
-  sheaf_condition.diagram F U ⋙ G ≅ sheaf_condition.diagram (F ⋙ G) U :=
+  diagram F U ⋙ G ≅ diagram (F ⋙ G) U :=
 begin
   fapply nat_iso.of_components,
   rintro ⟨j⟩,
@@ -71,16 +74,15 @@ begin
  { ext, simp, dsimp, simp, },
 end
 
-local attribute [reducible] sheaf_condition.res
+local attribute [reducible] res
 
 /--
 When `G` preserves limits, the image under `G` of the sheaf condition fork for `F`
 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 (sheaf_condition.fork F U) ≅
-  (cones.postcompose (diagram_comp_preserves_limits G F U).inv).obj
-    (sheaf_condition.fork (F ⋙ G) U) :=
+def map_cone_fork : G.map_cone (fork F U) ≅
+  (cones.postcompose (diagram_comp_preserves_limits G F U).inv).obj (fork (F ⋙ G) U) :=
 cones.ext (iso.refl _) (λ j,
 begin
   dsimp, simp [diagram_comp_preserves_limits], cases j; dsimp,
@@ -98,7 +100,7 @@ end sheaf_condition
 
 universes v u₁ u₂
 
-open sheaf_condition
+open sheaf_condition sheaf_condition_equalizer_products
 
 variables {C : Type u₁} [category.{v} C] {D : Type u₂} [category.{v} D]
 variables (G : C ⥤ D)
@@ -158,7 +160,7 @@ begin
       -- we note that `G.map f` is almost but not quite (see below) a morphism
       -- from the sheaf condition cone for `F ⋙ G` to the
       -- image under `G` of the equalizer cone for the sheaf condition diagram.
-      let c := sheaf_condition.fork (F ⋙ G) U,
+      let c := fork (F ⋙ G) U,
       have hc : is_limit c := S U,
       let d := G.map_cone (equalizer.fork (left_res F U) (right_res F U)),
       have hd : is_limit d := preserves_limit.preserves (limit.is_limit _),
@@ -202,4 +204,6 @@ example (X : Top) (F : presheaf CommRing X) (h : sheaf_condition (F ⋙ (forget
 ```
 -/
 
+end presheaf
+
 end Top

src/topology/sheaves/local_predicate.lean

@@ -159,7 +159,8 @@ into the presheaf of all functions.
 def subtype : subpresheaf_to_Types P ⟶ presheaf_to_Types X T :=
 { app := λ U f, f.1 }
 
-open Top.sheaf_condition
+open Top.presheaf
+open Top.presheaf.sheaf_condition_equalizer_products
 
 /--
 The natural transformation
@@ -285,8 +286,8 @@ begin
       -- the fact that the underlying presheaf is a presheaf of functions satisfying the predicate.
       let s' := (cones.postcompose (diagram_subtype P.to_prelocal_predicate U)).obj s,
       have fac_i := ((to_Types X T U).fac s' walking_parallel_pair.zero) =≫ pi.π _ i,
-      simp only [sheaf_condition.res, limit.lift_π, cones.postcompose_obj_π,
-        sheaf_condition.fork_π_app_walking_parallel_pair_zero, fan.mk_π_app,
+      simp only [sheaf_condition_equalizer_products.res, limit.lift_π, cones.postcompose_obj_π,
+        sheaf_condition_equalizer_products.fork_π_app_walking_parallel_pair_zero, fan.mk_π_app,
         nat_trans.comp_app, category.assoc] at fac_i,
       have fac_i_f := congr_fun fac_i f,
       simp only [diagram_subtype, discrete.nat_trans_app, types_comp_apply,
@@ -406,7 +407,7 @@ The sheaf of continuous functions on `X` with values in a space `T`.
 def sheaf_to_Top (T : Top.{v}) : sheaf (Type v) X :=
 { presheaf := presheaf_to_Top X T,
   sheaf_condition :=
-    sheaf_condition_equiv_of_iso (subpresheaf_continuous_prelocal_iso_presheaf_to_Top T)
+    presheaf.sheaf_condition_equiv_of_iso (subpresheaf_continuous_prelocal_iso_presheaf_to_Top T)
       (subpresheaf_to_Types.sheaf_condition (continuous_local X T)), }
 
 end Top