mvPolynomial — Mathlib

English

For any index set σ, the multivariate polynomial ring MVPolynomial(σ, R) is a formall y smooth R-algebra.

Русский

Для любого множества индексов σ многочленный MVPolynomial(σ, R) образует формально гладкую R-алгебру.

LaTeX

$$$\operatorname{FormallySmooth}(R, \operatorname{MvPolynomial}(\sigma, R))$$$

Lean4

instance mvPolynomial (σ : Type u) : FormallySmooth R (MvPolynomial σ R) :=
  by
  constructor
  intro C _ _ I _ f
  have : ∀ s : σ, ∃ c : C, Ideal.Quotient.mk I c = f (MvPolynomial.X s) := fun s => Ideal.Quotient.mk_surjective _
  choose g hg using this
  refine ⟨MvPolynomial.aeval g, ?_⟩
  ext s
  rw [← hg, AlgHom.comp_apply, MvPolynomial.aeval_X]
  rfl

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