# 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.

The Zariski pretopology on the category of schemes.

## Equations

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

## Instances For

@[reducible, inline]

The Zariski topology on the category of schemes.

## Equations

## Instances For

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))