The tensor-product transfer of Schur vanishing

Deligne 1.13, second half: if a Schur functor kills X and one kills Y, a product-hook Schur functor kills X ⊗ Y. The distribution isomorphism carries the diagonal action on (X ⊗ Y)^⊗n to the double action on X^⊗n ⊗ Y^⊗n, which extends to the group algebra of S_n × S_n; there the diagonal image of the central idempotent of λ meets the complete family of external products of block idempotents, where every term dies — by the Kronecker kill when the multiplicity vanishes, and through the killed whiskered factor when it does not, since a nonzero multiplicity pushes a bounding-box cell into μ' or ν' (Deligne 1.12).

noncomputable def RS.whiskerLeftAlg {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 X →ₐ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj P X)

Left whiskering by a fixed object is an algebra map on endomorphisms, the mirror of whiskerAlg. 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.pairPermHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] (X Y : A) (n : ℕ) : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) →* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X n) (tensorPow A Y n))

The double action of a pair of permutations on X ^ ⊗ n ⊗ Y ^ ⊗ n, as a monoid homomorphism on the product group: (σ, τ) acts by the two actions tensored together.

Equations

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

@[simp]

theorem RS.pairPermHom_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] (X Y : A) (n : ℕ) (g : Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) : (pairPermHom X Y n) g = CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n g.1) (permMor Y n g.2)

noncomputable def RS.pairAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) : MonoidAlgebra ℂ (Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) →ₐ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X n) (tensorPow A Y n))

The double action of the product group algebra on X ^ ⊗ n ⊗ Y ^ ⊗ n: the linear extension of (σ, τ) ↦ permMor X n σ ⊗ₘ permMor Y n τ. Since End multiplies in the order opposite to composition, pairAlg (a * b) is pairAlg b ≫ pairAlg a as a morphism.

Equations

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

@[simp]

theorem RS.pairAlg_single {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) (σ τ : Equiv.Perm (Fin n)) : (pairAlg X Y n) (MonoidAlgebra.single (σ, τ) 1) = CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n σ) (permMor Y n τ)

The pair algebra map sends a pair of group elements to the tensor product of their two actions.

theorem RS.pairAlg_diagEmbed {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) (x : SymGroupAlgebra n) : (pairAlg X Y n) (diagEmbed x) = (diagAlg X Y n) x

The double action restricted to the diagonal is the diagonal double action: pairAlg extends diagAlg along diagEmbed.

theorem RS.pairAlg_extFst {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X Y : A) (n : ℕ) (x : SymGroupAlgebra n) : (pairAlg X Y n) ((MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extFstHom n)) x) = CategoryTheory.MonoidalCategoryStruct.whiskerRight ((permAlg X n) x) (tensorPow A Y n)

The double action on the first external image is the right whiskering of the one-sided action: pairAlg extends permAlg X n · ▷ Y ^ ⊗ n along the first-factor embedding.

theorem RS.pairAlg_extSnd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X Y : A) (n : ℕ) (y : SymGroupAlgebra n) : (pairAlg X Y n) ((MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extSndHom n)) y) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow A X n) ((permAlg Y n) y)

The double action on the second external image is the left whiskering of the one-sided action: pairAlg extends X ^ ⊗ n ◁ permAlg Y n · along the second-factor embedding.

theorem RS.pairAlg_extProd {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (X Y : A) (n : ℕ) (x y : SymGroupAlgebra n) : (pairAlg X Y n) (extProd x y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow A X n) ((permAlg Y n) y)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((permAlg X n) x) (tensorPow A Y n))

The double action on an external product, as a morphism: the left whiskering of the second factor's action followed by the right whiskering of the first's. This composite order is End's pairAlg (extProd x y) = pairAlg (sndImage y) ≫ pairAlg (fstImage x), the form the per-term kill composes with.

theorem RS.sum_extProd_shape_e (P : SchurPackage) (n : ℕ) : ∑ μ' : Shape n, ∑ ν' : Shape n, extProd (Shape.e P μ') (Shape.e P ν') = 1

The external products of the recast block idempotents are a complete family in the product group algebra.

theorem RS.SchurKilled.tensorObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (P : SchurPackage) {X Y : A} {μ ν lam : YoungDiagram} {p q r s : ℕ} (hμc : μ.colLen 0 ≤ p + 1) (hμr : μ.rowLen 0 ≤ q + 1) (hνc : ν.colLen 0 ≤ r + 1) (hνr : ν.rowLen 0 ≤ s + 1) (hX : SchurKilled P X μ) (hY : SchurKilled P Y ν) (hcell : (p * r + q * s, p * s + q * r) ∈ lam) : SchurKilled P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) lam

The tensor-product transfer (Deligne 1.13, ⊗ half): Schur vanishing for X at μ and Y at ν forces Schur vanishing for X ⊗ Y at every diagram containing the product-hook cell of the two bounding boxes.