The symmetric algebra as a direct sum of symmetric powers

SymmetricPower.toSymmetricAlgebra : Sym[R] κ M →ₗ[R] SymmetricAlgebra R M sends ⨂ₛ[R] i, x i to ∏ i, ι R M (x i). It is the symmetric sibling of TensorPower.toTensorAlgebra, and its range is the Fintype.card κ-th power of the submodule LinearMap.range (ι R M). The decomposition TensorAlgebra.toDirectSum descends to the symmetric algebra, so that SymmetricAlgebra R M ≃ₗ[R] ⨁ n, Sym[R]^n M as for the tensor algebra, and toSymmetricAlgebra is injective on Sym[R]^n M. Together these identify the quotient Sym[R]^n M of the tensor power with the n-th power of the generating submodule of the symmetric algebra, the degree-n part of its grading. [UPSTREAM] Natural home Mathlib/LinearAlgebra/SymmetricAlgebra/ToSymmetricPower.lean, beside Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean.

Main definitions

• SymmetricPower.toSymmetricAlgebra: the map Sym[R] κ M →ₗ[R] SymmetricAlgebra R M.
• SymmetricAlgebra.toDirectSum, SymmetricAlgebra.ofDirectSum: the maps between SymmetricAlgebra R M and ⨁ n, Sym[R]^n M.
• SymmetricAlgebra.equivDirectSum: the linear equivalence they form.

Main statements

• SymmetricPower.range_toSymmetricAlgebra
• SymmetricAlgebra.toDirectSum_comp_toSymmetricAlgebra
• SymmetricPower.toSymmetricAlgebra_injective

Implementation notes

SymmetricAlgebra.toDirectSum is TensorAlgebra.toDirectSum followed by the quotient maps ⨂[R]^n M → Sym[R]^n M, descended along TensorAlgebra.symRingCon_toAddCon_le_ker: swapping two adjacent generators of a product of generators permutes the factors of one pure tensor. The statements about Sym[R]^n M take R : Type because mathlib's SymmetricPower R ι M puts R and ι in one universe.

TODO

• Upgrade SymmetricAlgebra.equivDirectSum to an algebra isomorphism once n ↦ Sym[R]^n M carries its graded commutative multiplication, a TODO of Mathlib/LinearAlgebra/TensorPower/Symmetric.lean.

def SymmetricPower.toSymmetricAlgebra {R κ : Type u} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype κ] : SymmetricPower R κ M →ₗ[R] SymmetricAlgebra R M

The linear map Sym[R] κ M →ₗ[R] SymmetricAlgebra R M sending ⨂ₛ[R] i, x i to ∏ i, ι R M (x i).

Equations

• SymmetricPower.toSymmetricAlgebra = SymmetricPower.lift (SymmetricAlgebra.ιMulti R M κ) ⋯

@[simp]

theorem SymmetricPower.toSymmetricAlgebra_tprod {R κ : Type u} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype κ] (x : κ → M) : toSymmetricAlgebra ((tprod R) x) = (SymmetricAlgebra.ιMulti R M κ) x

theorem SymmetricPower.range_toSymmetricAlgebra (R κ : Type u) (M : Type u_1) [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype κ] : toSymmetricAlgebra.range = (SymmetricAlgebra.ι R M).range ^ Fintype.card κ

theorem SymmetricPower.toSymmetricAlgebra_comp_mk {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : toSymmetricAlgebra ∘ₗ mk R (Fin n) M = (SymmetricAlgebra.algHom R M).toLinearMap ∘ₗ TensorPower.toTensorAlgebra

theorem SymmetricPower.lmap_mk_toDirectSum_mul_ι_mul_ι_mul {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : TensorAlgebra R M) (x y : M) : (DirectSum.lmap fun (n : ℕ) => mk R (Fin n) M) (TensorAlgebra.toDirectSum (a * ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y) * b)) = (DirectSum.lmap fun (n : ℕ) => mk R (Fin n) M) (TensorAlgebra.toDirectSum (a * ((TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x) * b))

Decomposing the tensor algebra into symmetric powers forgets the order of two adjacent generators, in any two-sided context.

noncomputable def SymmetricAlgebra.toDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] : SymmetricAlgebra R M →ₗ[R] DirectSum ℕ fun (n : ℕ) => SymmetricPower R (Fin n) M

The decomposition of SymmetricAlgebra R M into the symmetric powers of M: the descent of TensorAlgebra.toDirectSum followed by the quotient maps ⨂[R]^n M → Sym[R]^n M.

Equations

• One or more equations did not get rendered due to their size.

theorem SymmetricAlgebra.toDirectSum_algHom {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : TensorAlgebra R M) : toDirectSum ((algHom R M) a) = (DirectSum.lmap fun (n : ℕ) => SymmetricPower.mk R (Fin n) M) (TensorAlgebra.toDirectSum a)

@[simp]

theorem SymmetricAlgebra.toDirectSum_ιMulti {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : toDirectSum ((ιMulti R M (Fin n)) x) = (DirectSum.of (fun (i : ℕ) => SymmetricPower R (Fin i) M) n) ((SymmetricPower.tprod R) x)

theorem SymmetricAlgebra.toDirectSum_comp_toSymmetricAlgebra {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : toDirectSum ∘ₗ SymmetricPower.toSymmetricAlgebra = DirectSum.lof R ℕ (fun (n : ℕ) => SymmetricPower R (Fin n) M) n

noncomputable def SymmetricAlgebra.ofDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] : (DirectSum ℕ fun (n : ℕ) => SymmetricPower R (Fin n) M) →ₗ[R] SymmetricAlgebra R M

The sum of the maps SymmetricPower.toSymmetricAlgebra.

Equations

• SymmetricAlgebra.ofDirectSum = DirectSum.toModule R ℕ (SymmetricAlgebra R M) fun (x : ℕ) => SymmetricPower.toSymmetricAlgebra

@[simp]

theorem SymmetricAlgebra.ofDirectSum_of {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : SymmetricPower R (Fin n) M) : ofDirectSum ((DirectSum.of (fun (n : ℕ) => SymmetricPower R (Fin n) M) n) x) = SymmetricPower.toSymmetricAlgebra x

theorem SymmetricAlgebra.toDirectSum_comp_ofDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] : toDirectSum ∘ₗ ofDirectSum = LinearMap.id

@[simp]

theorem SymmetricAlgebra.toDirectSum_ofDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : DirectSum ℕ fun (n : ℕ) => SymmetricPower R (Fin n) M) : toDirectSum (ofDirectSum x) = x

theorem SymmetricAlgebra.ofDirectSum_comp_toDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] : ofDirectSum ∘ₗ toDirectSum = LinearMap.id

@[simp]

theorem SymmetricAlgebra.ofDirectSum_toDirectSum {R : Type} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : SymmetricAlgebra R M) : ofDirectSum (toDirectSum x) = x

noncomputable def SymmetricAlgebra.equivDirectSum (R : Type) (M : Type u_1) [CommSemiring R] [AddCommMonoid M] [Module R M] : SymmetricAlgebra R M ≃ₗ[R] DirectSum ℕ fun (n : ℕ) => SymmetricPower R (Fin n) M

The symmetric algebra is the direct sum of the symmetric powers, as a module.

Equations

• SymmetricAlgebra.equivDirectSum R M = LinearEquiv.ofLinearMap SymmetricAlgebra.toDirectSum SymmetricAlgebra.ofDirectSum ⋯ ⋯

@[simp]

theorem SymmetricAlgebra.equivDirectSum_symm_apply (R : Type) (M : Type u_1) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : DirectSum ℕ fun (n : ℕ) => SymmetricPower R (Fin n) M) : (equivDirectSum R M).symm a = ofDirectSum a

@[simp]

theorem SymmetricAlgebra.equivDirectSum_apply (R : Type) (M : Type u_1) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : (TensorAlgebra.symRingCon R M).toAddCon.Quotient) : (equivDirectSum R M) a = ((TensorAlgebra.symRingCon R M).toAddCon.lift ((DirectSum.lmap fun (n : ℕ) => SymmetricPower.mk R (Fin n) M) ∘ₗ TensorAlgebra.toDirectSum.toLinearMap).toAddMonoidHom ⋯) a

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