Étale morphisms #

A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

Main results #

AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero: Etale is equivalent to smooth of relative dimension 0.

source

class AlgebraicGeometry.Etale {X Y : Scheme} (f : X ⟶ Y) :

Prop

A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

etale_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale

Instances

source

theorem AlgebraicGeometry.etale_iff {X Y : Scheme} (f : X ⟶ Y) :

Etale f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale

source

theorem AlgebraicGeometry.Scheme.Hom.etale_appLE {X Y : Scheme} (f : X ⟶ Y) [self : Etale f] {U : Y.Opens} :

IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).Etale

Alias of AlgebraicGeometry.Etale.etale_appLE.

source

@[deprecated AlgebraicGeometry.Etale (since := "2026-02-09")]

def AlgebraicGeometry.IsEtale {X Y : Scheme} (f : X ⟶ Y) :

Prop

Alias of AlgebraicGeometry.Etale.

A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is étale.

Equations

Instances For

source

instance AlgebraicGeometry.Etale.instHasRingHomPropertyEtale :

HasRingHomProperty @Etale fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Etale

The property of scheme morphisms Etale is associated with the ring homomorphism property Etale.

source

instance AlgebraicGeometry.Etale.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @Etale

Being étale is multiplicative.

source

instance AlgebraicGeometry.Etale.etale_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [Etale f] [Etale g] :

Etale (CategoryTheory.CategoryStruct.comp f g)

The composition of étale morphisms is étale.

source

instance AlgebraicGeometry.Etale.etale_isStableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Etale

Etale is stable under base change.

source

@[instance 900]

instance AlgebraicGeometry.Etale.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :

Etale f

Open immersions are étale.

source

instance AlgebraicGeometry.Etale.instFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale g] :

Etale (CategoryTheory.Limits.pullback.fst f g)

source

instance AlgebraicGeometry.Etale.instSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Etale f] :

Etale (CategoryTheory.Limits.pullback.snd f g)

source

instance AlgebraicGeometry.Etale.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [Etale f] :

Etale (f ∣_ V)

source

instance AlgebraicGeometry.Etale.instResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [Etale f] :

Etale (Scheme.Hom.resLE f V U e)

source

theorem AlgebraicGeometry.Etale.eq_smoothOfRelativeDimension_zero :

@Etale = @SmoothOfRelativeDimension 0

source

theorem AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero {X Y : Scheme} (f : X ⟶ Y) :

Etale f ↔ SmoothOfRelativeDimension 0 f

source

instance AlgebraicGeometry.Etale.instSmoothOfRelativeDimensionOfNatNat {X Y : Scheme} (f : X ⟶ Y) [Etale f] :

SmoothOfRelativeDimension 0 f

source

@[instance 100]

instance AlgebraicGeometry.Etale.instSmooth {X Y : Scheme} (f : X ⟶ Y) [Etale f] :

Smooth f

source

@[instance 900]

instance AlgebraicGeometry.Etale.instFormallyUnramified {X Y : Scheme} (f : X ⟶ Y) [Etale f] :

FormallyUnramified f

source

instance AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified :

CategoryTheory.MorphismProperty.HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)

source

theorem AlgebraicGeometry.Etale.of_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [Etale (CategoryTheory.CategoryStruct.comp f g)] [LocallyOfFiniteType g] [FormallyUnramified g] :

Etale f

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

source

instance AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme :

CategoryTheory.MorphismProperty.HasOfPostcompProperty @Etale @Etale

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

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

Documentation

Mathlib.AlgebraicGeometry.Morphisms.Etale

Étale morphisms #

Main results #