The universal property of the symmetric tensor power

A multilinear map f : Mⁱ → N that is unchanged by permuting its arguments factors uniquely through the symmetric tensor power. This file builds that factorization, SymmetricPower.lift, as the descent of PiTensorProduct.lift f through the quotient map SymmetricPower.mk: the defining relation of the quotient identifies a pure tensor with each of its reorderings, and f takes the same value on all of them.

Together with SymmetricPower.ext, which says that a linear map out of the symmetric power is determined by its values on pure symmetric tensors, this says that composing with the pure symmetric tensor ⨂ₛ is a bijection from the linear maps Sym[R] ι M →ₗ[R] N onto the permutation-invariant multilinear maps Mⁱ → N, for every N.

Main definitions

• SymmetricPower.lift: the linear map on the symmetric power induced by a permutation-invariant multilinear map.

Main results

• SymmetricPower.lift_tprod: lift f agrees with f on pure symmetric tensors.
• SymmetricPower.ext: linear maps out of a symmetric power agreeing on pure symmetric tensors are equal.

noncomputable def SymmetricPower.lift {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : ι) => M) N) (hf : ∀ (e : Equiv.Perm ι), MultilinearMap.domDomCongr e f = f) : SymmetricPower R ι M →ₗ[R] N

The universal property of the symmetric tensor power: a multilinear map that is unchanged by permuting its arguments descends to a linear map on the symmetric power.

Equations

• SymmetricPower.lift f hf = { toFun := ⇑((addConGen (SymmetricPower.Rel R ι M)).lift (PiTensorProduct.lift f).toAddMonoidHom ⋯), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricPower.lift_mk {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : ι) => M) N) (hf : ∀ (e : Equiv.Perm ι), MultilinearMap.domDomCongr e f = f) (x : PiTensorProduct R fun (x : ι) => M) : (lift f hf) ((mk R ι M) x) = (PiTensorProduct.lift f) x

The descent of a multilinear map commutes with the quotient map from the tensor power.

@[simp]

theorem SymmetricPower.lift_tprod {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : ι) => M) N) (hf : ∀ (e : Equiv.Perm ι), MultilinearMap.domDomCongr e f = f) (m : ι → M) : (lift f hf) (⨂ₛ[R] (i : ι), m i) = f m

The descent of a multilinear map agrees with it on pure symmetric tensors.

theorem SymmetricPower.ext {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {g h : SymmetricPower R ι M →ₗ[R] N} (hgh : ∀ (m : ι → M), g (⨂ₛ[R] (i : ι), m i) = h (⨂ₛ[R] (i : ι), m i)) : g = h

A linear map out of a symmetric power is determined by its values on pure symmetric tensors.

theorem SymmetricPower.ext_iff {R ι : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {g h : SymmetricPower R ι M →ₗ[R] N} : g = h ↔ ∀ (m : ι → M), g (⨂ₛ[R] (i : ι), m i) = h (⨂ₛ[R] (i : ι), m i)