Documentation

Mathlib.AlgebraicGeometry.Morphisms.Etale

Etale morphisms #

A morphism of schemes f : X ⟶ Y is étale if it is smooth of relative dimension zero. We also define the category of schemes étale over X.

source
@[reducible, inline]
abbrev AlgebraicGeometry.IsEtale {X Y : Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes is étale if it is smooth of relative dimension zero.

Equations
Instances For
    source
    instance AlgebraicGeometry.IsEtale.instIsSmooth {X Y : Scheme} (f : X ⟶ Y) [IsEtale f] :
    IsSmooth f
    source
    instance AlgebraicGeometry.IsEtale.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsEtale
    source
    @[instance 900]
    instance AlgebraicGeometry.IsEtale.instFormallyUnramified {X Y : Scheme} (f : X ⟶ Y) [IsEtale f] :
    FormallyUnramified f
    source
    instance AlgebraicGeometry.IsEtale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified :
    CategoryTheory.MorphismProperty.HasOfPostcompProperty (@IsEtale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)
    source
    theorem AlgebraicGeometry.IsEtale.of_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [IsEtale (CategoryTheory.CategoryStruct.comp f g)] [LocallyOfFiniteType g] [FormallyUnramified g] :
    IsEtale f

    If f ≫ g is etale and g unramified, then f is étale.

    source
    instance AlgebraicGeometry.IsEtale.instHasOfPostcompPropertyScheme :
    CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsEtale @IsEtale
    source
    def AlgebraicGeometry.Scheme.Etale (X : Scheme) :
    Type (u + 1)

    The category Etale X is the category of schemes étale over X.

    Equations
    Instances For
      source
      instance AlgebraicGeometry.Scheme.instCategoryEtale (X : Scheme) :
      CategoryTheory.Category.{u, u + 1} X.Etale
      Equations
      source
      def AlgebraicGeometry.Scheme.Etale.forget (X : Scheme) :
      CategoryTheory.Functor X.Etale (CategoryTheory.Over X)

      The forgetful functor from schemes étale over X to schemes over X.

      Equations
      Instances For
        source
        def AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful (X : Scheme) :
        (forget X).FullyFaithful

        The forgetful functor from schemes étale over X to schemes over X is fully faithful.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance AlgebraicGeometry.Scheme.instFullEtaleOverForget (X : Scheme) :
          (Etale.forget X).Full
          source
          instance AlgebraicGeometry.Scheme.instFaithfulEtaleOverForget (X : Scheme) :
          (Etale.forget X).Faithful
          source
          instance AlgebraicGeometry.Scheme.instHasPullbacksEtale (X : Scheme) :
          CategoryTheory.Limits.HasPullbacks X.Etale