The action along the standard embeddings

A tower's compatibility field asks that vanishing propagate along the standard embeddings S_m ↪ S_n: an element of the group algebra killed at arity m stays killed at arity n. For the action on a tensor power this is a factorisation rather than a coincidence. Extending a permutation by fixed slots tensors its action with the identity on the new factors, so the level-n representation restricted along symCast is the level-m representation followed by repeated whiskering — and whiskering, being an algebra map, sends zero to zero.

The whiskering algebra map is where the linear structure of the category is used: additivity of ▷ is MonoidalPreadditive and its ℂ-homogeneity is MonoidalLinear.

Whiskering as an algebra map

noncomputable def RS.whiskerAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (P X : A) : CategoryTheory.End P →ₐ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj P X)

Whiskering by a fixed object is an algebra map on endomorphisms. Multiplicativity is functoriality of ▷ — note that End multiplies in the order opposite to composition, which is why no reversal appears.

Equations

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

noncomputable def RS.whiskerPowAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X : A) (m k : ℕ) : CategoryTheory.End (tensorPow A X m) →ₐ[ℂ] CategoryTheory.End (tensorPow A X (m + k))

Repeated whiskering: the algebra map carrying an endomorphism of X ^ ⊗ m to the endomorphism of X ^ ⊗ (m + k) that acts on the first m factors and fixes the last k.

Equations

• RS.whiskerPowAlg X m 0 = AlgHom.id ℂ (CategoryTheory.End (RS.tensorPow A X m))
• RS.whiskerPowAlg X m k.succ = (RS.whiskerAlg (RS.tensorPow A X (m + k)) X).comp (RS.whiskerPowAlg X m k)

The action factors through whiskering

theorem RS.permMor_viaEmbedding {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X : A) (m : ℕ) [CategoryTheory.SymmetricCategory A] (k : ℕ) (σ : Equiv.Perm (Fin m)) : permMor X (m + k) (σ.viaEmbedding (Fin.castLEEmb ⋯)) = (whiskerPowAlg X m k) (permMor X m σ)

The action of an extended permutation is the whiskered action: a permutation of Fin m, extended to Fin (m + k) by fixing the last k slots, acts on the first m tensor factors and fixes the last k.

theorem RS.permAlg_symCast {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X : A) [CategoryTheory.SymmetricCategory A] (m k : ℕ) (x : SymGroupAlgebra m) : (permAlg X (m + k)) ((symCast ⋯) x) = (whiskerPowAlg X m k) ((permAlg X m) x)

The representation restricted along the standard embedding is the lower representation followed by repeated whiskering.

theorem RS.permAlg_compat {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X : A) [CategoryTheory.SymmetricCategory A] {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) (hx : (permAlg X m) x = 0) : (permAlg X n) ((symCast h) x) = 0

Vanishing propagates along the standard embeddings. This is the compat field of a tower, for the action on a tensor power.