Hook confinement

A PermTower over a family of algebras E n is a family of representations of the symmetric-group algebras with exponentially bounded dimensions (finrank (E n) ≤ A ^ n, the accompanying paper's hypothesis, with A a real constant) in which vanishing propagates along the standard embeddings. The main theorem: relative to any SchurPackage, the shapes alive in a tower are confined to a hook — there is an s with every alive shape satisfying IsInHook (s − 1) (s − 1).

The argument: the square shape of side s, for s given by the package's square_dim growth field at ⌈√A⌉, has a block too large for the tower's dimension bound, so it is dead (dim_sq_le_finrank); by e_killed_of_contained and vanishing propagation no shape containing the square is alive; and a shape outside the hook contains the square.

structure RS.PermTower (E : ℕ → Type u) [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] (A : ℝ) : Type u

A tower of representations of the symmetric-group algebras on a family of complex algebras, with vanishing propagating along the standard embeddings (symCast) and exponentially bounded target dimensions. The skein endomorphism algebras form such a tower.

• rep (n : ℕ) : SymGroupAlgebra n →ₐ[ℂ] E n

  The representations.

• compat {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) : (self.rep m) x = 0 → (self.rep n) ((symCast h) x) = 0

  Vanishing propagates along the standard embeddings.

• bound (n : ℕ) : ↑(Module.finrank ℂ (E n)) ≤ A ^ n

  The exponential dimension bound.

def RS.PermTower.Alive {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} (T : PermTower E A) (P : SchurPackage) (μ : YoungDiagram) : Prop

A shape is alive in a tower when its idempotent is not killed.

Equations

• T.Alive P μ = ((T.rep μ.card) (P.e μ) ≠ 0)

theorem RS.PermTower.growth_nonneg {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} (T : PermTower E A) : 0 ≤ A

The growth constant of a tower is nonnegative: it dominates the dimension at one strand.

theorem RS.PermTower.not_alive_square {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : PermTower E A) (P : SchurPackage) {s : ℕ} (hs : A ^ s ^ 2 < ↑(P.dim (squareDiagram s)) ^ 2) : ¬T.Alive P (squareDiagram s)

Square death: the square of side s is not alive as soon as its block dimension squared exceeds the tower's dimension bound at s² strands. This is the accompanying paper's hypothesis verbatim: dim² ≤ finrank ≤ A ^ (s²) < dim².

theorem RS.PermTower.not_alive_of_le {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} (T : PermTower E A) (P : SchurPackage) {lam mu : YoungDiagram} (hle : lam ≤ mu) (hdead : ¬T.Alive P lam) : ¬T.Alive P mu

No shape containing a dead shape is alive.

theorem RS.PermTower.hook_confinement {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : PermTower E A) (P : SchurPackage) : ∃ (s : ℕ), ∀ (μ : YoungDiagram), T.Alive P μ → IsInHook (s - 1) (s - 1) μ

Hook confinement: every shape alive in a tower lies in the hook IsInHook (s − 1) (s − 1) for a side s given by the package's growth field at the tower's bound.