Symmetric powers as homogeneous symmetric polynomials

Multiplication of symmetric-algebra generators identifies the symmetric tensor power of any module with the homogeneous component of the same degree. Injectivity comes from a left inverse: the generators act on the symmetric tensors of all degrees by commuting multiplication operators, so the symmetric algebra acts there as well. For a free module the identification sends the symmetric tensor basis to the monomial basis. This identifies the quotient-tensor and polynomial descriptions of symmetric powers, allowing constructions on symmetric tensors to be used degreewise on the symmetric algebra.

The scalar semiring lies in Type because Mathlib's SymmetricPower R ι M requires R and ι to share a universe, and Sym[R]^n M uses ι = Fin n. This is also the universe convention of Module.Basis.symmetricPower, used in the basis comparison below. The module and its basis index type have independent universes.

Main declarations

• TauCeti.SymmetricPower.toSymmetricAlgebra multiplies the generators of a pure symmetric tensor.
• TauCeti.SymmetricPower.toHomogeneous restricts multiplication to its homogeneous component.
• TauCeti.SymmetricPower.equivHomogeneous is the resulting equivalence.

References

The multiplication map and its basis comparison are adapted from the closed Tau Ceti PR https://github.com/TauCetiProject/TauCeti/pull/18162 (feat: construct degreewise PBW symmetrization).

noncomputable def TauCeti.SymmetricPower.toSymmetricAlgebra (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : SymmetricPower R (Fin n) M →ₗ[R] SymmetricAlgebra R M

Multiplication of the canonical generators, descended to the symmetric tensor power.

@[simp]

theorem TauCeti.SymmetricPower.toSymmetricAlgebra_tprod (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : Fin n → M) : (toSymmetricAlgebra R M n) (⨂ₛ[R] (i : Fin n), m i) = ∏ i : Fin n, (SymmetricAlgebra.ι R M) (m i)

A pure symmetric tensor maps to the product of its generators.

theorem TauCeti.SymmetricPower.toSymmetricAlgebra_mem_homogeneousSubmodule (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : SymmetricPower R (Fin n) M) : (toSymmetricAlgebra R M n) x ∈ SymmetricAlgebra.homogeneousSubmodule R M n

Multiplication preserves the degree of a symmetric tensor.

noncomputable def TauCeti.SymmetricPower.toHomogeneous (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : SymmetricPower R (Fin n) M →ₗ[R] ↥(SymmetricAlgebra.homogeneousSubmodule R M n)

Multiplication with codomain restricted to the homogeneous component of the same degree.

@[simp]

theorem TauCeti.SymmetricPower.coe_toHomogeneous_apply (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : SymmetricPower R (Fin n) M) : ↑((toHomogeneous R M n) x) = (toSymmetricAlgebra R M n) x

The homogeneous multiplication map has ordinary multiplication as its underlying map.

theorem TauCeti.SymmetricPower.range_toSymmetricAlgebra (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : (toSymmetricAlgebra R M n).range = SymmetricAlgebra.homogeneousSubmodule R M n

The image of multiplication is exactly the homogeneous component of the same degree.

A left inverse of multiplication

The generators act on the symmetric tensors of all degrees by commuting multiplication operators, so the symmetric algebra acts there too. Acting on the degree-zero unit tensor and reading off degree n gives a left inverse of multiplication on Sym[R]^n M, with no assumption on M.

theorem TauCeti.SymmetricPower.toSymmetricAlgebra_symmetricPower_apply (R : Type) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {κ : Type w} (b : Module.Basis κ R M) (n : ℕ) (s : Sym κ n) : (toSymmetricAlgebra R M n) ((Module.Basis.symmetricPower n b) s) = ↑((b.symmetricAlgebraHomogeneous n) s)

Multiplication identifies the symmetric tensor basis with the homogeneous monomial basis.

theorem TauCeti.SymmetricPower.toSymmetricAlgebra_injective {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : Function.Injective ⇑(toSymmetricAlgebra R M n)

Multiplication embeds the symmetric tensor power of any module into its symmetric algebra, over any commutative semiring.

noncomputable def TauCeti.SymmetricPower.equivHomogeneous {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : SymmetricPower R (Fin n) M ≃ₗ[R] ↥(SymmetricAlgebra.homogeneousSubmodule R M n)

The symmetric tensor power of a module is canonically its degree-n homogeneous symmetric-algebra component.

@[simp]

theorem TauCeti.SymmetricPower.coe_equivHomogeneous_apply {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : SymmetricPower R (Fin n) M) : ↑((equivHomogeneous n) x) = (toSymmetricAlgebra R M n) x

The homogeneous equivalence has multiplication as its underlying map.

@[simp]

theorem TauCeti.SymmetricPower.toLinearMap_equivHomogeneous {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : ↑(equivHomogeneous n) = toHomogeneous R M n

The linear map underlying the homogeneous equivalence is homogeneous multiplication.

@[simp]

theorem TauCeti.SymmetricPower.equivHomogeneous_tprod {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : Fin n → M) : (equivHomogeneous n) (⨂ₛ[R] (i : Fin n), m i) = ⟨∏ i : Fin n, (SymmetricAlgebra.ι R M) (m i), ⋯⟩

The homogeneous equivalence sends a pure symmetric tensor to its product of generators.

@[simp]

theorem TauCeti.SymmetricPower.equivHomogeneous_symm_prod_ι {R : Type} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : Fin n → M) (h : ∏ i : Fin n, (SymmetricAlgebra.ι R M) (m i) ∈ SymmetricAlgebra.homogeneousSubmodule R M n) : (equivHomogeneous n).symm ⟨∏ i : Fin n, (SymmetricAlgebra.ι R M) (m i), h⟩ = ⨂ₛ[R] (i : Fin n), m i

The inverse homogeneous equivalence sends a product of generators to its pure tensor.