The natural map Sym[R]^n M → SymmetricAlgebra R M

For an R-module M and a natural number n, there is a canonical linear map Sym[R]^n M →ₗ[R] SymmetricAlgebra R M sending a symmetric tensor power of n vectors to their product in the symmetric algebra:

Sym[R]^n M  ∋  ⨂ₛ[R] i, g i  ↦  ι(g 0) · ι(g 1) · ⋯ · ι(g (n-1))  ∈  SymmetricAlgebra R M

This is symmetric (= well-defined modulo permutation of arguments) because SymmetricAlgebra R M is commutative — reordering factors of a product leaves it invariant.

Main definitions

• SymmetricPower.toSymmetricAlgebra n — the linear map Sym[R]^n M →ₗ[R] SymmetricAlgebra R M.

[UPSTREAM] status

Natural home: Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean sibling, or a new Mathlib/LinearAlgebra/SymmetricAlgebra/Power.lean. Foundational step toward the graded iso SymmetricAlgebra R M ≃ₐ ⨁_n Sym[R]^n M (Q1b.0b.2, mathlib TODO).

§1: The per-degree Sym^n M → SymmetricAlgebra R M map

For each n, the symmetric multilinear product (g : Fin n → M) ↦ ∏ᵢ ι(g i) ∈ SymmetricAlgebra R M is symmetric (by commutativity of SymmetricAlgebra) and so factors through Sym[R]^n M via the universal property (SymmetricPower.lift).

noncomputable def SymmetricPower.toSymmetricAlgebra {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : SymmetricPower R (Fin n) M →ₗ[R] SymmetricAlgebra R M

The canonical linear map Sym[R]^n M →ₗ[R] SymmetricAlgebra R M. Sends a symmetric tensor power of n vectors to their product in the symmetric algebra.

Equations

• SymmetricPower.toSymmetricAlgebra n = SymmetricPower.lift (SymmetricPower.productMultilinear✝ n) ⋯

@[simp]

theorem SymmetricPower.toSymmetricAlgebra_tprod {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (g : Fin n → M) : (toSymmetricAlgebra n) ((tprod R) g) = (List.ofFn fun (i : Fin n) => (SymmetricAlgebra.ι R M) (g i)).prod

@[simp]

theorem SymmetricPower.toSymmetricAlgebra_one_tprod {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : (toSymmetricAlgebra 1) (⨂ₛ[R] (x_1 : Fin 1), x) = (SymmetricAlgebra.ι R M) x

For n = 1, toSymmetricAlgebra recovers ι (composed with the canonical iso Sym[R]^1 M ≅ M).

Specifically: toSymmetricAlgebra 1 (tprod R (fun _ => x)) = ι(x).

@[simp]

theorem SymmetricPower.toSymmetricAlgebra_zero_tprod {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (g : Fin 0 → M) : (toSymmetricAlgebra 0) ((tprod R) g) = 1

For n = 0, toSymmetricAlgebra sends tprod of the empty function to 1 ∈ SymmetricAlgebra R M.