A basis of a symmetric tensor power

A basis b : Basis κ R M induces a basis of every symmetric tensor power Sym[R]^n M, indexed by the unordered n-tuples Sym κ n of basis indices: the basis vector at s is the pure symmetric tensor of the basis vectors listed by s. This is the symmetric counterpart of Basis.piTensorProduct, whose index type is the ordered tuples Fin n → κ, and of Module.Basis.exteriorPower, whose index type is the n-element subsets.

The coordinate map is built from the tensor-power basis: reading a pure tensor of basis vectors as the unordered tuple of its indices is invariant under permuting the factors, so it descends to the symmetric power by SymmetricPower.lift. Its inverse sends an unordered tuple to the pure symmetric tensor of the corresponding basis vectors, which is well defined because any two orderings of an unordered tuple differ by a permutation.

Main definitions

• SymmetricPower.tprodOfSym: the pure symmetric tensor whose factors are listed, without order, by a point of Sym κ n.
• Module.Basis.symmetricPower: the induced basis of Sym[R]^n M.

Main results

• Module.Basis.map_symmetricPower_of_apply: an endomorphism diagonal in a basis is diagonal in the induced basis of the symmetric power, with eigenvalue the product of the eigenvalues listed by the index.
• SymmetricPower.finrank_eq: the rank of Sym[R]^n M is Nat.multichoose (finrank R M) n.
• Module.Basis.trace_map_symmetricPower_of_apply: the trace on Sym[R]^n M of an endomorphism that is diagonal in a basis is the sum, over the unordered n-tuples of basis indices, of the product of the corresponding eigenvalues. This is the complete homogeneous symmetric polynomial in the eigenvalues, and is the symmetric counterpart of Module.Basis.trace_map_exteriorPower_of_apply.

Pure symmetric tensors indexed by unordered tuples

noncomputable def SymmetricPower.tprodOfSym (R : Type) {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (v : κ → M) (s : Sym κ n) : SymmetricPower R (Fin n) M

The pure symmetric tensor whose factors are the members of a family v : κ → M listed, with multiplicity but without order, by a point of Sym κ n.

Equations

• SymmetricPower.tprodOfSym R v s = ⨂ₛ[R] (i : Fin n), v (SymmetricPower.orderOfSym✝ s i)

@[simp]

theorem SymmetricPower.tprodOfSym_ofFn {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (v : κ → M) (f : Fin n → κ) : tprodOfSym R v (TauCeti.Sym.ofFn f) = ⨂ₛ[R] (i : Fin n), v (f i)

Reading off an ordered tuple of factors gives the pure symmetric tensor of those factors: the choice of ordering hidden in the definition of tprodOfSym does not matter.

The coordinate map in a basis

noncomputable def Module.Basis.symmetricPower {R : Type} {M : Type v} {κ : Type w} (n : ℕ) [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : Basis (Sym κ n) R (SymmetricPower R (Fin n) M)

A basis of the symmetric tensor power: a basis of M induces a basis of Sym[R]^n M indexed by the unordered n-tuples of basis indices.

Equations

• Module.Basis.symmetricPower n b = { repr := SymmetricPower.linearEquivFinsupp✝ n b }

@[simp]

theorem Module.Basis.symmetricPower_apply {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (s : Sym κ n) : (symmetricPower n b) s = SymmetricPower.tprodOfSym R (⇑b) s

The basis vector of Sym[R]^n M indexed by an unordered tuple s : Sym κ n of basis indices is the pure symmetric tensor SymmetricPower.tprodOfSym R b s of the corresponding basis vectors.

theorem Module.Basis.map_symmetricPower_of_apply {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (hf : ∀ (i : κ), f (b i) = a i • b i) (s : Sym κ n) : (SymmetricPower.map f) ((symmetricPower n b) s) = (Multiset.map a ↑s).prod • (symmetricPower n b) s

An endomorphism diagonal in a basis is diagonal in the induced basis of the symmetric power: the basis vector indexed by s is an eigenvector, with eigenvalue the product of the eigenvalues listed by s. Summing these eigenvalues gives the trace, Module.Basis.trace_map_symmetricPower_of_apply.

Freeness and rank

instance SymmetricPower.free {R : Type} {M : Type v} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : Module.Free R (SymmetricPower R (Fin n) M)

A symmetric power of a free module is free, on the unordered tuples of basis indices.

theorem SymmetricPower.finrank_eq {R : Type} {M : Type v} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] [Module.Free R M] [Module.Finite R M] : Module.finrank R (SymmetricPower R (Fin n) M) = (Module.finrank R M).multichoose n

The rank of a symmetric power of a finite free module: the number of unordered n-tuples of basis indices, Nat.multichoose (finrank R M) n.

Traces

theorem Module.Basis.trace_map_symmetricPower_of_apply {R : Type} {M : Type v} {κ : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype κ] [DecidableEq κ] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (n : ℕ) (hf : ∀ (i : κ), f (b i) = a i • b i) : (LinearMap.trace R (SymmetricPower R (Fin n) M)) (SymmetricPower.map f) = ∑ s : Sym κ n, (Multiset.map a ↑s).prod

If an endomorphism of a semimodule over a commutative semiring is diagonal in a finite basis, then its trace on the nth symmetric power is the sum, over the unordered n-tuples of basis indices, of the product of the corresponding eigenvalues.