Scalar self-braidings and the vanishing for even and odd lines

When the self-braiding of an object is a scalar, the whole symmetric-group action on its tensor powers is by that scalar's sign character: the top swap acts by the scalar, every transposition is conjugate to it, and transpositions generate. For a trivial self-braiding (the unit) the central idempotents then act by the plain character sum — the Schur specialisation at one even variable — and for braiding −1 (an odd line) by the signed sum — the specialisation at one odd variable. The one-variable indicator evaluations kill every non-row (respectively non-column) Schur functor, and iterated direct sums give the vanishing half of Deligne 1.9 for 𝟙^p ⊕ 1-bar^q inside any ambient category — the engine of the trichotomy 2.9.

theorem RS.swapTop_of_scalar {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 : A} {c : ℂ} (hβ : (β_ X X).hom = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) (n : ℕ) : swapTop X n = c • CategoryTheory.CategoryStruct.id (tensorPow A X (n + 2))

A scalar self-braiding makes the top swap act by the scalar.

theorem RS.permMor_swap_of_scalar {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 : A} {c : ℂ} (hβ : (β_ X X).hom = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) {n : ℕ} (x y : Fin n) : x ≠ y → permMor X n (Equiv.swap x y) = c • CategoryTheory.CategoryStruct.id (tensorPow A X n)

Every transposition acts by the scalar: the top swap does, and transpositions are conjugate with central scalar values.

theorem RS.permMor_of_scalar {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 : A} {c : ℂ} (hβ : (β_ X X).hom = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) (hc2 : c * c = 1) {n : ℕ} (σ : Equiv.Perm (Fin n)) : permMor X n σ = (if Equiv.Perm.sign σ = 1 then 1 else c) • CategoryTheory.CategoryStruct.id (tensorPow A X n)

Scalar self-braiding acts by the sign character: with a scalar square root of unity as self-braiding, every permutation acts by the scalar raised to its sign.

theorem RS.permAlg_of_scalar {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 : A} {c : ℂ} (hβ : (β_ X X).hom = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) (hc2 : c * c = 1) {n : ℕ} (x : SymGroupAlgebra n) : (permAlg X n) x = (∑ σ : Equiv.Perm (Fin n), x.coeff σ * if Equiv.Perm.sign σ = 1 then 1 else c) • CategoryTheory.CategoryStruct.id (tensorPow A X n)

The group-algebra action under a scalar self-braiding is multiplication by the twisted coefficient sum.

theorem RS.pe_eq_shape_e (P : SchurPackage) (lam : YoungDiagram) : P.e lam = Shape.e P ⟨lam, ⋯⟩

The identification of the raw idempotent with its Shape form at its own size.

theorem RS.sum_e_coeff (P : SchurPackage) (lam : YoungDiagram) : ∑ σ : Equiv.Perm (Fin lam.card), (P.e lam).coeff σ = ↑(P.dim lam) * diagramSchur lam (superPS 1 0)

The plain coefficient sum of the central idempotent is the dimension times the Schur specialisation at one even variable.

theorem RS.sum_e_coeff_sign (P : SchurPackage) (lam : YoungDiagram) : ∑ σ : Equiv.Perm (Fin lam.card), (P.e lam).coeff σ * ↑↑(Equiv.Perm.sign σ) = ↑(P.dim lam) * diagramSchur lam (superPS 0 1)

The signed coefficient sum of the central idempotent is the dimension times the Schur specialisation at one odd variable.

theorem RS.schurKilled_of_braiding_id {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} (hβ : (β_ X X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) {lam : YoungDiagram} (hlam : 1 < lam.colLen 0) : SchurKilled P X lam

Trivial self-braiding kills every non-row Schur functor: the central idempotent acts by the plain character sum, the Schur specialisation at one even variable.

theorem RS.schurKilled_of_braiding_neg {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} (hβ : (β_ X X).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X)) {lam : YoungDiagram} (hlam : 1 < lam.rowLen 0) : SchurKilled P X lam

Self-braiding −1 kills every non-column Schur functor: the central idempotent acts by the signed character sum, the Schur specialisation at one odd variable.

theorem RS.schurKilled_unit_col {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) : SchurKilled P (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) ↑(colShape 2)

The unit is killed at the two-cell column.

theorem RS.schurKilled_odd_row {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) {U : A} (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) : SchurKilled P U ↑(rowShape 2)

An odd line is killed at the two-cell row.

noncomputable def RS.sumPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasBinaryBiproducts A] (X : A) : ℕ → A

p + 1 biproduct copies of an object.

Equations

• RS.sumPow X 0 = X
• RS.sumPow X k.succ = (RS.sumPow X k ⊞ X)

theorem RS.colShape_colLen_le (m : ℕ) : (↑(colShape m)).colLen 0 ≤ m

Column bound for the one-column shape.

theorem RS.schurKilled_sumPow_unit {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 : ℕ) : SchurKilled P (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p) ↑(colShape (p + 2))

Iterated unit sums are killed at the corresponding column.

theorem RS.rowShape_colLen_le (m : ℕ) : (↑(rowShape m)).colLen 0 ≤ 1

Row bound for the one-row shape.

theorem RS.schurKilled_sumPow_odd {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) {U : A} (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (q : ℕ) : SchurKilled P (sumPow U q) ↑(rowShape (q + 2))

Iterated odd sums are killed at the corresponding row.

theorem RS.schurKilled_unit_odd {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) {U : A} (hβ : (β_ U U).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U U)) (p q : ℕ) {lam : YoungDiagram} (hcell : (p + 1, q + 1) ∈ lam) : SchurKilled P (sumPow (CategoryTheory.MonoidalCategoryStruct.tensorUnit A) p ⊞ sumPow U q) lam

The vanishing half of Deligne 1.9, internally: a direct sum of p + 1 unit copies and q + 1 odd-line copies is killed at every diagram containing the cell (p + 1, q + 1).