The coordinates of a pure symmetric tensor

TauCeti/LinearAlgebra/SymmetricPower/Basis.lean builds the basis Module.Basis.symmetricPower of Sym[R]^n M induced by a basis b : Basis κ R M, and reads off the coordinates of a pure symmetric tensor whose factors are basis vectors: it is a basis vector. This file reads off the coordinates of a pure symmetric tensor ⨂ₛ v whose factors are arbitrary.

Expanding each factor in the basis and using multilinearity writes ⨂ₛ v as a sum, over the ordered tuples p : Fin n → κ, of the pure tensors ⨂ₛ i, b (p i), each scaled by ∏ i, b.repr (v i) (p i). Collecting the terms by the unordered tuple TauCeti.Sym.ofFn p underlying p gives the coordinate at s as a sum over the orderings of s.

Two consequences are what the file exists for.

• At a constant index the sum has one term. Only the constant tuple orders the unordered tuple (k, …, k), so the coordinate of ⨂ₛ v there is the plain product ∏ i, b.repr (v i) k of one coordinate of each factor.
• A pure power has no vanishing coordinate. The product ∏ i, b.repr (v i) (p i) depends only on TauCeti.Sym.ofFn p when all the factors v i are equal, so the sum over the orderings of s has all its terms equal and no cancellation is possible: over a domain of characteristic zero, ⨂ₛ (u, …, u) has a nonzero coordinate at every s as soon as every coordinate of u is nonzero. For a general pure tensor this fails, the terms attached to different orderings being unrelated.

Main results

• SymmetricPower.repr_basis_symmetricPower_tprod: the coordinate of a pure symmetric tensor at s is the sum, over the orderings of s, of the products of the corresponding coordinates of the factors.
• SymmetricPower.repr_basis_symmetricPower_tprod_ofFn_const: its value at a constant unordered tuple is a single product.
• SymmetricPower.repr_basis_symmetricPower_tprod_const_ne_zero: a pure power of a vector with nonzero coordinates has nonzero coordinates.

References

• W. Fulton, J. Harris, Representation Theory: A First Course, Springer GTM 129 (1991), Appendix B, for the monomial basis of a symmetric power.

theorem SymmetricPower.repr_basis_symmetricPower_tprod {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) [Fintype κ] [DecidableEq κ] (v : Fin n → M) (s : Sym κ n) : ((Module.Basis.symmetricPower n b).repr (⨂ₛ[R] (i : Fin n), v i)) s = ∑ p : Fin n → κ with TauCeti.Sym.ofFn p = s, ∏ i : Fin n, (b.repr (v i)) (p i)

The coordinates of a pure symmetric tensor. Expanding each factor of ⨂ₛ v in the basis b and collecting the resulting pure tensors of basis vectors by the unordered tuple of indices they use, the coordinate at s is the sum, over the ordered tuples p underlying s, of the products of the corresponding coordinates of the factors.

For factors that are themselves basis vectors this recovers Module.Basis.symmetricPower_apply; the content here is the general case.

@[simp]

theorem SymmetricPower.repr_basis_symmetricPower_tprod_ofFn_const {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) (v : Fin n → M) (k : κ) : ((Module.Basis.symmetricPower n b).repr (⨂ₛ[R] (i : Fin n), v i)) (TauCeti.Sym.ofFn fun (x : Fin n) => k) = ∏ i : Fin n, (b.repr (v i)) k

The coordinates of a pure symmetric tensor at a constant unordered tuple. The only ordering of (k, …, k) is the constant tuple, so the sum of SymmetricPower.repr_basis_symmetricPower_tprod collapses to a single product: one coordinate of each factor.

The basis index type need not be finite: it is enough to expand each factor over the finitely many indices it uses, together with k.

theorem SymmetricPower.repr_basis_symmetricPower_tprod_const_ne_zero {R : Type} {M : Type v} {κ : Type w} {n : ℕ} [CommSemiring R] [IsDomain R] [CharZero R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) {u : M} (hu : ∀ (k : κ), (b.repr u) k ≠ 0) (s : Sym κ n) : ((Module.Basis.symmetricPower n b).repr (⨂ₛ[R] (x : Fin n), u)) s ≠ 0

A pure power has no vanishing coordinate. When all the factors are the same vector u, every term of the sum of SymmetricPower.repr_basis_symmetricPower_tprod is the same product of coordinates of u, so the coordinate at s is that product times the number of orderings of s, which is positive. Over a domain of characteristic zero neither factor vanishes.

Nothing like this holds for a general pure tensor: the terms attached to different orderings of s can cancel.