English
The symmetrized base-change map, restricted to R, composed with mapAlgHom equals includeRight.
Русский
Симметризированная карта изменения базы, с ограничением на R, в композиции с mapAlgHom равна includeRight.
LaTeX
$$(((algebraTensorAlgEquiv (σ := σ) R A).symm.restrictScalars R) : MvPolynomial(σ,A) →_a[R] A ⊗_R MvPolynomial(σ,R)).comp (MvPolynomial.mapAlgHom (R := R) (S₁ := R) (S₂ := A) (Algebra.ofId R A)) = Algebra.TensorProduct.includeRight$$
Lean4
@[simp]
theorem algebraTensorAlgEquiv_symm_monomial (m : σ →₀ ℕ) (a : A) :
(algebraTensorAlgEquiv R A).symm (monomial m a) = a ⊗ₜ monomial m 1 :=
by
apply @Finsupp.induction σ ℕ _ _ m
· simp [algebraTensorAlgEquiv]
· intro i n f _ _ hfa
simp only [algebraTensorAlgEquiv, AlgEquiv.ofAlgHom_symm_apply] at hfa ⊢
simp only [add_comm, monomial_add_single, map_mul, map_pow, aeval_X, Algebra.TensorProduct.tmul_pow, one_pow, hfa]
nth_rw 2 [← mul_one a]
rw [Algebra.TensorProduct.tmul_mul_tmul]
