feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage

Mathlib/CategoryTheory/Sites/Coverage.lean

@@ -5,8 +5,7 @@ Authors: Adam Topaz
 -/
 module
 
-public import Mathlib.CategoryTheory.Sites.Precoverage
-public import Mathlib.CategoryTheory.Sites.Sheaf
+public import Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
 
 /-!
 
@@ -368,29 +367,31 @@ lemma Pretopology.toGrothendieck_toCoverage [HasPullbacks C] (J : Pretopology C)
   · refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
     rwa [Sieve.generate_le_iff]
 
-namespace Precoverage
-
 /-- A precoverage with pullbacks defines a coverage. -/
 @[simps toPrecoverage]
-def toCoverage (J : Precoverage C) [J.HasPullbacks] [J.IsStableUnderBaseChange] :
+def Precoverage.toCoverage (J : Precoverage C) [J.HasPullbacks] [J.IsStableUnderBaseChange] :
     Coverage C where
   __ := J
   pullback X Y f S hS := by
     have : S.HasPullbacks f := J.hasPullbacks_of_mem _ hS
     exact ⟨S.pullbackArrows f, J.pullbackArrows_mem _ hS,
       Presieve.FactorsThruAlong.pullbackArrows f S⟩
 
-/-- A precoverage with pullbacks defines a Grothendieck topology. -/
-def toGrothendieck (J : Precoverage C) [J.HasPullbacks] [J.IsStableUnderBaseChange] :
-    GrothendieckTopology C :=
-  J.toCoverage.toGrothendieck
-
-lemma mem_toGrothendieck_iff {J : Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange]
-    {X : C} {S : Sieve X} :
-    S ∈ toGrothendieck J X ↔ J.toCoverage.Saturate X S :=
-  .rfl
-
-end Precoverage
+lemma Precoverage.toGrothendieck_toCoverage {J : Precoverage C} [J.HasPullbacks]
+    [J.IsStableUnderBaseChange] :
+    J.toCoverage.toGrothendieck = J.toGrothendieck := by
+  refine le_antisymm ?_ ?_
+  · intro _ _ hS
+    induction hS with
+    | of _ _ hS => exact generate_mem_toGrothendieck hS
+    | top => exact J.toGrothendieck.top_mem _
+    | transitive _ _ _ _ _ ih1 ih2 => exact J.toGrothendieck.transitive ih1 _ ih2
+  · intro _ _ hS
+    induction hS with
+    | of _ _ hS => exact .of _ _ hS
+    | top => exact J.toCoverage.toGrothendieck.top_mem _
+    | pullback _ _ _ _ ih => exact J.toCoverage.toGrothendieck.pullback_stable _ ih
+    | transitive _ _ _ _ _ ih1 ih2 => exact J.toCoverage.toGrothendieck.transitive ih1 _ ih2
 
 namespace GrothendieckTopology
 
@@ -420,8 +421,20 @@ end GrothendieckTopology
 defined. -/
 lemma Precoverage.toGrothendieck_le_iff_le_toPrecoverage {K : Precoverage C}
     {J : GrothendieckTopology C} [K.HasPullbacks] [K.IsStableUnderBaseChange] :
-    K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage :=
-  (Coverage.gi C).gc _ _
+    K.toGrothendieck ≤ J ↔ K ≤ J.toPrecoverage := by
+  rw [← toGrothendieck_toCoverage]
+  exact (Coverage.gi C).gc _ _
+
+lemma Coverage.toGrothendieck_toPrecoverage (J : Coverage C) :
+    J.toPrecoverage.toGrothendieck = J.toGrothendieck := by
+  refine le_antisymm ?_ ?_
+  · rw [Precoverage.toGrothendieck_eq_sInf]
+    exact sInf_le (fun _ _ hS => .of _ _ hS)
+  · intro _ _ hS
+    induction hS with
+    | of _ _ hS => exact .of _ _ hS
+    | top => exact J.toPrecoverage.toGrothendieck.top_mem _
+    | transitive _ _ _ _ _ ih ih' => exact J.toPrecoverage.toGrothendieck.transitive ih _ ih'
 
 open Coverage
 
@@ -435,72 +448,20 @@ the associated Grothendieck topology.
 theorem isSheaf_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
     Presieve.IsSheaf K.toGrothendieck P ↔
     (∀ {X : C} (R : Presieve X), R ∈ K X → Presieve.IsSheafFor P R) := by
+  rw [← toGrothendieck_toPrecoverage, Precoverage.isSheaf_toGrothendieck_iff]
   constructor
-  · intro H X R hR
-    rw [Presieve.isSheafFor_iff_generate]
-    apply H _ <| Saturate.of _ _ hR
   · intro H X S hS
-    -- This is the key point of the proof:
-    -- We must generalize the induction in the correct way.
-    suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by
-      simpa using this (f := 𝟙 _)
-    induction hS with
-    | of X S hS =>
-      intro Y f
-      obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
-      apply Presieve.isSheafFor_of_factorsThru (S := T)
-      · intro Z g hg
-        obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
-        exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
-      · apply H; assumption
-      · intro Z g _
-        obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
-        exact ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
-    | top => intros; simpa using Presieve.isSheafFor_top_sieve _
-    | transitive X R S _ _ H1 H2 =>
-      intro Y f
-      simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
-      choose H1 H1' using H1
-      choose H2 H2' using H2
-      refine ⟨?_, fun x hx => ?_⟩
-      · intro x t₁ t₂ h₁ h₂
-        refine (H1 f).ext (fun Z g hg => ?_)
-        refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
-        simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
-        simp only [← types_comp_apply]
-        rw [← P.map_comp, ← op_comp, h₁, h₂]
-        simpa only [Sieve.pullback_apply, Category.assoc] using hgg
-      let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
-        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
-        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
-      have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
-        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
-        rw [hx]
-        rw [reassoc_of% h]
-      choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
-        H2' hg (𝟙 _) (y g) (hy g)
-      let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
-      have hq : q.Compatible := by
-        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
-        apply (H2 h₁ g₁).ext
-        intro ZZ gg hgg
-        simp only [← types_comp_apply]
-        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
-        · dsimp [y]; congr 1; simp only [Category.assoc, h]
-        · simpa [reassoc_of% h] using hgg
-        · simpa using hgg
-      obtain ⟨t, ht⟩ := H1' f q hq
-      refine ⟨t, fun Z g hg => ?_⟩
-      refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
-      rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
-      on_goal 2 => simpa using hgg
-      refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
-      rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
-      on_goal 2 => simpa using hggg
-      refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
-      rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
-      apply hx
-      simp
+    simpa [← Presieve.isSheafFor_iff_generate] using H (f := 𝟙 X) S hS
+  · intro H X Y f S hS
+    obtain ⟨T, hT1, hT2⟩ := K.pullback f S hS
+    apply Presieve.isSheafFor_of_factorsThru (S := T)
+    · intro Z g hg
+      obtain ⟨W, i, e, h1, h2⟩ := hT2 hg
+      exact ⟨Z, 𝟙 _, g, ⟨W, i, e, h1, h2⟩, by simp⟩
+    · apply H; assumption
+    · intro Z g _
+      obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
+      exact ⟨R, (H _ hR1).isSeparatedFor, hR2⟩
 
 /--
 A presheaf is a sheaf for the Grothendieck topology generated by a union of coverages iff it is a

Mathlib/CategoryTheory/Sites/Over.lean

@@ -341,7 +341,8 @@ lemma over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
   refine le_antisymm ?_ ?_
   · intro ⟨Y, right, (s : Y ⟶ X)⟩ R hR
     obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R
-    simp only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply] at hR
+    simp only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply,
+      ← Precoverage.toGrothendieck_toCoverage] at hR
     induction hR with
     | of Z S hS =>
       rw [Sieve.overEquiv_symm_generate]
@@ -359,7 +360,7 @@ lemma over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
     rw [Precoverage.mem_comap_iff] at hR
     rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff,
       Sieve.overEquiv, Equiv.coe_fn_mk, ← Sieve.generate_map_eq_functorPushforward]
-    exact Coverage.Saturate.of _ _ hR
+    exact Precoverage.Saturate.of _ _ hR
 
 end
 

Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2025 Benoît Guillemet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benoît Guillemet
+-/
+module
+
+public import Mathlib.CategoryTheory.Sites.Precoverage
+public import Mathlib.CategoryTheory.Sites.Sheaf
+
+/-!
+
+# Grothendieck topology generated by a precoverage
+
+For any category `C`, we define the Grothendieck topology generated by a precoverage `J` on `C`.
+It is the smallest Grothendieck topology containing all the sieves generated by the covering
+presieves of `J`.
+
+The main definitions and theorems are:
+- `Precoverage.toGrothendieck C`: A function which associates a Grothendieck topology to any
+  precoverage.
+- `Presieve.isSheaf_toGrothendieck_iff`: Given `J : Precoverage C` with associated Grothendieck
+  topology `K`, a `Type*`-valued presheaf on `C` is a sheaf for `K` if and only if it is a sheaf
+  for all pullbacks of the presieves in `J`.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+variable {C : Type _} [Category C]
+
+namespace Precoverage
+
+variable {J : Precoverage C}
+
+/--
+An auxiliary definition used to define the Grothendieck topology associated to a precoverage.
+See `Precoverage.toGrothendieck`.
+-/
+inductive Saturate (J : Precoverage C) : (X : C) → Sieve X → Prop where
+  | of (X : C) (S : Presieve X) (hS : S ∈ J X) : J.Saturate X (Sieve.generate S)
+  | top (X : C) : J.Saturate X ⊤
+  | pullback (X : C) (S : Sieve X) : J.Saturate X S → ∀ {Y : C} (f : Y ⟶ X),
+      J.Saturate Y (S.pullback f)
+  | transitive (X : C) (S R : Sieve X) : J.Saturate X S →
+      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → J.Saturate Y (R.pullback f)) → J.Saturate X R
+
+/--
+The Grothendieck topology associated to a precoverage `J`.
+It is defined *inductively* as follows:
+1. If `S` is a covering presieve for `J`, then the sieve generated by `S` is a covering
+  sieve for the associated Grothendieck topology.
+2. The top sieves are in the associated Grothendieck topology.
+3. Add all sieves required by the pullback stability condition of a Grothendieck topology.
+4. Add all sieves required by the *local character* axiom of a Grothendieck topology.
+-/
+def toGrothendieck (J : Precoverage C) : GrothendieckTopology C where
+  sieves := J.Saturate
+  top_mem' := .top
+  pullback_stable' _ _ _ _ hS := .pullback _ _ hS _
+  transitive' _ _ hS _ hR := .transitive _ _ _ hS hR
+
+lemma mem_toGrothendieck_iff {X : C} {S : Sieve X} :
+    S ∈ J.toGrothendieck X ↔ J.Saturate X S := .rfl
+
+lemma generate_mem_toGrothendieck {X : C} {R : Presieve X} (hR : R ∈ J X) :
+    Sieve.generate R ∈ J.toGrothendieck X :=
+  .of _ _ hR
+
+/--
+An alternative characterization of the Grothendieck topology associated to a precoverage `J`:
+it is the infimum of all Grothendieck topologies containing `Sieve.generate S` for all presieve
+`S` in `J`.
+-/
+lemma toGrothendieck_eq_sInf (J : Precoverage C) :
+    J.toGrothendieck =
+      sInf { K | ∀ ⦃X : C⦄ (S : Presieve X), S ∈ J X → Sieve.generate S ∈ K X } := by
+  refine le_antisymm ?_ ?_
+  · rw [le_sInf_iff]
+    intro K hK _ _ hS
+    induction hS with
+    | of _ _ hS => exact hK _ hS
+    | top => exact K.top_mem _
+    | pullback _ _ _ _ ih => exact K.pullback_stable _ ih
+    | transitive _ _ _ _ _ ih1 ih2 => exact K.transitive ih1 _ ih2
+  · exact sInf_le (fun _ _ hS => .of _ _ hS)
+
+/--
+The main theorem of this file: given a precoverage `J` on `C`, a `Type*`-valued presheaf on `C` is
+a sheaf for the associated Grothendieck topology if and only if it is a sheaf for all pullback
+sieves of presieves in `J`.
+-/
+theorem isSheaf_toGrothendieck_iff (P : Cᵒᵖ ⥤ Type*) :
+    Presieve.IsSheaf J.toGrothendieck P ↔
+    (∀ {X Y : C} {f : Y ⟶ X} (R : Presieve X), R ∈ J X →
+      Presieve.IsSheafFor P ((Sieve.generate R).pullback f).arrows) := by
+  constructor
+  · refine fun H _ _ _ _ hR => H.isSheafFor _ _ ?_
+    rw [Sieve.generate_sieve]
+    exact J.toGrothendieck.pullback_stable _ (Saturate.of _ _ hR)
+  · intro H X S hS
+    -- This is the key point of the proof:
+    -- We must generalize the induction in the correct way.
+    suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by
+      simpa using this (f := 𝟙 _)
+    induction hS with
+    | of X S hS =>
+      exact fun _ _ => H S hS
+    | top =>
+      simp [Presieve.isSheafFor_top_sieve P]
+    | pullback X S hS f ih =>
+      intro Y f
+      rw [← S.pullback_comp]
+      exact ih (f ≫ _)
+    | transitive X R S hS h H1 H2 =>
+      intro Y f
+      simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
+      choose H1 H1' using H1
+      choose H2 H2' using H2
+      refine ⟨?_, fun x hx => ?_⟩
+      · intro x t₁ t₂ h₁ h₂
+        refine (H1 f).ext (fun Z g hg => ?_)
+        refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
+        simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
+        simp only [← types_comp_apply]
+        rw [← P.map_comp, ← op_comp, h₁, h₂]
+        simpa only [Sieve.pullback_apply, Category.assoc] using hgg
+      let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
+        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
+        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
+      have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
+        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
+        rw [hx]
+        rw [reassoc_of% h]
+      choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
+        H2' hg (𝟙 _) (y g) (hy g)
+      let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
+      have hq : q.Compatible := by
+        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
+        apply (H2 h₁ g₁).ext
+        intro ZZ gg hgg
+        simp only [← types_comp_apply]
+        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
+        · dsimp [y]; congr 1; simp only [Category.assoc, h]
+        · simpa [reassoc_of% h] using hgg
+        · simpa using hgg
+      obtain ⟨t, ht⟩ := H1' f q hq
+      refine ⟨t, fun Z g hg => ?_⟩
+      refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
+      rw [← types_comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
+      on_goal 2 => simpa using hgg
+      refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
+      rw [← types_comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
+      on_goal 2 => simpa using hggg
+      refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
+      rw [← types_comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
+      apply hx
+      simp
+
+end Precoverage
+
+end CategoryTheory