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 AlgebraicGeometry.Scheme

The Zariski pretopology on the category of schemes.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.zariskiTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme

The Zariski topology on the category of schemes.

Equations

• AlgebraicGeometry.Scheme.zariskiTopology = CategoryTheory.Pretopology.toGrothendieck AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.zariskiPretopology

theorem AlgebraicGeometry.Scheme.zariskiPretopology_openCover {Y : AlgebraicGeometry.Scheme} (U : Y.OpenCover) : AlgebraicGeometry.Scheme.zariskiPretopology.coverings Y (CategoryTheory.Presieve.ofArrows U.obj U.map)

theorem AlgebraicGeometry.Scheme.zariskiTopology_openCover {Y : AlgebraicGeometry.Scheme} (U : Y.OpenCover) : AlgebraicGeometry.Scheme.zariskiTopology Y (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows U.obj U.map))

instance AlgebraicGeometry.Scheme.subcanonical_zariskiTopology : AlgebraicGeometry.Scheme.zariskiTopology.Subcanonical

Equations

• AlgebraicGeometry.Scheme.subcanonical_zariskiTopology = ⋯