One-sided super specialisations are multiplicities

The Schur specialisations at the one-sided super power sums superPS p 0 and superPS 0 q are multiplicities of the recast Jacobi–Trudi irreducibles in genuine representations of S_n, hence natural numbers. The symmetric group permutes the colourings Fin n → Fin p — the basis of the n-th tensor power of ℂ^p — and the character of the resulting permutation representation is the completed cycle product of superPS p 0: the colourings fixed by a permutation are the colourings constant on its orbits. Twisting by the sign character produces the completed cycle product of superPS 0 q. Pairing either character against a recast Jacobi–Trudi character identifies the Schur specialisation as the dimension of an equivariant Hom space.

The colour space and its permutation action

def RS.colourSpace (n p : ℕ) : Type

The colour space: all colourings of n sites in p colours, the basis of the n-th tensor power of ℂ^p.

Equations

• RS.colourSpace n p = (Fin n → Fin p)

@[instance_reducible]

instance RS.colourSpace.fintype (n p : ℕ) : Fintype (colourSpace n p)

The colour space is finite.

Equations

• RS.colourSpace.fintype n p = { elems := RS.colourSpace.fintype._aux_1 n p, complete := ⋯ }

@[instance_reducible]

noncomputable instance RS.colourSpace.decidableEq (n p : ℕ) : DecidableEq (colourSpace n p)

And its members can be compared.

Equations

• RS.colourSpace.decidableEq n p = Classical.decEq (RS.colourSpace n p)

@[instance_reducible]

instance RS.colourSpace.mulAction {n p : ℕ} : MulAction (Equiv.Perm (Fin n)) (colourSpace n p)

The symmetric group acts on the colour space by precomposition with the inverse permutation.

Equations

• RS.colourSpace.mulAction = { smul := fun (π : Equiv.Perm (Fin n)) (g : RS.colourSpace n p) => g ∘ ⇑π⁻¹, mul_smul := ⋯, one_smul := ⋯ }

noncomputable def RS.permRep (p n : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (MonoidAlgebra ℂ (colourSpace n p))

The permutation representation of S_n on the free vector space over the colour space: the n-th tensor power of the defining p-dimensional permutation representation.

Equations

• RS.permRep p n = Representation.ofMulAction ℂ (Equiv.Perm (Fin n)) (RS.colourSpace n p)

The character of the permutation representation

theorem RS.cycleFun_superPS_h {n : ℕ} (p : ℕ) (π : Equiv.Perm (Fin n)) : cycleFun (superPS p 0) π = ↑p ^ (π.cycleType.card + (n - π.cycleType.sum))

The completed cycle product of the one-sided super power sums superPS p 0 is p raised to the number of orbits.

theorem RS.char_permRep (p n : ℕ) (π : Equiv.Perm (Fin n)) : (permRep p n).character π = cycleFun (superPS p 0) π

The character of the colour-space permutation representation is the completed cycle product of the one-sided super power sums superPS p 0.

The sign twist

noncomputable def RS.signRep (n : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) ℂ

The sign representation of the symmetric group on ℂ.

Equations

• RS.signRep n = { toFun := fun (π : Equiv.Perm (Fin n)) => ↑↑(Equiv.Perm.sign π) • LinearMap.id, map_one' := ⋯, map_mul' := ⋯ }

theorem RS.char_signRep (n : ℕ) (π : Equiv.Perm (Fin n)) : (signRep n).character π = ↑↑(Equiv.Perm.sign π)

The character of the sign representation is the sign.

noncomputable def RS.signPermRep (q n : ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (TensorProduct ℂ ℂ (MonoidAlgebra ℂ (colourSpace n q)))

The sign twist of the colour-space permutation representation: the tensor product with the sign character.

Equations

• RS.signPermRep q n = (RS.signRep n).tprod (RS.permRep q n)

theorem RS.cycleFun_superPS_e {n : ℕ} (q : ℕ) (π : Equiv.Perm (Fin n)) : cycleFun (superPS 0 q) π = ↑↑(Equiv.Perm.sign π) * ↑q ^ (π.cycleType.card + (n - π.cycleType.sum))

The completed cycle product of the one-sided super power sums superPS 0 q is the sign times q raised to the number of orbits.

theorem RS.char_signPermRep (q n : ℕ) (π : Equiv.Perm (Fin n)) : (signPermRep q n).character π = cycleFun (superPS 0 q) π

The character of the sign-twisted permutation representation is the completed cycle product of the one-sided super power sums superPS 0 q.

The multiplicity conclusions

Pairing either character against a recast Jacobi–Trudi character identifies the Schur specialisation at the one-sided super power sums as the dimension of an equivariant Hom space.

theorem RS.diagramSchur_superPS_h_exists_nat {n : ℕ} (p : ℕ) (μ : Shape n) : ∃ (m : ℕ), diagramSchur (↑μ) (superPS p 0) = ↑m

Schur specialisations at superPS p 0 are multiplicities: the value is the dimension of an equivariant Hom space, a natural number.

theorem RS.diagramSchur_superPS_e_exists_nat {n : ℕ} (q : ℕ) (μ : Shape n) : ∃ (m : ℕ), diagramSchur (↑μ) (superPS 0 q) = ↑m

Schur specialisations at superPS 0 q are multiplicities: the value is the dimension of an equivariant Hom space, a natural number.