Symmetric tensor power of a semimodule over a commutative semiring

We define the ι-indexed symmetric tensor power of M as the PiTensorProduct quotiented by the relation that the tprod of ι elements is equal to the tprod of the same elements permuted by a permutation of ι. We denote this space by Sym[R] ι M, and the canonical multilinear map from ι → M to Sym[R] ι M by ⨂ₛ[R] i, f i. We also reserve the notation Sym[R]^n M for the nth symmetric tensor power of M, which is the symmetric tensor power indexed by Fin n.

Main definitions:

• SymmetricPower.module: the symmetric tensor power is a module over R.

TODO:

• Grading: show that there is a map Sym[R]^i M × Sym[R]^j M → Sym[R]^(i + j) M that is associative and commutative, and that n ↦ Sym[R]^n M is a graded (semi)ring and algebra.
• Universal property: linear maps from Sym[R]^n M to N correspond to symmetric multilinear maps M ^ n to N.
• Relate to homogeneous (multivariate) polynomials of degree n.

inductive SymmetricPower.Rel (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (PiTensorProduct R fun (x : ι) => M) → (PiTensorProduct R fun (x : ι) => M) → Prop

The relation on the ι-indexed tensor power of M where two tensors are equal if they are related by a permutation of ι.

• perm {R ι : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (e : Equiv.Perm ι) (f : ι → M) : Rel R ι M ((PiTensorProduct.tprod R) fun (i : ι) => f i) ((PiTensorProduct.tprod R) fun (i : ι) => f (e i))

noncomputable def SymmetricPower (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : Type (max u v)

The ι-indexed symmetric tensor power of a semimodule M over a commutative semiring R is the quotient of the ι-indexed tensor power of M by the relation that two tensors are equal if they are related by a permutation of ι.

def TensorProduct.«termSym[_]__» : Lean.ParserDescr

The ι-indexed symmetric tensor power of a semimodule M over a commutative semiring R is the quotient of the ι-indexed tensor power of M by the relation that two tensors are equal if they are related by a permutation of ι.

def TensorProduct.«termSym[_]^__» : Lean.ParserDescr

The nth symmetric tensor power of a semimodule M over a commutative semiring R

@[implicit_reducible]

noncomputable instance SymmetricPower.instAddCommMonoid (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : AddCommMonoid (SymmetricPower R ι M)

@[implicit_reducible]

noncomputable instance SymmetricPower.instAddCommGroup (ι R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] : AddCommGroup (SymmetricPower R ι M)

theorem SymmetricPower.smul {R ι : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (x y : PiTensorProduct R fun (x : ι) => M) (h : (addConGen (Rel R ι M)) x y) : (addConGen (Rel R ι M)) (r • x) (r • y)

noncomputable def SymmetricPower.smul' {R : Type u} (ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] (r : R) : SymmetricPower R ι M →+ SymmetricPower R ι M

Scalar multiplication by r : R. Use • instead.

@[implicit_reducible]

noncomputable instance SymmetricPower.module (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : Module R (SymmetricPower R ι M)

noncomputable def SymmetricPower.mk (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (PiTensorProduct R fun (x : ι) => M) →ₗ[R] SymmetricPower R ι M

The canonical map from the ι-indexed tensor power to the symmetric tensor power.

noncomputable def SymmetricPower.tprod (R : Type u) {ι : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] : MultilinearMap R (fun (x : ι) => M) (SymmetricPower R ι M)

The multilinear map that takes ι-indexed elements of M and returns their symmetric tensor power. Denoted ⨂ₛ[R] i, f i.

def SymmetricPower.«term⨂ₛ[_]_,_» : Lean.ParserDescr

The multilinear map that takes ι-indexed elements of M and returns their symmetric tensor power. Denoted ⨂ₛ[R] i, f i.

@[simp]

theorem SymmetricPower.tprod_equiv {R ι : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (e : Equiv.Perm ι) (f : ι → M) : (⨂ₛ[R] (i : ι), f (e i)) = ⨂ₛ[R] (i : ι), f i

@[simp]

theorem SymmetricPower.domDomCongr_tprod {R : Type u} (ι : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (e : Equiv.Perm ι) : MultilinearMap.domDomCongr e (tprod R) = tprod R

theorem SymmetricPower.range_mk (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (mk R ι M).range = ⊤

theorem SymmetricPower.span_tprod_eq_top (R ι : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : Submodule.span R (Set.range ⇑(tprod R)) = ⊤

The pure tensors (i.e. the elements of the image of SymmetricPower.tprod) span the symmetric tensor power.