English
If r is a non-zero divisor, then the dimension drops by at least one on modding out by r: ringKrullDim(R/(r)) + 1 ≤ ringKrullDim(R).
Русский
Если r не делитель нуля, то при факторизации по r размерность уменьшается как минимум на единицу: ringKrullDim(R/(r)) + 1 ≤ ringKrullDim(R).
LaTeX
$$$\\operatorname{ringKrullDim}(R/(r)) + 1 \\le \\operatorname{ringKrullDim}(R)$$$
Lean4
theorem ringKrullDim_quotient_succ_le_of_nonZeroDivisor {r : R} (hr : r ∈ R⁰) :
ringKrullDim (R ⧸ Ideal.span { r }) + 1 ≤ ringKrullDim R :=
by
by_cases hr' : Ideal.span { r } = ⊤
· rw [hr', ringKrullDim_eq_bot_of_subsingleton]
simp
have : Nonempty (PrimeSpectrum.zeroLocus (R := R) (Ideal.span { r })) := by
rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq, PrimeSpectrum.zeroLocus_empty_iff_eq_top]
have := Ideal.Quotient.nontrivial hr'
have := (Ideal.Quotient.mk (Ideal.span { r })).domain_nontrivial
rw [ringKrullDim_quotient, Order.krullDim_eq_iSup_length, ringKrullDim, Order.krullDim_eq_iSup_length, ←
WithBot.coe_one, ← WithBot.coe_add, ENat.iSup_add, WithBot.coe_le_coe, iSup_le_iff]
intro l
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le (J := l.head.1.asIdeal) bot_le
let p' : PrimeSpectrum R := ⟨p, hp.1.1⟩
have hp' : p' < l.head :=
lt_of_le_of_ne hp' fun h ↦
Set.disjoint_iff.mp (Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes hp)
⟨show r ∈ p by simpa [← h] using l.head.2, hr⟩
refine le_trans ?_ (le_iSup _ ((l.map Subtype.val (fun _ _ ↦ id)).cons p' hp'))
simp
