feat(CategoryTheory/MorphismProperty): API for sites on P.Over ⊤ X (leanprover-community#36126)

From Proetale

Author: chrisflav

Mathlib.lean

@@ -2989,6 +2989,7 @@ public import Mathlib.CategoryTheory.Monoidal.Types.Basic
 public import Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
 public import Mathlib.CategoryTheory.MorphismProperty.Basic
 public import Mathlib.CategoryTheory.MorphismProperty.Comma
+public import Mathlib.CategoryTheory.MorphismProperty.CommaSites
 public import Mathlib.CategoryTheory.MorphismProperty.Composition
 public import Mathlib.CategoryTheory.MorphismProperty.Concrete
 public import Mathlib.CategoryTheory.MorphismProperty.Descent

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

@@ -435,6 +435,26 @@ lemma Over.w {A B : P.Over Q X} (f : A ⟶ B) :
     f.left ≫ B.hom = A.hom := by
   simp
 
+section
+
+variable {P' Q' : MorphismProperty T} [Q'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q')
+
+variable (X) in
+/-- The natural inclusion induced by implications of morphism properties. -/
+abbrev Over.changeProp (hPP' : P ≤ P') (hQQ' : Q ≤ Q') :
+    P.Over Q X ⥤ P'.Over Q' X :=
+  Comma.changeProp _ _ hPP' hQQ' le_rfl
+
+@[simp]
+lemma Over.changeProp_obj_left (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X) :
+    ((changeProp X hPP' hQQ').obj Y).left = Y.left := rfl
+
+@[simp]
+lemma Over.changeProp_obj_hom (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X) :
+    ((changeProp X hPP' hQQ').obj Y).hom = Y.hom := rfl
+
+end
+
 end Over
 
 section Under

Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.MorphismProperty.Comma
+public import Mathlib.CategoryTheory.Sites.MorphismProperty
+public import Mathlib.CategoryTheory.Sites.Over
+
+/-!
+
+# Sites on `P.Over ⊤ X`
+
+We provide some API for proving properties of `P.Over ⊤ X` in relation to precoverages. Consider
+a precoverage `K` on `C`.
+
+## Main results
+
+- `CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le`:
+  The forgetful functor `P.Over ⊤ X ⥤ Over X` is locally cover dense if morphisms in `K`
+  satisfy `P`.
+- `CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology`: The topology
+  generated by the precoverage induced from `K` via the composition `P.Over ⊤ X ⥤ Over X ⥤ C` is
+  the induced topology from the forgetful functor `P.Over ⊤ X ⥤ Over X`.
+
+-/
+
+@[expose] public section
+
+universe v u
+
+open CategoryTheory MorphismProperty Limits
+
+namespace CategoryTheory.MorphismProperty
+
+variable {C : Type*} [Category* C]
+
+variable {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma exists_map_eq_of_presieve (K : Precoverage C) (H : K ≤ P.precoverage)
+    {X : P.Over ⊤ S} {R : Presieve ((MorphismProperty.Over.forget P ⊤ S).obj X)}
+    (hR : R ∈ (K.comap <| CategoryTheory.Over.forget S) _) :
+    ∃ T : Presieve X, T.map (MorphismProperty.Over.forget P ⊤ S) = R := by
+  rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
+  obtain ⟨𝒰, rfl⟩ := hR
+  let 𝒱 : PreZeroHypercover X :=
+    ⟨𝒰.I₀, fun i ↦ Over.mk _ (𝒰.X i).hom ?_, fun i ↦ Over.homMk (𝒰.f i).left (by simp) trivial⟩
+  · use 𝒱.presieve₀
+    rw [Presieve.map_ofArrows]
+    rfl
+  · rw [← CategoryTheory.Over.w (𝒰.f i)]
+    exact P.comp_mem _ _ (H _ 𝒰.mem₀ ⟨⟨i⟩⟩) X.prop
+
+variable (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition]
+  [K.HasPullbacks]
+
+lemma locallyCoverDense_forget_of_le (H : K ≤ P.precoverage) :
+    (MorphismProperty.Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S) := by
+  rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
+  apply Precoverage.locallyCoverDense_of_map_functorPullback_mem
+  intro X R hR
+  obtain ⟨R, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve _ H hR
+  simpa
+
+lemma toGrothendieck_comap_forget_eq_inducedTopology
+    (H : K ≤ P.precoverage) :
+    haveI := MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
+    (K.comap (MorphismProperty.Over.forget P ⊤ _ ⋙ CategoryTheory.Over.forget S)).toGrothendieck =
+      (MorphismProperty.Over.forget P ⊤ _).inducedTopology (K.toGrothendieck.over S) := by
+  have : (Over.forget P ⊤ S).LocallyCoverDense
+      (K.comap (CategoryTheory.Over.forget S)).toGrothendieck := by
+    rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]
+    exact MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
+  rw [Precoverage.comap_comp]
+  simp_rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
+  apply Precoverage.toGrothendieck_comap_eq_inducedTopology
+  intro X R hR
+  obtain ⟨T, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve K H hR
+  simpa
+
+end CategoryTheory.MorphismProperty

Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean

@@ -146,4 +146,56 @@ noncomputable def sheafInducedTopologyEquivOfIsCoverDense
 
 end Functor
 
+namespace Precoverage
+
+variable {C D : Type*} [Category* C] [Category* D] (F : C ⥤ D) (K : Precoverage D)
+
+lemma toGrothendieck_comap_le_inducedTopology [F.IsLocallyFull K.toGrothendieck]
+    [F.IsLocallyFaithful K.toGrothendieck] [F.LocallyCoverDense K.toGrothendieck] :
+    (K.comap F).toGrothendieck ≤ F.inducedTopology K.toGrothendieck := by
+  rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]
+  intro X R hR
+  rw [Precoverage.mem_comap_iff] at hR
+  rw [GrothendieckTopology.mem_toPrecoverage_iff, Functor.mem_inducedTopology_sieves_iff,
+    ← Sieve.generate_map_eq_functorPushforward]
+  exact Precoverage.generate_mem_toGrothendieck hR
+
+variable [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition]
+  [K.HasPullbacks]
+
+lemma locallyCoverDense_of_map_functorPullback_mem
+    (H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K (F.obj S) →
+      Presieve.map F (Presieve.functorPullback F R) ∈ K (F.obj S)) :
+    F.LocallyCoverDense K.toGrothendieck where
+  functorPushforward_functorPullback_mem U := fun ⟨T, hT⟩ ↦ by
+    rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT ⊢
+    obtain ⟨R, hR, hle⟩ := hT
+    refine ⟨_, H hR, ?_⟩
+    refine le_trans ?_
+      (Presieve.functorPushforward_monotone (Presieve.functorPullback_monotone hle))
+    rw [← Sieve.arrows_generate_map_eq_functorPushforward]
+    exact Sieve.le_generate _
+
+lemma toGrothendieck_comap_eq_inducedTopology [F.Faithful] [F.Full]
+    (H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K (F.obj S) →
+      Presieve.map F (Presieve.functorPullback F R) ∈ K (F.obj S)) :
+    haveI : F.LocallyCoverDense K.toGrothendieck :=
+      K.locallyCoverDense_of_map_functorPullback_mem F H
+    (K.comap F).toGrothendieck = F.inducedTopology K.toGrothendieck := by
+  haveI : F.LocallyCoverDense K.toGrothendieck :=
+    K.locallyCoverDense_of_map_functorPullback_mem F H
+  refine le_antisymm ?_ fun X T hT ↦ ?_
+  · apply toGrothendieck_comap_le_inducedTopology
+  · rw [Functor.mem_inducedTopology_sieves_iff] at hT
+    rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT
+    obtain ⟨R, hR, hle⟩ := hT
+    refine GrothendieckTopology.superset_covering
+        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_
+    · refine le_trans (le_trans (Sieve.generate_functorPullback_le F R)
+        (Sieve.functorPullback_monotone _ _ (Sieve.generate_mono hle))) ?_
+      rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]
+    · exact Precoverage.generate_mem_toGrothendieck (H hR)
+
+end Precoverage
+
 end CategoryTheory