Zero-row padding for the Jacobi–Trudi character

When k ≥ μ.rowLens.length, the Jacobi–Trudi character jtChar μ can equivalently be written as a sum over Perm (Fin k): every extra permutation index beyond the diagram's row count contributes zero weight, because the guard forces it to be fixed.

Row lengths vanish beyond the diagram

theorem RS.rowLen_eq_zero_of_ge (μ : YoungDiagram) {i : ℕ} (hi : μ.rowLens.length ≤ i) : μ.rowLen i = 0

μ.rowLen i = 0 for i ≥ μ.rowLens.length.

theorem RS.get_rowLens_eq_rowLen (μ : YoungDiagram) (i : Fin μ.rowLens.length) : μ.rowLens.get i = μ.rowLen ↑i

μ.rowLens.get i = μ.rowLen i (bridging List.get and rowLen).

Tail-fixing: permutations satisfying the guard fix indices

beyond the diagram

theorem RS.tail_fixed_of_guard (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ : Equiv.Perm (Fin k)) (hguard : ∀ (i : Fin k), 0 ≤ ↑(μ.rowLen ↑i) + ↑↑(σ i) - ↑↑i) (i : Fin k) (hi : μ.rowLens.length ≤ ↑i) : σ i = i

The guard forces a permutation to fix every index beyond the diagram's rows: the row length there is zero, so the guard fails unless the index is fixed.

Restriction and extension of tail-fixing permutations

noncomputable def RS.restrictHead (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ : Equiv.Perm (Fin k)) (hfix : ∀ (i : Fin k), μ.rowLens.length ≤ ↑i → σ i = i) : Equiv.Perm (Fin μ.rowLens.length)

Restrict a tail-fixing permutation to the head indices.

Equations

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

noncomputable def RS.extendTail (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ' : Equiv.Perm (Fin μ.rowLens.length)) : Equiv.Perm (Fin k)

Extend a permutation of Fin μ.rowLens.length to Fin k by fixing tail indices.

Equations

• RS.extendTail μ hk σ' = σ'.viaEmbedding (Fin.castLEEmb hk)

theorem RS.extendTail_fixes_tail (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ' : Equiv.Perm (Fin μ.rowLens.length)) (i : Fin k) (hi : μ.rowLens.length ≤ ↑i) : (extendTail μ hk σ') i = i

The extension fixes the tail indices by construction.

theorem RS.extendTail_apply (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ' : Equiv.Perm (Fin μ.rowLens.length)) (j : Fin μ.rowLens.length) : (extendTail μ hk σ') (Fin.castLE hk j) = Fin.castLE hk (σ' j)

On head indices it acts as the permutation extended.

theorem RS.restrictHead_extendTail (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ' : Equiv.Perm (Fin μ.rowLens.length)) : restrictHead μ hk (extendTail μ hk σ') ⋯ = σ'

Restricting an extension recovers the permutation.

theorem RS.extendTail_restrictHead (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ : Equiv.Perm (Fin k)) (hfix : ∀ (i : Fin k), μ.rowLens.length ≤ ↑i → σ i = i) : extendTail μ hk (restrictHead μ hk σ hfix) = σ

And extending a restriction recovers the tail-fixing permutation: the two are inverse.

Sign preservation

theorem RS.sign_extendTail (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (σ' : Equiv.Perm (Fin μ.rowLens.length)) : Equiv.Perm.sign (extendTail μ hk σ') = Equiv.Perm.sign σ'

Extension preserves sign, fixing the added indices.

colourChar extension by zeros

theorem RS.colourChar_extend_zero {n N k : ℕ} (hNk : N ≤ k) (α : Fin N → ℕ) (_hsum : ∑ j : Fin N, α j = n) (π : Equiv.Perm (Fin n)) : colourChar α π = colourChar (fun (i : Fin k) => if h : ↑i < N then α ⟨↑i, h⟩ else 0) π

colourChar is invariant under extending the composition by zeros.

Main theorem

theorem RS.jtChar_pad (μ : YoungDiagram) {k : ℕ} (hk : μ.rowLens.length ≤ k) (π : Equiv.Perm (Fin μ.card)) : jtChar μ π = ∑ σ : Equiv.Perm (Fin k), ↑↑(Equiv.Perm.sign σ) * if ∀ (i : Fin k), 0 ≤ ↑(μ.rowLen ↑i) + ↑↑(σ i) - ↑↑i then ↑(colourChar (fun (i : Fin k) => (↑(μ.rowLen ↑i) + ↑↑(σ i) - ↑↑i).toNat) π) else 0

The padded Jacobi–Trudi character: summing over Perm (Fin k) for any k at least the row count gives the same value, the extra indices contributing only through the terms their guard admits.