English
For f: σ → S and p ∈ MvPolynomial(σ,R), (aeval f)(p) equals the evaluation after tensoring: (1 ⊗ f) evaluated on p equals 1 ⊗ (aeval f) p.
Русский
Для f: σ → S и p ∈ MvPolynomial(σ,R), (aeval f)(p) эквивалентно выражению с тензорным произведением: (1 ⊗ f) применяется к p и равно 1 ⊗ (aeval f) p.
LaTeX
$$$ (aeval (\\lambda x, 1 \\otimes f x))\, p = 1 \\otimes (aeval f)\, p $$$
Lean4
theorem aeval_one_tmul (f : σ → S) (p : MvPolynomial σ R) :
(aeval fun x ↦ (1 ⊗ₜ[R] f x : N ⊗[R] S)) p = 1 ⊗ₜ[R] (aeval f) p := by
induction p using MvPolynomial.induction_on with
| C a =>
simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
| add p q hp hq => simp [hp, hq, tmul_add]
| mul_X p i h => simp [h]
