The Kronecker kill: diagonal products die with their multiplicity

In the group algebra of the product group S_n × S_n, the external product of two recast Shape idempotents times the diagonal image of a third is an idempotent whose coefficient at the identity is a positive multiple of the Kronecker multiplicity [λ : μ ⊗ ν]. An idempotent of a finite group algebra over ℂ vanishes exactly when its identity coefficient does, so the product is zero as soon as the multiplicity is. This mirrors the induction kill of RS.Classical.Deligne.IndKill, with the block embedding replaced by the two external embeddings and the diagonal.

noncomputable def RS.extFstHom (n : ℕ) : Equiv.Perm (Fin n) →* Equiv.Perm (Fin n) × Equiv.Perm (Fin n)

The first-factor embedding of S_n into S_n × S_n.

Equations

• RS.extFstHom n = { toFun := fun (σ : Equiv.Perm (Fin n)) => (σ, 1), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RS.extSndHom (n : ℕ) : Equiv.Perm (Fin n) →* Equiv.Perm (Fin n) × Equiv.Perm (Fin n)

The second-factor embedding of S_n into S_n × S_n.

Equations

• RS.extSndHom n = { toFun := fun (τ : Equiv.Perm (Fin n)) => (1, τ), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RS.diagHom (n : ℕ) : Equiv.Perm (Fin n) →* Equiv.Perm (Fin n) × Equiv.Perm (Fin n)

The diagonal embedding of S_n into S_n × S_n.

Equations

• RS.diagHom n = { toFun := fun (σ : Equiv.Perm (Fin n)) => (σ, σ), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RS.extProd {n : ℕ} (x y : SymGroupAlgebra n) : MonoidAlgebra ℂ (Equiv.Perm (Fin n) × Equiv.Perm (Fin n))

The external product: the product of the two one-sided images of a pair of group-algebra elements in the group algebra of S_n × S_n.

Equations

• RS.extProd x y = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (RS.extFstHom n)) x * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (RS.extSndHom n)) y

noncomputable def RS.diagEmbed {n : ℕ} : SymGroupAlgebra n →ₐ[ℂ] MonoidAlgebra ℂ (Equiv.Perm (Fin n) × Equiv.Perm (Fin n))

The diagonal embedding of group algebras: extension of the diagonal along mapDomain, an algebra homomorphism.

Equations

• RS.diagEmbed = MonoidAlgebra.mapDomainAlgHom ℂ ℂ (RS.diagHom n)

theorem RS.extProd_single {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (c d : ℂ) : extProd (MonoidAlgebra.single σ c) (MonoidAlgebra.single τ d) = MonoidAlgebra.single (σ, τ) (c * d)

On basis permutations the external product is the single at the pair.

theorem RS.extImages_comm {n : ℕ} (x y : SymGroupAlgebra n) : (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extFstHom n)) x * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extSndHom n)) y = (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extSndHom n)) y * (MonoidAlgebra.mapDomainAlgHom ℂ ℂ (extFstHom n)) x

The two external images commute elementwise.

theorem RS.extProd_mul_extProd {n : ℕ} (x x' y y' : SymGroupAlgebra n) : extProd x y * extProd x' y' = extProd (x * x') (y * y')

The external product is multiplicative in the two slots jointly.

theorem RS.extProd_shape_e_idem (P : SchurPackage) {n : ℕ} (μ ν : Shape n) : extProd (Shape.e P μ) (Shape.e P ν) * extProd (Shape.e P μ) (Shape.e P ν) = extProd (Shape.e P μ) (Shape.e P ν)

The external product of Shape idempotents is idempotent.

theorem RS.extProd_add_fst {n : ℕ} (x x' y : SymGroupAlgebra n) : extProd (x + x') y = extProd x y + extProd x' y

The external product is additive in the first argument.

theorem RS.extProd_smul_fst {n : ℕ} (r : ℂ) (x y : SymGroupAlgebra n) : extProd (r • x) y = r • extProd x y

The external product is homogeneous in the first argument.

theorem RS.extProd_add_snd {n : ℕ} (x y y' : SymGroupAlgebra n) : extProd x (y + y') = extProd x y + extProd x y'

The external product is additive in the second argument.

theorem RS.extProd_smul_snd {n : ℕ} (r : ℂ) (x y : SymGroupAlgebra n) : extProd x (r • y) = r • extProd x y

The external product is homogeneous in the second argument.

theorem RS.extProd_apply_pair {n : ℕ} (x y : SymGroupAlgebra n) (σ τ : Equiv.Perm (Fin n)) : (extProd x y).coeff (σ, τ) = x.coeff σ * y.coeff τ

The external product's coefficient at a pair is the product of the coefficients.

theorem RS.extProd_shape_e_coeff_conj (P : SchurPackage) {n : ℕ} (μ ν : Shape n) (g k : Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) : (extProd (Shape.e P μ) (Shape.e P ν)).coeff (g⁻¹ * k * g) = (extProd (Shape.e P μ) (Shape.e P ν)).coeff k

The external product of Shape idempotents has conjugation invariant coefficients.

theorem RS.extProd_shape_e_central (P : SchurPackage) {n : ℕ} (μ ν : Shape n) (z : MonoidAlgebra ℂ (Equiv.Perm (Fin n) × Equiv.Perm (Fin n))) : extProd (Shape.e P μ) (Shape.e P ν) * z = z * extProd (Shape.e P μ) (Shape.e P ν)

The external products of Shape idempotents are central.

theorem RS.diagHom_injective (n : ℕ) : Function.Injective ⇑(diagHom n)

The diagonal embedding is injective on group elements.

theorem RS.diagEmbed_apply_diag {n : ℕ} (x : SymGroupAlgebra n) (σ : Equiv.Perm (Fin n)) : (diagEmbed x).coeff (σ, σ) = x.coeff σ

The diagonal image's coefficient on the diagonal.

theorem RS.diagEmbed_apply_off_diag {n : ℕ} (x : SymGroupAlgebra n) {p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n)} (h : p.1 ≠ p.2) : (diagEmbed x).coeff p = 0

The diagonal image vanishes off the diagonal.

theorem RS.extProd_mul_diagEmbed_apply_one (P : SchurPackage) {n : ℕ} (lam μ ν : Shape n) : (extProd (Shape.e P μ) (Shape.e P ν) * diagEmbed (Shape.e P lam)).coeff (1, 1) = ↑(P.dim ↑μ) * ↑(P.dim ↑ν) * ↑(P.dim ↑lam) / (↑n.factorial * ↑n.factorial) * kronMult lam μ ν

The identity coefficient of the diagonal product is a positive multiple of the Kronecker multiplicity.

theorem RS.extProd_mul_diagEmbed_eq_zero (P : SchurPackage) {n : ℕ} (lam μ ν : Shape n) (h : kronMult lam μ ν = 0) : extProd (Shape.e P μ) (Shape.e P ν) * diagEmbed (Shape.e P lam) = 0

The Kronecker kill: a vanishing Kronecker multiplicity kills the diagonal product in the product group algebra.