feat(CategoryTheory/Sites): pretopology induced by a morphism property (

#17736)

Introduces the pretopology induced by a morphism property satisfying sufficient stability properties.

Mathlib.lean

@@ -1905,6 +1905,7 @@ import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
 import Mathlib.CategoryTheory.Sites.LocallyInjective
 import Mathlib.CategoryTheory.Sites.LocallySurjective
 import Mathlib.CategoryTheory.Sites.MayerVietorisSquare
+import Mathlib.CategoryTheory.Sites.MorphismProperty
 import Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
 import Mathlib.CategoryTheory.Sites.OneHypercover
 import Mathlib.CategoryTheory.Sites.Over

Mathlib/CategoryTheory/MorphismProperty/Composition.lean

@@ -49,6 +49,10 @@ instance inverseImage {P : MorphismProperty D} [P.ContainsIdentities] (F : C ⥤
     (P.inverseImage F).ContainsIdentities where
   id_mem X := by simpa only [← F.map_id] using P.id_mem (F.obj X)
 
+instance inf {P Q : MorphismProperty C} [P.ContainsIdentities] [Q.ContainsIdentities] :
+    (P ⊓ Q).ContainsIdentities where
+  id_mem X := ⟨P.id_mem X, Q.id_mem X⟩
+
 end ContainsIdentities
 
 instance Prod.containsIdentities {C₁ C₂ : Type*} [Category C₁] [Category C₂]
@@ -61,6 +65,14 @@ instance Pi.containsIdentities {J : Type w} {C : J → Type u}
     (pi W).ContainsIdentities :=
   ⟨fun _ _ => MorphismProperty.id_mem _ _⟩
 
+lemma of_isIso (P : MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] {X Y : C} (f : X ⟶ Y)
+    [IsIso f] : P f :=
+  Category.id_comp f ▸ RespectsIso.postcomp P f (𝟙 X) (P.id_mem X)
+
+lemma isomorphisms_le_of_containsIdentities (P : MorphismProperty C) [P.ContainsIdentities]
+    [P.RespectsIso] :
+    isomorphisms C ≤ P := fun _ _ f (_ : IsIso f) ↦ P.of_isIso f
+
 /-- A morphism property satisfies `IsStableUnderComposition` if the composition of
 two such morphisms still falls in the class. -/
 class IsStableUnderComposition (P : MorphismProperty C) : Prop where
@@ -78,6 +90,11 @@ instance IsStableUnderComposition.unop {P : MorphismProperty Cᵒᵖ} [P.IsStabl
     P.unop.IsStableUnderComposition where
   comp_mem f g hf hg := P.comp_mem g.op f.op hg hf
 
+instance IsStableUnderComposition.inf {P Q : MorphismProperty C} [P.IsStableUnderComposition]
+    [Q.IsStableUnderComposition] :
+    (P ⊓ Q).IsStableUnderComposition where
+  comp_mem f g hf hg := ⟨P.comp_mem f g hf.left hg.left, Q.comp_mem f g hf.right hg.right⟩
+
 /-- A morphism property is `StableUnderInverse` if the inverse of a morphism satisfying
 the property still falls in the class. -/
 def StableUnderInverse (P : MorphismProperty C) : Prop :=
@@ -167,6 +184,9 @@ instance : (epimorphisms C).IsMultiplicative where
 instance {P : MorphismProperty D} [P.IsMultiplicative] (F : C ⥤ D) :
     (P.inverseImage F).IsMultiplicative where
 
+instance inf {P Q : MorphismProperty C} [P.IsMultiplicative] [Q.IsMultiplicative] :
+    (P ⊓ Q).IsMultiplicative where
+
 end IsMultiplicative
 
 /-- A class of morphisms `W` has the two-out-of-three property if whenever two out

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -163,6 +163,16 @@ theorem StableUnderBaseChange.op {P : MorphismProperty C} (hP : StableUnderBaseC
 theorem StableUnderBaseChange.unop {P : MorphismProperty Cᵒᵖ} (hP : StableUnderBaseChange P) :
     StableUnderCobaseChange P.unop := fun _ _ _ _ _ _ _ _ sq hf => hP sq.op hf
 
+lemma StableUnderBaseChange.inf {P Q : MorphismProperty C} (hP : StableUnderBaseChange P)
+    (hQ : StableUnderBaseChange Q) :
+    StableUnderBaseChange (P ⊓ Q) :=
+  fun _ _ _ _ _ _ _ _ hp hg ↦ ⟨hP hp hg.left, hQ hp hg.right⟩
+
+lemma StableUnderCobaseChange.inf {P Q : MorphismProperty C} (hP : StableUnderCobaseChange P)
+    (hQ : StableUnderCobaseChange Q) :
+    StableUnderCobaseChange (P ⊓ Q) :=
+  fun _ _ _ _ _ _ _ _ hp hg ↦ ⟨hP hp hg.left, hQ hp hg.right⟩
+
 section
 
 variable (W : MorphismProperty C)

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.MorphismProperty.Limits
+import Mathlib.CategoryTheory.Sites.Pretopology
+
+/-!
+# The site induced by a morphism property
+
+Let `C` be a category with pullbacks and `P` be a multiplicative morphism property which is
+stable under base change. Then `P` induces a pretopology, where coverings are given by presieves
+whose elements satisfy `P`.
+
+Standard examples of pretopologies in algebraic geometry, such as the étale site, are obtained from
+this construction by intersecting with the pretopology of surjective families.
+
+-/
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type*} [Category C] [HasPullbacks C]
+
+namespace MorphismProperty
+
+/-- 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`. -/
+def pretopology (P : MorphismProperty C) [P.IsMultiplicative] (hPb : P.StableUnderBaseChange) :
+    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
+    haveI : P.RespectsIso := hPb.respectsIso
+    exact P.of_isIso f
+  pullbacks X Y f S hS Z g hg := by
+    obtain ⟨Z, g, hg⟩ := hg
+    apply hPb.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]
+    (hPb : P.StableUnderBaseChange) : GrothendieckTopology C :=
+  (P.pretopology hPb).toGrothendieck
+
+variable {P Q : MorphismProperty C}
+  [P.IsMultiplicative] (hPb : P.StableUnderBaseChange)
+  [Q.IsMultiplicative] (hQb : Q.StableUnderBaseChange)
+
+lemma pretopology_le (hPQ : P ≤ Q) : P.pretopology hPb ≤ Q.pretopology hQb :=
+  fun _ _ hS _ f hf ↦ hPQ f (hS hf)
+
+variable (P Q) in
+lemma pretopology_inf :
+    (P ⊓ Q).pretopology (hPb.inf hQb) = P.pretopology hPb ⊓ Q.pretopology hQb := 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⟩⟩
+
+end CategoryTheory.MorphismProperty