ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial

English

For a finite or infinite index σ, the Krull dimension grows with the cardinality of σ in the multivariate polynomial ring: ringKrullDim(R) + ENat.card(σ) ≤ ringKrullDim(MvPolynomial σ R).

Русский

Для конечного или бесконечного множества индeterminант σ размерность Крулля возрастает с кардиналом σ в кольце многочленов: 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_natCard_le_ringKrullDim_mvPolynomial (σ : Type*) [Finite σ] :
    ringKrullDim R + Nat.card σ ≤ ringKrullDim (MvPolynomial σ R) := by
  induction σ using Finite.induction_empty_option with
  | of_equiv e H =>
    convert ← H using 1
    · rw [Nat.card_congr e]
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => simp
  | h_option
    IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one, ← add_assoc] at IH ⊢
    refine (add_le_add_right IH _).trans (ringKrullDim_succ_le_ringKrullDim_polynomial.trans ?_)
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge

Похожие утверждения