Unramified, étale and quasi-finite at a point, read off from the stalk map #
For a morphism of schemes f : X ⟶ Y and a point x : X, the Stacks Project calls f
unramified at x (Definition 29.36.1 (02G4)) if x has an open neighbourhood U such that
U.ι ≫ f is locally of finite type and formally unramified, and étale at x (Definition
29.37.1 (02GI)) if x has an open neighbourhood U such that U.ι ≫ f is étale. This file
shows that both conditions only depend on the stalk map f.stalkMap x:
- for
flocally of finite type,fis unramified atxifff.stalkMap xis formally unramified (AlgebraicGeometry.Scheme.Hom.unramifiedAt_iff_stalkMap); - for
flocally of finite presentation,fis étale atxifff.stalkMap xis flat and formally unramified (AlgebraicGeometry.Scheme.Hom.etaleAt_iff_stalkMap, Stacks, Lemma 29.37.15 (02GU), conditions (1) and (4)).
Both stalk conditions descend along flat morphisms: for g : X' ⟶ X with flat stalk map at
x', if the stalk map of g ≫ f at x' is flat (resp. formally unramified, with f and
g ≫ f locally of finite type), then so is the stalk map of f at g x'; the flat case is
AlgebraicGeometry.Scheme.Hom.flat_stalkMap_of_comp. Hence if f is locally of finite
presentation, g is flat and surjective and g ≫ f is étale, then f is étale
(AlgebraicGeometry.Etale.of_comp_surjective). For an étale surjective g this is the statement
of Stacks, Lemma 35.31.1 (036W), that étaleness is étale local on the source, for f locally of
finite presentation.
In a commutative square with étale vertical maps, the horizontal maps are étale at
corresponding points simultaneously, provided the bottom map is locally of finite presentation
(AlgebraicGeometry.Scheme.Hom.exists_etale_iff_of_etale_square). Neither a cartesian square nor
surjective vertical maps are needed. This permits passage to finite local models in purity of
the branch locus (Stacks, Lemma 58.21.4 (0BMB)).
When the local ring of Y at f x is a Dedekind domain, for instance a discrete valuation ring,
and the local ring of X at x is a domain but not a field, flatness of the stalk map is
automatic, so f is étale at x as soon as its stalk map is formally unramified
(AlgebraicGeometry.Scheme.Hom.exists_etale_of_formallyUnramified_stalkMap_of_isDedekindDomain).
This is purity of the branch locus in dimension one, the case from which the proof of Stacks,
Lemma 58.21.4 (0BMB) starts.
These are compared with Mathlib's affine pointwise notions: on affine opens V ⊆ f⁻¹ U, the stalk
map at x is formally unramified iff Γ(X, V) is unramified over Γ(Y, U) at the prime of x
(AlgebraicGeometry.formallyUnramified_stalkMap_iff), in parallel with Mathlib's
AlgebraicGeometry.formallySmooth_stalkMap_iff and with the flat analogue
AlgebraicGeometry.flat_stalkMap_iff. For Spec S ⟶ Spec R this gives
AlgebraicGeometry.Scheme.Hom.etaleAt_spec_iff and
AlgebraicGeometry.Scheme.Hom.unramifiedAt_spec_iff: Spec S ⟶ Spec R is étale (resp.
unramified) at q exactly when Algebra.IsEtaleAt R q (resp. Algebra.IsUnramifiedAt R q).
For f locally of finite type over a locally Noetherian Y whose local ring at f x is a normal
domain, a formally unramified stalk map at x already makes f étale near x as soon as
dim 𝒪_{Y, f x} ≤ dim 𝒪_{X, x}
(AlgebraicGeometry.Scheme.Hom.exists_etale_of_formallyUnramified_stalkMap_of_ringKrullDim_le,
the scheme form of Algebra.IsEtaleAt.of_isUnramifiedAt_of_height_le).
Mathlib defines quasi-finiteness at x in stalk form, f.QuasiFiniteAt x, and shows that it
implies quasi-finiteness of Γ(X, V) over Γ(Y, U) at the prime of x for affine opens
x ∈ V ⊆ f⁻¹ U (AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt). The converse is
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_of_appLE. With both directions,
AlgebraicGeometry.Scheme.Hom.exists_appLE_quasiFiniteAt_iff shows that f is quasi-finite at
x in the sense of the Stacks Project, Tag 01TD, iff f is locally of finite type near x and
f.QuasiFiniteAt x. For Spec S ⟶ Spec R,
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_spec_iff identifies quasi-finiteness at q with
Algebra.QuasiFiniteAt R q.
Viewing the stalk map as an algebra 𝒪_{Y, f x} → 𝒪_{X, x}, it is local
(AlgebraicGeometry.Scheme.Hom.isLocalHom_stalkMap_toAlgebra), essentially of finite type when f
is locally of finite type (AlgebraicGeometry.Scheme.Hom.essFiniteType_stalkMap_toAlgebra), and
formally unramified when f is
(AlgebraicGeometry.Scheme.Hom.formallyUnramified_stalkMap_toAlgebra). When f is moreover flat,
the stalk map is faithfully flat, so 𝒪_{Y, f x} is Noetherian exactly when 𝒪_{X, x} is
(AlgebraicGeometry.Scheme.Hom.isNoetherianRing_stalk_iff_of_flat_of_locallyOfFiniteType).
For f formally unramified and locally of finite type, the maximal ideal of 𝒪_{Y, f x}
generates the maximal ideal of 𝒪_{X, x} along the stalk map
(AlgebraicGeometry.Scheme.Hom.map_maximalIdeal_stalkMap_of_formallyUnramified).
The passage from the stalk to a neighbourhood follows Mathlib's
AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk: Mathlib's
Algebra.exists_formallyUnramified_of_isUnramifiedAt and Algebra.exists_etale_of_isEtaleAt
spread the condition from the prime of x to a basic open D(r), and
AlgebraicGeometry.HasRingHomProperty.exists_ι_comp_of_away turns this into an open
neighbourhood of x. For étaleness the stalk condition is first turned into Algebra.IsEtaleAt by
Algebra.isEtaleAt_iff_flat_and_isUnramifiedAt.
References #
On affine opens x ∈ V ⊆ f⁻¹ U, the stalk map of f at x is formally unramified iff
Γ(X, V) is unramified over Γ(Y, U) at the prime of x.
The stalk map of Spec S ⟶ Spec R at q is formally unramified iff S is unramified over
R at q.
For an open immersion i, a ring-hom property Q stable under isomorphisms holds for the
stalk map of i ≫ f at x iff it holds for the stalk map of f at i x.
Let V ⊆ f⁻¹ U with U and V affine, and let P be a morphism property attached to the
ring-hom property Q. If Q holds for Γ(Y, U) → Γ(X, V)_r, then P holds for the restriction
D(r) ⟶ U of f.
Let x ∈ V ⊆ f⁻¹ U with U and V affine, and let P be a morphism property attached to
the ring-hom property Q, stable under composition and containing identities. If Q holds for
Γ(Y, U) → Γ(X, V)_r for some r not in the prime of x, then x has an open neighbourhood
W with P (W.ι ≫ f), namely W = D(r).
If i ≫ f is formally unramified for an open immersion i, the stalk map of f at i x is
formally unramified.
A morphism locally of finite type is unramified at x in the sense of Stacks, Definition
29.36.1 (02G4), iff its stalk map at x is formally unramified.
A morphism locally of finite presentation is étale at x in the sense of Stacks, Definition
29.37.1 (02GI), iff its stalk map at x is flat and formally unramified.
Formal unramifiedness of stalk maps descends along flat morphisms: for f and g ≫ f locally
of finite type, if g has flat stalk map at x' and g ≫ f has formally unramified stalk map at
x', then f has formally unramified stalk map at g x'.
In a commutative square with flat, formally unramified source map and formally unramified target map, formal unramifiedness of the horizontal stalk maps is equivalent at corresponding points. The source map and bottom horizontal map are locally of finite type; no finite-type assumption is needed on the top horizontal map or the target map.
Étaleness descends along flat morphisms. Let f be locally of finite presentation and
g : X' ⟶ X a morphism with flat stalk map at x' such that g ≫ f is étale. Then f is étale
on an open neighbourhood of g x'.
In a commutative square with étale vertical maps, the horizontal maps are étale at corresponding points simultaneously. No cartesian or surjectivity hypothesis is needed.
Purity in dimension one. Let f be locally of finite presentation, for instance locally
of finite type with Y locally Noetherian, and let x : X be a point at which the local ring of
X is a domain but not a field (so x is not the generic point of an irreducible component of
X), while the local ring of Y at f x is a Dedekind domain, for instance a discrete valuation
ring. If the stalk map of f at x is formally unramified, then f is étale on an open
neighbourhood of x.
Unramified over a normal base of the same dimension implies étale (compare SGA 1,
Exposé I, Théorème 9.5 (ii)). Let f be locally of finite type over a locally Noetherian
Y, with formally unramified stalk map at x. If the local ring of Y at f x is a normal
domain of dimension at most that of the local ring of X at x, then f is étale on an open
neighbourhood of x.
For a finitely presented R-algebra S, the morphism Spec S ⟶ Spec R is étale at q in
the sense of Stacks, Definition 29.37.1 (02GI), iff S is étale over R at q in Mathlib's
sense Algebra.IsEtaleAt.
For a finite type R-algebra S, the morphism Spec S ⟶ Spec R is unramified at q in
the sense of Stacks, Definition 29.36.1 (02G4), iff S is unramified over R at q in
Mathlib's sense Algebra.IsUnramifiedAt.
Let x ∈ V ⊆ f⁻¹ U with U and V affine. If Γ(X, V) is quasi-finite over Γ(Y, U) at
the prime of x, then f is quasi-finite at x. This is the converse of Mathlib's
AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt.
The morphism Spec S ⟶ Spec R is quasi-finite at q iff S is quasi-finite over R at
q in Mathlib's sense Algebra.QuasiFiniteAt.
A morphism f is quasi-finite at x in the sense of the Stacks Project, Tag 01TD, that is,
there are affine opens x ∈ V ⊆ f⁻¹ U such that Γ(X, V) is of finite type over Γ(Y, U) and
quasi-finite over it at the prime of x, iff f is locally of finite type on an open
neighbourhood of x and quasi-finite at x in Mathlib's stalk form Scheme.Hom.QuasiFiniteAt.
Quasi-finiteness at a prime is Mathlib's Algebra.QuasiFiniteAt; for algebras of finite type it
agrees with the Stacks Project's notion (the prime is isolated in its fibre) by Mathlib's
Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber.
The stalk map at x of a morphism f : X ⟶ Y, as an algebra, is local.
The stalk map at x of a morphism f : X ⟶ Y locally of finite type, as an algebra, is
essentially of finite type.
A flat morphism f : X ⟶ Y locally of finite type preserves and reflects Noetherian local
rings: the local ring of Y at f x is Noetherian exactly when the local ring of X at x is.
The stalk map at x of a formally unramified morphism f : X ⟶ Y, as an algebra, is formally
unramified.
Along the stalk map at x of a morphism f : X ⟶ Y that is formally unramified and locally of
finite type, the maximal ideal of the local ring of Y at f x generates the maximal ideal of the
local ring of X at x.
Étaleness descends along flat surjections. Let f be locally of finite presentation and
g flat and surjective. If g ≫ f is étale, then f is étale. For an étale surjective g, this
is Stacks, Lemma 35.31.1 (036W) for f locally of finite presentation.