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.etalePrecoverage :
CategoryTheory.Precoverage Scheme

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

Equations
Instances For
    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
            source
            instance AlgebraicGeometry.Scheme.instEtaleF {S : Scheme} (𝒰 : Cover (precoverage @Etale) S) (i : 𝒰.I₀) :
            Etale (𝒰.f i)
            source
            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).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For