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