Norm one forces a single simple

A ±1-signed combination of native characters with norm one is ± a single native character: group the index set by equivalence of the underlying simples, express the norm as a sum of integer squares over the classes, and conclude a unique class with coefficient ±1.

theorem RS.sum_sq_eq_one {Q : Type u_1} [Fintype Q] (Z : Q → ℤ) (h : ∑ q : Q, Z q * Z q = 1) : ∃ (q₀ : Q), (Z q₀ = 1 ∨ Z q₀ = -1) ∧ ∀ (q : Q), q ≠ q₀ → Z q = 0

A finite sum of integer squares equal to one has exactly one nonzero term, of value ±1.

theorem RS.jt_pm_nChar (μ : YoungDiagram) {J : Type} [Fintype J] (ε : J → ℤ) (T : J → Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))) (hT : ∀ (j : J), IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥(T j)) (hchar : ∀ (π : Equiv.Perm (Fin μ.card)), jtChar μ π = ∑ j : J, ↑(ε j) * nChar (T j) π) : ∃ (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₀ π)

Norm one forces a single simple.