From d8328aec2ad8b738c44ecc70270118e6baea337a Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 6 Feb 2026 16:11:11 +0100 Subject: [PATCH 1/5] wip --- Mathlib.lean | 1 + .../AlgebraicGeometry/Cover/QuasiCompact.lean | 28 + .../Morphisms/UnderlyingMap.lean | 5 + .../AlgebraicGeometry/Sites/BigZariski.lean | 45 +- Mathlib/AlgebraicGeometry/Sites/Fpqc.lean | 582 ++++++++++++++++++ .../Sites/MorphismProperty.lean | 7 + .../AlgebraicGeometry/Sites/Pretopology.lean | 38 +- .../Limits/Shapes/DisjointCoproduct.lean | 11 +- Mathlib/CategoryTheory/Sites/Coverage.lean | 7 + .../CategoryTheory/Sites/Grothendieck.lean | 5 +- .../Sites/MorphismProperty.lean | 3 + .../Sites/PrecoverageToGrothendieck.lean | 10 + Mathlib/CategoryTheory/Sites/Sieves.lean | 4 + 13 files changed, 720 insertions(+), 26 deletions(-) create mode 100644 Mathlib/AlgebraicGeometry/Sites/Fpqc.lean diff --git a/Mathlib.lean b/Mathlib.lean index f1d0344181f230..d44cf70dafe7f4 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1355,6 +1355,7 @@ public import Mathlib.AlgebraicGeometry.Restrict public import Mathlib.AlgebraicGeometry.Scheme public import Mathlib.AlgebraicGeometry.Sites.BigZariski public import Mathlib.AlgebraicGeometry.Sites.Etale +public import Mathlib.AlgebraicGeometry.Sites.Fpqc public import Mathlib.AlgebraicGeometry.Sites.MorphismProperty public import Mathlib.AlgebraicGeometry.Sites.Pretopology public import Mathlib.AlgebraicGeometry.Sites.QuasiCompact diff --git a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean index 20bf8acb65d3fc..ea7c0efb6a1227 100644 --- a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean @@ -166,6 +166,34 @@ instance {𝒱 : PreZeroHypercover S} [QuasiCompactCover 𝒰] : QuasiCompactCov instance {𝒱 : PreZeroHypercover S} [QuasiCompactCover 𝒱] : QuasiCompactCover (𝒰.sum 𝒱) := .of_hom (PreZeroHypercover.sumInr _ _) +lemma exists_hom [P.IsMultiplicative] {S : Scheme.{u}} (𝒰 : S.Cover (Scheme.precoverage P)) + [P.RespectsLeft @IsOpenImmersion] [CompactSpace S] [QuasiCompactCover 𝒰.toPreZeroHypercover] : + ∃ (𝒱 : Scheme.AffineCover.{w} P S) (f : 𝒱.cover ⟶ 𝒰), + Finite 𝒱.I₀ ∧ ∀ j, IsOpenImmersion (f.h₀ j) := by + obtain ⟨n, f, V, hV, h⟩ := QuasiCompactCover.exists_isAffineOpen_of_isCompact 𝒰.1 + (show IsCompact (⊤ : TopologicalSpace.Opens S).carrier from isCompact_univ) + simp only [coe_top, ← Set.univ_subset_iff, Set.subset_def, Set.mem_univ, Set.mem_iUnion, + Set.mem_image, SetLike.mem_coe, forall_const] at h + choose idx x hmem hx using h + refine ⟨?_, ?_, ?_, ?_⟩ + · exact + { I₀ := ULift (Fin n) + X i := Γ(_, V i.down) + f i := (hV _).fromSpec ≫ 𝒰.f (f _) + idx s := ⟨idx s⟩ + covers s := by + use (hV _).isoSpec.hom.base ⟨x s, hmem s⟩ + rw [← Scheme.Hom.comp_apply, ← IsAffineOpen.isoSpec_inv_ι, Category.assoc, + Iso.hom_inv_id_assoc] + simp [hx] + map_prop i := + RespectsLeft.precomp (Q := IsOpenImmersion) _ inferInstance _ (𝒰.map_prop _) } + · exact + { s₀ i := f i.down + h₀ i := (hV i.down).fromSpec } + · infer_instance + · infer_instance + end QuasiCompactCover namespace Scheme diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean index 74c35055149e0f..aa32b140618e4e 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean @@ -130,6 +130,11 @@ def Scheme.Hom.cover {P : MorphismProperty Scheme.{u}} {X S : Scheme.{u}} (f : X rw [singleton_mem_precoverage_iff] exact ⟨f.surjective, hf⟩ +@[simp] +lemma Scheme.Hom.presieve₀_cover {P : MorphismProperty Scheme.{u}} {X S : Scheme.{u}} (f : X ⟶ S) + (hf : P f) [Surjective f] : (f.cover hf).presieve₀ = Presieve.singleton f := by + simp [cover] + instance {P : MorphismProperty Scheme.{u}} {X S : Scheme.{u}} (f : X ⟶ S) (hf : P f) [Surjective f] : Unique (Scheme.Hom.cover f hf).I₀ := inferInstanceAs <| Unique PUnit diff --git a/Mathlib/AlgebraicGeometry/Sites/BigZariski.lean b/Mathlib/AlgebraicGeometry/Sites/BigZariski.lean index e6b82fc4da7734..ccd67f225c8853 100644 --- a/Mathlib/AlgebraicGeometry/Sites/BigZariski.lean +++ b/Mathlib/AlgebraicGeometry/Sites/BigZariski.lean @@ -7,6 +7,8 @@ module public import Mathlib.AlgebraicGeometry.Sites.Pretopology public import Mathlib.CategoryTheory.Sites.Canonical +public import Mathlib.CategoryTheory.Sites.Preserves + /-! # The big Zariski site of schemes @@ -32,7 +34,7 @@ TODO: universe v u -open CategoryTheory +open CategoryTheory Limits Opposite namespace AlgebraicGeometry @@ -46,12 +48,13 @@ def zariskiPretopology : Pretopology Scheme.{u} := abbrev zariskiTopology : GrothendieckTopology Scheme.{u} := grothendieckTopology IsOpenImmersion -lemma zariskiTopology_eq : zariskiTopology.{u} = zariskiPretopology.toGrothendieck := rfl +lemma zariskiTopology_eq : zariskiTopology.{u} = zariskiPretopology.toGrothendieck := + Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck.symm instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical := by apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj intro X - rw [Presieve.isSheaf_pretopology] + rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange] rintro Y S hS x hx obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS let e : Y ⟶ X := 𝓤.glueMorphisms (fun j => x (𝓤.f _) (.mk _)) <| by @@ -70,4 +73,40 @@ instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical := by end Scheme +/-- Zariski sheaves preserve products. -/ +lemma preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology {F : Scheme.{u}ᵒᵖ ⥤ Type v} + {ι : Type*} [Small.{u} ι] [Small.{v} ι] (hF : Presieve.IsSheaf Scheme.zariskiTopology F) : + PreservesLimitsOfShape (Discrete ι) F := by + apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_of_discrete + intro X + have (i : ι) : Mono (Cofan.inj (Sigma.cocone (Discrete.functor <| unop ∘ X)) i) := + inferInstanceAs <| Mono (Sigma.ι _ _) + refine Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial + (Sigma.cocone (Discrete.functor <| unop ∘ X)) (coproductIsCoproduct' _) ?_ ?_ + · apply hF.isSheafFor + convert (⊥_ Scheme).bot_mem_grothendieckTopology + rw [eq_bot_iff] + rintro Y f ⟨g, _, _, ⟨i⟩, _⟩ + exact i.elim + · intro i j + exact CoproductDisjoint.isPullback_of_isInitial + (coproductIsCoproduct' <| Discrete.functor <| unop ∘ X) initialIsInitial + · exact hF.isSheafFor _ _ (sigmaOpenCover _).mem_grothendieckTopology + +/-- If `F` is a locally directed diagram of open immersions (e.g., the diagram indexing +a coproduct). Then the colimit inclusions are a Zariski covering. -/ +lemma ofArrows_ι_mem_zariskiTopology_of_isColimit {J : Type*} [Category J] + (F : J ⥤ Scheme.{u}) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] + [(F.comp Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u} J] + (c : Cocone F) (hc : IsColimit c) : + Sieve.ofArrows _ c.ι.app ∈ Scheme.zariskiTopology c.pt := by + let iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F) + rw [← GrothendieckTopology.pullback_mem_iff_of_isIso (i := iso.inv)] + apply GrothendieckTopology.superset_covering _ ?_ ?_ + · exact Sieve.ofArrows _ (colimit.ι F) + · rw [Sieve.ofArrows, Sieve.generate_le_iff] + rintro - - ⟨i⟩ + exact ⟨_, 𝟙 _, c.ι.app i, ⟨i⟩, by simp [iso]⟩ + · exact (Scheme.IsLocallyDirected.openCover F).mem_grothendieckTopology + end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean new file mode 100644 index 00000000000000..da1bbd16183e03 --- /dev/null +++ b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean @@ -0,0 +1,582 @@ +/- +Copyright (c) 2025 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +import Mathlib.AlgebraicGeometry.Sites.BigZariski +import Mathlib.AlgebraicGeometry.Sites.QuasiCompact +import Mathlib.AlgebraicGeometry.Cover.Sigma +import Mathlib.CategoryTheory.Sites.Preserves + +/-! +# The quasi-compact topology of a scheme + +The `qc`-pretopology of a scheme wrt. to a morphism property `P` is the pretopology +given by quasi compact covers satisfying `P`. + +We show that a presheaf is a sheaf in this topology if and only if it is a sheaf +in the Zariski topology and a sheaf on single object `P`-coverings of affine schemes. +-/ + +universe w' w v u + +open CategoryTheory Limits Opposite + +namespace CategoryTheory + +open Limits + +variable {C : Type*} [Category C] + +lemma Presieve.ofArrows_of_unique {S : C} {ι : Type*} [Unique ι] {X : ι → C} (f : ∀ i, X i ⟶ S) : + ofArrows X f = singleton (f default) := by + refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩ + rw [ofArrows_le_iff] + intro i + obtain rfl : i = default := Subsingleton.elim _ _ + simp + +-- TODO: this is almost in mathlib, with slightly less general universe assumptions on `F` +-- and with a wrong name +lemma Presieve.IsSheafFor.of_isSheafFor_pullback'' (F : Cᵒᵖ ⥤ Type*) {X : C} + (S T : Sieve X) + (hF : Presieve.IsSheafFor F S.arrows) + (hF' : ∀ {Y : C} (f : Y ⟶ X), Presieve.IsSeparatedFor F (S.pullback f).arrows) + (H : ∀ {Y : C} (f : Y ⟶ X), S f → Presieve.IsSheafFor F (T.pullback f).arrows) : + Presieve.IsSheafFor F T.arrows := by + intro t ht + have ⦃Y : C⦄ (f : Y ⟶ X) (hf : S f) := H f hf (t.pullback f) (ht.pullback f) + choose s hs huniq using this + have hr : FamilyOfElements.Compatible s := by + rw [Presieve.compatible_iff_sieveCompatible] + intro Y Z f g hf + refine (H (g ≫ f) (by simp [hf])).isSeparatedFor.ext fun U o ho ↦ ?_ + simp only [Sieve.pullback_apply] at ho + dsimp only [FamilyOfElements.IsAmalgamation, FamilyOfElements.pullback] at hs + rw [← FunctorToTypes.map_comp_apply, ← op_comp, hs _ _ _ ho, hs _ _ _ (by simpa)] + congr 1 + simp + obtain ⟨t', ht', hunique⟩ := hF s hr + refine ⟨t', fun Y f hf ↦ (hF' f).ext fun Z g hg ↦ ?_, fun y hy ↦ ?_⟩ + · rw [← FunctorToTypes.map_comp_apply, ← op_comp, ht' (g ≫ f) hg, ← t.comp_of_compatible _ ht] + have := hs (g ≫ f) hg (𝟙 _) + dsimp only [Presieve.FamilyOfElements.IsAmalgamation, + Presieve.FamilyOfElements.pullback] at this + simp only [Sieve.pullback_apply, Category.id_comp, op_id, FunctorToTypes.map_id_apply] at this + rw [this] + · congr 1 + simp + · simp [hf] + · refine hunique _ fun Y f hf ↦ huniq _ _ _ fun Z g hg ↦ ?_ + simp [Presieve.FamilyOfElements.pullback, ← hy _ hg] + +lemma Presieve.IsSheafFor.of_isSheafFor_pullback + (F : Cᵒᵖ ⥤ Type*) {X : C} + (S : Presieve X) (T : Sieve X) [S.HasPairwisePullbacks] + (hF : Presieve.IsSheafFor F S) + (hF' : ∀ {Y : C} (f : Y ⟶ X), Presieve.IsSeparatedFor F ((Sieve.generate S).pullback f).arrows) + (H' : ∀ {Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X) (hf : S f) (hg : S g), + haveI := HasPairwisePullbacks.has_pullbacks hf hg + ∃ (R : Presieve (pullback f g)), Presieve.IsSeparatedFor F R ∧ + ∀ {W : C} (w : W ⟶ pullback f g), + R w → Presieve.IsSeparatedFor F (T.pullback (w ≫ pullback.fst f g ≫ f)).arrows) + (H : ∀ {Y : C} (f : Y ⟶ X), S f → Presieve.IsSheafFor F (T.pullback f).arrows) : + Presieve.IsSheafFor F T.arrows := by + intro t ht + have ⦃Y : C⦄ (f : Y ⟶ X) (hf : S f) := H f hf (t.pullback f) (ht.pullback f) + choose s hs huniq using this + have hr : FamilyOfElements.Compatible s := by + rw [pullbackCompatible_iff] + intro Y Z f g hf hg + haveI := HasPairwisePullbacks.has_pullbacks hf hg + obtain ⟨R, hR, h⟩ := H' f g hf hg + refine hR.ext fun W w hw ↦ (h w hw).ext fun U u hu ↦ ?_ + simp only [← FunctorToTypes.map_comp_apply, ← op_comp] + dsimp only [FamilyOfElements.IsAmalgamation, FamilyOfElements.pullback] at hs + rw [hs f hf (u ≫ w ≫ pullback.fst f g) (by simpa), + hs g hg (u ≫ w ≫ pullback.snd f g) (by simpa [← pullback.condition])] + congr 1 + simp [pullback.condition] + obtain ⟨t', ht', hunique⟩ := hF s hr + refine ⟨t', fun Y f hf ↦ (hF' f).ext fun Z g hg ↦ ?_, fun y hy ↦ ?_⟩ + · rw [← FunctorToTypes.map_comp_apply, ← op_comp] + simp only [Sieve.pullback_apply, Sieve.generate_apply] at hg + obtain ⟨W, w, u, hu, heq⟩ := hg + simp only [← heq, op_comp, FunctorToTypes.map_comp_apply, ht' u hu] + have : t (g ≫ f) (by simp [hf]) = t (w ≫ u) (by simp [heq, hf]) := by + congr 1 + rw [heq] + rw [← t.comp_of_compatible _ ht, this] + apply hs + · refine hunique _ fun Y f hf ↦ huniq _ _ _ fun Z g hg ↦ ?_ + simp [Presieve.FamilyOfElements.pullback, ← hy _ hg] + +lemma Presieve.IsSheafFor.of_isSheafFor_pullback' (F : Cᵒᵖ ⥤ Type*) {X : C} + (S T : Presieve X) [S.HasPairwisePullbacks] + (hF : Presieve.IsSheafFor F S) + (hF' : ∀ {Y : C} (f : Y ⟶ X), Presieve.IsSeparatedFor F ((Sieve.generate S).pullback f).arrows) + (H' : ∀ {Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X) (hf : S f) (hg : S g), + haveI := HasPairwisePullbacks.has_pullbacks hf hg + ∃ (R : Presieve (pullback f g)), Presieve.IsSeparatedFor F R ∧ + ∀ {W : C} (w : W ⟶ pullback f g), + R w → Presieve.IsSeparatedFor F + ((Sieve.generate T).pullback (w ≫ pullback.fst f g ≫ f)).arrows) + (H : ∀ {Y : C} (f : Y ⟶ X), + S f → Presieve.IsSheafFor F ((Sieve.generate T).pullback f).arrows) : + Presieve.IsSheafFor F T := by + rw [isSheafFor_iff_generate] + apply Presieve.IsSheafFor.of_isSheafFor_pullback F S _ _ hF' + · assumption + · assumption + · assumption + +end CategoryTheory + +namespace CategoryTheory + +variable {C : Type*} [Category C] {X : C} + +@[simps] +def PreZeroHypercover.restrictIndexHom (E : PreZeroHypercover.{w} X) {ι : Type w'} + (f : ι → E.I₀) : + (E.restrictIndex f).Hom E where + s₀ := f + h₀ _ := 𝟙 _ + +@[simp] +lemma PreZeroHypercover.presieve₀_restrictIndex_le {X : C} (E : PreZeroHypercover X) {ι : Type*} + (f : ι → E.I₀) : + (E.restrictIndex f).presieve₀ ≤ E.presieve₀ := by + rw [Presieve.ofArrows_le_iff] + intro i + exact .mk _ + +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 ↦ ?_, fun h X R hR ↦ ?_⟩ + · apply h + exact E.mem₀ + · 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 + +lemma Presieve.isSheafFor_ofArrows_comp_iff {F : Cᵒᵖ ⥤ Type*} {ι : Type*} {Y Z : ι → C} + (g : ∀ i, Z i ⟶ X) + (e : ∀ i, Y i ≅ Z i) : + Presieve.IsSheafFor F (.ofArrows _ (fun i ↦ (e i).hom ≫ g i)) ↔ + Presieve.IsSheafFor F (.ofArrows _ g) := by + have : Sieve.generate (.ofArrows _ g) = + Sieve.generate (.ofArrows _ (fun i ↦ (e i).hom ≫ g i)) := by + refine le_antisymm ?_ ?_ + · rw [Sieve.generate_le_iff] + rintro - - ⟨i⟩ + exact ⟨_, (e i).inv, (e i).hom ≫ g i, ⟨i⟩, by simp⟩ + · rw [Sieve.generate_le_iff] + rintro - - ⟨i⟩ + exact ⟨_, (e i).hom, _, ⟨i⟩, by simp⟩ + rw [Presieve.isSheafFor_iff_generate, ← this, ← Presieve.isSheafFor_iff_generate] + +lemma 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) : + Presieve.IsSheafFor F (.singleton f) ↔ Presieve.IsSheafFor F (.singleton g) := by + subst he + rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit, + Presieve.isSheafFor_ofArrows_comp_iff] + +@[gcongr] +lemma Pretopology.toGrothendieck_mono {C : Type*} [Category C] [HasPullbacks C] + {J K : Pretopology C} (h : J ≤ K) : J.toGrothendieck ≤ K.toGrothendieck := + fun _ _ ⟨R, hR, hle⟩ ↦ ⟨R, h _ hR, hle⟩ + +attribute [grind .] GrothendieckTopology.pullback_stable GrothendieckTopology.transitive + +@[gcongr] +lemma Precoverage.toPretopology_mono {C : Type*} [Category C] [Limits.HasPullbacks C] + {J K : Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] + [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] + (h : J ≤ K) : J.toPretopology ≤ K.toPretopology := + h + +variable {C : Type*} [Category C] + +/-- +If +- `F` contravariantly maps (suitable) coproducts to products, +- (suitable) coproducts exist in `C`, and +- (suitable) coproducts distribute over pullbacks, then: + +`F` is a sheaf for the single object covering `{ ∐ᵢ Yᵢ ⟶ X }` +if and only if it is a presieve for `{ fᵢ : Yᵢ ⟶ X }ᵢ`. + +Note: The second two conditions are satisfied if `C` is (finitary) extensive. +-/ +lemma Presieve.isSheafFor_sigmaDesc_iff {F : Cᵒᵖ ⥤ Type v} {X : C} {ι : Type*} [Small.{v} ι] + {Y : ι → C} + (f : ∀ i, Y i ⟶ X) [(ofArrows Y f).HasPairwisePullbacks] + [HasCoproduct Y] [HasCoproduct fun (ij : ι × ι) ↦ pullback (f ij.1) (f ij.2)] + [HasPullback (Limits.Sigma.desc f) (Limits.Sigma.desc f)] + [PreservesLimit (Discrete.functor <| fun i ↦ op (Y i)) F] + [PreservesLimit (Discrete.functor fun (ij : ι × ι) ↦ op (pullback (f ij.1) (f ij.2))) F] + [IsIso (Limits.Sigma.desc fun (ij : ι × ι) ↦ Limits.pullback.map (f ij.fst) (f ij.snd) + (Limits.Sigma.desc f) (Limits.Sigma.desc f) (Limits.Sigma.ι _ _) (Limits.Sigma.ι _ _) (𝟙 X) + (by simp) (by simp))] : + Presieve.IsSheafFor F (.singleton <| Limits.Sigma.desc f) ↔ + Presieve.IsSheafFor F (.ofArrows Y f) := by + let e : (∐ fun (ij : ι × ι) ↦ pullback (f ij.1) (f ij.2)) ⟶ + pullback (Limits.Sigma.desc f) (Limits.Sigma.desc f) := + Limits.Sigma.desc fun ij ↦ + pullback.map _ _ _ _ (Limits.Sigma.ι _ _) (Limits.Sigma.ι _ _) (𝟙 X) (by simp) (by simp) + rw [Equalizer.Presieve.isSheafFor_singleton_iff (pullback.cone _ _) (pullback.isLimit _ _), + Equalizer.Presieve.Arrows.sheaf_condition] + refine (Fork.isLimitEquivOfIsos _ _ ?_ ?_ ?_ ?_ ?_ ?_).nonempty_congr + · exact F.mapIso (opCoproductIsoProduct Y) ≪≫ PreservesProduct.iso F _ + · exact F.mapIso (.op <| asIso e) ≪≫ F.mapIso (opCoproductIsoProduct _) ≪≫ + PreservesProduct.iso F _ + · exact Iso.refl _ + · refine Pi.hom_ext _ _ fun ij ↦ ?_ + simp only [Iso.trans_hom, Functor.mapIso_hom, PreservesProduct.iso_hom, Category.assoc, + limit.cone_x, PullbackCone.fst_limit_cone, Iso.op_hom, asIso_hom, e, piComparison_comp_π, + Equalizer.Presieve.Arrows.firstMap] + rw [← F.map_comp, opCoproductIsoProduct_hom_comp_π, ← F.map_comp, ← op_comp, Sigma.ι_desc, + ← F.map_comp, ← op_comp, pullback.lift_fst, Pi.lift_π, piComparison_comp_π_assoc, + ← F.map_comp, ← F.map_comp] + simp + · refine Pi.hom_ext _ _ fun ij ↦ ?_ + simp only [Iso.trans_hom, Functor.mapIso_hom, PreservesProduct.iso_hom, Category.assoc, + limit.cone_x, PullbackCone.snd_limit_cone, Iso.op_hom, asIso_hom, e, piComparison_comp_π, + Equalizer.Presieve.Arrows.secondMap] + rw [← F.map_comp, opCoproductIsoProduct_hom_comp_π, ← F.map_comp, ← op_comp, Sigma.ι_desc, + ← F.map_comp, ← op_comp, pullback.lift_snd, Pi.lift_π, piComparison_comp_π_assoc, + ← F.map_comp, ← F.map_comp] + simp + · refine Pi.hom_ext _ _ fun i ↦ ?_ + simp only [Fork.ofι_pt, Fork.ι_ofι, Iso.trans_hom, Functor.mapIso_hom, PreservesProduct.iso_hom, + Category.assoc, piComparison_comp_π] + rw [← F.map_comp, ← F.map_comp, opCoproductIsoProduct_hom_comp_π, ← op_comp, Sigma.ι_desc] + simp [Equalizer.Presieve.Arrows.forkMap] + +end CategoryTheory + +namespace AlgebraicGeometry + +open Scheme + +variable {P : MorphismProperty Scheme.{u}} + +@[simp] +lemma Scheme.Cover.ofArrows_sigma {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) + [IsZariskiLocalAtSource P] : + Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f = Presieve.singleton (Sigma.desc 𝒰.f) := by + refine le_antisymm ?_ ?_ + · intro T g ⟨i⟩ + exact Presieve.singleton_self _ + · intro T g ⟨⟩ + exact ⟨⟨⟩⟩ + +/-- The `qc`-precoverage of a scheme wrt. to a morphism property `P` is the precoverage +given by quasi compact covers satisfying `P`. -/ +abbrev propqcPrecoverage (P : MorphismProperty Scheme.{u}) : Precoverage Scheme.{u} := + qcPrecoverage ⊓ Scheme.precoverage P + +instance {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} + (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : QuasiCompactCover 𝒰.toPreZeroHypercover := by + rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] + exact 𝒰.mem₀.1 + +@[simps toPreZeroHypercover] +abbrev Scheme.Cover.forgetQc {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} + (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : + S.Cover (precoverage P) where + __ := 𝒰.toPreZeroHypercover + mem₀ := 𝒰.mem₀.2 + +instance {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} + (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : + QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover := by + dsimp; infer_instance + +@[simps toPreZeroHypercover] +def Scheme.Cover.ofQuasiCompactCover {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} + (𝒰 : Scheme.Cover (precoverage P) S) [qc : QuasiCompactCover 𝒰.1] : + Scheme.Cover (propqcPrecoverage P) S where + __ := 𝒰.toPreZeroHypercover + mem₀ := ⟨Scheme.presieve₀_mem_qcPrecoverage_iff.mpr ‹_›, 𝒰.mem₀⟩ + +namespace QuasiCompactCover + +def uliftaux {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + Type u := + Σ (U : S.affineOpens), Fin (exists_isAffineOpen_of_isCompact 𝒰 U.2.isCompact).choose + +structure IdxAux {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : Type u where + affineOpen : S.affineOpens + idx : Fin (exists_isAffineOpen_of_isCompact 𝒰 affineOpen.2.isCompact).choose + +noncomputable def ulift {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + PreZeroHypercover.{u} S := + 𝒰.restrictIndex fun i : IdxAux 𝒰 ↦ + (exists_isAffineOpen_of_isCompact 𝒰 i.affineOpen.2.isCompact).choose_spec.choose i.idx + +noncomputable +def uliftHom {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + (ulift 𝒰).Hom 𝒰 := + 𝒰.restrictIndexHom _ + +instance {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + QuasiCompactCover (ulift 𝒰) where + isCompactOpenCovered_of_isAffineOpen {U} hU := + let H := exists_isAffineOpen_of_isCompact 𝒰 hU.isCompact + .of_finite (fun i : Fin H.choose ↦ ⟨⟨U, hU⟩, i⟩) + (fun _ ↦ H.choose_spec.choose_spec.choose _) + (fun _ ↦ H.choose_spec.choose_spec.choose_spec.left _ |>.isCompact) + H.choose_spec.choose_spec.choose_spec.right + +end QuasiCompactCover + +noncomputable +def Scheme.Cover.ulift' {P : MorphismProperty Scheme.{u}} + {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] : + Scheme.Cover.{u} (precoverage P) S where + __ := 𝒰.ulift.toPreZeroHypercover.sum (QuasiCompactCover.ulift 𝒰.1) + mem₀ := by + rw [presieve₀_mem_precoverage_iff] + refine ⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩ + induction i <;> exact 𝒰.map_prop _ + +instance (P : MorphismProperty Scheme.{u}) + {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] : + QuasiCompactCover (Scheme.Cover.ulift' 𝒰).1 := + .of_hom (PreZeroHypercover.sumInr _ _) + +instance : Precoverage.Small.{u} (propqcPrecoverage P) where + zeroHypercoverSmall {S} (𝒰 : S.Cover _) := by + refine ⟨𝒰.forgetQc.ulift'.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀, + ⟨?_, ?_⟩⟩ + · rw [Scheme.presieve₀_mem_qcPrecoverage_iff] + exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩ + · rw [Scheme.presieve₀_mem_precoverage_iff] + exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩ + +@[grind .] +lemma propqcPrecoverage_le_precoverage (P : MorphismProperty Scheme.{u}) : + propqcPrecoverage P ≤ precoverage P := + inf_le_right + +lemma mem_propqcPrecoverage_iff_exists_quasiCompactCover {P : MorphismProperty Scheme.{u}} + {S : Scheme.{u}} {R : Presieve S} : + R ∈ propqcPrecoverage P S ↔ ∃ (𝒰 : Scheme.Cover.{u + 1} (precoverage P) S), + QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀ := by + rw [Precoverage.mem_iff_exists_zeroHypercover] + refine ⟨fun ⟨𝒰, h⟩ ↦ ⟨𝒰.weaken <| propqcPrecoverage_le_precoverage P, ?_, h⟩, + fun ⟨𝒰, _, h⟩ ↦ ⟨⟨𝒰.1, ⟨by simpa, 𝒰.mem₀⟩⟩, h⟩⟩ + rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] + exact 𝒰.mem₀.1 + +abbrev propqcTopology (P : MorphismProperty Scheme.{u}) : GrothendieckTopology Scheme.{u} := + (propqcPrecoverage P).toGrothendieck + +lemma Scheme.Hom.singleton_mem_qcPrecoverage {X Y : Scheme.{u}} (f : X ⟶ Y) + [Surjective f] [QuasiCompact f] : + Presieve.singleton f ∈ qcPrecoverage Y := by + let E : Cover.{u} _ _ := f.cover (P := ⊤) trivial + rw [qcPrecoverage, PreZeroHypercoverFamily.mem_precoverage_iff] + refine ⟨(f.cover (P := ⊤) trivial).toPreZeroHypercover, ?_, by simp⟩ + simp only [qcCoverFamily_property, quasiCompactCover_iff] + infer_instance + +attribute [grind .] Scheme.Hom.surjective + +@[simp] +lemma Scheme.Hom.singleton_mem_propqcPrecoverage [P.IsMultiplicative] [P.IsStableUnderBaseChange] + {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) [Surjective f] [QuasiCompact f] : + Presieve.singleton f ∈ propqcPrecoverage P Y := by + refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩ + grind [singleton_mem_precoverage_iff] + +@[simp] +lemma Scheme.Hom.generate_singleton_mem_propqcTopology [P.IsMultiplicative] + [P.IsStableUnderBaseChange] {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : P f) [Surjective f] + [QuasiCompact f] : Sieve.generate (Presieve.singleton f) ∈ propqcTopology P Y := by + apply Precoverage.generate_mem_toGrothendieck + exact f.singleton_mem_propqcPrecoverage hf + +@[simp] +lemma Scheme.Cover.generate_ofArrows_mem_propqcTopology [P.IsMultiplicative] + [P.IsStableUnderBaseChange] {S : Scheme.{u}} (𝒰 : Cover.{u} (precoverage P) S) + [QuasiCompactCover 𝒰.1] : + .generate (.ofArrows 𝒰.X 𝒰.f) ∈ propqcTopology P S := by + apply Precoverage.generate_mem_toGrothendieck + refine ⟨?_, ?_⟩ + · rwa [presieve₀_mem_qcPrecoverage_iff] + · exact 𝒰.mem₀ + +-- This holds more generally if `𝒰.J` is `u`-small, but we don't need that for now. +lemma Scheme.Cover.isSheafFor_sigma_iff {F : Scheme.{u}ᵒᵖ ⥤ Type w} [IsZariskiLocalAtSource P] + (hF : Presieve.IsSheaf Scheme.zariskiTopology F) + {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [Finite 𝒰.I₀] : + Presieve.IsSheafFor F (.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔ + Presieve.IsSheafFor F (.ofArrows 𝒰.X 𝒰.f) := by + have : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F := + preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF + have : PreservesLimitsOfShape (Discrete 𝒰.I₀) F := + preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF + conv_rhs => rw [← Presieve.isSheafFor_sigmaDesc_iff] + congr! + rw [Scheme.Cover.ofArrows_sigma] + +variable (P : MorphismProperty Scheme.{u}) + +lemma zariskiTopology_le_propqcTopology [P.IsMultiplicative] [IsZariskiLocalAtSource P] : + zariskiTopology ≤ propqcTopology P := by + apply Precoverage.toGrothendieck_mono + rw [le_inf_iff] + refine ⟨?_, ?_⟩ + · apply zariskiPrecoverage_le_qcPrecoverage + · rw [precoverage, precoverage] + gcongr + apply MorphismProperty.precoverage_monotone + intro X Y f hf + apply IsZariskiLocalAtSource.of_isOpenImmersion + +open Opposite + +@[simps!] +noncomputable +def Scheme.affineCover' (X : Scheme.{u}) : X.OpenCover := + .mkOfCovers X.affineOpens (fun i ↦ i.1) (fun i ↦ i.1.ι) fun x ↦ by + obtain ⟨U, hU, hx, -⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens + (show x ∈ ⊤ from trivial) + exact ⟨⟨U, hU⟩, ⟨x, hx⟩, rfl⟩ + +variable {P} [P.IsStableUnderBaseChange] + +lemma Scheme.Cover.Hom.isSheafFor {F : Scheme.{u}ᵒᵖ ⥤ Type*} {S : Scheme.{u}} + {𝒰 𝒱 : S.Cover (precoverage P)} + (f : 𝒰 ⟶ 𝒱) + (H₁ : Presieve.IsSheafFor F (.ofArrows _ 𝒰.f)) + (H₂ : ∀ {X : Scheme.{u}} (f : X ⟶ S), + Presieve.IsSeparatedFor F (.ofArrows (𝒰.pullback₂ f).X (𝒰.pullback₂ f).f)) : + Presieve.IsSheafFor F (.ofArrows 𝒱.X 𝒱.f) := by + rw [Presieve.isSheafFor_iff_generate] + apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f)) + · change Sieve.generate _ ≤ Sieve.generate _ + rw [Sieve.generate_le_iff] + rintro - - ⟨i⟩ + rw [← f.w₀] + exact ⟨_, f.h₀ i, 𝒱.f _, ⟨_⟩, rfl⟩ + · rwa [← Presieve.isSheafFor_iff_generate] + · intro Y f hf + rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate] + rw [← Presieve.ofArrows_pullback] + apply H₂ + +instance {S : Scheme.{u}} (𝒰 : S.AffineCover P) (i : 𝒰.I₀) : IsAffine (𝒰.cover.X i) := + inferInstanceAs <| IsAffine (Spec _) + +instance {S : Scheme.{u}} [IsAffine S] (𝒰 : S.AffineCover P) [Finite 𝒰.I₀] : + QuasiCompactCover 𝒰.cover.toPreZeroHypercover := + haveI : Finite 𝒰.cover.I₀ := ‹_› + .of_finite + +/-- A pre-sheaf is a sheaf for the `P`-qc topology if and only if it is a sheaf +for the Zariski topology and satisfies the sheaf property for all single object coverings +`{ f : Spec S ⟶ Spec R }` where `f` satisifies `P`. -/ +@[stacks 022H] +nonrec lemma isSheaf_propqcTopology_iff [P.IsMultiplicative] (F : Scheme.{u}ᵒᵖ ⥤ Type*) + [IsZariskiLocalAtSource P] : + Presieve.IsSheaf (propqcTopology P) F ↔ + Presieve.IsSheaf Scheme.zariskiTopology F ∧ + ∀ {R S : CommRingCat.{u}} (f : R ⟶ S), P (Spec.map f) → Surjective (Spec.map f) → + Presieve.IsSheafFor F (.singleton (Spec.map f)) := by + refine ⟨fun hF ↦ ⟨?_, fun {R S} f hf hs ↦ ?_⟩, fun ⟨hzar, hff⟩ ↦ ?_⟩ + · exact Presieve.isSheaf_of_le _ (zariskiTopology_le_propqcTopology P) hF + · apply hF.isSheafFor + rw [← Hom.presieve₀_cover _ hf] + exact Cover.generate_ofArrows_mem_propqcTopology _ + · rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small.{u}] + intro T (𝒰 : Scheme.Cover _ _) + wlog hT : ∃ (R : CommRingCat.{u}), T = Spec R generalizing T + · let 𝒱 : T.OpenCover := T.affineCover + have h (j : T.affineCover.I₀) : Presieve.IsSheafFor F + (.ofArrows (𝒰.pullback₂ (𝒱.f j)).X (𝒰.pullback₂ (𝒱.f j)).f) := + this _ ⟨_, rfl⟩ + refine .of_isSheafFor_pullback' F (.ofArrows 𝒱.X 𝒱.f) _ ?_ ?_ ?_ ?_ + · exact hzar.isSheafFor _ _ 𝒱.mem_grothendieckTopology + · intro Y f + refine (hzar.isSheafFor _ _ ?_).isSeparatedFor + rw [Sieve.generate_sieve, ← Sieve.pullbackArrows_comm, + ← PreZeroHypercover.presieve₀_pullback₁] + exact Scheme.Cover.mem_grothendieckTopology (𝒱.pullback₂ f) + · rintro - - - - ⟨i⟩ ⟨j⟩ + use .ofArrows (pullback (𝒱.f i) (𝒱.f j)).affineCover.X + (pullback (𝒱.f i) (𝒱.f j)).affineCover.f + refine ⟨(hzar.isSheafFor _ _ <| Cover.mem_grothendieckTopology _).isSeparatedFor, ?_⟩ + · rintro - - ⟨k⟩ + rw [← Sieve.pullbackArrows_comm, ← Presieve.isSeparatedFor_iff_generate] + apply Presieve.IsSheafFor.isSeparatedFor + rw [← Presieve.ofArrows_pullback] + exact this (𝒰.pullback₂ _) ⟨_, rfl⟩ + · rintro - - ⟨i⟩ + rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback, + ← Presieve.isSheafFor_iff_generate] + exact this (𝒰.pullback₂ (𝒱.f i)) ⟨_, rfl⟩ + obtain ⟨R, rfl⟩ := hT + wlog h𝒰 : (∀ i, IsAffine (𝒰.X i)) ∧ Finite 𝒰.I₀ generalizing R 𝒰 + · obtain ⟨𝒱, f, hfin, ho⟩ := QuasiCompactCover.exists_hom 𝒰.forgetQc + have H (V : Scheme.{u}) (f : V ⟶ Spec R) : Presieve.IsSheafFor F + (.ofArrows (𝒱.cover.pullback₂ f).X (𝒱.cover.pullback₂ f).f) := by + let 𝒰V := V.affineCover + refine .of_isSheafFor_pullback' F (.ofArrows 𝒰V.X 𝒰V.f) _ ?_ ?_ ?_ ?_ + · exact hzar.isSheafFor _ _ 𝒰V.mem_grothendieckTopology + · intro Y f + refine (hzar.isSheafFor _ _ ?_).isSeparatedFor + rw [Sieve.generate_sieve, ← Sieve.pullbackArrows_comm, + ← PreZeroHypercover.presieve₀_pullback₁] + exact Scheme.Cover.mem_grothendieckTopology (𝒰V.pullback₂ f) + · rintro - - - - ⟨i⟩ ⟨j⟩ + refine ⟨.ofArrows _ (pullback (𝒰V.f i) (𝒰V.f j)).affineCover.f, ?_, ?_⟩ + · exact hzar.isSheafFor _ _ (Cover.mem_grothendieckTopology _) |>.isSeparatedFor + · rintro - - ⟨k⟩ + rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback, + ← Presieve.isSeparatedFor_iff_generate] + refine (this _ (.ofQuasiCompactCover ((𝒱.cover.pullback₂ f).pullback₂ _) + (qc := by dsimp; infer_instance)) + ⟨fun l ↦ ?_, hfin⟩).isSeparatedFor + exact .of_isIso (pullbackLeftPullbackSndIso (𝒱.f l) f _).hom + · rintro - - ⟨i⟩ + rw [← Sieve.pullbackArrows_comm, ← Presieve.ofArrows_pullback, + ← Presieve.isSheafFor_iff_generate] + let 𝒰' := (𝒱.cover.pullback₂ f).pullback₂ (𝒰V.f i) + refine this _ (.ofQuasiCompactCover 𝒰' (qc := by dsimp [𝒰']; infer_instance)) + ⟨fun j ↦ .of_isIso (pullbackLeftPullbackSndIso (𝒱.f j) f (𝒰V.f i)).hom, hfin⟩ + refine Scheme.Cover.Hom.isSheafFor f ?_ fun f ↦ (H _ f).isSeparatedFor + exact this _ (.ofQuasiCompactCover 𝒱.cover) + ⟨fun i ↦ inferInstanceAs <| IsAffine (Spec _), hfin⟩ + obtain ⟨_, _⟩ := h𝒰 + let 𝒰' := 𝒰.forgetQc.sigma + rw [← Scheme.Cover.forgetQc_toPreZeroHypercover, + ← Scheme.Cover.isSheafFor_sigma_iff hzar, Presieve.ofArrows_of_unique] + have : IsAffine (𝒰.forgetQc.sigma.X default) := by dsimp; infer_instance + let f : Spec _ ⟶ Spec R := (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default + obtain ⟨φ, hφ⟩ := Spec.map_surjective f + rw [isSheafFor_singleton_iff_of_iso _ (Spec.map φ) + (𝒰.forgetQc.sigma.X default).isoSpec (by simp [hφ, f])] + refine hff _ ?_ ?_ + · simpa only [hφ, f] using IsZariskiLocalAtSource.comp (𝒰.forgetQc.sigma.map_prop _) _ + · simp only [hφ, f, Cover.sigma_I₀, PUnit.default_eq_unit, Cover.sigma_X, Cover.sigma_f, f] + have : Surjective (Sigma.desc 𝒰.f) := inferInstanceAs <| Surjective (Sigma.desc 𝒰.forgetQc.f) + infer_instance + +end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean b/Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean index 4f5e5a75cb82e8..7c22d6aa456f9a 100644 --- a/Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean +++ b/Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean @@ -91,6 +91,13 @@ lemma singleton_mem_precoverage_iff {X S : Scheme.{u}} (f : X ⟶ S) : rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ofArrows_mem_precoverage_iff] aesop +lemma bot_mem_precoverage (X : Scheme.{u}) [IsEmpty X] : ⊥ ∈ Scheme.precoverage P X := + ⟨fun x ↦ ‹IsEmpty X›.elim x, P.bot_mem_precoverage _⟩ + +lemma precoverage_mono {P Q : MorphismProperty Scheme.{u}} (h : P ≤ Q) : + precoverage P ≤ precoverage Q := by + grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h] + instance [P.IsStableUnderComposition] : (precoverage P).IsStableUnderComposition := by dsimp only [precoverage]; infer_instance diff --git a/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean b/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean index bb842078095c70..7b5c49fd09a4c0 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean @@ -43,7 +43,7 @@ def pretopology (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange] abbrev grothendieckTopology (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange] [P.IsMultiplicative] : GrothendieckTopology Scheme.{u} := - (pretopology P).toGrothendieck + (precoverage P).toGrothendieck instance : jointlySurjectivePrecoverage.IsStableUnderBaseChange := isStableUnderBaseChange_comap_jointlySurjectivePrecoverage _ @@ -57,9 +57,8 @@ variable {P : MorphismProperty Scheme.{u}} [P.IsStableUnderBaseChange] [P.IsMult @[grind ←] lemma Cover.mem_pretopology {X : Scheme.{u}} {𝒰 : X.Cover (precoverage P)} : - Presieve.ofArrows 𝒰.X 𝒰.f ∈ pretopology P X := by - rw [pretopology, Precoverage.toPretopology_toPrecoverage, ofArrows_mem_precoverage_iff] - exact ⟨fun x ↦ ⟨𝒰.idx x, 𝒰.covers x⟩, 𝒰.map_prop⟩ + Presieve.ofArrows 𝒰.X 𝒰.f ∈ pretopology P X := + 𝒰.mem₀ lemma mem_pretopology_iff {X : Scheme.{u}} {R : Presieve X} : R ∈ pretopology P X ↔ ∃ (𝒰 : Cover.{u + 1} (precoverage P) X), @@ -71,20 +70,22 @@ alias ⟨exists_cover_of_mem_pretopology, _⟩ := mem_pretopology_iff lemma mem_grothendieckTopology_iff {X : Scheme.{u}} {S : Sieve X} : S ∈ grothendieckTopology P X ↔ ∃ (𝒰 : Cover.{u} (precoverage P) X), Presieve.ofArrows 𝒰.X 𝒰.f ≤ S := by - simp_rw [grothendieckTopology, Pretopology.mem_toGrothendieck] + simp_rw [grothendieckTopology, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] refine ⟨fun ⟨R, hR, hle⟩ ↦ ?_, fun ⟨𝒰, hle⟩ ↦ ⟨.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology, hle⟩⟩ - rw [mem_pretopology_iff] at hR - obtain ⟨𝒰, rfl⟩ := hR + rw [Precoverage.mem_iff_exists_zeroHypercover] at hR + obtain ⟨(𝒰 : Scheme.Cover _ _), rfl⟩ := hR use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle alias ⟨exists_cover_of_mem_grothendieckTopology, _⟩ := mem_grothendieckTopology_iff @[grind ←] -lemma Cover.mem_grothendieckTopology {X : Scheme.{u}} {𝒰 : X.Cover (precoverage P)} : - Sieve.ofArrows 𝒰.X 𝒰.f ∈ grothendieckTopology P X := by - rw [Pretopology.mem_toGrothendieck] - use Presieve.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology - exact Sieve.le_generate (Presieve.ofArrows 𝒰.X 𝒰.f) +lemma Cover.mem_grothendieckTopology {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) : + Sieve.ofArrows 𝒰.X 𝒰.f ∈ grothendieckTopology P X := + Precoverage.generate_mem_toGrothendieck 𝒰.mem₀ + +lemma bot_mem_grothendieckTopology (X : Scheme.{u}) [IsEmpty X] : ⊥ ∈ grothendieckTopology P X := by + rw [← Sieve.generate_bot] + exact Precoverage.generate_mem_toGrothendieck (bot_mem_precoverage _ X) @[deprecated (since := "2025-08-28")] alias pretopology_cover := Cover.mem_pretopology @@ -133,7 +134,8 @@ the pretopology defined by `P`. -/ lemma grothendieckTopology_eq_inf : grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck := by - rw [grothendieckTopology, pretopology_eq_inf] + rw [grothendieckTopology, ← Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck] + rfl end @@ -141,19 +143,15 @@ section variable {Q : MorphismProperty Scheme.{u}} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] -lemma pretopology_monotone (hPQ : P ≤ Q) : pretopology P ≤ pretopology Q := by - rintro X R hR - obtain ⟨𝒰, rfl⟩ := exists_cover_of_mem_pretopology hR - rw [mem_pretopology_iff] - use 𝒰.changeProp (fun j ↦ hPQ _ (𝒰.map_prop j)) - rfl +lemma pretopology_monotone (hPQ : P ≤ Q) : pretopology P ≤ pretopology Q := + precoverage_mono hPQ @[deprecated (since := "2025-09-22")] alias pretopology_le_pretopology := pretopology_monotone lemma grothendieckTopology_monotone (hPQ : P ≤ Q) : grothendieckTopology P ≤ grothendieckTopology Q := - (Pretopology.gi Scheme.{u}).gc.monotone_l (pretopology_monotone hPQ) + Precoverage.toGrothendieck_mono (precoverage_mono hPQ) @[deprecated (since := "2025-09-22")] alias grothendieckTopology_le_grothendieckTopology := grothendieckTopology_monotone diff --git a/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean index 07d8c367370d79..e95a725f1ca011 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean @@ -6,7 +6,7 @@ Authors: Bhavik Mehta, Christian Merten module public import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts -public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback +public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic public import Mathlib.CategoryTheory.Limits.Shapes.Products public import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial @@ -133,6 +133,15 @@ noncomputable def ofCoproductDisjointOfCommSq [HasStrictInitialObjects C] end IsInitial +lemma CoproductDisjoint.isPullback_of_isInitial {c : Cofan X} (hc : IsColimit c) + {Y : C} (hY : IsInitial Y) {i j : ι} [HasPullback (c.inj i) (c.inj j)] (hij : i ≠ j) : + IsPullback (hY.to _) (hY.to _) (c.inj i) (c.inj j) := by + refine .of_iso_pullback (by simp) ?_ ?_ ?_ + · refine hY.uniqueUpToIso ?_ + exact IsInitial.ofCoproductDisjointOfIsColimit hij hc + · simp + · simp + end /-- The binary coproduct of `X` and `Y` is disjoint if the coproduct of the family `{X, Y}` is diff --git a/Mathlib/CategoryTheory/Sites/Coverage.lean b/Mathlib/CategoryTheory/Sites/Coverage.lean index 64b801455c4c14..e60a00869265b2 100644 --- a/Mathlib/CategoryTheory/Sites/Coverage.lean +++ b/Mathlib/CategoryTheory/Sites/Coverage.lean @@ -481,6 +481,13 @@ 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] + namespace Presheaf theorem isSheaf_iff_isLimit_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ D) : diff --git a/Mathlib/CategoryTheory/Sites/Grothendieck.lean b/Mathlib/CategoryTheory/Sites/Grothendieck.lean index 64e1af1ff4dce6..7e56a9548eaf68 100644 --- a/Mathlib/CategoryTheory/Sites/Grothendieck.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/MorphismProperty.lean b/Mathlib/CategoryTheory/Sites/MorphismProperty.lean index e63f88eec6b7e7..09cb4bc5d8733a 100644 --- a/Mathlib/CategoryTheory/Sites/MorphismProperty.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean b/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean index 1a9402c5ba57cb..97d8063c3e5cdf 100644 --- a/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 08ff14b8f91cba..3cef251d626715 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -644,6 +644,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 From ad6a461ea527ccb03fead5e8c7e856e05d03bfa9 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 6 Feb 2026 16:24:40 +0100 Subject: [PATCH 2/5] fix? --- Mathlib/AlgebraicGeometry/Sites/Fpqc.lean | 22 ------------------- Mathlib/AlgebraicGeometry/Sites/Small.lean | 3 ++- Mathlib/CategoryTheory/Sites/Pretopology.lean | 4 ++++ Mathlib/CategoryTheory/Sites/Sieves.lean | 20 +++++++++-------- 4 files changed, 17 insertions(+), 32 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean index da1bbd16183e03..8c3f9e9a7d4de0 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean @@ -28,14 +28,6 @@ open Limits variable {C : Type*} [Category C] -lemma Presieve.ofArrows_of_unique {S : C} {ι : Type*} [Unique ι] {X : ι → C} (f : ∀ i, X i ⟶ S) : - ofArrows X f = singleton (f default) := by - refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩ - rw [ofArrows_le_iff] - intro i - obtain rfl : i = default := Subsingleton.elim _ _ - simp - -- TODO: this is almost in mathlib, with slightly less general universe assumptions on `F` -- and with a wrong name lemma Presieve.IsSheafFor.of_isSheafFor_pullback'' (F : Cᵒᵖ ⥤ Type*) {X : C} @@ -195,20 +187,6 @@ lemma isSheafFor_singleton_iff_of_iso rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit, Presieve.isSheafFor_ofArrows_comp_iff] -@[gcongr] -lemma Pretopology.toGrothendieck_mono {C : Type*} [Category C] [HasPullbacks C] - {J K : Pretopology C} (h : J ≤ K) : J.toGrothendieck ≤ K.toGrothendieck := - fun _ _ ⟨R, hR, hle⟩ ↦ ⟨R, h _ hR, hle⟩ - -attribute [grind .] GrothendieckTopology.pullback_stable GrothendieckTopology.transitive - -@[gcongr] -lemma Precoverage.toPretopology_mono {C : Type*} [Category C] [Limits.HasPullbacks C] - {J K : Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] - [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] - (h : J ≤ K) : J.toPretopology ≤ K.toPretopology := - h - variable {C : Type*} [Category C] /-- diff --git a/Mathlib/AlgebraicGeometry/Sites/Small.lean b/Mathlib/AlgebraicGeometry/Sites/Small.lean index 697c45c7a62c64..5e6f6f445b2581 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Small.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Small.lean @@ -117,7 +117,8 @@ lemma overGrothendieckTopology_eq_toGrothendieck_overPretopology : use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩ rwa [Cover.toPresieveOver_le_arrows_iff] · rintro ⟨T, ⟨𝒰, h, rfl⟩, hT⟩ - use Presieve.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology + rw [mem_grothendieckTopology_iff] + use 𝒰 rwa [Cover.toPresieveOver_le_arrows_iff] at hT variable {S} diff --git a/Mathlib/CategoryTheory/Sites/Pretopology.lean b/Mathlib/CategoryTheory/Sites/Pretopology.lean index 9ff54504f61c61..03e36a919b9550 100644 --- a/Mathlib/CategoryTheory/Sites/Pretopology.lean +++ b/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) diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 3cef251d626715..93e425b0065c99 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/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. -/ From f52f5e4066cdf0408ec2e45f449c59597b03fc39 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 6 Feb 2026 16:58:52 +0100 Subject: [PATCH 3/5] cleanup --- Mathlib/AlgebraicGeometry/Sites/Etale.lean | 6 +- Mathlib/AlgebraicGeometry/Sites/Fpqc.lean | 79 +------------------ Mathlib/CategoryTheory/Sites/Coverage.lean | 17 ++++ .../CategoryTheory/Sites/Hypercover/Zero.lean | 23 ++++++ .../Sites/PrecoverageToGrothendieck.lean | 21 +++++ 5 files changed, 67 insertions(+), 79 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Sites/Etale.lean b/Mathlib/AlgebraicGeometry/Sites/Etale.lean index 017b35d30f1bc1..9e3677097b412e 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Etale.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Etale.lean @@ -27,13 +27,17 @@ open CategoryTheory MorphismProperty Limits namespace AlgebraicGeometry.Scheme +/-- Big étale site: the étale precoverage on the category of schemes. -/ +def etalePrecoverage : Precoverage Scheme.{u} := + precoverage @IsEtale + /-- Big étale site: the étale pretopology on the category of schemes. -/ def etalePretopology : Pretopology Scheme.{u} := pretopology @IsEtale /-- Big étale site: the étale topology on the category of schemes. -/ abbrev etaleTopology : GrothendieckTopology Scheme.{u} := - etalePretopology.toGrothendieck + etalePrecoverage.toGrothendieck lemma zariskiTopology_le_etaleTopology : zariskiTopology ≤ etaleTopology := by apply grothendieckTopology_monotone diff --git a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean index 8c3f9e9a7d4de0..e128f3f646efd1 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean @@ -122,73 +122,8 @@ lemma Presieve.IsSheafFor.of_isSheafFor_pullback' (F : Cᵒᵖ ⥤ Type*) {X : C · assumption · assumption -end CategoryTheory - -namespace CategoryTheory - variable {C : Type*} [Category C] {X : C} -@[simps] -def PreZeroHypercover.restrictIndexHom (E : PreZeroHypercover.{w} X) {ι : Type w'} - (f : ι → E.I₀) : - (E.restrictIndex f).Hom E where - s₀ := f - h₀ _ := 𝟙 _ - -@[simp] -lemma PreZeroHypercover.presieve₀_restrictIndex_le {X : C} (E : PreZeroHypercover X) {ι : Type*} - (f : ι → E.I₀) : - (E.restrictIndex f).presieve₀ ≤ E.presieve₀ := by - rw [Presieve.ofArrows_le_iff] - intro i - exact .mk _ - -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 ↦ ?_, fun h X R hR ↦ ?_⟩ - · apply h - exact E.mem₀ - · 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 - -lemma Presieve.isSheafFor_ofArrows_comp_iff {F : Cᵒᵖ ⥤ Type*} {ι : Type*} {Y Z : ι → C} - (g : ∀ i, Z i ⟶ X) - (e : ∀ i, Y i ≅ Z i) : - Presieve.IsSheafFor F (.ofArrows _ (fun i ↦ (e i).hom ≫ g i)) ↔ - Presieve.IsSheafFor F (.ofArrows _ g) := by - have : Sieve.generate (.ofArrows _ g) = - Sieve.generate (.ofArrows _ (fun i ↦ (e i).hom ≫ g i)) := by - refine le_antisymm ?_ ?_ - · rw [Sieve.generate_le_iff] - rintro - - ⟨i⟩ - exact ⟨_, (e i).inv, (e i).hom ≫ g i, ⟨i⟩, by simp⟩ - · rw [Sieve.generate_le_iff] - rintro - - ⟨i⟩ - exact ⟨_, (e i).hom, _, ⟨i⟩, by simp⟩ - rw [Presieve.isSheafFor_iff_generate, ← this, ← Presieve.isSheafFor_iff_generate] - -lemma 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) : - Presieve.IsSheafFor F (.singleton f) ↔ Presieve.IsSheafFor F (.singleton g) := by - subst he - rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ← Presieve.ofArrows_pUnit, - Presieve.isSheafFor_ofArrows_comp_iff] - -variable {C : Type*} [Category C] - /-- If - `F` contravariantly maps (suitable) coproducts to products, @@ -294,10 +229,6 @@ def Scheme.Cover.ofQuasiCompactCover {P : MorphismProperty Scheme.{u}} {S : Sche namespace QuasiCompactCover -def uliftaux {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : - Type u := - Σ (U : S.affineOpens), Fin (exists_isAffineOpen_of_isCompact 𝒰 U.2.isCompact).choose - structure IdxAux {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : Type u where affineOpen : S.affineOpens idx : Fin (exists_isAffineOpen_of_isCompact 𝒰 affineOpen.2.isCompact).choose @@ -430,14 +361,6 @@ lemma zariskiTopology_le_propqcTopology [P.IsMultiplicative] [IsZariskiLocalAtSo open Opposite -@[simps!] -noncomputable -def Scheme.affineCover' (X : Scheme.{u}) : X.OpenCover := - .mkOfCovers X.affineOpens (fun i ↦ i.1) (fun i ↦ i.1.ι) fun x ↦ by - obtain ⟨U, hU, hx, -⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens - (show x ∈ ⊤ from trivial) - exact ⟨⟨U, hU⟩, ⟨x, hx⟩, rfl⟩ - variable {P} [P.IsStableUnderBaseChange] lemma Scheme.Cover.Hom.isSheafFor {F : Scheme.{u}ᵒᵖ ⥤ Type*} {S : Scheme.{u}} @@ -549,7 +472,7 @@ nonrec lemma isSheaf_propqcTopology_iff [P.IsMultiplicative] (F : Scheme.{u}ᵒ have : IsAffine (𝒰.forgetQc.sigma.X default) := by dsimp; infer_instance let f : Spec _ ⟶ Spec R := (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default obtain ⟨φ, hφ⟩ := Spec.map_surjective f - rw [isSheafFor_singleton_iff_of_iso _ (Spec.map φ) + rw [Presieve.isSheafFor_singleton_iff_of_iso _ (Spec.map φ) (𝒰.forgetQc.sigma.X default).isoSpec (by simp [hφ, f])] refine hff _ ?_ ?_ · simpa only [hφ, f] using IsZariskiLocalAtSource.comp (𝒰.forgetQc.sigma.map_prop _) _ diff --git a/Mathlib/CategoryTheory/Sites/Coverage.lean b/Mathlib/CategoryTheory/Sites/Coverage.lean index e60a00869265b2..473d6765ddecd1 100644 --- a/Mathlib/CategoryTheory/Sites/Coverage.lean +++ b/Mathlib/CategoryTheory/Sites/Coverage.lean @@ -488,6 +488,23 @@ lemma Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange 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) : diff --git a/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean b/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean index e83da8ebac74f7..b757b142e69a13 100644 --- a/Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean b/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean index 97d8063c3e5cdf..abfe867740ba6c 100644 --- a/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean +++ b/Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean @@ -223,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 From 98257d6fe3af439dc291f164e9f2962969237dfe Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 6 Feb 2026 17:36:59 +0100 Subject: [PATCH 4/5] more cleanup --- .../AlgebraicGeometry/Cover/QuasiCompact.lean | 25 +++ Mathlib/AlgebraicGeometry/Cover/Sigma.lean | 10 +- Mathlib/AlgebraicGeometry/Sites/Fpqc.lean | 191 +----------------- .../AlgebraicGeometry/Sites/QuasiCompact.lean | 106 ++++++++++ Mathlib/CategoryTheory/Sites/Canonical.lean | 4 +- 5 files changed, 152 insertions(+), 184 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean index ea7c0efb6a1227..ac182f2f1330ed 100644 --- a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean @@ -194,6 +194,31 @@ lemma exists_hom [P.IsMultiplicative] {S : Scheme.{u}} (𝒰 : S.Cover (Scheme.p · infer_instance · infer_instance +/-- +Lift a quasi-compact cover of a `u`-scheme in an arbitrary universe to `u`. The indexing +type is constructed by choosing finitely many compact opens above every affine open. +This cover is again quasi-compact. +-/ +noncomputable def ulift {S : Scheme.{u}} (𝒰 : PreZeroHypercover.{w} S) [QuasiCompactCover 𝒰] : + PreZeroHypercover.{u} S := + 𝒰.restrictIndex + fun i : (Σ U : S.affineOpens, Fin (exists_isAffineOpen_of_isCompact 𝒰 U.2.isCompact).choose) ↦ + (exists_isAffineOpen_of_isCompact 𝒰 i.1.2.isCompact).choose_spec.choose i.2 + +/-- The refinement morphism of the lifted cover. -/ +noncomputable def uliftHom {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + (ulift 𝒰).Hom 𝒰 := + 𝒰.restrictIndexHom _ + +instance {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : + QuasiCompactCover (ulift 𝒰) where + isCompactOpenCovered_of_isAffineOpen {U} hU := + let H := exists_isAffineOpen_of_isCompact 𝒰 hU.isCompact + .of_finite (fun i : Fin H.choose ↦ ⟨⟨U, hU⟩, i⟩) + (fun _ ↦ H.choose_spec.choose_spec.choose _) + (fun _ ↦ H.choose_spec.choose_spec.choose_spec.left _ |>.isCompact) + H.choose_spec.choose_spec.choose_spec.right + end QuasiCompactCover namespace Scheme diff --git a/Mathlib/AlgebraicGeometry/Cover/Sigma.lean b/Mathlib/AlgebraicGeometry/Cover/Sigma.lean index f870ea2caebb76..a72bfd3746d00e 100644 --- a/Mathlib/AlgebraicGeometry/Cover/Sigma.lean +++ b/Mathlib/AlgebraicGeometry/Cover/Sigma.lean @@ -22,7 +22,7 @@ open CategoryTheory Limits namespace AlgebraicGeometry.Scheme.Cover variable {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} [IsZariskiLocalAtSource P] - [UnivLE.{v, u}] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] + [UnivLE.{v, u}] /-- If `𝒰` is a cover of `S`, this is the single object cover where the covering object is the disjoint union. -/ @@ -37,6 +37,14 @@ noncomputable def sigma (𝒰 : Cover.{v} (precoverage P) S) : S.Cover (precover obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq s refine ⟨default, Sigma.ι 𝒰.X i y, by simp [← Scheme.Hom.comp_apply]⟩ +@[simp] +lemma presieve₀_sigma {S : Scheme.{u}} (𝒰 : Cover.{v} (precoverage P) S) : + 𝒰.sigma.presieve₀ = Presieve.singleton (Sigma.desc 𝒰.f) := by + refine le_antisymm ?_ fun T g ⟨⟩ ↦ ⟨⟨⟩⟩ + rw [Presieve.ofArrows_le_iff] + intro i + exact Presieve.singleton_self _ + variable [P.IsMultiplicative] {𝒰 𝒱 : Scheme.Cover.{v} (precoverage P) S} variable (𝒰) in diff --git a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean index e128f3f646efd1..a3886197868d1a 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Fpqc.lean @@ -3,10 +3,12 @@ Copyright (c) 2025 Christian Merten. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Christian Merten -/ -import Mathlib.AlgebraicGeometry.Sites.BigZariski -import Mathlib.AlgebraicGeometry.Sites.QuasiCompact -import Mathlib.AlgebraicGeometry.Cover.Sigma -import Mathlib.CategoryTheory.Sites.Preserves +module + +public import Mathlib.AlgebraicGeometry.Sites.BigZariski +public import Mathlib.AlgebraicGeometry.Sites.QuasiCompact +public import Mathlib.AlgebraicGeometry.Cover.Sigma +public import Mathlib.CategoryTheory.Sites.Preserves /-! # The quasi-compact topology of a scheme @@ -18,6 +20,8 @@ We show that a presheaf is a sheaf in this topology if and only if it is a sheaf in the Zariski topology and a sheaf on single object `P`-coverings of affine schemes. -/ +@[expose] public section + universe w' w v u open CategoryTheory Limits Opposite @@ -28,40 +32,6 @@ open Limits variable {C : Type*} [Category C] --- TODO: this is almost in mathlib, with slightly less general universe assumptions on `F` --- and with a wrong name -lemma Presieve.IsSheafFor.of_isSheafFor_pullback'' (F : Cᵒᵖ ⥤ Type*) {X : C} - (S T : Sieve X) - (hF : Presieve.IsSheafFor F S.arrows) - (hF' : ∀ {Y : C} (f : Y ⟶ X), Presieve.IsSeparatedFor F (S.pullback f).arrows) - (H : ∀ {Y : C} (f : Y ⟶ X), S f → Presieve.IsSheafFor F (T.pullback f).arrows) : - Presieve.IsSheafFor F T.arrows := by - intro t ht - have ⦃Y : C⦄ (f : Y ⟶ X) (hf : S f) := H f hf (t.pullback f) (ht.pullback f) - choose s hs huniq using this - have hr : FamilyOfElements.Compatible s := by - rw [Presieve.compatible_iff_sieveCompatible] - intro Y Z f g hf - refine (H (g ≫ f) (by simp [hf])).isSeparatedFor.ext fun U o ho ↦ ?_ - simp only [Sieve.pullback_apply] at ho - dsimp only [FamilyOfElements.IsAmalgamation, FamilyOfElements.pullback] at hs - rw [← FunctorToTypes.map_comp_apply, ← op_comp, hs _ _ _ ho, hs _ _ _ (by simpa)] - congr 1 - simp - obtain ⟨t', ht', hunique⟩ := hF s hr - refine ⟨t', fun Y f hf ↦ (hF' f).ext fun Z g hg ↦ ?_, fun y hy ↦ ?_⟩ - · rw [← FunctorToTypes.map_comp_apply, ← op_comp, ht' (g ≫ f) hg, ← t.comp_of_compatible _ ht] - have := hs (g ≫ f) hg (𝟙 _) - dsimp only [Presieve.FamilyOfElements.IsAmalgamation, - Presieve.FamilyOfElements.pullback] at this - simp only [Sieve.pullback_apply, Category.id_comp, op_id, FunctorToTypes.map_id_apply] at this - rw [this] - · congr 1 - simp - · simp [hf] - · refine hunique _ fun Y f hf ↦ huniq _ _ _ fun Z g hg ↦ ?_ - simp [Presieve.FamilyOfElements.pullback, ← hy _ hg] - lemma Presieve.IsSheafFor.of_isSheafFor_pullback (F : Cᵒᵖ ⥤ Type*) {X : C} (S : Presieve X) (T : Sieve X) [S.HasPairwisePullbacks] @@ -188,149 +158,8 @@ open Scheme variable {P : MorphismProperty Scheme.{u}} -@[simp] -lemma Scheme.Cover.ofArrows_sigma {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) - [IsZariskiLocalAtSource P] : - Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f = Presieve.singleton (Sigma.desc 𝒰.f) := by - refine le_antisymm ?_ ?_ - · intro T g ⟨i⟩ - exact Presieve.singleton_self _ - · intro T g ⟨⟩ - exact ⟨⟨⟩⟩ - -/-- The `qc`-precoverage of a scheme wrt. to a morphism property `P` is the precoverage -given by quasi compact covers satisfying `P`. -/ -abbrev propqcPrecoverage (P : MorphismProperty Scheme.{u}) : Precoverage Scheme.{u} := - qcPrecoverage ⊓ Scheme.precoverage P - -instance {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} - (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : QuasiCompactCover 𝒰.toPreZeroHypercover := by - rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] - exact 𝒰.mem₀.1 - -@[simps toPreZeroHypercover] -abbrev Scheme.Cover.forgetQc {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} - (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : - S.Cover (precoverage P) where - __ := 𝒰.toPreZeroHypercover - mem₀ := 𝒰.mem₀.2 - -instance {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} - (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : - QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover := by - dsimp; infer_instance - -@[simps toPreZeroHypercover] -def Scheme.Cover.ofQuasiCompactCover {P : MorphismProperty Scheme.{u}} {S : Scheme.{u}} - (𝒰 : Scheme.Cover (precoverage P) S) [qc : QuasiCompactCover 𝒰.1] : - Scheme.Cover (propqcPrecoverage P) S where - __ := 𝒰.toPreZeroHypercover - mem₀ := ⟨Scheme.presieve₀_mem_qcPrecoverage_iff.mpr ‹_›, 𝒰.mem₀⟩ - -namespace QuasiCompactCover - -structure IdxAux {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : Type u where - affineOpen : S.affineOpens - idx : Fin (exists_isAffineOpen_of_isCompact 𝒰 affineOpen.2.isCompact).choose - -noncomputable def ulift {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : - PreZeroHypercover.{u} S := - 𝒰.restrictIndex fun i : IdxAux 𝒰 ↦ - (exists_isAffineOpen_of_isCompact 𝒰 i.affineOpen.2.isCompact).choose_spec.choose i.idx - -noncomputable -def uliftHom {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : - (ulift 𝒰).Hom 𝒰 := - 𝒰.restrictIndexHom _ - -instance {S : Scheme.{u}} (𝒰 : PreZeroHypercover S) [QuasiCompactCover 𝒰] : - QuasiCompactCover (ulift 𝒰) where - isCompactOpenCovered_of_isAffineOpen {U} hU := - let H := exists_isAffineOpen_of_isCompact 𝒰 hU.isCompact - .of_finite (fun i : Fin H.choose ↦ ⟨⟨U, hU⟩, i⟩) - (fun _ ↦ H.choose_spec.choose_spec.choose _) - (fun _ ↦ H.choose_spec.choose_spec.choose_spec.left _ |>.isCompact) - H.choose_spec.choose_spec.choose_spec.right - -end QuasiCompactCover - -noncomputable -def Scheme.Cover.ulift' {P : MorphismProperty Scheme.{u}} - {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] : - Scheme.Cover.{u} (precoverage P) S where - __ := 𝒰.ulift.toPreZeroHypercover.sum (QuasiCompactCover.ulift 𝒰.1) - mem₀ := by - rw [presieve₀_mem_precoverage_iff] - refine ⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩ - induction i <;> exact 𝒰.map_prop _ - -instance (P : MorphismProperty Scheme.{u}) - {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] : - QuasiCompactCover (Scheme.Cover.ulift' 𝒰).1 := - .of_hom (PreZeroHypercover.sumInr _ _) - -instance : Precoverage.Small.{u} (propqcPrecoverage P) where - zeroHypercoverSmall {S} (𝒰 : S.Cover _) := by - refine ⟨𝒰.forgetQc.ulift'.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀, - ⟨?_, ?_⟩⟩ - · rw [Scheme.presieve₀_mem_qcPrecoverage_iff] - exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩ - · rw [Scheme.presieve₀_mem_precoverage_iff] - exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩ - -@[grind .] -lemma propqcPrecoverage_le_precoverage (P : MorphismProperty Scheme.{u}) : - propqcPrecoverage P ≤ precoverage P := - inf_le_right - -lemma mem_propqcPrecoverage_iff_exists_quasiCompactCover {P : MorphismProperty Scheme.{u}} - {S : Scheme.{u}} {R : Presieve S} : - R ∈ propqcPrecoverage P S ↔ ∃ (𝒰 : Scheme.Cover.{u + 1} (precoverage P) S), - QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀ := by - rw [Precoverage.mem_iff_exists_zeroHypercover] - refine ⟨fun ⟨𝒰, h⟩ ↦ ⟨𝒰.weaken <| propqcPrecoverage_le_precoverage P, ?_, h⟩, - fun ⟨𝒰, _, h⟩ ↦ ⟨⟨𝒰.1, ⟨by simpa, 𝒰.mem₀⟩⟩, h⟩⟩ - rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] - exact 𝒰.mem₀.1 - -abbrev propqcTopology (P : MorphismProperty Scheme.{u}) : GrothendieckTopology Scheme.{u} := - (propqcPrecoverage P).toGrothendieck - -lemma Scheme.Hom.singleton_mem_qcPrecoverage {X Y : Scheme.{u}} (f : X ⟶ Y) - [Surjective f] [QuasiCompact f] : - Presieve.singleton f ∈ qcPrecoverage Y := by - let E : Cover.{u} _ _ := f.cover (P := ⊤) trivial - rw [qcPrecoverage, PreZeroHypercoverFamily.mem_precoverage_iff] - refine ⟨(f.cover (P := ⊤) trivial).toPreZeroHypercover, ?_, by simp⟩ - simp only [qcCoverFamily_property, quasiCompactCover_iff] - infer_instance - attribute [grind .] Scheme.Hom.surjective -@[simp] -lemma Scheme.Hom.singleton_mem_propqcPrecoverage [P.IsMultiplicative] [P.IsStableUnderBaseChange] - {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) [Surjective f] [QuasiCompact f] : - Presieve.singleton f ∈ propqcPrecoverage P Y := by - refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩ - grind [singleton_mem_precoverage_iff] - -@[simp] -lemma Scheme.Hom.generate_singleton_mem_propqcTopology [P.IsMultiplicative] - [P.IsStableUnderBaseChange] {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : P f) [Surjective f] - [QuasiCompact f] : Sieve.generate (Presieve.singleton f) ∈ propqcTopology P Y := by - apply Precoverage.generate_mem_toGrothendieck - exact f.singleton_mem_propqcPrecoverage hf - -@[simp] -lemma Scheme.Cover.generate_ofArrows_mem_propqcTopology [P.IsMultiplicative] - [P.IsStableUnderBaseChange] {S : Scheme.{u}} (𝒰 : Cover.{u} (precoverage P) S) - [QuasiCompactCover 𝒰.1] : - .generate (.ofArrows 𝒰.X 𝒰.f) ∈ propqcTopology P S := by - apply Precoverage.generate_mem_toGrothendieck - refine ⟨?_, ?_⟩ - · rwa [presieve₀_mem_qcPrecoverage_iff] - · exact 𝒰.mem₀ - -- This holds more generally if `𝒰.J` is `u`-small, but we don't need that for now. lemma Scheme.Cover.isSheafFor_sigma_iff {F : Scheme.{u}ᵒᵖ ⥤ Type w} [IsZariskiLocalAtSource P] (hF : Presieve.IsSheaf Scheme.zariskiTopology F) @@ -343,7 +172,7 @@ lemma Scheme.Cover.isSheafFor_sigma_iff {F : Scheme.{u}ᵒᵖ ⥤ Type w} [IsZar preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology hF conv_rhs => rw [← Presieve.isSheafFor_sigmaDesc_iff] congr! - rw [Scheme.Cover.ofArrows_sigma] + rw [← PreZeroHypercover.presieve₀, 𝒰.presieve₀_sigma] variable (P : MorphismProperty Scheme.{u}) @@ -405,7 +234,7 @@ nonrec lemma isSheaf_propqcTopology_iff [P.IsMultiplicative] (F : Scheme.{u}ᵒ · exact Presieve.isSheaf_of_le _ (zariskiTopology_le_propqcTopology P) hF · apply hF.isSheafFor rw [← Hom.presieve₀_cover _ hf] - exact Cover.generate_ofArrows_mem_propqcTopology _ + exact Cover.mem_propqcTopology _ · rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small.{u}] intro T (𝒰 : Scheme.Cover _ _) wlog hT : ∃ (R : CommRingCat.{u}), T = Spec R generalizing T diff --git a/Mathlib/AlgebraicGeometry/Sites/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Sites/QuasiCompact.lean index d33841c5ef3b9d..f5819db8dcb4f0 100644 --- a/Mathlib/AlgebraicGeometry/Sites/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Sites/QuasiCompact.lean @@ -90,4 +90,110 @@ lemma zariskiPrecoverage_le_qcPrecoverage : zariskiPrecoverage ≤ qcPrecoverage := precoverage_le_qcPrecoverage_of_isOpenMap fun _ _ f _ ↦ f.isOpenEmbedding.isOpenMap +lemma Hom.singleton_mem_qcPrecoverage {X Y : Scheme.{u}} (f : X ⟶ Y) [Surjective f] + [QuasiCompact f] : Presieve.singleton f ∈ qcPrecoverage Y := by + let E : Cover.{u} _ _ := f.cover (P := ⊤) trivial + rw [qcPrecoverage, PreZeroHypercoverFamily.mem_precoverage_iff] + refine ⟨(f.cover (P := ⊤) trivial).toPreZeroHypercover, ?_, by simp⟩ + simp only [qcCoverFamily_property, quasiCompactCover_iff] + infer_instance + +attribute [grind .] Scheme.Hom.surjective + +section Property + +variable {P : MorphismProperty Scheme.{u}} + +/-- The `qc`-precoverage of a scheme wrt. to a morphism property `P` is the precoverage +given by quasi-compact covers satisfying `P`. -/ +abbrev propqcPrecoverage (P : MorphismProperty Scheme.{u}) : Precoverage Scheme.{u} := + qcPrecoverage ⊓ Scheme.precoverage P + +@[grind .] +lemma propqcPrecoverage_le_precoverage : propqcPrecoverage P ≤ precoverage P := + inf_le_right + +instance {S : Scheme.{u}} (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : + QuasiCompactCover 𝒰.toPreZeroHypercover := by + rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] + exact 𝒰.mem₀.1 + +/-- Forget being quasi-compact. -/ +@[simps toPreZeroHypercover] +abbrev Cover.forgetQc {S : Scheme.{u}} (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : + S.Cover (precoverage P) where + __ := 𝒰.toPreZeroHypercover + mem₀ := 𝒰.mem₀.2 + +instance {S : Scheme.{u}} (𝒰 : Scheme.Cover (propqcPrecoverage P) S) : + QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover := by + dsimp; infer_instance + +/-- Construct a cover in the `P`-qc topology from a quasi-compact cover in the `P`-topology. -/ +@[simps toPreZeroHypercover] +def Cover.ofQuasiCompactCover {S : Scheme.{u}} (𝒰 : Scheme.Cover (precoverage P) S) + [qc : QuasiCompactCover 𝒰.1] : + Scheme.Cover (propqcPrecoverage P) S where + __ := 𝒰.toPreZeroHypercover + mem₀ := ⟨Scheme.presieve₀_mem_qcPrecoverage_iff.mpr ‹_›, 𝒰.mem₀⟩ + +/-- Lift a quasi-compact `P`-cover of a `u`-scheme in an arbitrary universe to universe `u`. +This is again quasi-compact. -/ +noncomputable def Cover.qculift {S : Scheme.{u}} (𝒰 : Cover.{w} (precoverage P) S) + [QuasiCompactCover 𝒰.1] : Scheme.Cover.{u} (precoverage P) S where + __ := 𝒰.ulift.toPreZeroHypercover.sum (QuasiCompactCover.ulift 𝒰.1) + mem₀ := by + rw [presieve₀_mem_precoverage_iff] + refine ⟨fun x ↦ ⟨.inl x, 𝒰.covers _⟩, fun i ↦ ?_⟩ + induction i <;> exact 𝒰.map_prop _ + +instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] : + QuasiCompactCover (Scheme.Cover.qculift 𝒰).1 := + .of_hom (PreZeroHypercover.sumInr _ _) + +instance : Precoverage.Small.{u} (propqcPrecoverage P) where + zeroHypercoverSmall {S} (𝒰 : S.Cover _) := by + refine ⟨𝒰.forgetQc.qculift.I₀, Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom _).s₀, + ⟨?_, ?_⟩⟩ + · rw [Scheme.presieve₀_mem_qcPrecoverage_iff] + exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩ + · rw [Scheme.presieve₀_mem_precoverage_iff] + exact ⟨fun x ↦ ⟨Sum.inl x, 𝒰.forgetQc.covers _⟩, fun i ↦ 𝒰.forgetQc.map_prop _⟩ + +lemma mem_propqcPrecoverage_iff_exists_quasiCompactCover {S : Scheme.{u}} {R : Presieve S} : + R ∈ propqcPrecoverage P S ↔ ∃ (𝒰 : Scheme.Cover.{u + 1} (precoverage P) S), + QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀ := by + rw [Precoverage.mem_iff_exists_zeroHypercover] + refine ⟨fun ⟨𝒰, h⟩ ↦ ⟨𝒰.weaken propqcPrecoverage_le_precoverage, ?_, h⟩, + fun ⟨𝒰, _, h⟩ ↦ ⟨⟨𝒰.1, ⟨by simpa, 𝒰.mem₀⟩⟩, h⟩⟩ + rw [← Scheme.presieve₀_mem_qcPrecoverage_iff] + exact 𝒰.mem₀.1 + +@[simp] +lemma Hom.singleton_mem_propqcPrecoverage {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) [Surjective f] + [QuasiCompact f] : Presieve.singleton f ∈ propqcPrecoverage P Y := by + refine ⟨f.singleton_mem_qcPrecoverage, ?_⟩ + grind [singleton_mem_precoverage_iff] + +/-- The `P`-`qc`-topology on the category of schemes wrt. to a morphism property `P` is the +topology generated by quasi-compact covers satisfying `P`. -/ +abbrev propqcTopology (P : MorphismProperty Scheme.{u}) : GrothendieckTopology Scheme.{u} := + (propqcPrecoverage P).toGrothendieck + +@[simp] +lemma Hom.generate_singleton_mem_propqcTopology {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : P f) + [Surjective f] [QuasiCompact f] : + .generate (.singleton f) ∈ propqcTopology P Y := by + apply Precoverage.generate_mem_toGrothendieck + exact f.singleton_mem_propqcPrecoverage hf + +@[simp, grind .] +lemma Cover.mem_propqcTopology {S : Scheme.{u}} (𝒰 : Cover.{u} (precoverage P) S) + [QuasiCompactCover 𝒰.1] : + .ofArrows 𝒰.X 𝒰.f ∈ propqcTopology P S := by + refine Precoverage.generate_mem_toGrothendieck ⟨?_, 𝒰.mem₀⟩ + rwa [presieve₀_mem_qcPrecoverage_iff] + +end Property + end AlgebraicGeometry.Scheme diff --git a/Mathlib/CategoryTheory/Sites/Canonical.lean b/Mathlib/CategoryTheory/Sites/Canonical.lean index 281fedb98df38c..3ad1355cb3ace8 100644 --- a/Mathlib/CategoryTheory/Sites/Canonical.lean +++ b/Mathlib/CategoryTheory/Sites/Canonical.lean @@ -58,7 +58,7 @@ This is mostly an auxiliary lemma to show `isSheafFor_trans`. Adapted from [Elephant], Lemma C2.1.7(i) with suggestions as mentioned in https://math.stackexchange.com/a/358709/ -/ -theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type v) (U : Sieve X) (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y) +theorem isSheafFor_bind (P : Cᵒᵖ ⥤ Type*) (U : Sieve X) (B : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, U f → Sieve Y) (hU : Presieve.IsSheafFor P (U : Presieve X)) (hB : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.IsSheafFor P (B hf : Presieve Y)) (hB' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (h : U f) ⦃Z⦄ (g : Z ⟶ Y), @@ -113,7 +113,7 @@ This is mostly an auxiliary lemma to construct `finestTopology`. Adapted from [Elephant], Lemma C2.1.7(ii) with suggestions as mentioned in https://math.stackexchange.com/a/358709 -/ -theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X) +theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type*) (R S : Sieve X) (hR : Presieve.IsSheafFor P (R : Presieve X)) (hR' : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : S f), Presieve.IsSeparatedFor P (R.pullback f : Presieve Y)) (hS : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (_ : R f), Presieve.IsSheafFor P (S.pullback f : Presieve Y)) : From 92d5e040c62b971744ac880e5a4b3462d9fe3245 Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Fri, 6 Feb 2026 18:44:26 +0100 Subject: [PATCH 5/5] fix lint --- .../AlgebraicGeometry/Cover/QuasiCompact.lean | 2 +- .../AlgebraicGeometry/Sites/Pretopology.lean | 54 ++++++++++--------- 2 files changed, 30 insertions(+), 26 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean index ac182f2f1330ed..a932b9977afc8a 100644 --- a/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.lean @@ -166,7 +166,7 @@ instance {𝒱 : PreZeroHypercover S} [QuasiCompactCover 𝒰] : QuasiCompactCov instance {𝒱 : PreZeroHypercover S} [QuasiCompactCover 𝒱] : QuasiCompactCover (𝒰.sum 𝒱) := .of_hom (PreZeroHypercover.sumInr _ _) -lemma exists_hom [P.IsMultiplicative] {S : Scheme.{u}} (𝒰 : S.Cover (Scheme.precoverage P)) +lemma exists_hom {S : Scheme.{u}} (𝒰 : S.Cover (Scheme.precoverage P)) [P.RespectsLeft @IsOpenImmersion] [CompactSpace S] [QuasiCompactCover 𝒰.toPreZeroHypercover] : ∃ (𝒱 : Scheme.AffineCover.{w} P S) (f : 𝒱.cover ⟶ 𝒰), Finite 𝒱.I₀ ∧ ∀ j, IsOpenImmersion (f.h₀ j) := by diff --git a/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean b/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean index 7b5c49fd09a4c0..2b4469a95f6234 100644 --- a/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean +++ b/Mathlib/AlgebraicGeometry/Sites/Pretopology.lean @@ -40,8 +40,7 @@ def pretopology (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange] /-- The Grothendieck topology on the category of schemes induced by the pretopology defined by `P`-covers. -/ -abbrev grothendieckTopology (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange] - [P.IsMultiplicative] : +abbrev grothendieckTopology (P : MorphismProperty Scheme.{u}) : GrothendieckTopology Scheme.{u} := (precoverage P).toGrothendieck @@ -53,13 +52,30 @@ instance : jointlySurjectivePrecoverage.IsStableUnderBaseChange := def jointlySurjectivePretopology : Pretopology Scheme.{u} := jointlySurjectivePrecoverage.toPretopology -variable {P : MorphismProperty Scheme.{u}} [P.IsStableUnderBaseChange] [P.IsMultiplicative] +variable {P : MorphismProperty Scheme.{u}} + +@[grind ←] +lemma Cover.mem_grothendieckTopology {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) : + Sieve.ofArrows 𝒰.X 𝒰.f ∈ grothendieckTopology P X := + Precoverage.generate_mem_toGrothendieck 𝒰.mem₀ + +lemma bot_mem_grothendieckTopology (X : Scheme.{u}) [IsEmpty X] : ⊥ ∈ grothendieckTopology P X := by + rw [← Sieve.generate_bot] + exact Precoverage.generate_mem_toGrothendieck (bot_mem_precoverage _ X) + +@[deprecated (since := "2025-08-28")] +alias grothendieckTopology_cover := Cover.mem_grothendieckTopology + +variable [P.IsStableUnderBaseChange] [P.IsMultiplicative] @[grind ←] lemma Cover.mem_pretopology {X : Scheme.{u}} {𝒰 : X.Cover (precoverage P)} : Presieve.ofArrows 𝒰.X 𝒰.f ∈ pretopology P X := 𝒰.mem₀ +@[deprecated (since := "2025-08-28")] +alias pretopology_cover := Cover.mem_pretopology + lemma mem_pretopology_iff {X : Scheme.{u}} {R : Presieve X} : R ∈ pretopology P X ↔ ∃ (𝒰 : Cover.{u + 1} (precoverage P) X), R = Presieve.ofArrows 𝒰.X 𝒰.f := @@ -78,21 +94,6 @@ lemma mem_grothendieckTopology_iff {X : Scheme.{u}} {S : Sieve X} : alias ⟨exists_cover_of_mem_grothendieckTopology, _⟩ := mem_grothendieckTopology_iff -@[grind ←] -lemma Cover.mem_grothendieckTopology {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) : - Sieve.ofArrows 𝒰.X 𝒰.f ∈ grothendieckTopology P X := - Precoverage.generate_mem_toGrothendieck 𝒰.mem₀ - -lemma bot_mem_grothendieckTopology (X : Scheme.{u}) [IsEmpty X] : ⊥ ∈ grothendieckTopology P X := by - rw [← Sieve.generate_bot] - exact Precoverage.generate_mem_toGrothendieck (bot_mem_precoverage _ X) - -@[deprecated (since := "2025-08-28")] -alias pretopology_cover := Cover.mem_pretopology - -@[deprecated (since := "2025-08-28")] -alias grothendieckTopology_cover := Cover.mem_grothendieckTopology - section @[deprecated (since := "2025-08-18")] alias surjectiveFamiliesPretopology := @@ -141,13 +142,7 @@ end section -variable {Q : MorphismProperty Scheme.{u}} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] - -lemma pretopology_monotone (hPQ : P ≤ Q) : pretopology P ≤ pretopology Q := - precoverage_mono hPQ - -@[deprecated (since := "2025-09-22")] -alias pretopology_le_pretopology := pretopology_monotone +variable {P Q : MorphismProperty Scheme.{u}} lemma grothendieckTopology_monotone (hPQ : P ≤ Q) : grothendieckTopology P ≤ grothendieckTopology Q := @@ -156,6 +151,15 @@ lemma grothendieckTopology_monotone (hPQ : P ≤ Q) : @[deprecated (since := "2025-09-22")] alias grothendieckTopology_le_grothendieckTopology := grothendieckTopology_monotone +variable [P.IsMultiplicative] [P.IsStableUnderBaseChange] + [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] + +lemma pretopology_monotone (hPQ : P ≤ Q) : pretopology P ≤ pretopology Q := + precoverage_mono hPQ + +@[deprecated (since := "2025-09-22")] +alias pretopology_le_pretopology := pretopology_monotone + end end AlgebraicGeometry.Scheme