The étale site

In this file we define the big étale site, i.e. the étale topology as a Grothendieck topology on the category of schemes.

TODO:

• define the small étale site

def AlgebraicGeometry.Scheme.etalePretopology : CategoryTheory.Pretopology AlgebraicGeometry.Scheme

Big étale site: the étale pretopology on the category of schemes.

Equations

• AlgebraicGeometry.Scheme.etalePretopology = AlgebraicGeometry.Scheme.pretopology @AlgebraicGeometry.IsEtale

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.etaleTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme

Big étale site: the étale topology on the category of schemes.

Equations

• AlgebraicGeometry.Scheme.etaleTopology = CategoryTheory.Pretopology.toGrothendieck AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.etalePretopology

theorem AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology : AlgebraicGeometry.Scheme.zariskiTopology ≤ AlgebraicGeometry.Scheme.etaleTopology