Heights of primes along quasi-finite extensions over a normal base

Let S be a finite type R-algebra which is a domain containing R. At a prime q of S at which S is quasi-finite over R, lying over a prime p of R with R_p integrally closed, the heights of q and p agree. Geometrically: a quasi-finite dominant morphism of integral schemes onto a scheme which is normal at the image point preserves the dimension of the local rings. This is the dimension equality behind the purity of the branch locus, where the local ring of the target is regular, hence normal.

For the equality, Zariski's main theorem (Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Stacks 00Q9) gives a module-finite subalgebra S' of S and r ∈ S' ∖ q with S'[1/r] = S[1/r], so q has the same height as q ∩ S'. The finite extension R ⊆ S' preserves heights over a normal R_p (Ideal.height_eq_height_of_isIntegral_of_isIntegrallyClosed, through going down, Stacks 00H8). No Noetherian hypothesis is needed.

Over a Noetherian base with S_q Noetherian (for instance, S of finite type), the inequality ht q ≤ ht p needs neither normality nor injectivity: the fibre S_q ⧸ p S_q is Artinian, so Mathlib's Ideal.height_le_height_add_of_liesOver (Stacks 00OM) applies with a fibre term zero.

Main results

• Ideal.height_le_height_of_quasiFiniteAt: over a Noetherian ring, a prime q at which the algebra is quasi-finite, with S_q Noetherian, has height at most that of the prime below it.
• Ideal.height_eq_height_of_quasiFiniteAt: equality, for a domain containing R and a normal local ring R_p, over an arbitrary base.

References

• Stacks Project, Tag 00Q9, Zariski's main theorem.
• Stacks Project, Tag 00H8, going down for integral extensions of a normal domain.
• Stacks Project, Tag 00OM, heights along an algebra and its fibres.

theorem Ideal.height_le_height_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q] [IsNoetherianRing (Localization.AtPrime q)] : q.height ≤ p.height

Let S be an algebra over a Noetherian ring R and q a prime of S over p at which S is quasi-finite over R, with S_q Noetherian (for instance, S of finite type over R). Then the height of q is at most the height of p.

theorem Ideal.height_eq_height_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] [IsDomain S] [FaithfulSMul R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q] [IsIntegrallyClosed (Localization.AtPrime p)] : q.height = p.height

Let S be a finite type R-algebra which is a domain containing R, and q a prime of S over p at which S is quasi-finite over R. If R_p is integrally closed, then q and p have the same height. No Noetherian hypothesis is needed.