Rings of finite Krull dimension

A ring whose Krull dimension is a natural number has finite Krull dimension. This is the form in which finiteness of the dimension usually arises, from a computation dim R = n.

A surjection from a domain of finite Krull dimension onto a ring of at least the same dimension is injective, since a nonzero kernel element would be a nonzerodivisor and so would lower the dimension.

Main results

• FiniteRingKrullDim.of_ringKrullDim_eq_natCast: a ring of Krull dimension n : ℕ has finite Krull dimension.
• RingHom.injective_of_surjective_of_ringKrullDim_le: a surjection from a domain of finite Krull dimension onto a ring of at least the same dimension is injective.

theorem FiniteRingKrullDim.of_ringKrullDim_eq_natCast {R : Type u_1} [CommRing R] {n : ℕ} (h : ringKrullDim R = ↑n) : FiniteRingKrullDim R

A ring whose Krull dimension is a natural number n has finite Krull dimension.

theorem RingHom.injective_of_surjective_of_ringKrullDim_le {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [FiniteRingKrullDim R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (hdim : ringKrullDim R ≤ ringKrullDim S) : Function.Injective ⇑f

A surjective ring homomorphism from a domain of finite Krull dimension onto a ring of at least the same dimension is injective.