TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The determinantal form of a Specht character

Statement

Let $R_{S} = ⨁_{m \geq 0} R (S_{m})$ be the graded ordinary representation ring of the symmetric groups, whose multiplication is the outer induction product $\circ$ and whose unit is the trivial character of $S_{0}$ (The graded ordinary representation ring of the symmetric groups, The outer induction product of symmetric-group characters). For $m \geq 0$ let $[m] \in R (S_{m})$ denote the trivial character of $S_{m}$ (so $[0]$ is the unit of $R_{S}$ ), and set $[m] : = 0 \in R_{S}$ for $m < 0$ ; the Frobenius characteristic $ch$ is the degree-preserving ring isomorphism of The Frobenius characteristic is an isometric graded ring isomorphism normed by $ch (χ^{ν}) = s_{ν}$ (The characteristic of a Specht character is a Schur function, The Frobenius characteristic map).

Then for every partition $λ = (λ_{1} \geq \dots \geq λ_{k} > 0)$ of $n$ , with $χ^{λ} \in R (S_{n})$ the character of the complex Specht module $S^{λ}$ (Column antisymmetrizers, polytabloids, and Specht modules, Complex Specht modules are irreducible), $χ^{λ} = \det ([λ_{i} - i + j])_{1 \leq i, j \leq k} in R_{S},$ where the determinant is the Leibniz expansion $\det ([λ_{i} - i + j]) = \sum_{w} sgn (w) [λ_{1} - 1 + w (1)] \circ [λ_{2} - 2 + w (2)] \circ \dots \circ [λ_{k} - k + w (k)]$ over the bijections $w$ of ${1, \dots, k}$ , with $sgn$ the sign of the corresponding permutation (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations). For every such $w$ the degrees add up to $\sum_{i = 1}^{k} (λ_{i} - i + w (i)) = \sum_{i} λ_{i} = n$ , so every nonzero monomial is homogeneous of degree $n$ and the determinant is a well-defined element of $R (S_{n})$ . For $n = 0$ use $λ = \emptyset$ , $k = 0$ , and the empty determinant and empty product equal to $[0]$ . The convention $[0] = 1$ (the multiplicative identity of $R_{S}$ ) must be distinguished from the zero element $0$ . No choice principle is used.

Facts & Assumptions

Given: A partition $λ = (λ_{1} \geq \dots \geq λ_{k} > 0)$ of $n$ , the graded ring $R_{S} = ⨁_{m \geq 0} R (S_{m})$ with the outer product $\circ$ and unit the trivial character of $S_{0}$ , the elements $[m] \in R (S_{m})$ for $m \geq 0$ and $[m] : = 0$ for $m < 0$ , and the characteristic map $ch$ .

[F1]

$R (S_{m})$ is the $Z$ -span of the irreducible characters of $S_{m}$ ; $R_{S}$ is the direct sum with degree- $m$ components, and under the outer product it is a commutative graded $Z$ -algebra with unit the trivial character of $S_{0}$ (The graded ordinary representation ring of the symmetric groups, The outer induction product of symmetric-group characters, The Frobenius characteristic is an isometric graded ring isomorphism). The outer product of elements of degrees $a_{1}, \dots, a_{k} \geq 0$ is homogeneous of degree $a_{1} + \dots + a_{k}$ , and if some degree is negative the corresponding entry is $0$ by the convention on $[m]$ .

[F2]

$ch : R_{S} \to Λ$ is a degree-preserving $Z$ -module isomorphism, carries the outer product to the product in $Λ$ and the unit to $1$ , and is therefore injective (The Frobenius characteristic is an isometric graded ring isomorphism, The Frobenius characteristic preserves outer products).

[F3]

$ch (χ^{ν}) = s_{ν}$ for every $n \geq 0$ and every partition $ν ⊢ n$ (The characteristic of a Specht character is a Schur function); for $m \geq 1$ the one-row Specht module is trivial, since its tabloid space has one basis vector and its column stabilizer is trivial (Column antisymmetrizers, polytabloids, and Specht modules). Thus $ch ([m]) = s_{(m)}$ for $m \geq 1$ ; for $m = 0$ use the empty partition and $ch ([0]) = 1$ .

[F4]

Jacobi–Trudi: for $r \geq ℓ (λ)$ , $s_{λ} = \det (h_{λ_{i} - i + j})_{1 \leq i, j \leq r}$ , where $h_{q}$ is the stable complete homogeneous function, $h_{0} = 1$ , and $h_{q} = 0$ for $q < 0$ (Jacobi–Trudi and dual Jacobi–Trudi identities). In particular $s_{(m)} = h_{m}$ for every $m \geq 1$ by the case $r = 1$ ; for the empty partition $s_{\emptyset} = h_{0} = 1$ , and $h_{m} = 0$ for $m < 0$ .

[F5]

The determinant over a commutative ring is the Leibniz sum $\det (A) = \sum_{σ} sgn (σ) \prod_{i} a_{σ (i), i}$ of the entries (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations); the equivalent row-indexed sum uses $w = σ^{- 1}$ . Their signs agree: $(i, j) \mapsto (σ (j), σ (i))$ bijects the inversions of $σ$ with those of $σ^{- 1}$ . A unital ring homomorphism $φ$ sends the finite sums and products defining the determinant of $A$ to those defining the determinant of the entrywise image $φ (A)$ .

Proof

technique · direct

1.1F3F4given

For every integer $m$ one has $ch ([m]) = h_{m}$ . For $m \geq 1$ this is $ch ([m]) = ch (χ^{(m)}) = s_{(m)} = h_{m}$ by [F3] and the case $r = 1$ of [F4]; for $m = 0$ both sides are $1$ by [F3] and [F4]; for $m < 0$ both sides are $0$ , since $[m] : = 0$ and $ch$ is additive with $ch (0) = 0$ , while $h_{m} = 0$ by the convention of [F4].

1.2F1F5algebra

Every bijection $w$ of ${1, \dots, k}$ satisfies $\sum_{i} (λ_{i} - i + w (i)) = \sum_{i} λ_{i} = n$ , because $\sum_{i} i = \sum_{i} w (i)$ . Hence the Leibniz term $[λ_{1} - 1 + w (1)] \circ \dots \circ [λ_{k} - k + w (k)]$ is a product of $k$ homogeneous elements whose degrees sum to $n$ : if every $λ_{i} - i + w (i) \geq 0$ it lies in the degree- $n$ component $R (S_{n})$ of $R_{S}$ , and if some $λ_{i} - i + w (i) < 0$ then the corresponding factor is the zero element, so the term is $0$ by [F1]. For $k = 0$ the sole empty term is $[0]$ . The determinant $\det H$ is the finite sum of these $k!$ terms, hence is a well-defined element of the degree- $n$ component $R (S_{n})$ of $R_{S}$ .

2.1step 1.1F1F2F3F4F5algebra

Let $H$ be the $k \times k$ matrix with entries $h_{i j} : = [λ_{i} - i + j] \in R_{S}$ over the commutative ring $R_{S}$ of [F1]. Applying the unital ring homomorphism $ch$ entrywise to $H$ gives the matrix with entries $ch (h_{i j}) = h_{λ_{i} - i + j}$ by step 1.1. Since $ch$ preserves finite sums and products, it commutes with the Leibniz determinant [F5], so $ch (\det H) = \det (h_{λ_{i} - i + j}) = s_{λ} = ch (χ^{λ}),$ where the middle equality is Jacobi–Trudi at $r = k \geq ℓ (λ)$ and the last is [F3].

3.1step 2.1step 1.2F1F2F3F4algebra∎

Since $ch$ is injective by [F2], the equality $ch (\det H) = ch (χ^{λ})$ of step 2.1 gives $\det H = χ^{λ}$ in $R_{S}$ , which is the asserted determinant identity. Finally $[0] \in R (S_{0})$ is the trivial character of the trivial group and the identity of $R_{S}$ , with $ch ([0]) = h_{0} = 1$ , whereas the zero element $0 \in R_{S}$ satisfies $ch (0) = 0$ ; since $1 \neq 0$ in $Λ$ and $ch$ is injective on the degree- $0$ component, $[0] \neq 0$ , so the two conventions are distinct.

Remarks

Where the two determinant conventions enter. The entries $[λ_{i} - i + j]$ are zero as soon as the index $λ_{i} - i + j$ is negative, so very few of the $k!$ Leibniz terms survive; the terms that do survive all lie in the same degree- $n$ component. The identity $\sum_{i} (λ_{i} - i + w (i)) = n$ is the reason the determinant is an element of the homogeneous piece $R (S_{n})$ rather than of the whole graded ring.
The Jacobi–Trudi route. The proof transports the Jacobi–Trudi determinant for Schur functions through the characteristic isomorphism, which is the reason the statement is an identity in $R_{S}$ rather than a numerical formula: the theorem is the character-theoretic mirror of $s_{λ} = \det (h_{λ_{i} - i + j})$ . James's §19 expansion of the same determinant is an independent combinatorial proof of the identical identity and is the source recorded for the statement.

Depends on

Used by

Dependency tree · two levels

60 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

G. D. James, The Representation Theory of the Symmetric Groups, Lecture Notes in Mathematics 682, Springer 1978 (complete author-hosted scan, 161 pp.) (standard reference, not scraped)
I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford Mathematical Monographs, 1995 (complete author-hosted scan, 486 pp.) (standard reference, not scraped)