Schur-functor vanishing at the idempotent level

Deligne's Schur functor S_μ(X) (Catégories tensorielles, 1.4) is the multiplicity space of the shape μ in the tensor power X ^ ⊗ μ.card; its vanishing is equivalent to the vanishing of the μ-isotypic summand, which is the image of the central idempotent e μ acting through permAlg. This module phrases the condition on the idempotent's action — no image objects are needed — and proves Deligne's upward closure (Catégories tensorielles, 1.7) from the Schur package alone: branching puts a nonzero sandwich e μ · (e λ ⊗ 1) · e μ in the block of μ, block_faithful turns nonvanishing of e μ's action into injectivity on that block, and permAlg_compat carries the vanishing of e λ's action up the standard embedding.

def RS.SchurKilled {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (P : SchurPackage) (X : A) (μ : YoungDiagram) : Prop

Schur vanishing: the shape μ kills X when the central idempotent of its block acts as zero on the μ.card-th tensor power of X. This is the vanishing of the μ-isotypic summand of X ^ ⊗ μ.card, i.e. of Deligne's Schur functor S_μ(X).

Equations

• RS.SchurKilled P X μ = ((RS.permAlg X μ.card) (P.e μ) = 0)

theorem RS.SchurKilled.mono {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 : A} {lam mu : YoungDiagram} (hle : lam ≤ mu) (h : SchurKilled P X lam) : SchurKilled P X mu

Upward closure of Schur vanishing (Catégories tensorielles, 1.7): if the shape λ kills X then so does every shape containing it.