English
The tensor product of a polynomial ring by a module is canonically linearly isomorphic to a finsupp-typed tensor product over a coefficient-free base: there exists a canonical S-linear equivalence rTensor: MvPolynomial σ S ⊗_R N ≃_S (σ →₀ ℕ) →₀ (S ⊗_R N).
Русский
Тензорное произведение полиномиального кольца на модуль эквивалентно каноническому линейному тождеству между соответствующими объектами: существует каноническое S-линейное эквивалентное отображение rTensor.
LaTeX
$$$rTensor:\\; MvPolynomial\\; σ\\; S\\; ⊗_R\\; N \\cong_S (σ \\to_0 ℕ) \\; ⊗_0 \\; (S ⊗_R N)$$$
Lean4
/-- The tensor product of a polynomial ring by a module is
linearly equivalent to a Finsupp of a tensor product -/
noncomputable def rTensor : MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
TensorProduct.finsuppLeft' _ _ _ _ _
