The symmetric-group Schur interface

SchurPackage bundles, as hypotheses, the classical representation theory of the symmetric groups that the development consumes: for each Young diagram μ a dimension dim μ and a character char μ : Perm (Fin μ.card) → ℂ, such that the attached elements

`e μ = (dim μ / μ.card !) • ∑ π, char μ π • π`

are central idempotents of the group algebra ℂ[S_{μ.card}] whose blocks have dimension (dim μ)² and are faithfully represented or killed as a whole (block_faithful); together with the branching containment (branching), the growth of the square-diagram dimension (square_dim), and the Frobenius character formula stated against the Jacobi–Trudi determinant of SymFun/PowerSums.lean (frobenius).

Everything here is standard — Fulton–Harris §4, Sagan, or James–Kerber; the fields are exactly what the hook-confinement and trace arguments of Envelope/ consume, no more. A term is constructed from mathlib's linear algebra as RS.schurPackage in RS/Classical/SchurTheory/Package.lean.

@[reducible, inline]

abbrev RS.SymGroupAlgebra (n : ℕ) : Type

The complex group algebra of the symmetric group S_n.

Equations

• RS.SymGroupAlgebra n = MonoidAlgebra ℂ (Equiv.Perm (Fin n))

noncomputable def RS.symCast {m n : ℕ} (h : m ≤ n) : SymGroupAlgebra m →ₐ[ℂ] SymGroupAlgebra n

Extension of scalars of the group algebra along the standard embedding S_m ↪ S_n (permutations extended by the identity), for m ≤ n.

Equations

• RS.symCast h = MonoidAlgebra.mapDomainAlgHom ℂ ℂ (Equiv.Perm.viaEmbeddingHom (Fin.castLEEmb h))

noncomputable def RS.charIdempotent {n : ℕ} (d : ℕ) (χ : Equiv.Perm (Fin n) → ℂ) : SymGroupAlgebra n

The group-algebra element (d / n!) • ∑ π, χ π • π attached to a prospective dimension d and character χ.

Equations

• RS.charIdempotent d χ = (↑d / ↑n.factorial) • ∑ π : Equiv.Perm (Fin n), χ π • (MonoidAlgebra.of ℂ (Equiv.Perm (Fin n))) π

structure RS.SchurPackage : Type

The classical representation theory of the symmetric groups, as consumed by this development. A term of this structure is an input of the development.

• dim : YoungDiagram → ℕ

  The dimension of the irreducible representation of shape μ.

• char (μ : YoungDiagram) : Equiv.Perm (Fin μ.card) → ℂ

  The irreducible character of shape μ.

• dim_pos (μ : YoungDiagram) : 0 < self.dim μ

  Dimensions are positive.

• central (μ : YoungDiagram) (x : SymGroupAlgebra μ.card) : charIdempotent (self.dim μ) (self.char μ) * x = x * charIdempotent (self.dim μ) (self.char μ)

  The attached idempotents are central.

• idem (μ : YoungDiagram) : charIdempotent (self.dim μ) (self.char μ) * charIdempotent (self.dim μ) (self.char μ) = charIdempotent (self.dim μ) (self.char μ)

  The attached elements are idempotent.

• block_rank (μ : YoungDiagram) : Module.finrank ℂ ↥(LinearMap.mulLeft ℂ (charIdempotent (self.dim μ) (self.char μ))).range = self.dim μ ^ 2

  The block of shape μ — the ideal e μ * ℂ[S_n] — has dimension (dim μ)².

• block_faithful (μ : YoungDiagram) (B : Type u) [Ring B] [Algebra ℂ B] (φ : SymGroupAlgebra μ.card →ₐ[ℂ] B) : φ (charIdempotent (self.dim μ) (self.char μ)) ≠ 0 → ∀ (x : SymGroupAlgebra μ.card), φ (charIdempotent (self.dim μ) (self.char μ) * x) = 0 → charIdempotent (self.dim μ) (self.char μ) * x = 0

  Blocks are simple: an algebra morphism that does not kill e μ is injective on the block of μ.

• branching (lam mu : YoungDiagram) : lam ≤ mu → ∀ (h : lam.card ≤ mu.card), charIdempotent (self.dim mu) (self.char mu) * (symCast h) (charIdempotent (self.dim lam) (self.char lam)) * charIdempotent (self.dim mu) (self.char mu) ≠ 0

  Branching containment: for lam ⊆ mu the element e mu * (e lam ⊗ 1) * e mu of the block of mu is nonzero.

• square_dim (R : ℕ) : ∃ (s : ℕ), R ^ s ^ 2 < self.dim (squareDiagram s)

  The square-diagram dimensions outgrow every exponential R ^ (s²).

• frobenius (μ : YoungDiagram) (t : ℕ → ℂ) : (↑μ.card.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin μ.card), self.char μ π * ((Multiset.map t π.cycleType).prod * t 1 ^ (μ.card - π.cycleType.sum)) = diagramSchur μ t

  The Frobenius character formula, stated against the Jacobi–Trudi determinant: for every scalar sequence t, (1/n!) ∑ π, char μ π · ∏_{c ∈ ρ(π)} t c = s_μ[t], where ρ(π) is the full cycle type including fixed points — the cycleType of mathlib excludes one-cycles, so the product is completed by (t 1) ^ (#fixed points). (The uncompleted form is false already at n = 1.)

noncomputable def RS.SchurPackage.e (P : SchurPackage) (μ : YoungDiagram) : SymGroupAlgebra μ.card

The central idempotent of shape μ.

Equations

• P.e μ = RS.charIdempotent (P.dim μ) (P.char μ)

theorem RS.SchurPackage.e_def (P : SchurPackage) (μ : YoungDiagram) : P.e μ = charIdempotent (P.dim μ) (P.char μ)

e unfolds to charIdempotent of the package's data.