The Jacobi–Trudi virtual character as a signed sum of native characters

Every summand in the Jacobi–Trudi character formula is a colour-class representation character, hence decomposes into native characters of simple submodules. Assembling these decompositions over the Leibniz sum yields jtChar μ as a signed combination of native characters with signs in {±1}.

theorem RS.jtChar_eq_sum_sign_nChar (μ : YoungDiagram) : ∃ (J : Type) (x : Fintype J) (ε : J → ℤ) (T : J → Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))), (∀ (j : J), IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥(T j)) ∧ (∀ (j : J), ε j = 1 ∨ ε j = -1) ∧ ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = ∑ j : J, ↑(ε j) * nChar (T j) π

The Jacobi–Trudi character is a signed sum of native characters: each summand of the formula is a colour-class character, which decomposes into simples.