Branching from the restriction pairing

If the mixed character pairing of lam against the restriction of mu does not vanish, the branching sandwich is nonzero: apply the block representation of mu, use that its projector acts as the identity, and compute the trace of the cast idempotent as the pairing.

noncomputable def RS.restrPairing (lam mu : YoungDiagram) (h : lam.card ≤ mu.card) : ℂ

The mixed restriction pairing.

Equations

• RS.restrPairing lam mu h = ∑ σ : Equiv.Perm (Fin lam.card), RS.jtChar lam σ * RS.jtChar mu ((Equiv.Perm.viaEmbeddingHom (Fin.castLEEmb h)) σ)

theorem RS.trace_symCast_charIdempotent (lam mu : YoungDiagram) (h : lam.card ≤ mu.card) : (LinearMap.trace ℂ (subCarrier (jtSimple mu))) ((rhoS (jtSimple mu)).asAlgebraHom ((symCast h) (charIdempotent (nDim (jtSimple lam)) (jtChar lam)))) = ↑(nDim (jtSimple lam)) / ↑lam.card.factorial * restrPairing lam mu h

The trace of the block representation on the cast idempotent is the normalized restriction pairing.

theorem RS.branching_of_pairing (lam mu : YoungDiagram) (h : lam.card ≤ mu.card) (HB : restrPairing lam mu h ≠ 0) : charIdempotent (nDim (jtSimple mu)) (jtChar mu) * (symCast h) (charIdempotent (nDim (jtSimple lam)) (jtChar lam)) * charIdempotent (nDim (jtSimple mu)) (jtChar mu) ≠ 0

Branching from a nonvanishing pairing.