diff --git a/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean b/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean index 0d9c2017ae7dac..f6eb02b8ece63e 100644 --- a/Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean +++ b/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` diff --git a/Mathlib/CategoryTheory/MorphismProperty/Local.lean b/Mathlib/CategoryTheory/MorphismProperty/Local.lean index b755263ffea2b2..c0920f0408bd18 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Local.lean +++ b/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,7 +106,13 @@ 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 /-- @@ -111,6 +120,9 @@ A property of morphisms `P` in `C` is local at the source 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 `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 diff --git a/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean b/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean index 8bc79abe2d5496..fae7e1d1b1ab29 100644 --- a/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/MorphismProperty.lean b/Mathlib/CategoryTheory/Sites/MorphismProperty.lean index ef1f10626603f9..cbfcaa7bd9d44b 100644 --- a/Mathlib/CategoryTheory/Sites/MorphismProperty.lean +++ b/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)