English
Let f: R → S be a surjective ring homomorphism whose kernel contains a non-zero divisor; then ringKrullDim(S) + 1 ≤ ringKrullDim(R).
Русский
Пусть f: R → S сюръективен и ядро содержит не нуль-дивизор; тогда ringKrullDim(S) + 1 ≤ ringKrullDim(R).
LaTeX
$$$\\text{ringKrullDim}(S) + 1 \\le \\text{ringKrullDim}(R)$ under surjectivity and kernel conditions$$
Lean4
/-- If `R →+* S` is surjective whose kernel contains a nonzero divisor, then `dim S + 1 ≤ dim R`. -/
theorem ringKrullDim_succ_le_of_surjective (f : R →+* S) (hf : Function.Surjective f) {r : R} (hr : r ∈ R⁰)
(hr' : f r = 0) : ringKrullDim S + 1 ≤ ringKrullDim R :=
by
refine le_trans ?_ (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr)
gcongr
exact
ringKrullDim_le_of_surjective (Ideal.Quotient.lift _ f (RingHom.ker f |>.span_singleton_le_iff_mem.mpr hr'))
(Ideal.Quotient.lift_surjective_of_surjective _ _ hf)
