Documentation

Mathlib.AlgebraicGeometry.Sites.Proetale

The pro-étale site #

In this file we define the big and small pro-étale site. The big pro-étale site is the category of schemes equipped with the pro-étale topology, which is the topology generated by fpqc covers of weakly étale morphisms.

We prefer to work with weakly étale morphisms instead of pro-étale morphisms, since the property of being pro-étale is not well-behaved: it is not local on the target.

We also define the small pro-étale site of a scheme S to be the category of schemes weakly-étale over S and equip it with the induced topology.

References #

source
def AlgebraicGeometry.Scheme.proetalePrecoverage :
CategoryTheory.Precoverage Scheme

Big pro-étale site: the pro-étale precoverage on the category of schemes given by fpqc covers of weakly étale morphisms. Definition 4.1.1

Equations
Instances For
    source
    @[implicit_reducible]
    instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeProetalePrecoverage :
    proetalePrecoverage.IsStableUnderBaseChange
    Equations
    source
    @[implicit_reducible]
    instance AlgebraicGeometry.Scheme.instIsStableUnderCompositionProetalePrecoverage :
    proetalePrecoverage.IsStableUnderComposition
    Equations
    source
    @[implicit_reducible]
    instance AlgebraicGeometry.Scheme.instHasIsosProetalePrecoverage :
    proetalePrecoverage.HasIsos
    Equations
    source
    theorem AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale :
    proetalePrecoverage ≤ CategoryTheory.MorphismProperty.precoverage @WeaklyEtale
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.proetaleTopology :
    CategoryTheory.GrothendieckTopology Scheme

    Big pro-étale site: the pro-étale topology on the category of schemes is generated by the pro-étale precoverage.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage :
      etalePrecoverage ≤ proetalePrecoverage
      source
      theorem AlgebraicGeometry.Scheme.etaleTopology_le_proetaleTopology :
      etaleTopology ≤ proetaleTopology
      source
      instance AlgebraicGeometry.Scheme.instWeaklyEtaleF {S : Scheme} (𝒰 : Cover (precoverage @WeaklyEtale) S) (i : 𝒰.I₀) :
      WeaklyEtale (𝒰.f i)
      source
      def AlgebraicGeometry.Scheme.ProEt (S : Scheme) :
      Type (u + 1)

      The (small) pro-étale site of a scheme S: Its objects are the schemes weakly étale over S. We prefer to work with weakly étale morphisms instead of pro-étale morphisms, since the property of being pro-étale is not well-behaved: it is not local on the target. Definition 4.1.1

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Scheme.instCategoryProEt (S : Scheme) :
        CategoryTheory.Category.{u_1, u_1 + 1} S.ProEt
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Scheme.instHasFiniteLimitsProEt (S : Scheme) :
        CategoryTheory.Limits.HasFiniteLimits S.ProEt
        Equations
        • ⋯ = ⋯
        source
        instance AlgebraicGeometry.Scheme.ProEt.instWeaklyEtaleHomDiscretePUnit (S : Scheme) (U : S.ProEt) :
        WeaklyEtale U.hom
        source
        def AlgebraicGeometry.Scheme.ProEt.mk {S X : Scheme} (f : X ⟶ S) [WeaklyEtale f] :
        S.ProEt

        Construct an object of the pro-étale site of S by giving a weakly étale morphism f : X ⟶ S.

        Equations
        Instances For
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.ProEt.mk_right_as {S X : Scheme} (f : X ⟶ S) [WeaklyEtale f] :
          (ProEt.mk f).right.as = PUnit.unit
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.ProEt.mk_hom {S X : Scheme} (f : X ⟶ S) [WeaklyEtale f] :
          (ProEt.mk f).hom = f
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.ProEt.mk_left {S X : Scheme} (f : X ⟶ S) [WeaklyEtale f] :
          (ProEt.mk f).left = X
          source
          def AlgebraicGeometry.Scheme.ProEt.forget (S : Scheme) :
          CategoryTheory.Functor S.ProEt (CategoryTheory.Over S)

          The forgetful functor the pro-étale site of S to schemes over S.

          Equations
          Instances For
            source
            def AlgebraicGeometry.Scheme.ProEt.forgetFullyFaithful (S : Scheme) :
            (ProEt.forget S).FullyFaithful

            The forgetful functor from the pro-étale site of S to schemes over S is fully faithful.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance AlgebraicGeometry.Scheme.ProEt.instFullOverForget (S : Scheme) :
              (ProEt.forget S).Full
              source
              instance AlgebraicGeometry.Scheme.ProEt.instFaithfulOverForget (S : Scheme) :
              (ProEt.forget S).Faithful
              source
              instance AlgebraicGeometry.Scheme.ProEt.instPreservesFiniteLimitsOverForget (S : Scheme) :
              CategoryTheory.Limits.PreservesFiniteLimits (ProEt.forget S)
              source
              instance AlgebraicGeometry.Scheme.ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology (S : Scheme) :
              (ProEt.forget S).LocallyCoverDense (proetaleTopology.over S)
              source
              def AlgebraicGeometry.Scheme.ProEt.precoverage (S : Scheme) :
              CategoryTheory.Precoverage S.ProEt

              The pro-étale precoverage on the small pro-étale site.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                abbrev AlgebraicGeometry.Scheme.ProEt.topology (S : Scheme) :
                CategoryTheory.GrothendieckTopology S.ProEt

                The pro-étale topology on the small pro-étale site.

                Equations
                Instances For
                  source
                  theorem AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology (S : Scheme) :
                  topology S = (ProEt.forget S).inducedTopology (proetaleTopology.over S)