The Jacobi–Trudi virtual character

For a Young diagram μ with n = μ.card cells and k rows, the virtual character jtChar μ is the signed sum, over σ ∈ S_k, of the colour characters of the shifted compositions i ↦ μᵢ + σ(i) − i (terms with a negative part vanish). Its Frobenius transform is the Jacobi–Trudi determinant diagramSchur μ: each Leibniz term is evaluated by the colour cycle sum. The two cycle-type transport facts enter as explicit hypotheses, discharged in ColourCycleSum.lean.

def RS.jtSigned (μ : YoungDiagram) (σ : Equiv.Perm (Fin μ.rowLens.length)) (i : Fin μ.rowLens.length) : ℤ

The signed Jacobi–Trudi degree of row i under σ.

Equations

• RS.jtSigned μ σ i = ↑(μ.rowLens.get i) + ↑↑(σ i) - ↑↑i

theorem RS.sum_jtSigned (μ : YoungDiagram) (σ : Equiv.Perm (Fin μ.rowLens.length)) : ∑ i : Fin μ.rowLens.length, jtSigned μ σ i = ↑μ.card

The shifted composition sums to the diagram's size, the shifts cancelling.

def RS.jtComp (μ : YoungDiagram) (σ : Equiv.Perm (Fin μ.rowLens.length)) (i : Fin μ.rowLens.length) : ℕ

The shifted composition attached to a Leibniz term, when nonnegative.

Equations

• RS.jtComp μ σ i = (RS.jtSigned μ σ i).toNat

theorem RS.sum_jtComp (μ : YoungDiagram) (σ : Equiv.Perm (Fin μ.rowLens.length)) (hp : ∀ (i : Fin μ.rowLens.length), 0 ≤ jtSigned μ σ i) : ∑ i : Fin μ.rowLens.length, jtComp μ σ i = μ.card

Hence when no part is negative the composition itself does.

noncomputable def RS.jtChar (μ : YoungDiagram) (π : Equiv.Perm (Fin μ.card)) : ℂ

The Jacobi–Trudi virtual character of shape μ.

Equations

• RS.jtChar μ π = ∑ σ : Equiv.Perm (Fin μ.rowLens.length), ↑↑(Equiv.Perm.sign σ) * if ∀ (i : Fin μ.rowLens.length), 0 ≤ RS.jtSigned μ σ i then ↑(RS.colourChar (RS.jtComp μ σ) π) else 0

theorem RS.jtChar_frobenius (H1 : PermCongrCT) (H2 : SigmaCT) (μ : YoungDiagram) (t : ℕ → ℂ) : (↑μ.card.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin μ.card), jtChar μ π * cycleProd t π = diagramSchur μ t

The Frobenius formula for the Jacobi–Trudi character: its normalized cycle-weighted sum is the Jacobi–Trudi determinant.