Krull dimension and non zero-divisors #
Main results #
ringKrullDim_quotient_succ_le_of_nonZeroDivisor
: Ifr
is not a zero divisor, thendim R/r + 1 ≤ dim R
.ringKrullDim_succ_le_ringKrullDim_polynomial
:dim R + 1 ≤ dim R[X]
.ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial
:dim R + #σ ≤ dim R[σ]
.
theorem
ringKrullDim_quotient_succ_le_of_nonZeroDivisor
{R : Type u_1}
[CommRing R]
{r : R}
(hr : r ∈ nonZeroDivisors R)
:
theorem
ringKrullDim_succ_le_of_surjective
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
{r : R}
(hr : r ∈ nonZeroDivisors R)
(hr' : f r = 0)
:
If R →+* S
is surjective whose kernel contains a nonzerodivisor, then dim S + 1 ≤ dim R
.
@[simp]
theorem
ringKrullDim_mvPolynomial_of_isEmpty
{R : Type u_1}
[CommRing R]
(σ : Type u_3)
[IsEmpty σ]
:
theorem
ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial
{R : Type u_1}
[CommRing R]
(σ : Type u_3)
[Finite σ]
:
theorem
ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial
{R : Type u_1}
[CommRing R]
(σ : Type u_3)
: