scalarRTensor — Mathlib

English

There is a canonical S-linear equivalence between the tensor product MvPolynomial σ R ⊗_R N and the finsupp-valued module (σ →₀ ℕ) →₀ N, called scalarRTensor.

Русский

Существует каноническое S-линейное эквиваленство между MvPolynomial σ R ⊗ N и модулем, значения которого лежат в finsupp, называемое scalarRTensor.

LaTeX

$$$scalarRTensor:\\; MvPolynomial\\; σ\\; R \\otimes_R N \\simeq_S (σ \\to_0 ℕ) \\; ⟶_0 \\; N$$$

Lean4

/-- The tensor product of the polynomial algebra by a module
  is linearly equivalent to a Finsupp of that module -/
noncomputable def scalarRTensor : MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
  TensorProduct.finsuppScalarLeft _ _ _

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