Functoriality of symmetric tensor powers, and the symmetrization back into the tensor power

This file equips Mathlib's symmetric tensor power with the linear map induced by a linear map of the underlying modules. It proves the expected action on pure tensors, identity law, and composition law. It also records that a symmetric power indexed by a finite type is finitely generated when its underlying module is.

It then builds the map back, SymmetricPower.toTensorPower : Sym[R] ι M →ₗ[R] ⨂[R] (_ : ι), M, for a finite index type. The symmetrization ∑_σ σ of the tensor power is constant on the fibres of the quotient map SymmetricPower.mk, because reindexing a pure tensor only permutes the terms of that sum, so it descends to the symmetric power; toTensorPower is that descent. It is the exact counterpart of Mathlib's exteriorPower.toTensorPower, and it takes a pure symmetric tensor to the sum of the pure tensors over all orderings of its factors.

Composing back the other way multiplies by the order of the permutation group: mk ∘ toTensorPower is (card ι)!, because each of the (card ι)! reorderings becomes the same symmetric tensor again. So as soon as (card ι)! is a unit -- for instance over a ℚ-algebra -- the symmetrization is injective, and it identifies the symmetric power with the image of the symmetrization operator inside the tensor power. That is the statement a Young symmetrizer of a one-row shape consumes.

Main definitions

• SymmetricPower.map is the map induced on a symmetric tensor power.
• SymmetricPower.toTensorPower is the symmetrization, from the symmetric power back into the tensor power.

Main results

• SymmetricPower.toTensorPower_tprod: the symmetrization of a pure symmetric tensor is the sum of the pure tensors over all orderings of its factors.
• SymmetricPower.mk_comp_toTensorPower: composing the symmetrization with the quotient map is multiplication by (card ι)!.
• SymmetricPower.toTensorPower_injective: the symmetrization is injective once (card ι)! is a unit.
• SymmetricPower.range_toTensorPower: its image is the image of the symmetrization operator on the tensor power.
• SymmetricPower.toTensorPower_comp_map: the symmetrization is natural in the module.

References

The quotient construction of SymmetricPower, including SymmetricPower.mk and SymmetricPower.tprod, is from Kenny Lau's Mathlib.LinearAlgebra.TensorPower.Symmetric.

noncomputable def SymmetricPower.map {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_1} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : SymmetricPower R ι M →ₗ[R] SymmetricPower R ι N

A linear map induces a linear map on every symmetric tensor power.

Equations

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

@[simp]

theorem SymmetricPower.map_mk {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_1} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : PiTensorProduct R fun (x : ι) => M) : (map f) ((mk R ι M) x) = (mk R ι N) ((PiTensorProduct.map fun (x : ι) => f) x)

The map on symmetric powers commutes with the quotient map from the tensor power.

@[simp]

theorem SymmetricPower.map_tprod {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_1} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (m : ι → M) : (map f) (⨂ₛ[R] (i : ι), m i) = ⨂ₛ[R] (i : ι), f (m i)

The map induced on symmetric powers sends a pure tensor to the tensor of the images.

@[simp]

theorem SymmetricPower.map_id {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] : map LinearMap.id = LinearMap.id

The map induced by the identity is the identity on the symmetric power.

@[simp]

theorem SymmetricPower.map_comp {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_1} {P : Type u_2} [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : map (g ∘ₗ f) = map g ∘ₗ map f

Symmetric powers preserve composition of linear maps.

The symmetrization back into the tensor power

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

The symmetrization, from the symmetric power back into the tensor power: the descent of the symmetrization operator ∑_σ σ through the quotient map SymmetricPower.mk.

This is the counterpart of Mathlib's exteriorPower.toTensorPower.

Equations

• SymmetricPower.toTensorPower R ι M = { toFun := ⇑((addConGen (SymmetricPower.Rel R ι M)).lift (SymmetricPower.symmetrizer✝ R ι M).toAddMonoidHom ⋯), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SymmetricPower.toTensorPower_mk {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (x : PiTensorProduct R fun (x : ι) => M) : (toTensorPower R ι M) ((mk R ι M) x) = ∑ σ : Equiv.Perm ι, (PiTensorProduct.reindex R (fun (x : ι) => M) σ) x

@[simp]

theorem SymmetricPower.toTensorPower_tprod {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (m : ι → M) : (toTensorPower R ι M) (⨂ₛ[R] (i : ι), m i) = ∑ σ : Equiv.Perm ι, (PiTensorProduct.tprod R) fun (i : ι) => m (σ i)

The symmetrization of a pure symmetric tensor is the sum of the pure tensors over all orderings of its factors.

theorem SymmetricPower.range_toTensorPower {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] : (toTensorPower R ι M).range = (∑ σ : Equiv.Perm ι, ↑(PiTensorProduct.reindex R (fun (x : ι) => M) σ)).range

The image of the symmetrization is the image of the symmetrization operator ∑_σ σ on the tensor power.

@[simp]

theorem SymmetricPower.mk_comp_toTensorPower {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] : mk R ι M ∘ₗ toTensorPower R ι M = (Fintype.card ι).factorial • LinearMap.id

Symmetrizing and then projecting back to the symmetric power multiplies by (card ι)!: the (card ι)! reorderings of a pure tensor all become the same symmetric tensor.

theorem SymmetricPower.toTensorPower_injective {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (h : IsUnit ↑(Fintype.card ι).factorial) : Function.Injective ⇑(toTensorPower R ι M)

The symmetrization is injective as soon as (card ι)! is a unit in the base ring, for instance over a ℚ-algebra.

theorem SymmetricPower.toTensorPower_comp_map {R ι : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] {N : Type v} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : toTensorPower R ι N ∘ₗ map f = (PiTensorProduct.map fun (x : ι) => f) ∘ₗ toTensorPower R ι M

The symmetrization is natural in the module.

instance SymmetricPower.finite {R ι : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Finite ι] [Module.Finite R M] : Module.Finite R (SymmetricPower R ι M)

A symmetric power indexed by a finite type is finitely generated when the underlying module is finitely generated.