The interface idempotent as a class element #
charIdempotent of the interface unfolds to a classElem of the
projector theory; for inversion-invariant class functions the
normalizations agree, identifying charIdempotent (nDim S) (nChar S)
with nProjector S over the symmetric group.
theorem
RS.charIdempotent_eq_classElem
{n : ℕ}
(d : ℕ)
(χ : Equiv.Perm (Fin n) → ℂ)
(hinv : ∀ (π : Equiv.Perm (Fin n)), χ π⁻¹ = χ π)
:
charIdempotent is the class element of the normalized
inverted character.
theorem
RS.charIdempotent_eq_nProjector
{n : ℕ}
(S : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin n))) (MonoidAlgebra ℂ (Equiv.Perm (Fin n))))
(χ : Equiv.Perm (Fin n) → ℂ)
(hχ : ∀ (π : Equiv.Perm (Fin n)), χ π = nChar S π)
(hinv : ∀ (π : Equiv.Perm (Fin n)), χ π⁻¹ = χ π)
:
Over the symmetric group, charIdempotent of a simple
submodule's data is the native projector.