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.

@[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

• AlgebraicGeometry.IsEtale f = AlgebraicGeometry.IsSmoothOfRelativeDimension 0 f

instance AlgebraicGeometry.IsEtale.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsEtale

def AlgebraicGeometry.Etale (X : Scheme) : Type (u + 1)

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

Equations

• AlgebraicGeometry.Etale X = CategoryTheory.MorphismProperty.Over @AlgebraicGeometry.IsEtale ⊤ X

instance AlgebraicGeometry.instCategoryEtale (X : Scheme) : CategoryTheory.Category.{u, u + 1} (Etale X)

Equations

• AlgebraicGeometry.instCategoryEtale X = inferInstanceAs (CategoryTheory.Category.{?u.12, ?u.12 + 1} (CategoryTheory.MorphismProperty.Over @AlgebraicGeometry.IsEtale ⊤ X))

def AlgebraicGeometry.Etale.forget (X : Scheme) : CategoryTheory.Functor (Etale X) (CategoryTheory.Over X)

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

Equations

• AlgebraicGeometry.Etale.forget X = CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsEtale ⊤ X

def AlgebraicGeometry.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.

instance AlgebraicGeometry.instFullEtaleOverSchemeForget (X : Scheme) : (Etale.forget X).Full

instance AlgebraicGeometry.instFaithfulEtaleOverSchemeForget (X : Scheme) : (Etale.forget X).Faithful