Locally quasi-finite morphisms

Formal unramifiedness together with local finite type implies local quasi-finiteness.

A locally quasi-finite morphism is strictly monotone for the specialization order on points (x ≤ y when y generizes x): it preserves specializations because it is continuous, and two distinct points of one fibre never specialize to each other because the fibres are discrete. This is incomparability for quasi-finite morphisms. Consequently the codimension of a point is at most the codimension of its image, and the dimension of the source is at most that of the target.

Main results

• AlgebraicGeometry.LocallyQuasiFinite.of_formallyUnramified: a formally unramified morphism locally of finite type is locally quasi-finite.
• AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.finite_residueField: the residue field extension at a point where a morphism is quasi-finite is finite; AlgebraicGeometry.Scheme.Hom.finite_residueField is the instance for a locally quasi-finite morphism.
• AlgebraicGeometry.Scheme.Hom.strictMono: a locally quasi-finite morphism is strictly monotone for the specialization order.
• AlgebraicGeometry.Scheme.Hom.coheight_le_coheight_apply: under a locally quasi-finite morphism the coheight of a point is at most the coheight of its image.
• AlgebraicGeometry.Scheme.Hom.topologicalKrullDim_le: the source of a locally quasi-finite morphism has dimension at most that of its target.
• AlgebraicGeometry.Scheme.Hom.ringKrullDim_stalk_eq_of_quasiFiniteAt: a dominant morphism of integral schemes, locally of finite type, which is quasi-finite at x with integrally closed local ring at f x, preserves the dimension of the local ring at x; AlgebraicGeometry.Scheme.Hom.ringKrullDim_stalk_eq_of_locallyQuasiFinite is the form for a locally quasi-finite morphism onto a normal scheme. Over a normal base the inequality between coheights becomes an equality; the ring-level input is Ideal.height_eq_height_of_quasiFiniteAt.

References

• The Stacks Project, Tag 00PK (a quasi-finite ring map has finite residue field extensions).
• The strict monotonicity is a scheme form of Pcf.height_eq_one_of_liesOver_heightOne in T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Bounding/Divisors.lean, whose incomparability step is proved there for integral extensions of rings.

@[instance 100]

instance AlgebraicGeometry.LocallyQuasiFinite.of_formallyUnramified {X Y : Scheme} (f : X ⟶ Y) [hform : FormallyUnramified f] [htype : LocallyOfFiniteType f] : LocallyQuasiFinite f

A formally unramified morphism that is locally of finite type is locally quasi-finite.

theorem AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.finite_residueField {X Y : Scheme} {f : X ⟶ Y} {x : ↥X} (hx : QuasiFiniteAt f x) : Module.Finite ↑(Y.residueField (f x)) ↑(X.residueField x)

Residue field extensions at a quasi-finite point are finite. If f is quasi-finite at x, then κ(x) is a finite extension of κ(f x). Stacks, Lemma 00PK. The proof is adapted from that of Mathlib's Algebra.IsSeparable instance for f.residueFieldMap x in Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean.

instance AlgebraicGeometry.Scheme.Hom.finite_residueField {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] (x : ↥X) : Module.Finite ↑(Y.residueField (f x)) ↑(X.residueField x)

Residue field extensions of a locally quasi-finite morphism are finite. If f is locally quasi-finite, then κ(x) is a finite extension of κ(f x) at every point x. Stacks, Lemma 00PK.

theorem AlgebraicGeometry.Scheme.Hom.strictMono {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] : StrictMono ⇑f

A locally quasi-finite morphism is strictly monotone for the specialization order.

theorem AlgebraicGeometry.Scheme.Hom.coheight_le_coheight_apply {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] (x : ↥X) : Order.coheight x ≤ Order.coheight (f x)

Under a locally quasi-finite morphism the coheight of a point is at most the coheight of its image.

theorem AlgebraicGeometry.Scheme.Hom.topologicalKrullDim_le {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] : topologicalKrullDim ↥X ≤ topologicalKrullDim ↥Y

The source of a locally quasi-finite morphism has dimension at most that of its target: the dimension of a scheme is the supremum of the coheights of its points.

theorem AlgebraicGeometry.Scheme.Hom.ringKrullDim_stalk_eq_of_quasiFiniteAt {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y] [IsDominant f] [LocallyOfFiniteType f] {x : ↥X} (hx : QuasiFiniteAt f x) [IsIntegrallyClosed ↑(Y.presheaf.stalk (f x))] : ringKrullDim ↑(X.presheaf.stalk x) = ringKrullDim ↑(Y.presheaf.stalk (f x))

Quasi-finite morphisms over a normal base preserve the dimension of local rings. Let f : X ⟶ Y be a dominant morphism of integral schemes, locally of finite type. If f is quasi-finite at x and the local ring of Y at f x is integrally closed, then the local rings at x and at f x have the same dimension.

theorem AlgebraicGeometry.Scheme.Hom.ringKrullDim_stalk_eq_of_locallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) [IsIntegral X] [IsDominant f] [LocallyOfFiniteType f] [LocallyQuasiFinite f] [TauCeti.AlgebraicGeometry.IsNormalScheme Y] (x : ↥X) : ringKrullDim ↑(X.presheaf.stalk x) = ringKrullDim ↑(Y.presheaf.stalk (f x))

A locally quasi-finite dominant morphism f : X ⟶ Y, locally of finite type, from an integral scheme onto a normal scheme preserves the dimension of every local ring: dim 𝒪_{X,x} = dim 𝒪_{Y,f x} for all x. Normality of X is not needed, and Y is integral for free, being reduced and the dominant image of an irreducible scheme.