Merge branch 'erd1/sheafOverU' into qcoh-tilde-foo.1

Author: chrisflav

Mathlib.lean

@@ -8013,6 +8013,7 @@ public import Mathlib.Topology.Sheaves.Limits
 public import Mathlib.Topology.Sheaves.LocalPredicate
 public import Mathlib.Topology.Sheaves.LocallySurjective
 public import Mathlib.Topology.Sheaves.MayerVietoris
+public import Mathlib.Topology.Sheaves.Module
 public import Mathlib.Topology.Sheaves.Over
 public import Mathlib.Topology.Sheaves.PUnit
 public import Mathlib.Topology.Sheaves.Points

Mathlib/CategoryTheory/Sites/Spaces.lean

@@ -57,6 +57,10 @@ def grothendieckTopology : GrothendieckTopology (Opens T) where
     rcases hR hf _ hU with ⟨V, g, hg, hV⟩
     exact ⟨_, g ≫ f, hg, hV⟩
 
+lemma mem_grothendieckTopology {U : Opens T} {S : Sieve U} :
+    S ∈ Opens.grothendieckTopology T U ↔ ∀ x ∈ U, ∃ (V : _) (f : V ⟶ U), S f ∧ x ∈ V := .rfl
+
+set_option backward.isDefEq.respectTransparency false in
 /-- The Grothendieck pretopology associated to a topological space. -/
 def pretopology : Pretopology (Opens T) where
   coverings X := {R | ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), R f ∧ x ∈ U}

Mathlib/Topology/Sheaves/Module.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
+public import Mathlib.Algebra.Category.Ring.Limits
+public import Mathlib.Topology.Sheaves.Over
+public import Mathlib.Topology.Sheaves.SheafCondition.Sites
+
+/-! # Specialized results for sheaf of modules over topological spaces -/
+
+@[expose] public section
+
+noncomputable section
+
+open CategoryTheory
+
+universe w v u
+
+namespace TopologicalSpace.Opens
+
+variable {X : TopCat.{u}} (U : Opens X) (R : X.Sheaf RingCat.{v})
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Sheaves of modules over `R.over U` are equivalent to sheaves of modules over `R |_ U`. -/
+def sheafOfModulesEquivOver :
+    SheafOfModules.{w} (R.over U) ≌ SheafOfModules.{w} (U.sheafRestrict.obj R) := by
+  refine SheafOfModules.pushforwardPushforwardEquivalence (eqv := U.overEquivalence.symm)
+    (U.overPullbackSheafEquivOver.app _).inv (U.sheafRestrictSheafEquivOver.app _).inv rfl ?_
+  ext : 2
+  dsimp [sheafRestrictSheafEquivOver, Iso.isoCompInverse, -sheafRestrict_obj_val_map]
+  simp only [Category.id_comp, Category.assoc, ← NatTrans.naturality]
+  dsimp
+  rw [← R.val.map_comp_assoc, eqToHom_map]
+  simp [← NatTrans.comp_app, ← Sheaf.comp_val]
+
+/-- `sheafOfModulesEquivOver` takes `R.over U` to `R |_ U`. -/
+def sheafOfModulesEquivOverUnit (R : X.Sheaf RingCat.{u}) :
+    (U.sheafOfModulesEquivOver R).functor.obj (SheafOfModules.unit.{u} _) ≅
+      SheafOfModules.unit.{u} _ := .refl _
+
+/-- `sheafOfModulesEquivOver.inverse` takes `R |_ U` to `R.over U`. -/
+def sheafOfModulesEquivOverInverseUnit (R : X.Sheaf RingCat.{u}) :
+    (U.sheafOfModulesEquivOver R).inverse.obj (SheafOfModules.unit.{u} _) ≅
+      SheafOfModules.unit.{u} _ :=
+  (U.sheafOfModulesEquivOver R).inverse.mapIso (U.sheafOfModulesEquivOverUnit R).symm ≪≫
+    ((U.sheafOfModulesEquivOver R).unitIso.app _).symm
+
+end TopologicalSpace.Opens

Mathlib/Topology/Sheaves/Over.lean

@@ -5,8 +5,10 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Topology.Sets.Opens
 public import Mathlib.CategoryTheory.Comma.Over.Basic
+public import Mathlib.CategoryTheory.Sites.Over
+public import Mathlib.Topology.Sets.Opens
+public import Mathlib.Topology.Sheaves.SheafCondition.Sites
 
 /-!
 # Opens and Over categories
@@ -15,11 +17,7 @@ In this file, given a topological space `X`, and `U : Opens X`,
 we show that the category `Over U` (whose objects are the
 `V : Opens X` equipped with a morphism `V ⟶ U`) is equivalent
 to the category `Opens U`.
-
-## TODO
-* show that both functors of the equivalence `overEquivalence U` are continuous and
-  induce an equivalence between `Sheaf ((Opens.grothendieckTopology X).over U) A`
-  and `Sheaf (Opens.grothendieckTopology U) A` for any category `A`.
+This equivalence is bi-continuous, and thus induces an equivalence of sheaf categories.
 
 -/
 
@@ -31,7 +29,7 @@ open CategoryTheory Topology
 
 namespace TopologicalSpace
 
-variable {X : Type u} [TopologicalSpace X] (U : Opens X)
+variable {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type*} [Category* A]
 
 namespace Opens
 
@@ -53,6 +51,53 @@ def overEquivalence : Over U ≌ Opens ↥U where
     apply leOfHom V.hom)))
   counitIso := NatIso.ofComponents (fun V ↦ eqToIso (by aesop))
 
+variable {U} in
+@[simp] lemma mem_overEquivalence_functor_obj {V : Over U} {x : U} :
+  x ∈ U.overEquivalence.functor.obj V ↔ x.1 ∈ V.left := .rfl
+
+section grothendieckTopology
+
+instance : U.overEquivalence.functor.IsDenseSubsite
+    ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology U) where
+  functorPushforward_mem_iff {V S} := by
+    simp only [Opens.mem_grothendieckTopology, Sieve.mem_functorPushforward_functor]
+    constructor
+    · intro H x hxV
+      obtain ⟨W, f, hW, hxW⟩ := H ⟨x, V.hom.le hxV⟩ hxV
+      exact ⟨_, ((U.overEquivalence.symm.toAdjunction.homEquiv _ _ ).symm f).left,
+        ⟨_, _, 𝟙 _, hW, rfl⟩, _, hxW, rfl⟩
+    · intro H x hxV
+      obtain ⟨W, f, ⟨W', hW'V, hWW', hSW'V, rfl⟩, hxW⟩ := H x hxV
+      exact ⟨_, U.overEquivalence.functor.map hW'V,
+        S.downward_closed hSW'V (U.overEquivalence.unitInv.app W'), hWW'.le hxW⟩
+
+instance : U.overEquivalence.symm.inverse.IsDenseSubsite
+      ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology U) :=
+  inferInstanceAs (U.overEquivalence.functor.IsDenseSubsite ..)
+
+instance : U.overEquivalence.inverse.IsDenseSubsite
+      (Opens.grothendieckTopology U) ((Opens.grothendieckTopology X).over U) :=
+  inferInstanceAs (U.overEquivalence.symm.functor.IsDenseSubsite ..)
+
+/-- Sheaves on the over category of `U` is equivalent to sheaves on `U` as a topological space. -/
+@[simps!] def sheafEquivOver :
+    Sheaf ((Opens.grothendieckTopology X).over U) A ≌ Sheaf (Opens.grothendieckTopology U) A :=
+  U.overEquivalence.sheafCongr
+    ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology U) A
+
+/-- `overPullback` and `sheafRestrict` are isomorphic under `sheafEquivOver`. -/
+def overPullbackSheafEquivOver {X : TopCat} (U : Opens X) :
+    (Opens.grothendieckTopology X).overPullback A U ⋙ U.sheafEquivOver.functor ≅
+      U.sheafRestrict := .refl _
+
+/-- `overPullback` and `sheafRestrict` are isomorphic under `sheafEquivOver`. -/
+def sheafRestrictSheafEquivOver {X : TopCat} (U : Opens X) :
+    U.sheafRestrict ⋙ U.sheafEquivOver.inverse ≅
+      (Opens.grothendieckTopology X).overPullback A U :=
+  U.overPullbackSheafEquivOver.isoCompInverse.symm
+
+end grothendieckTopology
+
 end Opens
 
 end TopologicalSpace

Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

@@ -174,6 +174,15 @@ theorem TopCat.Presheaf.isSheaf_of_isOpenEmbedding (h : IsOpenEmbedding f) (hF :
   have := h.functor_isContinuous
   exact Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩
 
+/-- The restriction functor of a sheaf to an open subspace. -/
+@[simps!]
+def TopologicalSpace.Opens.sheafRestrict (U : Opens X) :
+    Sheaf (Opens.grothendieckTopology X) C ⥤ Sheaf (Opens.grothendieckTopology U) C :=
+  haveI H : IsOpenEmbedding (TopCat.Hom.hom (X := .of U) (Y := X) ⟨_, continuous_subtype_val⟩) :=
+    U.isOpenEmbedding
+  haveI := H.functor_isContinuous
+  H.isOpenMap.functor.sheafPushforwardContinuous C _ _
+
 variable (f)
 
 instance : RepresentablyFlat (Opens.map f) := by