The whiskered mixed sum at arbitrary counts

The two generalisations of the nonvanishing of the mixed sum combine: the letter systems built on the indexed biproduct work at every pair of counts, and the extraction of the colour sums survives whiskering by an auxiliary object, so the block idempotent acts nontrivially on the whiskered tensor power at every pair of counts and every diagram avoiding the corresponding cell.

theorem RS.OddLine.whisker_permAlg_mix_ne_zero' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasFiniteBiproducts D] (P : SchurPackage) (P₀ : SchurPackage) (W : D) (L : OddLine D) (r s : ℕ) {lam : YoungDiagram} (hW : ∀ (k : ℕ), CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W (tensorPow D L.obj k)) ≠ 0) (hcell : (r, s) ∉ lam) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft W ((permAlg (L.mix r s) lam.card) (P.e lam)) ≠ 0

Nonvanishing of the whiskered mixed sum at arbitrary counts: no positivity of either count is needed, and the nontriviality hypothesis is carried by the whiskering object.