chore(CategoryTheory/Sites): rename Sheaf.isSheafFor_trans to Presieve.isSheafFor_trans and move to earlier file (leanprover-community#34924)

We move the lemmas `Sheaf.isSheafFor_trans` and `Sheaf.isSheafFor_bind` from `Mathlib/CategoryTheory/Sites/Canonical.lean` to `Mathlib/CategoryTheory/Sites/IsSheafFor.lean`, because they are more generally useful.

We also change the names to match their content:
- `Sheaf.isSheafFor_trans` -> `Presieve.isSheafFor_trans`
- `Sheaf.isSheafFor_bind` -> `Presieve.isSheafFor_bind`

Finally, we generalize the universe of the codomain of the presheaf in both lemmas.

Author: chrisflav

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -45,100 +45,13 @@ open CategoryTheory Category Limits Sieve
 
 variable {C : Type u} [Category.{v} C]
 
-namespace Sheaf
-
 variable {P : Cᵒᵖ ⥤ Type v} {X : C} (J : GrothendieckTopology C)
 
-/--
-To show `P` is a sheaf for the binding of `U` with `B`, it suffices to show that `P` is a sheaf for
-`U`, that `P` is a sheaf for each sieve in `B`, and that it is separated for any pullback of any
-sieve in `B`.
+namespace Sheaf
 
-This is mostly an auxiliary lemma to show `isSheafFor_trans`.
-Adapted from [Elephant], Lemma C2.1.7(i) with suggestions as mentioned in
-https://math.stackexchange.com/a/358709/
--/
-theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type v) (U : Sieve X) (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y)
-    (hU : Presieve.IsSheafFor P (U : Presieve X))
-    (hB : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.IsSheafFor P (B hf : Presieve Y))
-    (hB' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (h : U f) ⦃Z⦄ (g : Z ⟶ Y),
-      Presieve.IsSeparatedFor P (((B h).pullback g) : Presieve Z)) :
-    Presieve.IsSheafFor P (Sieve.bind (U : Presieve X) B : Presieve X) := by
-  intro s hs
-  let y : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.FamilyOfElements P (B hf : Presieve Y) :=
-    fun Y f hf Z g hg => s _ (Presieve.bind_comp _ _ hg)
-  have hy : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).Compatible := by
-    intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
-    apply hs
-    apply reassoc_of% comm
-  let t : Presieve.FamilyOfElements P (U : Presieve X) :=
-    fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)
-  have ht : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).IsAmalgamation (t f hf) := fun Y f hf =>
-    (hB hf).isAmalgamation _
-  have hT : t.Compatible := by
-    rw [Presieve.compatible_iff_sieveCompatible]
-    intro Z W f h hf
-    apply (hB (U.downward_closed hf h)).isSeparatedFor.ext
-    intro Y l hl
-    apply (hB' hf (l ≫ h)).ext
-    intro M m hm
-    have : bind U B (m ≫ l ≫ h ≫ f) := by simpa using (Presieve.bind_comp f hf hm : bind U B _)
-    trans s (m ≫ l ≫ h ≫ f) this
-    · have := ht (U.downward_closed hf h) _ ((B _).downward_closed hl m)
-      rw [op_comp, FunctorToTypes.map_comp_apply] at this
-      grind
-    · have h : s _ _ = _ := (ht hf _ hm).symm
-      -- Porting note: this was done by `simp only [assoc] at`
-      conv_lhs at h => congr; rw [assoc, assoc]
-      rw [h]
-      simp only [op_comp, assoc, FunctorToTypes.map_comp_apply]
-  refine ⟨hU.amalgamate t hT, ?_, ?_⟩
-  · rintro Z _ ⟨Y, f, g, hg, hf, rfl⟩
-    rw [op_comp, FunctorToTypes.map_comp_apply, Presieve.IsSheafFor.valid_glue _ _ _ hg]
-    apply ht hg _ hf
-  · intro y hy
-    apply hU.isSeparatedFor.ext
-    intro Y f hf
-    apply (hB hf).isSeparatedFor.ext
-    intro Z g hg
-    rw [← FunctorToTypes.map_comp_apply, ← op_comp, hy _ (Presieve.bind_comp _ _ hg),
-      hU.valid_glue _ _ hf, ht hf _ hg]
-
-/-- Given two sieves `R` and `S`, to show that `P` is a sheaf for `S`, we can show:
-* `P` is a sheaf for `R`
-* `P` is a sheaf for the pullback of `S` along any arrow in `R`
-* `P` is separated for the pullback of `R` along any arrow in `S`.
-
-This is mostly an auxiliary lemma to construct `finestTopology`.
-Adapted from [Elephant], Lemma C2.1.7(ii) with suggestions as mentioned in
-https://math.stackexchange.com/a/358709
--/
-theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X)
-    (hR : Presieve.IsSheafFor P (R : Presieve X))
-    (hR' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : S f), Presieve.IsSeparatedFor P (R.pullback f : Presieve Y))
-    (hS : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : R f), Presieve.IsSheafFor P (S.pullback f : Presieve Y)) :
-    Presieve.IsSheafFor P (S : Presieve X) := by
-  have : (bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
-    rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
-    apply hf
-  apply Presieve.isSheafFor_subsieve_aux P this
-  · apply isSheafFor_bind _ _ _ hR hS
-    intro Y f hf Z g
-    rw [← pullback_comp]
-    apply (hS (R.downward_closed hf _)).isSeparatedFor
-  · intro Y f hf
-    have : Sieve.pullback f (bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) =
-        R.pullback f := by
-      ext Z g
-      constructor
-      · rintro ⟨W, k, l, hl, _, comm⟩
-        rw [pullback_apply, ← comm]
-        simp [hl]
-      · intro a
-        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
-        simp [hf]
-    rw [this]
-    apply hR' hf
+@[deprecated (since := "2026-02-06")] alias isSheafFor_bind := Presieve.isSheafFor_bind
+
+@[deprecated (since := "2026-02-06")] alias isSheafFor_trans := Presieve.isSheafFor_trans
 
 /-- Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf. -/
 @[stacks 00Z9 "This is a special case of the Stacks entry, but following a different
@@ -154,7 +67,7 @@ def finestTopologySingle (P : Cᵒᵖ ⥤ Type v) : GrothendieckTopology C where
   transitive' X S hS R hR Z g := by
     -- This is the hard part of the construction, showing that the given set of sieves satisfies
     -- the transitivity axiom.
-    refine isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
+    refine Presieve.isSheafFor_trans P (pullback g S) _ (hS Z g) ?_ ?_
     · intro Y f _
       rw [← pullback_comp]
       apply (hS _ _).isSeparatedFor

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -938,6 +938,98 @@ lemma isSheafFor_singleton {X Y : C} {f : X ⟶ Y} :
   simp_rw [FamilyOfElements.compatible_singleton_iff,
     FamilyOfElements.isAmalgamation_singleton_iff, FamilyOfElements.singletonEquiv_symm_apply_self]
 
+/--
+To show `P` is a sheaf for the binding of `U` with `B`, it suffices to show that `P` is a sheaf for
+`U`, that `P` is a sheaf for each sieve in `B`, and that it is separated for any pullback of any
+sieve in `B`.
+
+This is mostly an auxiliary lemma to show `Presieve.isSheafFor_trans`.
+Adapted from [Elephant], Lemma C2.1.7(i) with suggestions as mentioned in
+https://math.stackexchange.com/a/358709/
+-/
+theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type*) (U : Sieve X)
+    (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y)
+    (hU : Presieve.IsSheafFor P (U : Presieve X))
+    (hB : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.IsSheafFor P (B hf : Presieve Y))
+    (hB' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (h : U f) ⦃Z⦄ (g : Z ⟶ Y),
+      Presieve.IsSeparatedFor P (((B h).pullback g) : Presieve Z)) :
+    Presieve.IsSheafFor P (Sieve.bind (U : Presieve X) B : Presieve X) := by
+  intro s hs
+  let y : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.FamilyOfElements P (B hf : Presieve Y) :=
+    fun Y f hf Z g hg => s _ (Presieve.bind_comp _ _ hg)
+  have hy : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).Compatible := by
+    intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
+    apply hs
+    apply reassoc_of% comm
+  let t : Presieve.FamilyOfElements P (U : Presieve X) :=
+    fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)
+  have ht : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).IsAmalgamation (t f hf) := fun Y f hf =>
+    (hB hf).isAmalgamation _
+  have hT : t.Compatible := by
+    rw [Presieve.compatible_iff_sieveCompatible]
+    intro Z W f h hf
+    apply (hB (U.downward_closed hf h)).isSeparatedFor.ext
+    intro Y l hl
+    apply (hB' hf (l ≫ h)).ext
+    intro M m hm
+    have : Sieve.bind U B (m ≫ l ≫ h ≫ f) := by simpa using (bind_comp f hf hm : Sieve.bind U B _)
+    trans s (m ≫ l ≫ h ≫ f) this
+    · have := ht (U.downward_closed hf h) _ ((B _).downward_closed hl m)
+      rw [op_comp, FunctorToTypes.map_comp_apply] at this
+      grind
+    · have h : s _ _ = _ := (ht hf _ hm).symm
+      -- Porting note: this was done by `simp only [assoc] at`
+      conv_lhs at h => congr; rw [assoc, assoc]
+      rw [h]
+      simp only [op_comp, assoc, FunctorToTypes.map_comp_apply]
+  refine ⟨hU.amalgamate t hT, ?_, ?_⟩
+  · rintro Z _ ⟨Y, f, g, hg, hf, rfl⟩
+    rw [op_comp, FunctorToTypes.map_comp_apply, Presieve.IsSheafFor.valid_glue _ _ _ hg]
+    apply ht hg _ hf
+  · intro y hy
+    apply hU.isSeparatedFor.ext
+    intro Y f hf
+    apply (hB hf).isSeparatedFor.ext
+    intro Z g hg
+    rw [← FunctorToTypes.map_comp_apply, ← op_comp, hy _ (Presieve.bind_comp _ _ hg),
+      hU.valid_glue _ _ hf, ht hf _ hg]
+
+/-- Given two sieves `R` and `S`, to show that `P` is a sheaf for `S`, we can show:
+* `P` is a sheaf for `R`
+* `P` is a sheaf for the pullback of `S` along any arrow in `R`
+* `P` is separated for the pullback of `R` along any arrow in `S`.
+
+This is mostly an auxiliary lemma to construct `Sheaf.finestTopology`.
+Adapted from [Elephant], Lemma C2.1.7(ii) with suggestions as mentioned in
+https://math.stackexchange.com/a/358709
+-/
+theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type*) (R S : Sieve X)
+    (hR : Presieve.IsSheafFor P (R : Presieve X))
+    (hR' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : S f), Presieve.IsSeparatedFor P (R.pullback f : Presieve Y))
+    (hS : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : R f), Presieve.IsSheafFor P (S.pullback f : Presieve Y)) :
+    Presieve.IsSheafFor P (S : Presieve X) := by
+  have : (Sieve.bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
+    rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
+    apply hf
+  apply Presieve.isSheafFor_subsieve_aux P this
+  · apply isSheafFor_bind _ _ _ hR hS
+    intro Y f hf Z g
+    rw [← pullback_comp]
+    apply (hS (R.downward_closed hf _)).isSeparatedFor
+  · intro Y f hf
+    have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) =
+        R.pullback f := by
+      ext Z g
+      constructor
+      · rintro ⟨W, k, l, hl, _, comm⟩
+        rw [pullback_apply, ← comm]
+        simp [hl]
+      · intro a
+        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
+        simp [hf]
+    rw [this]
+    apply hR' hf
+
 end Presieve
 
 end CategoryTheory