The central idempotents, indexed by shapes of a fixed size

SchurPackage.e μ lives in the group algebra of S_{μ.card}; the Deligne development sums such idempotents over all shapes of one size n, so it needs them all in the same algebra. Shape.e recasts the idempotent of μ : Shape n into SymGroupAlgebra n along the standard embedding at μ.prop : μ.val.card = n — an algebra map, so idempotence and products transport; an injective one, so nonvanishing transports too.

theorem RS.symCast_injective {m n : ℕ} (h : m ≤ n) : Function.Injective ⇑(symCast h)

symCast along an equality of sizes is injective (it is mapDomain along an injective map).

noncomputable def RS.Shape.e (P : SchurPackage) {n : ℕ} (μ : Shape n) : SymGroupAlgebra n

The central idempotent of a shape of size n, recast into the group algebra of S_n.

Equations

• RS.Shape.e P μ = (RS.symCast ⋯) (P.e ↑μ)

theorem RS.Shape.e_mul_self (P : SchurPackage) {n : ℕ} (μ : Shape n) : e P μ * e P μ = e P μ

The recast idempotent is idempotent.

theorem RS.Shape.e_eq_zero_iff (P : SchurPackage) {n : ℕ} (μ : Shape n) : e P μ = 0 ↔ P.e ↑μ = 0

The recast idempotent is nonzero exactly when the original is.