The Jacobi–Trudi character is plus-or-minus a native character #
theorem
RS.jtChar_pm_simple
(μ : YoungDiagram)
:
∃ (S₀ : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))),
IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥S₀ ∧ ((∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = nChar S₀ π) ∨ ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = -nChar S₀ π)
The Jacobi–Trudi character is ± a single native
character.