Documentation

Mathlib.AlgebraicGeometry.Sites.BigZariski

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:

The Zariski pretopology on the category of schemes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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))