Documentation

Mathlib.AlgebraicGeometry.Sites.Etale

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.

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

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.etaleTopology :
    CategoryTheory.GrothendieckTopology Scheme

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

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology :
      zariskiTopology ≤ etaleTopology
      source
      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}.

      Equations
      Instances For
        source
        def AlgebraicGeometry.Scheme.smallEtalePretopology (X : Scheme) :
        CategoryTheory.Pretopology X.Etale

        The pretopology generating the small étale site.

        Equations
        Instances For