Krull dimension and the fibres of a ring homomorphism

Let S be a Noetherian algebra over a Noetherian ring R. For a prime P of S lying over a prime p of R, the height of P is at most the height of p plus the Krull dimension of the fibre p.Fiber S = κ(p) ⊗[R] S. Consequently the Krull dimension of S is at most the Krull dimension of R plus any common bound on the Krull dimensions of the fibres.

This is the algebraic input for the fibrewise dimension inequality of morphisms of schemes: the Krull dimension of a locally Noetherian scheme is at most the dimension of the target plus the maximal dimension of a fibre, so relative dimension bounds add up under composition.

The key input is Mathlib's Ideal.height_le_height_add_of_liesOver, which bounds the height of P using the height of its image in S ⧸ pS. A chain of primes of S ⧸ pS ending at the image of P consists of primes lying over p, so its length is bounded by the Krull dimension of the set-theoretic fibre of Spec S → Spec R over p. Mathlib's PrimeSpectrum.preimageOrderIsoFiber identifies that fibre with Spec (p.Fiber S).

Main results

• Ideal.height_map_quotientMk_le_ringKrullDim_fiber: the height of the image in S ⧸ pS of a prime P lying over p is at most the Krull dimension of the fibre over p.
• Ideal.height_le_height_add_ringKrullDim_fiber: the height of a prime P lying over p is at most the height of p plus the Krull dimension of the fibre over p.
• Ideal.height_eq_height_under_of_quasiFinite: along a quasi-finite algebra satisfying going down, for instance an étale algebra, the height of a prime equals the height of the prime below it.
• TauCeti.ringKrullDim_le_ringKrullDim_add_of_ringKrullDim_fiber_le: the Krull dimension of S is at most that of R plus a bound on the Krull dimensions of all fibres.

References

• Stacks Project, Tag 00OM
• Stacks Project, Tag 00ON

theorem Ideal.height_map_quotientMk_le_ringKrullDim_fiber {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : ↑(map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ ringKrullDim (p.Fiber S)

The height of the image in S ⧸ pS of a prime P of S lying over p is at most the Krull dimension of the fibre κ(p) ⊗[R] S.

theorem Ideal.height_le_height_add_ringKrullDim_fiber {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] : ↑P.height ≤ ↑p.height + ringKrullDim (p.Fiber S)

Let S be a Noetherian algebra over a Noetherian ring R. The height of a prime P of S lying over p is at most the height of p plus the Krull dimension of the fibre κ(p) ⊗[R] S.

theorem Ideal.height_eq_height_under_of_quasiFinite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] [Algebra.HasGoingDown R S] [Algebra.QuasiFinite R S] (P : Ideal S) [P.IsPrime] : P.height = (under R P).height

Let S be a Noetherian R-algebra which is quasi-finite and satisfies going down, for instance a flat quasi-finite algebra. Then the height of a prime P of S is the height of the prime of R below it.

theorem TauCeti.ringKrullDim_le_ringKrullDim_add_of_ringKrullDim_fiber_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsNoetherianRing S] {d : WithBot ℕ∞} (h : ∀ (p : Ideal R) [inst : p.IsPrime], ringKrullDim (p.Fiber S) ≤ d) : ringKrullDim S ≤ ringKrullDim R + d

The Krull dimension of a Noetherian algebra S over a Noetherian ring R is at most the Krull dimension of R plus any common bound on the Krull dimensions of the fibres κ(p) ⊗[R] S.