É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.

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

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

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.

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

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.

instance AlgebraicGeometry.Etale.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @Etale

Being étale is multiplicative.

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.

instance AlgebraicGeometry.Etale.etale_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Etale

Etale is stable under base change.

@[instance 900]

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

Open immersions are étale.

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

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

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

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)

theorem AlgebraicGeometry.Etale.eq_smoothOfRelativeDimension_zero : @Etale = @SmoothOfRelativeDimension 0

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

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

@[instance 100]

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

@[instance 900]

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

instance AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified : CategoryTheory.MorphismProperty.HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)

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.

instance AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme : CategoryTheory.MorphismProperty.HasOfPostcompProperty @Etale @Etale

theorem AlgebraicGeometry.Etale.iff_flat_and_formallyUnramified {X Y : Scheme} {f : X ⟶ Y} : Etale f ↔ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

theorem AlgebraicGeometry.Etale.of_formallyUnramified_of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] [FormallyUnramified f] [LocallyOfFinitePresentation f] : Etale f

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.instHasPullbacksEtale (X : Scheme) : CategoryTheory.Limits.HasPullbacks X.Etale

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

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.