The image of a group-algebra element acting on a tensor power

Permuting the tensor factors of ⨂[R]^d M commutes with the diagonal action of a representation ρ on M, so an element a of the group algebra R[S_d] acts on the tensor power by an intertwining map of ρ.tensorPower d with itself. Its image is therefore a subrepresentation of the tensor power. This file records that image and the elementary ways it depends on a: the identity cuts out the whole tensor power, the zero cuts out ⊥, multiplying on the right shrinks the image, and conjugating by a permutation moves the image by that permutation of the factors.

Nothing here is specific to Young symmetrizers; taking a to be one is the Weyl construction.

Main definitions

• TauCeti.tensorPowerPermMap: acting on ⨂[R]^d M by an element of R[S_d], as an intertwining map of the tensor power with itself.
• TauCeti.tensorPowerRange: the image of that map, as a subrepresentation.

References

• Classical groups roadmap, Layer 2, "Young symmetrizers and the Schur functor", whose Weyl-module target consumes this construction.

noncomputable def TauCeti.tensorPowerPermMap {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a : MonoidAlgebra R (Equiv.Perm (Fin d))) : (ρ.tensorPower d).IntertwiningMap (ρ.tensorPower d)

Acting on ⨂[R]^d M by an element of R[S_d], permuting tensor factors, is an intertwining map of the diagonal action of ρ on the tensor power with itself: the two actions commute.

Equations

• TauCeti.tensorPowerPermMap ρ d a = { toLinearMap := (PiTensorProduct.reindexRepresentation R M (Fin d)).asAlgebraHom a, isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.tensorPowerPermMap_toLinearMap {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a : MonoidAlgebra R (Equiv.Perm (Fin d))) : (tensorPowerPermMap ρ d a).toLinearMap = (PiTensorProduct.reindexRepresentation R M (Fin d)).asAlgebraHom a

The linear map underlying the tensor-power action of a group-algebra element.

noncomputable def TauCeti.tensorPowerRange {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a : MonoidAlgebra R (Equiv.Perm (Fin d))) : Subrepresentation (ρ.tensorPower d)

The image of a ∈ R[S_d], acting on ⨂[R]^d M by permuting tensor factors, as a subrepresentation of the d-th tensor power of ρ.

Equations

• TauCeti.tensorPowerRange ρ d a = Representation.IntertwiningMap.range (ρ.tensorPower d) (ρ.tensorPower d) (TauCeti.tensorPowerPermMap ρ d a)

@[simp]

theorem TauCeti.tensorPowerRange_toSubmodule {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a : MonoidAlgebra R (Equiv.Perm (Fin d))) : (tensorPowerRange ρ d a).toSubmodule = LinearMap.range ((PiTensorProduct.reindexRepresentation R M (Fin d)).asAlgebraHom a)

The submodule underlying tensorPowerRange is the range of the group-algebra action.

@[simp]

theorem TauCeti.tensorPowerRange_one {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) : tensorPowerRange ρ d 1 = ⊤

The identity of the group algebra cuts out the whole tensor power.

@[simp]

theorem TauCeti.tensorPowerRange_zero {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) : tensorPowerRange ρ d 0 = ⊥

The zero of the group algebra cuts out the zero subrepresentation.

theorem TauCeti.tensorPowerRange_mul_le {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a b : MonoidAlgebra R (Equiv.Perm (Fin d))) : tensorPowerRange ρ d (a * b) ≤ tensorPowerRange ρ d a

Multiplying on the right shrinks the image: ⨂^d M · a b ⊆ ⨂^d M · a.

theorem TauCeti.tensorPowerRange_conj {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (a : MonoidAlgebra R (Equiv.Perm (Fin d))) (σ : Equiv.Perm (Fin d)) : (tensorPowerRange ρ d (MonoidAlgebra.single σ 1 * a * MonoidAlgebra.single σ⁻¹ 1)).toSubmodule = Submodule.map (↑(PiTensorProduct.reindex R (fun (x : Fin d) => M) σ)) (tensorPowerRange ρ d a).toSubmodule

Conjugating the group-algebra element by a permutation moves the image by the corresponding permutation of the tensor factors.