refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (#17361)

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

Author: alreadydone

src/algebraic_geometry/open_immersion.lean

@@ -77,8 +77,7 @@ class PresheafedSpace.is_open_immersion {X Y : PresheafedSpace.{v} C} (f : X ⟶
 A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism
 of PresheafedSpaces
 -/
-abbreviation SheafedSpace.is_open_immersion
-  [has_products.{v} C] {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) : Prop :=
+abbreviation SheafedSpace.is_open_immersion {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) : Prop :=
 PresheafedSpace.is_open_immersion f
 
 /--
@@ -539,7 +538,7 @@ open category_theory.limits.walking_cospan
 
 section to_SheafedSpace
 
-variables [has_products.{v} C] {X : PresheafedSpace.{v} C} (Y : SheafedSpace C)
+variables {X : PresheafedSpace.{v} C} (Y : SheafedSpace C)
 variables (f : X ⟶ Y.to_PresheafedSpace) [H : is_open_immersion f]
 
 include H
@@ -630,8 +629,6 @@ end PresheafedSpace.is_open_immersion
 
 namespace SheafedSpace.is_open_immersion
 
-variables [has_products.{v} C]
-
 @[priority 100]
 instance of_is_iso {X Y : SheafedSpace.{v} C} (f : X ⟶ Y) [is_iso f] :
   SheafedSpace.is_open_immersion f :=

src/algebraic_geometry/sheafed_space.lean

@@ -25,7 +25,7 @@ open opposite
 open category_theory.limits
 open category_theory.category category_theory.functor
 
-variables (C : Type u) [category.{v} C] [has_products.{v} C]
+variables (C : Type u) [category.{v} C]
 
 local attribute [tidy] tactic.op_induction'
 
@@ -119,10 +119,7 @@ The restriction of a sheafed space along an open embedding into the space.
 -/
 def restrict {U : Top} (X : SheafedSpace C)
   {f : U ⟶ (X : Top.{v})} (h : open_embedding f) : SheafedSpace C :=
-{ is_sheaf := (is_sheaf_iff_is_sheaf_equalizer_products _).mpr $ λ ι 𝒰, ⟨is_limit.of_iso_limit
-    ((is_limit.postcompose_inv_equiv _ _).inv_fun
-    ((is_sheaf_iff_is_sheaf_equalizer_products _).mp X.is_sheaf _).some)
-    (sheaf_condition_equalizer_products.fork.iso_of_open_embedding h 𝒰).symm⟩,
+{ is_sheaf := is_sheaf_of_open_embedding h X.is_sheaf,
   ..X.to_PresheafedSpace.restrict h }
 
 /--

src/category_theory/sites/cover_preserving.lean

@@ -162,6 +162,18 @@ begin
   exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)
 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 :=
+begin
+  constructor,
+  introv hx he,
+  obtain ⟨X', e⟩ := hF f₁,
+  apply (ℱ.1.map_iso e.op).to_equiv.injective,
+  simp only [iso.op_hom, iso.to_equiv_fun, ℱ.1.map_iso_hom, ← functor_to_types.map_comp_apply],
+  simpa using hx (F.preimage $ e.hom ≫ f₁) (F.preimage $ e.hom ≫ f₂) hg₁ hg₂
+    (F.map_injective $ by simpa using he),
+end
+
 /--
 If `G` is cover-preserving and compatible-preserving,
 then `G.op ⋙ _` pulls sheaves back to sheaves.

src/topology/sheaves/sheaf_condition/equalizer_products.lean

@@ -146,110 +146,6 @@ begin
     simp [res, diagram.iso_of_iso], }
 end
 
-section open_embedding
-
-variables {V : Top.{v'}} {j : V ⟶ X} (oe : open_embedding j)
-variables (𝒰 : ι → opens V)
-
-/--
-Push forward a cover along an open embedding.
--/
-@[simp]
-def cover.of_open_embedding : ι → opens X := (λ i, oe.is_open_map.functor.obj (𝒰 i))
-
-/--
-The isomorphism between `pi_opens` corresponding to an open embedding.
--/
-@[simp]
-def pi_opens.iso_of_open_embedding :
-  pi_opens (oe.is_open_map.functor.op ⋙ F) 𝒰 ≅ pi_opens F (cover.of_open_embedding oe 𝒰) :=
-pi.map_iso (λ X, F.map_iso (iso.refl _))
-
-/--
-The isomorphism between `pi_inters` corresponding to an open embedding.
--/
-@[simp]
-def pi_inters.iso_of_open_embedding :
-  pi_inters (oe.is_open_map.functor.op ⋙ F) 𝒰 ≅ pi_inters F (cover.of_open_embedding oe 𝒰) :=
-pi.map_iso (λ X, F.map_iso
-  begin
-    dsimp [is_open_map.functor],
-    exact iso.op
-    { hom := hom_of_le (by
-      { simp only [oe.to_embedding.inj, set.image_inter],
-        exact le_rfl, }),
-      inv := hom_of_le (by
-      { simp only [oe.to_embedding.inj, set.image_inter],
-        exact le_rfl, }), },
-  end)
-
-/-- The isomorphism of sheaf condition diagrams corresponding to an open embedding. -/
-def diagram.iso_of_open_embedding :
-  diagram (oe.is_open_map.functor.op ⋙ F) 𝒰 ≅ diagram F (cover.of_open_embedding oe 𝒰) :=
-nat_iso.of_components
-  begin
-    rintro ⟨⟩,
-    exact pi_opens.iso_of_open_embedding oe 𝒰,
-    exact pi_inters.iso_of_open_embedding oe 𝒰
-  end
-  begin
-    rintro ⟨⟩ ⟨⟩ ⟨⟩,
-    { simp, },
-    { ext,
-      dsimp [left_res, is_open_map.functor],
-      simp only [limit.lift_π, cones.postcompose_obj_π, iso.op_hom, discrete.nat_iso_hom_app,
-        functor.map_iso_refl, functor.map_iso_hom, lim_map_π_assoc, limit.lift_map, fan.mk_π_app,
-        nat_trans.comp_app, category.assoc],
-      dsimp,
-      rw [category.id_comp, ←F.map_comp],
-      refl, },
-    { ext,
-      dsimp [right_res, is_open_map.functor],
-      simp only [limit.lift_π, cones.postcompose_obj_π, iso.op_hom, discrete.nat_iso_hom_app,
-        functor.map_iso_refl, functor.map_iso_hom, lim_map_π_assoc, limit.lift_map, fan.mk_π_app,
-        nat_trans.comp_app, category.assoc],
-      dsimp,
-      rw [category.id_comp, ←F.map_comp],
-      refl, },
-    { simp, },
-  end.
-
-/--
-If `F : presheaf C X` is a presheaf, and `oe : U ⟶ X` is an open embedding,
-then the sheaf condition fork for a cover `𝒰` in `U` for the composition of `oe` and `F` is
-isomorphic to sheaf condition fork for `oe '' 𝒰`, precomposed with the isomorphism
-of indexing diagrams `diagram.iso_of_open_embedding`.
-
-We use this to show that the restriction of sheaf along an open embedding is still a sheaf.
--/
-def fork.iso_of_open_embedding :
-  fork (oe.is_open_map.functor.op ⋙ F) 𝒰 ≅
-    (cones.postcompose (diagram.iso_of_open_embedding oe 𝒰).inv).obj
-      (fork F (cover.of_open_embedding oe 𝒰)) :=
-begin
-  fapply fork.ext,
-  { dsimp [is_open_map.functor],
-    exact
-    F.map_iso (iso.op
-    { hom := hom_of_le
-      (by simp only [coe_supr, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset, set.image_Union]),
-      inv := hom_of_le
-      (by simp only [coe_supr, supr_mk, le_def, subtype.coe_mk, set.le_eq_subset,
-                     set.image_Union]) }), },
-  { ext ⟨j⟩,
-    dunfold fork.ι, -- Ugh, it is unpleasant that we need this.
-    simp only [res, diagram.iso_of_open_embedding, discrete.nat_iso_inv_app, functor.map_iso_inv,
-      limit.lift_π, cones.postcompose_obj_π, functor.comp_map,
-      fork_π_app_walking_parallel_pair_zero, pi_opens.iso_of_open_embedding,
-      nat_iso.of_components_inv_app, functor.map_iso_refl, functor.op_map, limit.lift_map,
-      fan.mk_π_app, nat_trans.comp_app, quiver.hom.unop_op, category.assoc, lim_map_eq_lim_map],
-    dsimp,
-    rw [category.comp_id, ←F.map_comp],
-    refl, },
-end
-
-end open_embedding
-
 end sheaf_condition_equalizer_products
 
 /--

src/topology/sheaves/sheaf_condition/opens_le_cover.lean

@@ -261,9 +261,8 @@ variables {Y : opens X} (hY : Y = supr U)
     associated to the sieve generated by the presieve associated to `U` with indexing
     category changed using the above equivalence. -/
 @[simps] def whisker_iso_map_generate_cocone :
-  cone.whisker (generate_equivalence_opens_le U hY).op.functor
-    (F.map_cone (opens_le_cover_cocone U).op) ≅
-  F.map_cone (sieve.generate (presieve_of_covering_aux U Y)).arrows.cocone.op :=
+  (F.map_cone (opens_le_cover_cocone U).op).whisker (generate_equivalence_opens_le U hY).op.functor
+    ≅ F.map_cone (sieve.generate (presieve_of_covering_aux U Y)).arrows.cocone.op :=
 { hom :=
   { hom := F.map (eq_to_hom (congr_arg op hY.symm)),
     w' := λ j, by { erw ← F.map_comp, congr } },

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -75,8 +75,8 @@ def is_sheaf_preserves_limit_pairwise_intersections (F : presheaf C X) : Prop :=
 end
 
 /-!
-The remainder of this file shows that these conditions are equivalent
-to the usual sheaf condition.
+The next part of this file shows that these conditions are equivalent
+to the "equalizer products" sheaf condition.
 -/
 
 variables {X : Top.{v}} [has_products.{v} C]
@@ -89,8 +89,8 @@ open sheaf_condition_equalizer_products
 /-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/
 @[simps]
 def cone_equiv_functor_obj (F : presheaf C X)
-  ⦃ι : Type v⦄ (U : ι → opens ↥X) (c : limits.cone ((diagram U).op ⋙ F)) :
-  limits.cone (sheaf_condition_equalizer_products.diagram F U) :=
+  ⦃ι : Type v⦄ (U : ι → opens ↥X) (c : cone ((diagram U).op ⋙ F)) :
+  cone (sheaf_condition_equalizer_products.diagram F U) :=
 { X := c.X,
   π :=
   { app := λ Z,

src/topology/sheaves/sheaf_condition/sites.lean

@@ -482,6 +482,39 @@ lemma cover_dense_induced_functor {B : ι → opens X} (h : opens.is_basis (set.
 
 end Top.opens
 
+section open_embedding
+
+open category_theory topological_space Top.presheaf opposite
+
+variables {C : Type u} [category.{v} C]
+variables {X Y : Top.{w}} {f : X ⟶ Y} {F : Y.presheaf C}
+
+lemma open_embedding.compatible_preserving (hf : open_embedding f) :
+  compatible_preserving (opens.grothendieck_topology Y) hf.is_open_map.functor :=
+begin
+  haveI : mono f := (Top.mono_iff_injective f).mpr hf.inj,
+  apply compatible_preserving_of_downwards_closed,
+  intros U V i,
+  refine ⟨(opens.map f).obj V, eq_to_iso $ opens.ext $ set.image_preimage_eq_of_subset $ λ x h, _⟩,
+  obtain ⟨_, _, rfl⟩ := i.le h,
+  exact ⟨_, rfl⟩
+end
+
+lemma is_open_map.cover_preserving (hf : is_open_map f) :
+  cover_preserving (opens.grothendieck_topology X) (opens.grothendieck_topology Y) hf.functor :=
+begin
+  constructor,
+  rintros U S hU _ ⟨x, hx, rfl⟩,
+  obtain ⟨V, i, hV, hxV⟩ := hU x hx,
+  exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, set.mem_image_of_mem f hxV⟩
+end
+
+lemma Top.presheaf.is_sheaf_of_open_embedding (h : open_embedding f)
+  (hF : F.is_sheaf) : is_sheaf (h.is_open_map.functor.op ⋙ F) :=
+pullback_is_sheaf_of_cover_preserving h.compatible_preserving h.is_open_map.cover_preserving ⟨_, hF⟩
+
+end open_embedding
+
 namespace Top.sheaf
 
 open category_theory topological_space Top opposite