English
For a polynomial ring, the Krull dimension bound yields that the ring of polynomials in σ over R has Krull dimension at most 2·dim(R) + 1.
Русский
Для кольца многочленов над R размерность Крулля не превосходит 2·dim(R) + 1.
LaTeX
$$$\\operatorname{ringKrullDim}(\\operatorname{Polynomial} R) \\le 2 \\cdot \\operatorname{ringKrullDim}(R) + 1$$$
Lean4
theorem ringKrullDim_le {R : Type*} [CommRing R] : ringKrullDim (Polynomial R) ≤ 2 * (ringKrullDim R) + 1 :=
by
rw [ringKrullDim, ringKrullDim]
apply Order.krullDim_le_of_krullDim_preimage_le' C.specComap ?_ (fun p ↦ ?_)
· exact fun {a b} h ↦ Ideal.comap_mono h
· rw [show C = (algebraMap R (Polynomial R)) from rfl,
Order.krullDim_eq_of_orderIso (PrimeSpectrum.preimageOrderIsoTensorResidueField R (Polynomial R) p), ←
ringKrullDim, ← ringKrullDim_eq_of_ringEquiv (polyEquivTensor R (p.asIdeal.ResidueField)).toRingEquiv, ←
Ring.krullDimLE_iff]
infer_instance
