feat(CategoryTheory/Sites): various API additions for leanprover-community#34917 (leanprover-community#34921)

Author: chrisflav

Mathlib/CategoryTheory/Sites/Coverage.lean

@@ -481,6 +481,30 @@ theorem isSheaf_sup (K L : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
 
 end Presieve
 
+lemma Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
+    {J : Precoverage C} [J.HasPullbacks] [J.IsStableUnderBaseChange] (P : Cᵒᵖ ⥤ Type*) :
+    Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (R : Presieve X),
+      R ∈ J X → Presieve.IsSheafFor P R := by
+  rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
+    Presieve.isSheaf_coverage]
+
+lemma Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small {J : Precoverage C}
+    [J.IsStableUnderBaseChange] [J.HasPullbacks] [Small.{w} J] (P : Cᵒᵖ ⥤ Type*) :
+    Presieve.IsSheaf J.toGrothendieck P ↔
+      ∀ ⦃X : C⦄ (E : ZeroHypercover.{w} J X), Presieve.IsSheafFor P E.presieve₀ := by
+  rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange]
+  refine ⟨fun h X E ↦ h _ E.mem₀, fun h X R hR ↦ ?_⟩
+  obtain ⟨E₀, rfl⟩ := R.exists_eq_preZeroHypercover
+  rw [Presieve.isSheafFor_iff_generate]
+  let E : ZeroHypercover J X := ⟨E₀, hR⟩
+  apply Presieve.isSheafFor_subsieve
+      (S := .generate <| (ZeroHypercover.restrictIndexOfSmall.{w} E).presieve₀)
+  · exact Sieve.generate_mono (by simp [E])
+  · intro Y f
+    rw [← Sieve.pullbackArrows_comm, ← Presieve.isSheafFor_iff_generate,
+      ← PreZeroHypercover.presieve₀_pullback₁, ← ZeroHypercover.pullback₂_toPreZeroHypercover]
+    apply h
+
 namespace Presheaf
 
 theorem isSheaf_iff_isLimit_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ D) :

Mathlib/CategoryTheory/Sites/Grothendieck.lean

@@ -110,12 +110,12 @@ theorem mem_sieves_iff_coe : S ∈ J.sieves X ↔ S ∈ J X :=
   Iff.rfl
 
 /-- Also known as the maximality axiom. -/
-@[simp]
+@[simp, grind .]
 theorem top_mem (X : C) : ⊤ ∈ J X :=
   J.top_mem' X
 
 /-- Also known as the stability axiom. -/
-@[simp]
+@[simp, grind .]
 theorem pullback_stable (f : Y ⟶ X) (hS : S ∈ J X) : S.pullback f ∈ J Y :=
   J.pullback_stable' f hS
 
@@ -127,6 +127,7 @@ lemma pullback_mem_iff_of_isIso {i : X ⟶ Y} [IsIso i] {S : Sieve Y} :
   convert J.pullback_stable (inv i) H
   rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
 
+@[grind .]
 theorem transitive (hS : S ∈ J X) (R : Sieve X) (h : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → R.pullback f ∈ J Y) :
     R ∈ J X :=
   J.transitive' hS R h

Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

@@ -145,6 +145,13 @@ lemma presieve₀_restrictIndex_equiv {ι : Type w'} (e : ι ≃ E.I₀) :
   obtain ⟨i, rfl⟩ := e.surjective i
   exact ⟨i⟩
 
+@[simp]
+lemma presieve₀_restrictIndex_le {ι : Type*} (f : ι → E.I₀) :
+    (E.restrictIndex f).presieve₀ ≤ E.presieve₀ := by
+  rw [Presieve.ofArrows_le_iff]
+  intro i
+  exact .mk _
+
 /-- Replace the indexing type of a pre-`0`-hypercover. -/
 @[simps!]
 def reindex (E : PreZeroHypercover.{w} T) {ι : Type w'} (e : ι ≃ E.I₀) :
@@ -337,6 +344,16 @@ lemma inv_hom_h₀_comp_f {E F : PreZeroHypercover.{w} S} (e : E ≅ F) (i : E.I
 lemma inv_inv_h₀_comp_f {E F : PreZeroHypercover.{w} S} (e : E ≅ F) (i : F.I₀) :
     inv (e.inv.h₀ i) ≫ F.f i = E.f _ := by simp
 
+lemma Hom.sieve₀_le_sieve₀ {E F : PreZeroHypercover S} (f : E.Hom F) : E.sieve₀ ≤ F.sieve₀ := by
+  rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]
+  intro i
+  rw [← f.w₀ i]
+  apply Sieve.downward_closed
+  exact Sieve.le_generate _ _ ⟨f.s₀ i⟩
+
+lemma sieve₀_eq_of_iso {E F : PreZeroHypercover S} (e : E ≅ F) : E.sieve₀ = F.sieve₀ :=
+  le_antisymm e.hom.sieve₀_le_sieve₀ e.inv.sieve₀_le_sieve₀
+
 end Category
 
 section Functoriality
@@ -427,6 +444,12 @@ def interLift (f : G.Hom E) (g : G.Hom F) :
   s₀ i := ⟨f.s₀ i, g.s₀ i⟩
   h₀ i := pullback.lift (f.h₀ i) (g.h₀ i) (by simp)
 
+/-- The refinement given by restricting the indexing type. -/
+@[simps]
+def restrictIndexHom {ι : Type w'} (f : ι → E.I₀) : (E.restrictIndex f).Hom E where
+  s₀ := f
+  h₀ _ := 𝟙 _
+
 end
 
 /-- If `{Uᵢ}` covers `X`, the pre-`0`-hypercover `{Uᵢ ×[Z] Y}` of `X ×[Z] Y` is isomorphic

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

@@ -74,6 +74,9 @@ lemma precoverage_inf : precoverage (P ⊓ Q) = precoverage P ⊓ precoverage Q
   exact ⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
     fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩
 
+@[simp, grind .]
+lemma bot_mem_precoverage (X : C) : ⊥ ∈ precoverage P X := fun _ _ h ↦ h.elim
+
 lemma comap_precoverage {D : Type*} [Category* D] (P : MorphismProperty D) (F : C ⥤ D) :
     P.precoverage.comap F = (P.inverseImage F).precoverage := by
   ext X R

Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

@@ -72,6 +72,16 @@ lemma generate_mem_toGrothendieck {X : C} {R : Presieve X} (hR : R ∈ J X) :
     Sieve.generate R ∈ J.toGrothendieck X :=
   .of _ _ hR
 
+@[gcongr]
+lemma toGrothendieck_mono {J K : Precoverage C} (h : J ≤ K) :
+    J.toGrothendieck ≤ K.toGrothendieck := by
+  intro X S hS
+  induction hS with
+  | of X S hS => exact generate_mem_toGrothendieck (h _ hS)
+  | top X => simp
+  | pullback X S _ Y f _ => grind
+  | transitive X S R _ _ _ _ => grind
+
 /--
 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 presieves
@@ -213,4 +223,25 @@ lemma Presieve.IsSheaf.isSheafFor_of_mem_precoverage {J : Precoverage C} {P : C
   rw [J.isSheaf_toGrothendieck_iff] at h
   simpa [Presieve.isSheafFor_iff_generate] using h (f := 𝟙 S) R hR
 
+lemma PreZeroHypercover.isSheafFor_iff_of_iso {F : Cᵒᵖ ⥤ Type*} {S : C} {𝒰 𝒱 : PreZeroHypercover S}
+    (e : 𝒰 ≅ 𝒱) :
+    𝒰.presieve₀.IsSheafFor F ↔ 𝒱.presieve₀.IsSheafFor F := by
+  rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
+    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]
+
+lemma Presieve.isSheafFor_ofArrows_comp_iff {F : Cᵒᵖ ⥤ Type*} {X : C} {ι : Type*} {Y Z : ι → C}
+    (g : ∀ i, Z i ⟶ X) (e : ∀ i, Y i ≅ Z i) :
+    IsSheafFor F (ofArrows _ (fun i ↦ (e i).hom ≫ g i)) ↔ IsSheafFor F (ofArrows _ g) := by
+  let 𝒰 : PreZeroHypercover X := ⟨_, _, g⟩
+  let 𝒱 : PreZeroHypercover X := ⟨_, _, fun i ↦ (e i).hom ≫ g i⟩
+  let e : 𝒰 ≅ 𝒱 := PreZeroHypercover.isoMk (.refl _) (fun i ↦ (e i).symm)
+  exact PreZeroHypercover.isSheafFor_iff_of_iso e.symm
+
+lemma Presieve.isSheafFor_singleton_iff_of_iso {F : Cᵒᵖ ⥤ Type*} {S X Y : C} (f : X ⟶ S) (g : Y ⟶ S)
+    (e : X ≅ Y) (he : e.hom ≫ g = f) :
+    (singleton f).IsSheafFor F ↔ (singleton g).IsSheafFor F := by
+  subst he
+  rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit,
+    Presieve.isSheafFor_ofArrows_comp_iff]
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Pretopology.lean

@@ -222,6 +222,10 @@ instance orderBot : OrderBot (Pretopology C) where
 theorem toGrothendieck_bot : toGrothendieck (C := C) ⊥ = ⊥ :=
   (gi C).gc.l_bot
 
+@[gcongr]
+lemma toGrothendieck_mono {J K : Pretopology C} (h : J ≤ K) : J.toGrothendieck ≤ K.toGrothendieck :=
+  fun _ _ ⟨R, hR, hle⟩ ↦ ⟨R, h _ hR, hle⟩
+
 instance : InfSet (Pretopology C) where
   sInf T := {
     coverings := sInf ((fun J ↦ J.coverings) '' T)

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -177,15 +177,6 @@ lemma ofArrows.mk' {ι : Type*} {Y : ι → C} {f : ∀ i, Y i ⟶ X} {Z : C} {g
   subst hg
   constructor
 
-theorem ofArrows_pUnit : (ofArrows _ fun _ : PUnit => f) = singleton f := by
-  funext Y
-  ext g
-  constructor
-  · rintro ⟨_⟩
-    apply singleton.mk
-  · rintro ⟨_⟩
-    exact ofArrows.mk PUnit.unit
-
 instance {ι : Type*} (Z : ι → C) (g : ∀ i : ι, Z i ⟶ X)
     [∀ i, HasPullback (g i) f] : (ofArrows Z g).HasPullbacks f where
   hasPullback {_} _ := fun ⟨i⟩ ↦ inferInstance
@@ -274,6 +265,17 @@ lemma ofArrows_le_iff {X : C} {ι : Type*} {Y : ι → C} {f : ∀ i, Y i ⟶ X}
     Presieve.ofArrows Y f ≤ R ↔ ∀ i, R (f i) :=
   ⟨fun hle i ↦ hle _ ⟨i⟩, fun h _ g ⟨i⟩ ↦ h i⟩
 
+lemma ofArrows_of_unique {X : C} {ι : Type*} [Unique ι] {Y : ι → C} (f : ∀ i, Y i ⟶ X) :
+    ofArrows Y f = singleton (f default) := by
+  refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩
+  rw [ofArrows_le_iff]
+  intro i
+  obtain rfl : i = default := Subsingleton.elim _ _
+  simp
+
+theorem ofArrows_pUnit : (ofArrows _ fun _ : PUnit => f) = singleton f := by
+  rw [ofArrows_of_unique]
+
 /-- A convenient constructor for a refinement of a presieve of the form `Presieve.ofArrows`.
 This contains a sieve obtained by `Sieve.bind` and `Sieve.ofArrows`, see
 `Presieve.bind_ofArrows_le_bindOfArrows`, but has better definitional properties. -/
@@ -644,6 +646,10 @@ theorem generate_of_singleton_isSplitEpi (f : Y ⟶ X) [IsSplitEpi f] :
 theorem generate_top : generate (⊤ : Presieve X) = ⊤ :=
   generate_of_contains_isSplitEpi (𝟙 _) ⟨⟩
 
+@[simp]
+lemma generate_bot : generate (⊥ : Presieve X) = ⊥ := by
+  simp only [eq_bot_iff, generate_le_iff, bot_le]
+
 @[simp]
 lemma comp_mem_iff (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) :
     S (i ≫ f) ↔ S f := by