Whiskered nonvanishing of the mixed sum

The nonvanishing of MixSumPow.lean says that the block idempotent of a diagram avoiding the cell (p + 1, q + 1) acts nonzero on the tensor power of the mixed sum. For the dévissage one needs the same statement after whiskering by an auxiliary object W: the action stays nonzero inside W ⊗ −.

Whiskering is a ℂ-linear functor, so the whole extraction of SuperEmbed.lean survives it verbatim. The colour sums are the model-independent middle of that argument: the entry formula nIn_permAlg_nOut pins the normalised matrix entry of a group-algebra element to a scalar times a transport, and applying W ◁ − to it leaves the scalar alone. Once every colour sum vanishes the ambient endgame — reconstruction in SuperVect and the super trace computation — is reused unchanged.

The hypothesis feeding the whiskered form is that no power of the odd line is killed by W ⊗ −; for W a monoid object with nonzero unit this is automatic, since the odd line is invertible.

Whiskered extraction of the colour sums

theorem RS.MixedLetters.colourSum_eq_zero_whisker {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] {K : Type} [Fintype K] [DecidableEq K] {par : K → Bool} {U M : A} (S : MixedLetters K par U M) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (W : A) (hW : ∀ (k : ℕ), CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W (tensorPow A U k)) ≠ 0) {n : ℕ} {x : SymGroupAlgebra n} (hx : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg M n) x) = 0) (c d : Fin n → K) : colourSum par x c d = 0

Whiskered extraction: if a group-algebra element acts as zero on the tensor power of the mixed object after whiskering by W, all its colour sums vanish — provided no power of the odd line is annihilated by W ⊗ −. The proof is the unwhiskered one run through the ℂ-linear functor W ◁ −.

The whiskered ambient extraction and endgame

theorem RS.colourSum_eq_zero_of_whisker_sum {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) (W : A) {U : A} (hW : ∀ (k : ℕ), CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W (tensorPow A U k)) ≠ 0) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (p q : ℕ) {lam : YoungDiagram} (hkill : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q) lam.card) (P.e lam)) = 0) (c d : Fin lam.card → Fin (p + 1) ⊕ Fin (q + 1)) : colourSum mixedPar (P.e lam) c d = 0

Whiskered extraction in the ambient category: if the block idempotent acts as zero on the whiskered tensor power of the mixed sum, every colour sum of the idempotent vanishes.

theorem RS.whisker_permAlg_sum_ne_zero {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) (P₀ : SchurPackage) (W : A) {U : A} (hW : ∀ (k : ℕ), CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W (tensorPow A U k)) ≠ 0) (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (p q : ℕ) {lam : YoungDiagram} (hcell : (p + 1, q + 1) ∉ lam) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q) lam.card) (P.e lam)) ≠ 0

The whiskered nonvanishing half of Deligne 1.9: whiskering by W does not destroy the action of the block idempotent on a direct sum of p + 1 unit copies and q + 1 odd-line copies, at any diagram avoiding the cell (p + 1, q + 1). The nontriviality of the ambient category is replaced by the sharper hypothesis that W ⊗ − kills no power of the line.

Transport of the whiskered action along an isomorphism

theorem RS.whisker_permAlg_eq_zero_of_iso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (W : A) {X Y : A} (e : X ≅ Y) {n : ℕ} (x : SymGroupAlgebra n) (h : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg X n) x) = 0) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg Y n) x) = 0

The whiskered action is an isomorphism invariant: the tensor power of the inverse splits the tensor power of the isomorphism, and W ◁ − is a functor, so the naturality square of permAlg transports the vanishing.

Whiskered powers of an odd line

theorem RS.OddLine.whisker_tensorPow_id_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] (L : OddLine A) {W : A} [CategoryTheory.MonObj W] (hW : CategoryTheory.MonObj.one ≠ 0) (k : ℕ) : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W (tensorPow A L.obj k)) ≠ 0

Whiskered powers of an odd line are nonzero when the unit of the whiskering monoid is: one more copy of the line is undone through the line's self-pairing, and the empty power leaves W itself, whose identity carries the unit.

The whiskered mixed sum