Universal property of SymmetricPower R ι M

For an R-module M and an indexing type ι, the symmetric tensor power Sym[R] ι M (mathlib's SymmetricPower) is universal for symmetric multilinear maps out of ι → M: any multilinear map f : (ι → M) → N that is invariant under permutation of arguments factors uniquely through Sym[R] ι M.

This closes the universal property TODO in Mathlib/LinearAlgebra/TensorPower/Symmetric.lean.

Main definitions

• SymmetricPower.lift: given a multilinear map f : (ι → M) → N with f.domDomCongr σ = f for every permutation σ : Equiv.Perm ι, returns the unique linear map Sym[R] ι M →ₗ[R] N factoring f through tprod.
• SymmetricPower.lift_tprod: characterization that lift f composed with tprod recovers f.

References

• @cite{oudom-guin-2008} §2 (Lemma 2.5) — symmetric multilinear lift on rank-n symmetric power.

[UPSTREAM] status

Natural home in Mathlib/LinearAlgebra/TensorPower/Symmetric.lean (or sibling file). Closes the documented "Universal property" TODO listed in that file's preamble.

§1: The lift of a symmetric multilinear map

Given a multilinear map f : (ι → M) → N that is invariant under permutation of arguments (f.domDomCongr σ = f for all σ), we lift to a linear map Sym[R] ι M →ₗ[R] N.

Construction: lift f to a linear map g : (⨂[R] M) →ₗ[R] N via PiTensorProduct.lift. Verify that g respects the symmetric quotient relation SymmetricPower.Rel. Descend to Sym[R] ι M →ₗ[R] N via AddCon.lift plus R-action compatibility.

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) (hsym : ∀ (σ : Equiv.Perm ι), MultilinearMap.domDomCongr σ f = f) : SymmetricPower R ι M →ₗ[R] N

Universal property of SymmetricPower R ι M: a multilinear map (ι → M) → N invariant under permutation lifts uniquely to a linear map Sym[R] ι M →ₗ[R] N.

Closes the universal-property TODO in Mathlib/LinearAlgebra/TensorPower/Symmetric.lean.

Equations

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

@[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) (hsym : ∀ (σ : Equiv.Perm ι), MultilinearMap.domDomCongr σ f = f) (g : ι → M) : (lift f hsym) ((tprod R) g) = f g

@[simp]

theorem SymmetricPower.lift_comp_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) (hsym : ∀ (σ : Equiv.Perm ι), MultilinearMap.domDomCongr σ f = f) : (lift f hsym).compMultilinearMap (tprod R) = f

theorem SymmetricPower.lift_unique {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) (hsym : ∀ (σ : Equiv.Perm ι), MultilinearMap.domDomCongr σ f = f) {g : SymmetricPower R ι M →ₗ[R] N} (hg : g.compMultilinearMap (tprod R) = f) : g = lift f hsym

Uniqueness of the lift: any linear map Sym[R] ι M →ₗ N that agrees with f on the image of tprod equals lift f hsym.