The big Zariski site of schemes

In this file, we define the Zariski topology, as a Grothendieck topology on the category Scheme.{u}: this is Scheme.zariskiTopology.{u}. If X : Scheme.{u}, the Zariski topology on Over X can be obtained as Scheme.zariskiTopology.over X (see CategoryTheory.Sites.Over.).

TODO:

• If Y : Scheme.{u}, define a continuous functor from the category of opens of Y to Over Y, and show that a presheaf on Over Y is a sheaf for the Zariski topology iff its "restriction" to the topological space Z is a sheaf for all Z : Over Y.
• We should have good notions of (pre)sheaves of Type (u + 1) (e.g. associated sheaf functor, pushforward, pullbacks) on Scheme.{u} for this topology. However, some constructions in the CategoryTheory.Sites folder currently assume that the site is a small category: this should be generalized. As a result, this big Zariski site can considered as a test case of the Grothendieck topology API for future applications to étale cohomology.

def AlgebraicGeometry.Scheme.zariskiPretopology : CategoryTheory.Pretopology Scheme

The Zariski pretopology on the category of schemes.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.zariskiTopology : CategoryTheory.GrothendieckTopology Scheme

The Zariski topology on the category of schemes.

theorem AlgebraicGeometry.Scheme.zariskiTopology_eq : zariskiTopology = zariskiPretopology.toGrothendieck

instance AlgebraicGeometry.Scheme.subcanonical_zariskiTopology : zariskiTopology.Subcanonical

instance AlgebraicGeometry.Scheme.instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology : forgetToTop.IsContinuous zariskiTopology TopCat.grothendieckTopology

noncomputable def AlgebraicGeometry.Scheme.affineOneHypercover (X : Scheme) : zariskiTopology.OneHypercover X

A Zariski-1-hypercover of a scheme where all components are affine.

@[simp]

theorem AlgebraicGeometry.Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover (X : Scheme) : X.affineOneHypercover.toPreZeroHypercover = X.affineCover.toPreZeroHypercover

theorem AlgebraicGeometry.preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology {F : CategoryTheory.Functor Schemeᵒᵖ (Type v)} {ι : Type u_1} [Small.{u, u_1} ι] [Small.{v, u_1} ι] (hF : CategoryTheory.Presieve.IsSheaf Scheme.zariskiTopology F) : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ι) F

Zariski sheaves preserve products.

theorem AlgebraicGeometry.ofArrows_ι_mem_zariskiTopology_of_isColimit {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Sieve.ofArrows F.obj c.ι.app ∈ Scheme.zariskiTopology c.pt

Let F be a locally directed diagram of open immersions, i.e., a diagram of schemes for which whenever xᵢ ∈ Fᵢ and xⱼ ∈ Fⱼ map to the same xₖ ∈ Fₖ, there exists some xₗ ∈ Fₗ that maps to xᵢ and xⱼ (e.g, the diagram indexing a coproduct). Then the colimit inclusions are a Zariski covering.

theorem AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff {P : CategoryTheory.MorphismProperty Scheme} {F : CategoryTheory.Functor Schemeᵒᵖ (Type u_1)} [IsZariskiLocalAtSource P] (hF : CategoryTheory.Presieve.IsSheaf zariskiTopology F) {S : Scheme} (𝒰 : Cover (precoverage P) S) [Finite 𝒰.I₀] : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔ CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)