feat(AlgebraicGeometry/Sites): characterization of sheaves for the P-qc topology

Mathlib.lean

@@ -1359,6 +1359,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

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

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

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
 
@@ -71,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