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 ofYtoOver Y, and show that a presheaf onOver Yis a sheaf for the Zariski topology iff its "restriction" to the topological spaceZis a sheaf for allZ : Over Y. - We should have good notions of (pre)sheaves of
Type (u + 1)(e.g. associated sheaf functor, pushforward, pullbacks) onScheme.{u}for this topology. However, some constructions in theCategoryTheory.Sitesfolder 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
Instances For
@[reducible, inline]
The Zariski topology on the category of schemes.