Moderate growth forces Schur vanishing

Deligne's 1.20 (Catégories tensorielles): if no Schur functor kills X, then for every n the tensor power X ^ ⊗ n carries, through permAlg, one nonzero idempotent for each unit of each block — ∑_{μ ⊢ n} dim μ many, pairwise orthogonal — so its length is at least √(n!) − 1, which outgrows every geometric progression. Contrapositive: moderate length growth yields a shape whose Schur functor vanishes.

The two block-theoretic inputs — completeness and orthogonality of the central idempotents at each size — are named Props here and discharged for the tree's package where the block theory lives.

def RS.SchurPackage.Complete (P : SchurPackage) : Prop

Completeness of the blocks: at every size the central idempotents sum to the identity of the group algebra.

Equations

• P.Complete = ∀ (n : ℕ), ∑ μ : RS.Shape n, RS.Shape.e P μ = 1

def RS.SchurPackage.Orthogonal (P : SchurPackage) : Prop

Orthogonality of the blocks: distinct shapes of one size have orthogonal central idempotents.

Equations

• P.Orthogonal = ∀ (n : ℕ) (μ ν : RS.Shape n), μ ≠ ν → RS.Shape.e P μ * RS.Shape.e P ν = 0

theorem RS.exists_schurKilled_of_lengthLE {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] (P : SchurPackage) (hO : P.Orthogonal) (hunits : ∀ (μ : YoungDiagram), ∃ (u : Fin (P.dim μ) → SymGroupAlgebra μ.card), (∀ (i : Fin (P.dim μ)), u i * u i = u i) ∧ (∀ (i j : Fin (P.dim μ)), i ≠ j → u i * u j = 0) ∧ (∀ (i : Fin (P.dim μ)), P.e μ * u i = u i) ∧ (∀ (i : Fin (P.dim μ)), u i * P.e μ = u i) ∧ ∀ (i : Fin (P.dim μ)), u i ≠ 0) (hsum : ∀ (n : ℕ), √↑n.factorial ≤ ↑(∑ μ : Shape n, P.dim ↑μ)) (X : A) (hup : ∀ {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m), (permAlg X m) x ≠ 0 → (permAlg X n) ((symCast h) x) ≠ 0) {C c : ℕ} (hlen : ∀ (N : ℕ), LengthLE (tensorPow A X N) (C * c ^ N)) : ∃ (μ : YoungDiagram), SchurKilled P X μ

Moderate growth forces Schur vanishing (Catégories tensorielles, 1.20), assembly form: the block-theoretic inputs — completeness, orthogonality, the block units — and the nonvanishing transport up the standard embedding are hypotheses, discharged elsewhere.

theorem RS.exists_schurKilled_of_moderateGrowth {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (P : SchurPackage) (hs : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {X : A} (hX : ¬CategoryTheory.Limits.IsZero X) {C c : ℕ} (hlen : ∀ (N : ℕ), LengthLE (tensorPow A X N) (C * c ^ N)) : ∃ (μ : YoungDiagram), SchurKilled P X μ

Moderate growth forces Schur vanishing (Catégories tensorielles, 1.20), final form: every hypothesis slot discharged — orthogonality and the dimension bound from the package's block theory, the block units from its matrix structure, and the transport from whisker faithfulness. Only simplicity of the unit and nonvanishing of X remain, both facts of the ambient category.

theorem RS.isZero_tensorPow_of_schurKilled {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] (P : SchurPackage) {X : A} {k : ℕ} (h : ∀ (μ : Shape k), SchurKilled P X ↑μ) : CategoryTheory.Limits.IsZero (tensorPow A X k)

The completeness collapse: if every shape of size k kills X, the k-th tensor power is zero — the central idempotents sum to the identity, and each acts as zero.

theorem RS.exists_schurKilled_of_moderateGrowth' {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (P : SchurPackage) (hu : HasScalarUnit A) {X : A} (hX : ¬CategoryTheory.Limits.IsZero X) {C c : ℕ} (hlen : ∀ (N : ℕ), LengthLE (tensorPow A X N) (C * c ^ N)) : ∃ (μ : YoungDiagram), SchurKilled P X μ

The moderate-growth dichotomy over a scalar unit: with End (𝟙) = ℂ the simplicity hypothesis discharges as well, leaving only nonvanishing of the generator.

theorem RS.exists_lengthLE_of_moderateGrowth {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (h : ModerateLengthGrowth C) (X : C) : ∃ (N : ℕ), LengthLE X N

Under moderate growth every object has finite length: evaluate the growth bound at the first tensor power.

theorem RS.SchurKilled.of_isZero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] (P : SchurPackage) {X : A} (hX : CategoryTheory.Limits.IsZero X) {lam : YoungDiagram} (hcard : 0 < lam.card) : SchurKilled P X lam

A zero object is killed by every Schur functor of positive size: its positive tensor powers are zero.

theorem RS.forall_exists_schurKilled {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (P : SchurPackage) (hu : HasScalarUnit A) (hg : ModerateLengthGrowth A) (X : A) : ∃ (μ : YoungDiagram), SchurKilled P X μ

Every object is Schur-killed under moderate growth — the hypothesis of Deligne 2.1 in the form the pinned statement supplies it.

theorem RS.rowShape_le_iff {m : ℕ} {lam : YoungDiagram} : ↑(rowShape m) ≤ lam ↔ m ≤ lam.rowLen 0

Containment of the single row.

theorem RS.colShape_le_iff {m : ℕ} {lam : YoungDiagram} : ↑(colShape m) ≤ lam ↔ m ≤ lam.colLen 0

Containment of the single column.

theorem RS.cell_lt_card {lam : YoungDiagram} {p q : ℕ} (h : (p, q) ∈ lam) : p < lam.card ∧ q < lam.card

A cell's coordinates are bounded by the cell count.

theorem RS.card_le_colLen_mul_rowLen (lam : YoungDiagram) : lam.card ≤ lam.colLen 0 * lam.rowLen 0

The bounding-box count: a diagram fits in the rectangle of its first row and column.