Permuting tensor factors

This file defines the symmetric-group action on a power of a module by permuting its tensor factors. Mathlib's Representation.asAlgebraHom then extends the action linearly to the group algebra, which is the action used by Young symmetrizers.

The construction is the first target in Layer 2 of the classical-groups roadmap and the first construction in Layer 8 of the Schur--Weyl roadmap. It reuses PiTensorProduct.reindex; the convention is σ • (⨂ₜ i, m i) = ⨂ₜ i, m (σ⁻¹ i).

Main definitions

• PiTensorProduct.reindexRepresentation is the permutation action for an arbitrary index type and module.
• permTensorAction specializes it to (Fin n → R)^{⊗d}.
• permTensorActionAlgHom is its Representation.asAlgebraHom extension to R[S_d].
• TauCeti.tensorPowerBasis is the monomial basis of (Rⁿ)^{⊗d}, on which the action is a reindexing.

noncomputable def PiTensorProduct.reindexRepresentation (R : Type u) (M : Type v) (ι : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] : Representation R (Equiv.Perm ι) (PiTensorProduct R fun (x : ι) => M)

The representation of the permutation group of ι on the ι-indexed tensor power, acting by reindexing the tensor factors.

Equations

• PiTensorProduct.reindexRepresentation R M ι = { toFun := fun (σ : Equiv.Perm ι) => ↑(PiTensorProduct.reindex R (fun (x : ι) => M) σ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PiTensorProduct.reindexRepresentation_apply (R : Type u) (M : Type v) (ι : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] (σ : Equiv.Perm ι) : (reindexRepresentation R M ι) σ = ↑(reindex R (fun (x : ι) => M) σ)

The permutation representation acts by PiTensorProduct.reindex.

theorem PiTensorProduct.commute_reindexRepresentation_map (R : Type u) (M : Type v) (ι : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] (σ : Equiv.Perm ι) (f : M →ₗ[R] M) : Commute ((reindexRepresentation R M ι) σ) (map fun (x : ι) => f)

Permuting factors commutes with applying the same linear map in every tensor factor.

theorem PiTensorProduct.commute_reindexRepresentation_asAlgebraHom_map (R : Type u) (M : Type v) (ι : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : MonoidAlgebra R (Equiv.Perm ι)) (f : M →ₗ[R] M) : Commute ((reindexRepresentation R M ι).asAlgebraHom a) (map fun (x : ι) => f)

Every element of the group algebra commutes with applying the same linear map in every tensor factor.

theorem PiTensorProduct.reindexRepresentation_asAlgebraHom_apply_tprod (R : Type u) (M : Type v) (ι : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : MonoidAlgebra R (Equiv.Perm ι)) (m : ι → M) : ((reindexRepresentation R M ι).asAlgebraHom a) ((tprod R) m) = a.coeff.sum fun (σ : Equiv.Perm ι) (r : R) => r • (tprod R) fun (i : ι) => m ((Equiv.symm σ) i)

The group-algebra action on a pure tensor is the corresponding finite linear combination of reindexed pure tensors.

noncomputable def TauCeti.permTensorAction (R : Type u) (n d : ℕ) [CommSemiring R] : Representation R (Equiv.Perm (Fin d)) (PiTensorProduct R fun (x : Fin d) => Fin n → R)

The symmetric-group action on (Fin n → R)^{⊗d} by permutation of tensor factors.

Equations

• TauCeti.permTensorAction R n d = PiTensorProduct.reindexRepresentation R (Fin n → R) (Fin d)

theorem TauCeti.permTensorAction_def (R : Type u) (n d : ℕ) [CommSemiring R] : permTensorAction R n d = PiTensorProduct.reindexRepresentation R (Fin n → R) (Fin d)

The symmetric-group action on (Fin n → R)^{⊗d} is the reindexing representation for the index type Fin d.

@[simp]

theorem TauCeti.permTensorAction_apply (R : Type u) (n d : ℕ) [CommSemiring R] (σ : Equiv.Perm (Fin d)) : (permTensorAction R n d) σ = ↑(PiTensorProduct.reindex R (fun (x : Fin d) => Fin n → R) σ)

A permutation acts on (Fin n → R)^{⊗d} by PiTensorProduct.reindex.

noncomputable def TauCeti.permTensorActionAlgHom (R : Type u) (n d : ℕ) [CommSemiring R] : MonoidAlgebra R (Equiv.Perm (Fin d)) →ₐ[R] Module.End R (PiTensorProduct R fun (x : Fin d) => Fin n → R)

The group-algebra action of R[S_d] on (Fin n → R)^{⊗d} induced by factor permutations.

Equations

• TauCeti.permTensorActionAlgHom R n d = (TauCeti.permTensorAction R n d).asAlgebraHom

theorem TauCeti.permTensorActionAlgHom_def (R : Type u) (n d : ℕ) [CommSemiring R] : permTensorActionAlgHom R n d = (permTensorAction R n d).asAlgebraHom

The group-algebra action of R[S_d] is the linear extension of permTensorAction.

theorem TauCeti.permTensorActionAlgHom_of (R : Type u) (n d : ℕ) [CommSemiring R] (σ : Equiv.Perm (Fin d)) : (permTensorActionAlgHom R n d) ((MonoidAlgebra.of R (Equiv.Perm (Fin d))) σ) = (permTensorAction R n d) σ

A single permutation, viewed in the group algebra, acts by permTensorAction.

theorem TauCeti.permTensorActionAlgHom_eq_sum (R : Type u) (n d : ℕ) [CommSemiring R] (a : MonoidAlgebra R (Equiv.Perm (Fin d))) : (permTensorActionAlgHom R n d) a = ∑ σ : Equiv.Perm (Fin d), a.coeff σ • (permTensorAction R n d) σ

The group-algebra action of a ∈ R[S_d] is the coefficient-weighted sum of the permutation actions.

@[simp]

theorem TauCeti.permTensorActionAlgHom_apply_tprod (R : Type u) (n d : ℕ) [CommSemiring R] (a : MonoidAlgebra R (Equiv.Perm (Fin d))) (m : Fin d → Fin n → R) : ((permTensorActionAlgHom R n d) a) ((PiTensorProduct.tprod R) m) = a.coeff.sum fun (σ : Equiv.Perm (Fin d)) (r : R) => r • (PiTensorProduct.tprod R) fun (i : Fin d) => m ((Equiv.symm σ) i)

The group-algebra action on a pure tensor of (Fin n → R)^{⊗d} is the corresponding finite linear combination of reindexed pure tensors.

noncomputable def TauCeti.tensorPowerBasis (R : Type u) (n d : ℕ) [CommSemiring R] : Module.Basis (Fin d → Fin n) R (PiTensorProduct R fun (x : Fin d) => Fin n → R)

The monomial basis of (Rⁿ)^{⊗d}: the basis vector at f : Fin d → Fin n is the pure tensor whose i-th factor is the f i-th standard basis vector of Rⁿ.

Equations

• TauCeti.tensorPowerBasis R n d = Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun R (Fin n)

theorem TauCeti.tensorPowerBasis_def (R : Type u) (n d : ℕ) [CommSemiring R] : tensorPowerBasis R n d = Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun R (Fin n)

The monomial basis is the tensor product of the standard bases. The definition is not exposed, so this is its defining equation, used to compare it with the Basis.piTensorProduct spelling of the weight theory.

@[simp]

theorem TauCeti.tensorPowerBasis_apply (R : Type u) (n d : ℕ) [CommSemiring R] (f : Fin d → Fin n) : (tensorPowerBasis R n d) f = (PiTensorProduct.tprod R) fun (i : Fin d) => Pi.single (f i) 1

theorem TauCeti.permTensorAction_tensorPowerBasis (R : Type u) (n d : ℕ) [CommSemiring R] (σ : Equiv.Perm (Fin d)) (f : Fin d → Fin n) : ((permTensorAction R n d) σ) ((tensorPowerBasis R n d) f) = (tensorPowerBasis R n d) fun (i : Fin d) => f ((Equiv.symm σ) i)

A permutation acts on the monomial basis of (Rⁿ)^{⊗d} by precomposing the index function with its inverse.

theorem TauCeti.permTensorActionAlgHom_single_tensorPowerBasis (R : Type u) (n d : ℕ) [CommSemiring R] (ρ : Equiv.Perm (Fin d)) (r : R) (f : Fin d → Fin n) : ((permTensorActionAlgHom R n d) (MonoidAlgebra.single ρ r)) ((tensorPowerBasis R n d) f) = r • (tensorPowerBasis R n d) fun (i : Fin d) => f ((Equiv.symm ρ) i)

A group-algebra basis element acts on a monomial basis vector by precomposition and scaling.

theorem TauCeti.permTensorActionAlgHom_apply_tensorPowerBasis (R : Type u) (n d : ℕ) [CommSemiring R] (a : MonoidAlgebra R (Equiv.Perm (Fin d))) (f : Fin d → Fin n) : ((permTensorActionAlgHom R n d) a) ((tensorPowerBasis R n d) f) = ∑ σ ∈ a.coeff.support, a.coeff σ • (tensorPowerBasis R n d) fun (i : Fin d) => f ((Equiv.symm σ) i)

The group-algebra action on a monomial basis vector is the coefficient-weighted sum of the precomposed monomial basis vectors.