English
If σ is finite or infinite, the bound holds with ENat.card: ringKrullDim(R) + ENat.card(σ) ≤ ringKrullDim(MvPolynomial σ R).
Русский
Для всякого σ справедлива граница: ringKrullDim(R) + ENat.card(σ) ≤ ringKrullDim(MvPolynomial σ R).
LaTeX
$$$\\operatorname{ringKrullDim}(R) + \\operatorname{ENat.card}(\\sigma) \\le \\operatorname{ringKrullDim}(\\operatorname{MvPolynomial}(\\sigma, R))$$$
Lean4
theorem ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial (σ : Type*) :
ringKrullDim R + ENat.card σ ≤ ringKrullDim (MvPolynomial σ R) :=
by
nontriviality R
cases finite_or_infinite σ
· rw [ENat.card_eq_coe_natCard]
push_cast
exact ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _
· simp only [ENat.card_eq_top_of_infinite, WithBot.coe_top]
suffices ringKrullDim (MvPolynomial σ R) = ⊤ by simp_all
rw [WithBot.eq_top_iff_forall_ge]
intro n
let ι := Infinite.natEmbedding σ ∘ Fin.val (n := n + 1)
have := Function.invFun_surjective (f := ι) ((Infinite.natEmbedding σ).2.comp Fin.val_injective)
refine le_trans ?_ (ringKrullDim_le_of_surjective (rename (R := R) _).toRingHom (rename_surjective _ this))
refine le_trans ?_ (ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _)
simp only [ENat.some_eq_coe, Nat.card_eq_fintype_card, Fintype.card_fin, Nat.cast_add, Nat.cast_one]
trans n + 1
· norm_cast
simp
· exact WithBot.le_add_self Order.bot_lt_krullDim.ne' _
