feat(CategoryTheory/Sites): small 0-hypercovers (#30321)

A `w`-`0`-hypercover `E` is `w'`-small if there exists an indexing type `ι` in `Type w'` and a
restriction map `ι → E.I₀` such that the restriction of `E` to `ι` is still covering.

This is weaker than `E.I₀` being `w'`-small. For example, every Zariski cover of `X : Scheme.{u}` is `u`-small,
because `X` itself suffices as indexing type.

Author: chrisflav

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -238,6 +238,9 @@ def Cover.ulift (𝒰 : Cover.{v} (precoverage P) X) : Cover.{u} (precoverage P)
     refine ⟨fun x ↦ ?_, fun i ↦ 𝒰.map_prop _⟩
     use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec
 
+instance : Precoverage.Small.{u} (precoverage P) where
+  zeroHypercoverSmall {S} 𝒰 := ⟨S, Cover.idx 𝒰, (Cover.ulift 𝒰).mem₀⟩
+
 section category
 
 -- TODO: replace this by `ZeroHypercover.Hom`

Mathlib/CategoryTheory/MorphismProperty/Local.lean

@@ -46,6 +46,9 @@ A property of morphisms `P` in `C` is local at the target with respect to the pr
 it respects ismorphisms, and:
 `P` holds for `f : X ⟶ Y` if and only if it holds for the restrictions of `f` to `Uᵢ` for a
 `0`-hypercover `{Uᵢ}` of `Y` in the precoverage `K`.
+
+For a version of `of_zeroHypercover` that takes a `v`-small `0`-hypercover in an arbitrary
+universe, use `CategoryTheory.MorphismProperty.of_zeroHypercover_target`.
 -/
 class IsLocalAtTarget (P : MorphismProperty C) (K : Precoverage C) [K.HasPullbacks]
     extends RespectsIso P where
@@ -103,14 +106,23 @@ instance inf (P Q : MorphismProperty C) [IsLocalAtTarget P K] [IsLocalAtTarget Q
 
 end IsLocalAtTarget
 
-alias of_zeroHypercover_target := IsLocalAtTarget.of_zeroHypercover
+lemma of_zeroHypercover_target {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks]
+    [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : Precoverage.ZeroHypercover.{w} K Y)
+    [Precoverage.ZeroHypercover.Small.{v} 𝒰] (h : ∀ i, P (pullback.snd f (𝒰.f i))) :
+    P f := by
+  rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
+  simp [h]
+
 alias iff_of_zeroHypercover_target := IsLocalAtTarget.iff_of_zeroHypercover
 
 /--
 A property of morphisms `P` in `C` is local at the source with respect to the precoverage `K` if
 it respects ismorphisms, and:
 `P` holds for `f : X ⟶ Y` if and only if it holds for the restrictions of `f` to `Uᵢ` for a
 `0`-hypercover `{Uᵢ}` of `X` in the precoverage `K`.
+
+For a version of `of_zeroHypercover` that takes a `v`-small `0`-hypercover in an arbitrary
+universe, use `CategoryTheory.MorphismProperty.of_zeroHypercover_source`.
 -/
 class IsLocalAtSource (P : MorphismProperty C) (K : Precoverage C) extends RespectsIso P where
   /-- If `P` holds for `f : X ⟶ Y`, it also holds for `𝒰.f i ≫ f` for any `K`-cover `𝒰` of `X`. -/
@@ -153,7 +165,13 @@ instance inf (P Q : MorphismProperty C) [IsLocalAtSource P K] [IsLocalAtSource Q
 
 end IsLocalAtSource
 
-alias of_zeroHypercover_source := IsLocalAtSource.of_zeroHypercover
+lemma of_zeroHypercover_source {P : MorphismProperty C} {K : Precoverage C}
+    [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : Precoverage.ZeroHypercover.{w} K X)
+    [Precoverage.ZeroHypercover.Small.{v} 𝒰] (h : ∀ i, P (𝒰.f i ≫ f)) :
+    P f := by
+  rw [IsLocalAtSource.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
+  simp [h]
+
 alias iff_of_zeroHypercover_source := IsLocalAtSource.iff_of_zeroHypercover
 
 end MorphismProperty

Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

@@ -104,20 +104,31 @@ def bind (E : PreZeroHypercover.{w} T) (F : ∀ i, PreZeroHypercover.{w'} (E.X i
   X ij := (F ij.1).X ij.2
   f ij := (F ij.1).f ij.2 ≫ E.f ij.1
 
-/-- Replace the indexing type of a pre-`0`-hypercover. -/
+/-- Restrict the indexing type to `ι` by precomposing with a function `ι → E.I₀`. -/
 @[simps]
-def reindex (E : PreZeroHypercover.{w} T) {ι : Type w'} (e : ι ≃ E.I₀) :
+def restrictIndex (E : PreZeroHypercover.{w} T) {ι : Type w'} (f : ι → E.I₀) :
     PreZeroHypercover.{w'} T where
   I₀ := ι
-  X := E.X ∘ e
-  f i := E.f (e i)
+  X := E.X ∘ f
+  f i := E.f (f i)
 
 @[simp]
-lemma presieve₀_reindex {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).presieve₀ = E.presieve₀ := by
+lemma presieve₀_restrictIndex_equiv {ι : Type w'} (e : ι ≃ E.I₀) :
+    (E.restrictIndex e).presieve₀ = E.presieve₀ := by
   refine le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_
   obtain ⟨i, rfl⟩ := e.surjective i
   exact ⟨i⟩
 
+/-- Replace the indexing type of a pre-`0`-hypercover. -/
+@[simps!]
+def reindex (E : PreZeroHypercover.{w} T) {ι : Type w'} (e : ι ≃ E.I₀) :
+    PreZeroHypercover.{w'} T :=
+  E.restrictIndex e
+
+@[simp]
+lemma presieve₀_reindex {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).presieve₀ = E.presieve₀ := by
+  simp [reindex]
+
 /-- Pairwise intersection of two pre-`0`-hypercovers. -/
 @[simps!]
 noncomputable
@@ -416,6 +427,61 @@ def map (F : C ⥤ D) (E : ZeroHypercover.{w} J S) (h : J ≤ K.comap F) :
 
 end Functoriality
 
+/--
+A `w`-`0`-hypercover `E` is `w'`-small if there exists an indexing type `ι` in `Type w'` and a
+restriction map `ι → E.I₀` such that the restriction of `E` to `ι` is still covering.
+
+Note: This is weaker than `E.I₀` being `w'`-small. For example, every Zariski cover of
+`X : Scheme.{u}` is `u`-small, because `X` itself suffices as indexing type.
+-/
+protected class Small (E : ZeroHypercover.{w} J S) where
+  exists_restrictIndex_mem (E) : ∃ (ι : Type w') (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J S
+
+instance (E : ZeroHypercover.{w} J S) [Small.{w'} E.I₀] : ZeroHypercover.Small.{w'} E where
+  exists_restrictIndex_mem := ⟨_, (equivShrink E.I₀).symm, by simp [E.mem₀]⟩
+
+/-- The `w'`-index type of a `w'`-small `0`-hypercover. -/
+def Small.Index (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] : Type w' :=
+  (Small.exists_restrictIndex_mem E).choose
+
+/-- The index restriction function of a small `0`-hypercover. -/
+noncomputable def Small.restrictFun (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] :
+    Index E → E.I₀ :=
+  (Small.exists_restrictIndex_mem E).choose_spec.choose
+
+lemma Small.mem₀ (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] :
+    (E.restrictIndex <| Small.restrictFun E).presieve₀ ∈ J S :=
+  (Small.exists_restrictIndex_mem E).choose_spec.choose_spec
+
+instance (E : ZeroHypercover.{w} J S) : ZeroHypercover.Small.{max u v} E where
+  exists_restrictIndex_mem := by
+    obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows
+    have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) :
+        ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j := by
+      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
+      use j, rfl
+      simp
+    choose j h₁ h₂ using this
+    refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
+    convert E.mem₀
+    exact le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))
+
+/-- Restrict a `w'`-small `0`-hypercover to a `w'`-`0`-hypercover. -/
+@[simps toPreZeroHypercover]
+noncomputable
+def restrictIndexOfSmall (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] :
+    ZeroHypercover.{w'} J S where
+  __ := E.toPreZeroHypercover.restrictIndex (Small.restrictFun E)
+  mem₀ := Small.mem₀ E
+
+instance (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] {T : C} (f : T ⟶ S)
+    [IsStableUnderBaseChange.{w} J] [IsStableUnderBaseChange.{w'} J]
+    [∀ (i : E.I₀), HasPullback f (E.f i)] :
+    ZeroHypercover.Small.{w'} (E.pullback₁ f) := by
+  use Small.Index E, Small.restrictFun E
+  have _ (i) : HasPullback f (E.restrictIndexOfSmall.f i) := by dsimp; infer_instance
+  exact ((restrictIndexOfSmall.{w'} E).pullback₁ f).mem₀
+
 end ZeroHypercover
 
 lemma mem_iff_exists_zeroHypercover {X : C} {R : Presieve X} :
@@ -424,6 +490,19 @@ lemma mem_iff_exists_zeroHypercover {X : C} {R : Presieve X} :
   obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
   use ⟨⟨ι, Y, f⟩, hR⟩
 
+/-- A precoverage is `w`-small, if every `0`-hypercover is `w`-small. -/
+class Small (J : Precoverage C) : Prop where
+  zeroHypercoverSmall : ∀ {S : C} (E : ZeroHypercover.{max u v} J S), ZeroHypercover.Small.{w'} E
+
+instance (J : Precoverage C) [Small.{w} J] {S : C} (E : ZeroHypercover.{w'} J S) :
+    ZeroHypercover.Small.{w} E := by
+  have : ZeroHypercover.Small.{w} (ZeroHypercover.restrictIndexOfSmall.{max u v} E) :=
+    Small.zeroHypercoverSmall _
+  let E' := ZeroHypercover.restrictIndexOfSmall.{w}
+    (ZeroHypercover.restrictIndexOfSmall.{max u v} E)
+  use E'.I₀, ZeroHypercover.Small.restrictFun _ ∘ ZeroHypercover.Small.restrictFun _
+  exact E'.mem₀
+
 end Precoverage
 
 end CategoryTheory

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

@@ -6,6 +6,7 @@ Authors: Christian Merten
 import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.Sites.Pretopology
 import Mathlib.CategoryTheory.Sites.Coverage
+import Mathlib.CategoryTheory.Sites.Hypercover.Zero
 
 /-!
 # The site induced by a morphism property
@@ -19,6 +20,8 @@ this construction by intersecting with the pretopology of surjective families.
 
 -/
 
+universe w
+
 namespace CategoryTheory
 
 open Limits
@@ -52,6 +55,12 @@ instance [P.IsStableUnderComposition] : P.precoverage.IsStableUnderComposition w
     intro ⟨i⟩
     exact P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)
 
+instance : Precoverage.Small.{w} P.precoverage where
+  zeroHypercoverSmall E := by
+    constructor
+    use PEmpty, PEmpty.elim
+    simp
+
 lemma precoverage_monotone (hPQ : P ≤ Q) : precoverage P ≤ precoverage Q :=
   fun _ _ hR _ _ hg ↦ hPQ _ (hR hg)