Additive splitting of Schur specialisations

The Schur specialisation of a diagram at a pointwise sum of scalar sequences splits over pairs of shapes whose sizes add to the size of the diagram, with induction multiplicities: the normalized pairings of the recast Jacobi–Trudi character of the diagram, restricted to a block product of symmetric groups, against the characters of the two shapes. The multiplicities are nonnegative integers, being dimensions of equivariant Hom spaces over the product group.

The route: the Frobenius formula at a sum of sequences, the additive splitting of the completed cycle product over invariant subsets, a reindexing of the invariant permutations of a subset of fixed size by pairs of block permutations, the collapse of the subset sum by the binomial count, and the character expansion of each block factor.

Conjugation invariance of the Jacobi–Trudi character

theorem RS.jtChar_conj (μ : YoungDiagram) (τ π : Equiv.Perm (Fin μ.card)) : jtChar μ (τ * π * τ⁻¹) = jtChar μ π

The Jacobi–Trudi character is a class function.

theorem RS.jtChar_permCongr_congr (lam : YoungDiagram) {α : Type u_1} (g₁ g₂ : α ≃ Fin lam.card) (π : Equiv.Perm α) : jtChar lam (g₁.permCongr π) = jtChar lam (g₂.permCongr π)

Transport independence of the recast Jacobi–Trudi character: relabelling a permutation of an abstract carrier into the symmetric group of the diagram gives the same character value whichever equivalence performs the relabelling — two choices differ by an inner automorphism.

The block embedding as a homomorphism from the product

noncomputable def RS.blockEmbedHom (a b : ℕ) : Equiv.Perm (Fin a) × Equiv.Perm (Fin b) →* Equiv.Perm (Fin (a + b))

The block embedding of the product group: the monoid homomorphism S_a × S_b →* S_{a + b} carrying a pair to its block embedding, the first factor on the first a slots and the second on the last b.

Equations

• RS.blockEmbedHom a b = { toFun := fun (p : Equiv.Perm (Fin a) × Equiv.Perm (Fin b)) => RS.blockEmbed p.1 p.2, map_one' := ⋯, map_mul' := ⋯ }

theorem RS.blockEmbed_inv {a b : ℕ} (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : blockEmbed σ⁻¹ τ⁻¹ = (blockEmbed σ τ)⁻¹

The block embedding carries inverses to inverses.

Induction multiplicities

noncomputable def RS.indMult {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) : ℂ

The induction multiplicity of a pair of shapes in a shape of the joint size: the normalized pairing, over the block product S_a × S_b, of the recast Jacobi–Trudi character of the joint shape with the recast characters of the two shapes.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.indMult_exists_nat {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) : ∃ (m : ℕ), indMult lam μ ν = ↑m

Induction multiplicities are nonnegative integers: the pairing is the dimension of the space of S_a × S_b-equivariant maps from the restricted joint irreducible to the external tensor product of the two block irreducibles.

Assembling a subset and its complement into a block carrier

A subset of Fin n of size a with complement of size b, once equivalences of the subset with Fin a and of the complement with Fin b are chosen, assembles into an equivalence Fin n ≃ Fin (a + b) carrying the subset onto the first block. Conjugation along it carries a permutation preserving the subset to the block embedding of its two restrictions.

The invariant-permutation sum at a fixed subset

Character expansion of the block sums

The splitting identity

theorem RS.diagramSchur_add (lam : YoungDiagram) (t t' : ℕ → ℂ) : (diagramSchur lam fun (c : ℕ) => t c + t' c) = ∑ ab ∈ (Finset.antidiagonal lam.card).attach, ∑ μ : Shape (↑ab).1, ∑ ν : Shape (↑ab).2, indMult ⟨lam, ⋯⟩ μ ν * diagramSchur (↑μ) t * diagramSchur (↑ν) t'

The additive splitting of Schur specialisations — the character shadow of the ⊕-splitting: the Schur specialisation of a diagram at a pointwise sum of scalar sequences is the sum, over splittings of its size recorded on the antidiagonal and over pairs of shapes of the two parts, of the induction-multiplicity-weighted products of the Schur specialisations of the parts. The antidiagonal is attached so that each index carries the proof that its parts sum to the size of the diagram.