feat(CategoryTheory/Sites/MorphismProperty): add induced coverage (leanprover-community#28778)

We add the (pre)coverage induced by a morphism property and show the induced topology is the same as the one induced by `MorphismProperty.pretopology`.

This will be used in the upcoming refactor of `Scheme.Cover`, which will be built upon `Precoverage.ZeroHypercover`.

Author: chrisflav

Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

@@ -102,7 +102,7 @@ lemma jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology
 lemma pretopology_le_inf [IsJointlySurjectivePreserving ⊤] :
     pretopology P ≤ jointlySurjectivePretopology ⊓ P.pretopology := by
   rintro X S ⟨𝒰, rfl⟩
-  refine ⟨fun x ↦ ?_, fun ⟨i⟩ ↦ 𝒰.map_prop i⟩
+  refine ⟨fun x ↦ ?_, fun _ _ ⟨i⟩ ↦ 𝒰.map_prop i⟩
   obtain ⟨a, ha⟩ := 𝒰.covers x
   refine ⟨𝒰.obj (𝒰.f x), a, 𝒰.map (𝒰.f x), ⟨_⟩, ha⟩
 

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -843,6 +843,17 @@ lemma universally_mk' (P : MorphismProperty C) [P.RespectsIso] {X Y : C} (g : X
 
 end Universally
 
+variable (P : MorphismProperty C)
+
+/-- `P` has pullbacks if for every `f` satisfying `P`, pullbacks of arbitrary morphisms along `f`
+exist. -/
+protected class HasPullbacks : Prop where
+  hasPullback {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S) : P f → HasPullback f g := by infer_instance
+
+instance [HasPullbacks C] : P.HasPullbacks where
+
+alias hasPullback := HasPullbacks.hasPullback
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Coverage.lean

@@ -248,6 +248,9 @@ def toGrothendieck (K : Coverage C) : GrothendieckTopology C where
       exact hS hg
   transitive' _ _ hS _ hR := .transitive _ _ _ hS hR
 
+lemma mem_toGrothendieck {K : Coverage C} {X : C} {S : Sieve X} :
+    S ∈ K.toGrothendieck C X ↔ Saturate K X S := .rfl
+
 instance : PartialOrder (Coverage C) where
   le A B := A.coverings ≤ B.coverings
   le_refl _ _ := le_refl _
@@ -329,6 +332,28 @@ def Pretopology.toCoverage [HasPullbacks C] (J : Pretopology C) : Coverage C whe
   coverings := J
   pullback _ _ f R hR := ⟨R.pullbackArrows f, J.pullbacks _ _ hR, .pullbackArrows f R⟩
 
+@[simp]
+lemma Pretopology.mem_toCoverage [HasPullbacks C] (J : Pretopology C) {X : C} (S : Presieve X) :
+    S ∈ J.toCoverage X ↔ S ∈ J X := .rfl
+
+lemma Pretopology.toGrothendieck_toCoverage [HasPullbacks C] (J : Pretopology C) :
+    J.toCoverage.toGrothendieck = J.toGrothendieck := by
+  ext T S
+  rw [mem_toGrothendieck, Coverage.mem_toGrothendieck]
+  refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
+  · induction h with
+    | of X S hS => use S, hS, Sieve.le_generate S
+    | top X => use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
+    | transitive X R S hR hRS hle hfS =>
+        obtain ⟨R', hR', hle⟩ := hle
+        choose S' hS' hS'le using hfS
+        refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ hf)), ?_, fun Z u hu ↦ ?_⟩
+        · exact J.transitive R' (fun Y f hf ↦ S' (hle Y hf)) hR' fun Y f H ↦ hS' (hle Y H)
+        · obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
+          exact hS'le _ _ hg
+  · refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
+    rwa [Sieve.generate_le_iff]
+
 open Coverage
 
 namespace Presieve

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

@@ -5,6 +5,7 @@ Authors: Christian Merten
 -/
 import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.Sites.Pretopology
+import Mathlib.CategoryTheory.Sites.Coverage
 
 /-!
 # The site induced by a morphism property
@@ -22,44 +23,106 @@ namespace CategoryTheory
 
 open Limits
 
-variable {C : Type*} [Category C] [HasPullbacks C]
+variable {C : Type*} [Category C]
 
 namespace MorphismProperty
 
+variable {P Q : MorphismProperty C}
+
+/-- This is the precoverage on `C` where covering presieves are those where every
+morphism satisfies `P`. -/
+def precoverage (P : MorphismProperty C) : Precoverage C where
+  coverings X S := ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → P f
+
+@[simp]
+lemma ofArrows_mem_precoverage {X : C} {ι : Type*} {Y : ι → C} {f : ∀ i, Y i ⟶ X} :
+    .ofArrows Y f ∈ precoverage P X ↔ ∀ i, P (f i) :=
+  ⟨fun h i ↦ h ⟨i⟩, fun h _ g ⟨i⟩ ↦ h i⟩
+
+instance [P.ContainsIdentities] [P.RespectsIso] : P.precoverage.HasIsos where
+  mem_coverings_of_isIso f _ _ _ := fun ⟨⟩ ↦ P.of_isIso f
+
+instance [P.IsStableUnderBaseChange] : P.precoverage.IsStableUnderBaseChange where
+  mem_coverings_of_isPullback {ι} S X f hf T g W p₁ p₂ h Z g hg := by
+    obtain ⟨i⟩ := hg
+    exact P.of_isPullback (h i).flip (hf ⟨i⟩)
+
+instance [P.IsStableUnderComposition] : P.precoverage.IsStableUnderComposition where
+  comp_mem_coverings {ι} S X f hf σ Y g hg Z p := by
+    intro ⟨i⟩
+    exact P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)
+
+lemma precoverage_monotone (hPQ : P ≤ Q) : precoverage P ≤ precoverage Q :=
+  fun _ _ hR _ _ hg ↦ hPQ _ (hR hg)
+
+variable (P Q) in
+lemma precoverage_inf : precoverage (P ⊓ Q) = precoverage P ⊓ precoverage Q := by
+  ext X R
+  exact ⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
+    fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩
+
+/-- If `P` is stable under base change, this is the coverage on `C` where covering presieves
+are those where every morphism satisfies `P`. -/
+@[simps toPrecoverage]
+def coverage (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.HasPullbacks] :
+    Coverage C where
+  __ := precoverage P
+  pullback X Y f S hS := by
+    have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩
+    refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩
+    intro Z g ⟨W, a, h⟩
+    have := S.hasPullback f h
+    exact P.pullback_snd _ _ (hS h)
+
+/-- If `P` is stable under base change, it induces a Grothendieck topology: the one associated
+to `coverage P`. -/
+abbrev grothendieckTopology (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.HasPullbacks] :
+    GrothendieckTopology C :=
+  P.coverage.toGrothendieck
+
+section HasPullbacks
+
+variable [P.IsStableUnderBaseChange] [HasPullbacks C]
+
 /-- If `P` is a multiplicative morphism property which is stable under base change on a category
 `C` with pullbacks, then `P` induces a pretopology, where coverings are given by presieves whose
 elements satisfy `P`. -/
+@[simps! toPrecoverage]
 def pretopology (P : MorphismProperty C) [P.IsMultiplicative] [P.IsStableUnderBaseChange] :
-    Pretopology C where
-  coverings X S := ∀ {Y : C} {f : Y ⟶ X}, S f → P f
-  has_isos X Y f h Z g hg := by
-    cases hg
-    exact P.of_isIso f
-  pullbacks X Y f S hS Z g hg := by
-    obtain ⟨Z, g, hg⟩ := hg
-    apply P.pullback_snd g f (hS hg)
-  transitive X S Ti hS hTi Y f hf := by
-    obtain ⟨Z, g, h, H, H', rfl⟩ := hf
-    exact comp_mem _ _ _ (hTi h H H') (hS H)
-
-/-- To a morphism property `P` satisfying the conditions of `MorphismProperty.pretopology`, we
-associate the Grothendieck topology generated by `P.pretopology`. -/
-abbrev grothendieckTopology (P : MorphismProperty C) [P.IsMultiplicative]
-    [P.IsStableUnderBaseChange] : GrothendieckTopology C :=
-  P.pretopology.toGrothendieck
+    Pretopology C :=
+  (precoverage P).toPretopology
+
+/-- If `P` is also multiplicative, the coverage induced by `P` is the pretopology induced by `P`. -/
+lemma coverage_eq_toCoverage_pretopology [P.IsMultiplicative] :
+    P.coverage = P.pretopology.toCoverage := rfl
+
+/-- If `P` is also multiplicative, the topology induced by `P` is the topology induced by the
+pretopology induced by `P`. -/
+lemma grothendieckTopology_eq_toGrothendieck_pretopology [P.IsMultiplicative] :
+    P.grothendieckTopology = P.pretopology.toGrothendieck := by
+  rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
+    Pretopology.toGrothendieck_toCoverage]
+
+section
 
 variable {P Q : MorphismProperty C}
   [P.IsMultiplicative] [P.IsStableUnderBaseChange]
   [Q.IsMultiplicative] [Q.IsStableUnderBaseChange]
 
-lemma pretopology_le (hPQ : P ≤ Q) : P.pretopology ≤ Q.pretopology :=
-  fun _ _ hS _ f hf ↦ hPQ f (hS hf)
+lemma pretopology_monotone (hPQ : P ≤ Q) : P.pretopology ≤ Q.pretopology :=
+  precoverage_monotone hPQ
+
+@[deprecated (since := "2025-08-28")]
+alias pretopology_le := pretopology_monotone
 
 variable (P Q) in
-lemma pretopology_inf :
-    (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology := by
-  ext X S
-  exact ⟨fun hS ↦ ⟨fun hf ↦ (hS hf).left, fun hf ↦ (hS hf).right⟩,
-    fun h ↦ fun hf ↦ ⟨h.left hf, h.right hf⟩⟩
+lemma pretopology_inf : (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology := by
+  ext : 1
+  simp only [pretopology_toPrecoverage, precoverage_inf]
+  rfl
+
+end
+
+end HasPullbacks
 
 end CategoryTheory.MorphismProperty