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

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.

Equations

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

@[instance_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) : Etale Y.hom

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

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

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.

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] : X.Etale

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 ⋯

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

instance AlgebraicGeometry.Scheme.instPreservesFiniteLimitsEtaleOverForget (X : Scheme) : CategoryTheory.Limits.PreservesFiniteLimits (Etale.forget X)