The induction kill: block products die with their multiplicity

The product of the central idempotent of λ with the embedded block idempotent of (μ, ν) is an idempotent of the group algebra whose coefficient at the identity is a positive multiple of the induction multiplicity [λ : μ, ν]. An idempotent of a group algebra over ℂ vanishes exactly when its identity coefficient does — the trace of its left-regular action — so the product is zero as soon as the multiplicity is. This is the bridge from the character combinatorics to the categorical direct-sum transfer of Schur vanishing.

theorem RS.trace_mulLeft_monoidAlgebra {G : Type u_1} [Group G] [Fintype G] (x : MonoidAlgebra ℂ G) : (LinearMap.trace ℂ (MonoidAlgebra ℂ G)) (LinearMap.mulLeft ℂ x) = ↑(Fintype.card G) * x.coeff 1

The trace of left multiplication on a group algebra is the group order times the identity coefficient.

theorem RS.eq_zero_of_idem_of_coeff_one {G : Type u_1} [Group G] [Finite G] {x : MonoidAlgebra ℂ G} (hidem : x * x = x) (h1 : x.coeff 1 = 0) : x = 0

An idempotent of a finite group algebra over ℂ with vanishing identity coefficient is zero.

theorem RS.shape_e_coeff_conj (P : SchurPackage) {n : ℕ} (lam : Shape n) (g k : Equiv.Perm (Fin n)) : (Shape.e P lam).coeff (g⁻¹ * k * g) = (Shape.e P lam).coeff k

The Shape idempotent's coefficients are conjugation invariant.

theorem RS.shape_e_central (P : SchurPackage) {n : ℕ} (lam : Shape n) (y : SymGroupAlgebra n) : Shape.e P lam * y = y * Shape.e P lam

The Shape idempotents are central.

theorem RS.blockImages_comm {a b : ℕ} (x : SymGroupAlgebra a) (y : SymGroupAlgebra b) : (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedFstHom a b)) x * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedSndHom a b)) y = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedSndHom a b)) y * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (blockEmbedFstHom a b)) x

The two block images commute elementwise.

theorem RS.blockAlgEmbed_mul_blockAlgEmbed {a b : ℕ} (x x' : SymGroupAlgebra a) (y y' : SymGroupAlgebra b) : blockAlgEmbed x y * blockAlgEmbed x' y' = blockAlgEmbed (x * x') (y * y')

The block embedding is multiplicative in the two slots jointly.

theorem RS.blockAlgEmbed_shape_e_idem (P : SchurPackage) {a b : ℕ} (μ : Shape a) (ν : Shape b) : blockAlgEmbed (Shape.e P μ) (Shape.e P ν) * blockAlgEmbed (Shape.e P μ) (Shape.e P ν) = blockAlgEmbed (Shape.e P μ) (Shape.e P ν)

The embedded block idempotent is idempotent.

theorem RS.blockEmbed_inj {a b : ℕ} {σ σ' : Equiv.Perm (Fin a)} {τ τ' : Equiv.Perm (Fin b)} (h : blockEmbed σ τ = blockEmbed σ' τ') : σ = σ' ∧ τ = τ'

Joint injectivity of the block embedding.

theorem RS.blockAlgEmbed_apply_blockEmbed {a b : ℕ} (x : SymGroupAlgebra a) (y : SymGroupAlgebra b) (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : (blockAlgEmbed x y).coeff (blockEmbed σ τ) = x.coeff σ * y.coeff τ

The block image's coefficient on the block.

theorem RS.blockAlgEmbed_apply_eq_zero {a b : ℕ} (x : SymGroupAlgebra a) (y : SymGroupAlgebra b) {g : Equiv.Perm (Fin (a + b))} (h : ∀ (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)), g ≠ blockEmbed σ τ) : (blockAlgEmbed x y).coeff g = 0

The block image vanishes off the block.

theorem RS.mul_apply_one {G : Type u_1} [Group G] [Fintype G] (x y : MonoidAlgebra ℂ G) : (x * y).coeff 1 = ∑ g : G, x.coeff g * y.coeff g⁻¹

Convolution at the identity.

theorem RS.shape_e_mul_block_apply_one (P : SchurPackage) {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) : (Shape.e P lam * blockAlgEmbed (Shape.e P μ) (Shape.e P ν)).coeff 1 = ↑(P.dim ↑lam) * ↑(P.dim ↑μ) * ↑(P.dim ↑ν) / ↑(a + b).factorial * indMult lam μ ν

The identity coefficient of the block product is a positive multiple of the induction multiplicity.

theorem RS.shape_e_mul_blockAlgEmbed_eq_zero (P : SchurPackage) {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) (h : indMult lam μ ν = 0) : Shape.e P lam * blockAlgEmbed (Shape.e P μ) (Shape.e P ν) = 0

The induction kill: a vanishing induction multiplicity kills the block product in the group algebra.