Documentation

Mathlib.AlgebraicGeometry.Morphisms.Etale

É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) :

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

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) :

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

@AlgebraicGeometry.IsEtale = @AlgebraicGeometry.Etale

Instances For

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] :

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] :

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

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] :

def AlgebraicGeometry.Scheme.Etale (X : Scheme) :

Type (u + 1)

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

Equations

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

Instances For

@[implicit_reducible]

instance AlgebraicGeometry.Scheme.instCategoryEtale (X : Scheme) :

CategoryTheory.Category.{u_1, u_1 + 1} X.Etale

Equations

One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instHasPullbacksEtale (X : Scheme) :

CategoryTheory.Limits.HasPullbacks X.Etale

instance AlgebraicGeometry.Scheme.instHasFiniteLimitsEtale (X : Scheme) :

CategoryTheory.Limits.HasFiniteLimits X.Etale

instance AlgebraicGeometry.Scheme.instEtaleHomDiscretePUnit (X : Scheme) (Y : X.Etale) :

instance AlgebraicGeometry.Scheme.instEtaleLeftDiscretePUnit {X : Scheme} {Z Y : X.Etale} (f : Z ⟶ Y) :

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

AlgebraicGeometry.Scheme.Etale.forget X = CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.Etale ⊤ X

Instances For

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

instance AlgebraicGeometry.Scheme.instFullEtaleOverForget (X : Scheme) :

(Etale.forget X).Full

instance AlgebraicGeometry.Scheme.instFaithfulEtaleOverForget (X : Scheme) :

(Etale.forget X).Faithful

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Etale.mk {X Y : Scheme} (f : Y ⟶ X) [Etale f] :

Constructor for objects in the étale site of a scheme X: it takes an étale morphism f : Y ⟶ X as an input.

Equations

AlgebraicGeometry.Scheme.Etale.mk f = CategoryTheory.MorphismProperty.Over.mk ⊤ f ⋯

Instances For

@[simp]

theorem AlgebraicGeometry.Scheme.Etale.forget_mk {X Y : Scheme} (f : Y ⟶ X) [Etale f] :

(forget X).obj (mk f) = CategoryTheory.Over.mk f

@[simp]

theorem AlgebraicGeometry.Scheme.Etale.forget_obj_left (X : Scheme) (Y : X.Etale) :

((forget X).obj Y).left = Y.left

@[simp]

theorem AlgebraicGeometry.Scheme.Etale.forget_obj_hom (X : Scheme) (Y : X.Etale) :

((forget X).obj Y).hom = Y.hom

instance AlgebraicGeometry.Scheme.instEtaleOverLeftDiscretePUnitInferInstanceOverClass (X : Scheme) (Y : X.Etale) :

Etale (Y.left ↘ X)

def AlgebraicGeometry.Scheme.Etale.rec (X : Scheme) {motive : X.Etale → Sort u_1} (mk : (Y : Scheme) → (f : Y ⟶ X) → (x : Etale f) → motive (mk f)) (T : X.Etale) :

motive T

Induction principle for the objects of the small étale site of a scheme.

Equations

AlgebraicGeometry.Scheme.Etale.rec X mk T = mk ((CategoryTheory.Functor.id AlgebraicGeometry.Scheme).obj T.left) T.hom ⋯

Instances For

instance AlgebraicGeometry.Scheme.instPreservesFiniteLimitsEtaleOverForget (X : Scheme) :

CategoryTheory.Limits.PreservesFiniteLimits (Etale.forget X)