The regular-representation dimension bound #
For every SchurPackage and every size n, the central
idempotents of the shapes of size n are pairwise orthogonal and
sum to the identity of ℂ[S_n]; reading off the coefficient of
the identity permutation, the squares of the dimensions sum to
n! — the Wedderburn completeness of the blocks. The
Cauchy–Schwarz-free consequences n! ≤ (∑ dim)² and
√(n!) ≤ ∑ dim are the forms consumed by the Deligne development
(Catégories tensorielles, 1.20).
The proof pins the package's characters: centrality makes them
class functions, and the Frobenius field determines a class
function completely, by linear independence of the completed
cycle-type monomials — so they agree with the Jacobi–Trudi
characters and the package idempotents are the native projectors.
Orthogonality then reduces, through the action table and the
faithfulness trick, to injectivity of the Schur specialisation
μ ↦ diagramSchur μ, proved by evaluating at genuine variable
families and extracting an alternant coefficient. Completeness is
a dimension count in the centre of the group algebra against the
class sums, which are no more numerous than the shapes.
Polynomial identities from evaluations #
Two multivariate polynomials over ℂ agreeing at every point are
equal. (Mathlib's MvPolynomial.funext is not part of the tree's
Mathlib footprint, so the finitely-many-variables case is rebuilt
here from the one-variable statement.)
A multivariate polynomial over ℂ in finitely many variables
vanishing at every point is zero.
Two multivariate polynomials over ℂ in finitely many
variables agreeing at every point are equal.
A multivariate polynomial over ℂ in countably many variables
vanishing at every point is zero.
Separation by the Schur specialisation #
The Jacobi–Trudi determinant is stable under padding the row-length
vector with zero rows, evaluates at genuine power sums to the
polynomial Jacobi–Trudi determinant, and — through the bialternant
identity and the strict alternant coefficient — separates diagrams:
μ ↦ diagramSchur μ is injective.
Evaluating the complete homogeneous polynomial in all variables gives the complete homogeneous value.
Evaluating the ℤ-indexed complete homogeneous polynomial
gives the Newton lift of the power sums of the variables.
The Jacobi–Trudi determinant of a diagram, evaluated at a variable family, is the Schur specialisation at its power sums.
Injectivity of the Schur specialisation: diagrams with the same Schur values at every prospective power-sum sequence are equal.
Transport along an equality of sizes #
Shape.e recasts idempotents along symCast at an equality of
sizes; on coefficients this is relabelling of permutations along
permCast, which preserves products, inverses, and cycle types.
Relabelling of permutations along an equality of sizes.
Equations
- RS.permCast h = (finCongr h).permCongr
Instances For
At rfl, relabelling is the identity.
Relabelling preserves cycle types.
symCast at a reflexive inequality is the identity.
Coefficients of a recast element are coefficients of the original, at the relabelled permutation.
Recasting a class element relabels its coefficient function.
Coefficients of the package idempotents #
The coefficient function of P.e μ, the block-rank computation of
the identity coefficient, and the conjugation invariance of the
package's characters, forced by centrality.
charIdempotent is the class element of the normalised
character — no inversion invariance required.
The coefficients of the central idempotent of a shape.
The block rank at the identity coefficient: the square of the
dimension is n! times the identity coefficient of the
idempotent.
The package's character at the identity is the dimension.
The central idempotents are nonzero.
The package's characters are class functions: conjugation invariance is forced by the centrality of the idempotents.
The Frobenius field determines the characters #
The completed cycle-type monomials attached to distinct cycle types
are distinct monomials, hence linearly independent as functions of
the prospective power sums; a class function with vanishing
cycle-weighted sums at every t is therefore zero. Comparing the
package's Frobenius field with the Jacobi–Trudi one pins
P.char = jtChar and P.dim = nDim ∘ jtSimple, identifying the
package idempotents with the native projectors.
Products of powers over a multiset's counting record.
The completed cycle-type monomial evaluates to the completed cycle-type product.
A class function is determined by its Frobenius pairings: if all its completed cycle-weighted sums vanish, it vanishes.
The package's characters are the Jacobi–Trudi ones.
The package's dimensions are the native ones.
The package idempotents are the native projectors.
Orthogonality of the blocks #
Distinct shapes of one size have orthogonal central idempotents: through the native action table, a common simple module would force the two Jacobi–Trudi characters to agree, hence the two Schur specialisations, hence the shapes — by the separation theorem.
Relabelling as a homomorphism of permutation groups.
Equations
- RS.permCastHom h = { toFun := ⇑(RS.permCast h), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Pulling a representation back along a relabelling preserves irreducibility.
Orthogonality of the recast idempotents, unbundled form: distinct diagrams of one size have orthogonal idempotents.
Orthogonality of the blocks: distinct shapes of one size have orthogonal recast idempotents.
Completeness of the blocks #
The recast idempotents are linearly independent — orthogonal
nonzero idempotents — and all lie in the span of the class sums,
which is at most p(n)-dimensional; as there are exactly p(n)
shapes, they must span, and expanding the identity over them forces
every coefficient to be 1.
The full cycle type determines the cycle type.
The class sum of a full cycle type.
Equations
- RS.classSum n ρ = ∑ π : Equiv.Perm (Fin n) with RS.fullPartition π = ρ, MonoidAlgebra.single π 1
Instances For
Class elements lie in the span of the class sums: the
conjugation-invariant elements are spanned by p(n) vectors.
The recast idempotent of a shape is a class element.
The recast idempotents lie in the span of the class sums.
The recast idempotents are nonzero.
The recast idempotents are linearly independent.
The identity of the group algebra lies in the span of the class sums.
Every element in the class-sum span has coordinates in the recast central idempotents.
Completeness of the blocks: at every size the recast central idempotents sum to the identity of the group algebra.
The regular-representation dimension bound #
Reading the identity coefficient off the completeness identity
gives ∑ (dim μ)² = n!; the elementary inequality
∑ aᵢ² ≤ (∑ aᵢ)² for naturals and a square root then give the
forms consumed by the Deligne development.
Wedderburn completeness of the blocks: the squares of the
dimensions of the shapes of size n sum to n!.
The factorial is at most the square of the dimension sum.
The regular-representation dimension bound: the dimensions
of the shapes of size n sum to at least √(n!).