Block bounds

The two abstract consequences of the Schur interface that drive hook confinement: an algebra morphism that does not kill the idempotent of shape μ transports the full (dim μ)²-dimensional block (dim_sq_le_finrank), and killing a shape kills every shape containing it (e_killed_of_contained), by the branching containment. Both are stated against an arbitrary target algebra; the skein endomorphism algebras are substituted downstream.

theorem RS.SchurPackage.dim_sq_le_finrank (P : SchurPackage) (μ : YoungDiagram) {B : Type u} [Ring B] [Algebra ℂ B] [Module.Finite ℂ B] (φ : SymGroupAlgebra μ.card →ₐ[ℂ] B) (hne : φ (P.e μ) ≠ 0) : P.dim μ ^ 2 ≤ Module.finrank ℂ B

If an algebra morphism does not kill e μ, its target has dimension at least (dim μ)²: the block of μ embeds.

theorem RS.SchurPackage.e_killed_of_contained (P : SchurPackage) {lam mu : YoungDiagram} (hle : lam ≤ mu) (h : lam.card ≤ mu.card) {B : Type u} [Ring B] [Algebra ℂ B] (φ : SymGroupAlgebra mu.card →ₐ[ℂ] B) (hkill : φ ((symCast h) (P.e lam)) = 0) : φ (P.e mu) = 0

Killing a shape kills every shape containing it: if φ annihilates e lam extended to arity mu.card, and lam ≤ mu, then φ annihilates e mu.