English
There is a natural equivalence between ring homomorphisms from MvPolynomial σ ℤ to S and functions σ → S; the forward map sends f to its action on the indeterminates X_i.
Русский
Существует естественная эквивалентность между кольцевыми гомоморфизмами от MvPolynomial σ ℤ к S и функциями σ → S; переход вперёд отправляет f в его действие на независимые переменные X_i.
LaTeX
$$$\\mathrm{homEquiv} : (\\mathrm{MvPolynomial}\\;\\sigma\\; \\mathbb{Z} \\to+* S) \\simeq (\\sigma \\to S)$$$
Lean4
/-- A ring homomorphism `f : Z[X_1, X_2, ...] → R`
is determined by the evaluations `f(X_1)`, `f(X_2)`, ... -/
@[simp]
theorem eval₂Hom_X {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ) :
eval₂ c (f ∘ X) x = f x := by
apply
MvPolynomial.induction_on x
(fun n => by
rw [hom_C f, eval₂_C]
exact eq_intCast c n)
(fun p q hp hq => by
rw [eval₂_add, hp, hq]
exact (f.map_add _ _).symm)
(fun p n hp => by
rw [eval₂_mul, eval₂_X, hp]
exact (f.map_mul _ _).symm)
