feat(CategoryTheory/Sites): add coversTop.over (#38657)

Extract a lemma from `Quasicoherent.bind`, which is a statement purely about Grothendieck topologies. I put it into it's own file in order to not increase imports on either `Sites/Over.lean` or `Sites/CoversTop.lean`. Both files have been moved into a new directory `Sites/CoversTop/`.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: justus-springer

Mathlib.lean

@@ -3276,7 +3276,8 @@ public import Mathlib.CategoryTheory.Sites.CoproductSheafCondition
 public import Mathlib.CategoryTheory.Sites.CoverLifting
 public import Mathlib.CategoryTheory.Sites.CoverPreserving
 public import Mathlib.CategoryTheory.Sites.Coverage
-public import Mathlib.CategoryTheory.Sites.CoversTop
+public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
+public import Mathlib.CategoryTheory.Sites.CoversTop.Over
 public import Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
 public import Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
 public import Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
-public import Mathlib.CategoryTheory.Sites.CoversTop
+public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
 
 /-!
 # Generating sections of sheaves of modules

Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

@@ -5,9 +5,9 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
-public import Mathlib.CategoryTheory.Comma.Over.Pullback
+public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
+public import Mathlib.CategoryTheory.Sites.CoversTop.Over
 
 /-!
 # Quasicoherent sheaves
@@ -361,11 +361,9 @@ noncomputable def QuasicoherentData.bind {R : Sheaf J RingCat.{u}}
     (M : SheafOfModules.{u} R) {I : Type u}
     (X : I → C) (hX : J.CoversTop X) (D : Π i, QuasicoherentData (M.over (X i))) :
     M.QuasicoherentData where
-  I := Σ i, (D i).I
+  I := (i : I) × (D i).I
   X ij := ((D ij.1).X ij.2).left
-  coversTop Y := J.transitive (hX Y) _ fun Z f ⟨i, ⟨g⟩⟩ ↦
-      J.superset_covering ((Sieve.functorPushforward_ofObjects_le _ _ _).trans
-      (Sieve.ofObjects_mono fun i' ↦ by aesop)) ((D i).coversTop (.mk g))
+  coversTop := hX.over (fun i ↦ (D i).coversTop)
   presentation i :=
     letI e := pushforwardPushforwardEquivalence (Over.iteratedSliceEquiv ((D i.1).X i.2))
       (S := (R.over _).over _) (R := R.over _) (𝟙 _) (𝟙 _)

…hlib/CategoryTheory/Sites/CoversTop.lean …ategoryTheory/Sites/CoversTop/Basic.leanMathlib/CategoryTheory/Sites/CoversTop.lean renamed to Mathlib/CategoryTheory/Sites/CoversTop/Basic.lean Mathlib/CategoryTheory/Sites/CoversTop.lean renamed to Mathlib/CategoryTheory/Sites/CoversTop/Basic.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+-/
+module
+
+public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
+public import Mathlib.CategoryTheory.Sites.Over
+
+/-!
+# CoversTop in over-categories
+
+This file contains a transitivity lemma for `GrothendieckTopology.CoversTop`: if a family
+`X : I → C` covers the top for `J`, and for each `i` a family `Y i` covers the top for the
+induced topology on `Over (X i)`, then the combined family covers the top for `J`.
+
+-/
+
+@[expose] public section
+
+universe u
+
+namespace CategoryTheory.GrothendieckTopology
+
+variable {C : Type*} [Category* C] {J : GrothendieckTopology C}
+
+lemma CoversTop.over {I : Type*} {X : I → C} (hX : J.CoversTop X) {I' : I → Type u}
+    {Y : (i : I) → I' i → Over (X i)} (hY : ∀ i, (J.over (X i)).CoversTop (Y i)) :
+    J.CoversTop (fun (j : (i : I) × I' i) ↦ (Y j.1 j.2).left) :=
+  fun j ↦ J.transitive (hX j) _ fun Z f ⟨i, ⟨g⟩⟩ ↦ J.superset_covering
+    ((Sieve.functorPushforward_ofObjects_le _ _ _).trans (Sieve.ofObjects_mono fun i' ↦ by aesop))
+    (hY _ (.mk g))
+
+end CategoryTheory.GrothendieckTopology

Mathlib/CategoryTheory/Sites/CoversTop/Over.lean

@@ -6,7 +6,7 @@ Authors: Christian Merten
 module
 
 public import Mathlib.CategoryTheory.Sites.Over
-public import Mathlib.CategoryTheory.Sites.CoversTop
+public import Mathlib.CategoryTheory.Sites.CoversTop.Basic
 
 /-!
 # Local properties of sheaves