Schur vanishing at the module level

The block decomposition of the symmetric-group algebra acts on the relative tensor powers of a module through modPowAlg; when every block of one size acts as zero, the completeness of the blocks collapses the whole power.

def RS.ModSchurKilled {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) (μ : YoungDiagram) : Prop

Module-level Schur vanishing: the block of the shape acts as zero on the relative tensor power of the module.

Equations

• RS.ModSchurKilled A X P μ = ((RS.modPowAlg A X μ.card) (P.e μ) = 0)

theorem RS.ModSchurKilled.mono {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) {lam mu : YoungDiagram} (hle : lam ≤ mu) (h : ModSchurKilled A X P lam) : ModSchurKilled A X P mu

Module-level upward closure (Deligne 1.7 over the base): vanishing of a block's action ascends along containment of shapes.

theorem RS.isZero_modPow_of_cuts {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) {k : ℕ} (h : ∀ (μ : Shape k), (modPowAlg A X k) (Shape.e P μ) = 0) : CategoryTheory.Limits.IsZero (modPow A X k)

Completeness collapses the power: if every block of one size acts as zero on the relative power, the power itself vanishes.

theorem RS.symPowIdem_eq_zero_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : symPowIdem A X n = 0 ↔ CategoryTheory.Limits.IsZero (symPow A X n)

The symmetric power vanishes exactly when the symmetriser acts as zero.

theorem RS.modSchurKilled_row_of_isZero_symPow {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) (n : ℕ) (h : CategoryTheory.Limits.IsZero (symPow A X (n + 1))) : ModSchurKilled A X P ↑(rowShape (n + 1))

A dead symmetric power kills the row block.

theorem RS.isZero_modPow_of_row_col {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) {n m : ℕ} (hrow : ModSchurKilled A X P ↑(rowShape (n + 1))) (hcol : ModSchurKilled A X P ↑(colShape (m + 1))) : CategoryTheory.Limits.IsZero (modPow A X (n * m + 1))

Row and column kills collapse the whole power (Deligne 2.9 case (c), module level, Schur half): a module whose row and column blocks act as zero has vanishing relative power at the product size.

theorem RS.altPowIdem_eq_zero_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : altPowIdem A X n = 0 ↔ CategoryTheory.Limits.IsZero (altPow A X n)

The alternating power vanishes exactly when the antisymmetriser acts as zero.

theorem RS.modSchurKilled_col_of_isZero_altPow {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) (m : ℕ) (h : CategoryTheory.Limits.IsZero (altPow A X (m + 1))) : ModSchurKilled A X P ↑(colShape (m + 1))

A dead alternating power kills the column block.

theorem RS.isZero_modPow_of_isZero_sym_alt {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Y : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Y)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : SchurPackage) {n m : ℕ} (hs : CategoryTheory.Limits.IsZero (symPow A X (n + 1))) (ha : CategoryTheory.Limits.IsZero (altPow A X (m + 1))) : CategoryTheory.Limits.IsZero (modPow A X (n * m + 1))

Dead symmetric and alternating powers collapse the relative power (Deligne 2.9 case (c), Schur half): the row and column bridges feed the block collapse.

theorem RS.modPowCutIdem_eq_zero_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) (e : SymGroupAlgebra n) (he : e * e = e) : (modPowAlg A X n) e = 0 ↔ CategoryTheory.Limits.IsZero (modPowCut A X n e)

An idempotent's cut vanishes exactly when it acts as zero.