The direct-sum transfer of Schur vanishing

Deligne 1.13, first half: if a Schur functor kills X and one kills Y, a fat-hook Schur functor kills X ⊞ Y. The identity of (X ⊞ Y)^⊗n expands over mixed words; each mixed inclusion sorts to the standard block inclusion; the central idempotent of λ then meets the complete family of embedded block idempotents, where every term dies — by the induction kill when the multiplicity vanishes, and through the killed factor and naturality when it does not, since a nonzero multiplicity pushes a bounding-box cell into μ' or ν' (Deligne 1.10).

theorem RS.permAlg_eqToHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (Z : A) {m n : ℕ} (h : m = n) (x : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((permAlg Z n) x) = CategoryTheory.CategoryStruct.comp ((permAlg Z m) ((symCast ⋯) x)) (CategoryTheory.eqToHom ⋯)

Transport of the group-algebra action along an arity equality.

theorem RS.sum_blockAlgEmbed_shape_e (P : SchurPackage) (a b : ℕ) : ∑ μ' : Shape a, ∑ ν' : Shape b, blockAlgEmbed (Shape.e P μ') (Shape.e P ν') = 1

The embedded block idempotents are a complete family.

theorem RS.le_of_box_of_cell {μ μ' : YoungDiagram} {p q : ℕ} (hc : μ.colLen 0 ≤ p + 1) (hr : μ.rowLen 0 ≤ q + 1) (hcell : (p, q) ∈ μ') : μ ≤ μ'

A diagram inside the (p+1) × (q+1) bounding box is contained in any diagram holding the cell (p, q).

theorem RS.permMor_comp_permAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (Z : A) {n : ℕ} (g : Equiv.Perm (Fin n)) {x : SymGroupAlgebra n} (hcen : ∀ (y : SymGroupAlgebra n), x * y = y * x) : CategoryTheory.CategoryStruct.comp (permMor Z n g) ((permAlg Z n) x) = CategoryTheory.CategoryStruct.comp ((permAlg Z n) x) (permMor Z n g)

A central element commutes with every permutation action.

theorem RS.permMor_comp_inverse {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (Z : A) (n : ℕ) (g : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (permMor Z n g) (permMor Z n g⁻¹) = CategoryTheory.CategoryStruct.id (tensorPow A Z n)

The permutation action followed by its inverse is the identity.

theorem RS.SchurKilled.biprod {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] [CategoryTheory.Limits.HasBinaryBiproducts 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) ∈ lam) : SchurKilled P (X ⊞ Y) lam

The direct-sum transfer (Deligne 1.13, ⊕ half): Schur vanishing for X at μ and Y at ν forces Schur vanishing for X ⊞ Y at every diagram containing the fat-hook cell of the two bounding boxes.