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.

def AlgebraicGeometry.Scheme.etalePrecoverage : CategoryTheory.Precoverage Scheme

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

def AlgebraicGeometry.Scheme.etalePretopology : CategoryTheory.Pretopology Scheme

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

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.etaleTopology : CategoryTheory.GrothendieckTopology Scheme

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

theorem AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology : zariskiTopology ≤ etaleTopology

def AlgebraicGeometry.Scheme.smallEtaleTopology (X : Scheme) : CategoryTheory.GrothendieckTopology X.Etale

The small étale site of a scheme is the Grothendieck topology on the category of schemes étale over X induced from the étale topology on Scheme.{u}.

def AlgebraicGeometry.Scheme.smallEtalePretopology (X : Scheme) : CategoryTheory.Pretopology X.Etale

The pretopology generating the small étale site.

instance AlgebraicGeometry.Scheme.instEtaleF {S : Scheme} (𝒰 : Cover (precoverage @Etale) S) (i : 𝒰.I₀) : Etale (𝒰.f i)

noncomputable def AlgebraicGeometry.Scheme.geometricFiber (Ω : Type u) [Field Ω] [IsSepClosed Ω] : etaleTopology.Point

A separably closed field Ω defines a point on the étale topology by the fiber functor X ↦ Hom(Spec Ω, X).