feat(AlgebraicGeometry): Zariski sheaves preserve products

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

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