TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Standard polytabloids form a basis of a complex Specht module

Statement

For every $n \geq 0$ and partition $λ ⊢ n$ , the family ${e_{t} : t is a standard λ -tableau}$ is a $C$ -basis of $S^{λ}$ . In particular, $\dim_{C} S^{λ} = f^{λ},$ including $\dim_{C} S^{\emptyset} = 1$ .

Facts & Assumptions

Given: $n \geq 0$ and a partition $λ ⊢ n$ .

[F1]

A $λ$ -tableau is a bijection from its finite Young diagram to ${1, \dots, n}$ (Tableaux and standard tableaux).

[F2]

A standard tableau has entries strictly increasing along rows and down columns (Tableaux and standard tableaux).

[F3]

The empty tableau is the unique standard tableau of shape $\emptyset$ (Tableaux and standard tableaux).

[F4]

$f^{λ}$ is the number of standard $λ$ -tableaux (Tableaux and standard tableaux).

[F5]

A canonical standard row-filled $λ$ -tableau $t_{0}$ exists; for $λ = \emptyset$ it is the empty tableau (Young subgroups, tabloids, and permutation modules).

[F6]

Two tabloids are equal exactly when their corresponding tableaux have the same row sets (Young subgroups, tabloids, and permutation modules).

[F7]

The tabloid order is a finite strict total order (Tabloid and column orders for Specht straightening).

[F8]

$e_{t} \in M^{λ}$ for every $λ$ -tableau $t$ , and $S^{λ} = {span}_{C} {e_{t} : t is a λ -tableau};$ for the empty shape, $e_{t_{0}} = {\emptyset}$ and $S^{\emptyset} = C$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F9]

For a column-standard tableau, the coefficient of its own tabloid in its polytabloid is $1$ and every other tabloid in it is strictly lower; the standard polytabloids are linearly independent (Leading tabloid of a column-standard polytabloid).

[F10]

Every polytabloid is a finite complex linear combination of standard polytabloids (Garnir straightening spans the complex Specht module).

[F11]

The span of a subset of a vector space is exactly the set of finite linear combinations of its elements ( $span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ ).

[F12]

A span is a linear subspace containing its generators (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[F13]

A span is contained in every linear subspace containing its generators (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[F14]

A basis is a linearly independent subset whose span is the whole vector space (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[F15]

The dimension of a vector space with a finite basis is the unique natural number equinumerous with that basis (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

No form of the Axiom of Choice (AC) is used. The tableau set is finite, the row-filled tableau is canonical, and Garnir straightening gives finite sums.

Proof

technique · direct

1.1givenF5F8

Let $E_{λ} = {e_{t} : t is a standard λ -tableau}$ . The canonical tableau $t_{0}$ from [F5] makes the indexing set nonempty, and [F8] gives $E_{λ} \subseteq S^{λ}$ .

1.2givenF2F6F7F9algebra

The family $(e_{t})_{t standard}$ is linearly independent by [F9]. The increasing rows [F2] and the row-set characterization [F6] show distinct standard tableaux have distinct tabloids; by the total order [F7], one of ${t}, {u}$ is greater, with coefficient $1$ in its own polytabloid by [F9] and coefficient $0$ in the other, whose terms are below its smaller leading tabloid. Thus $t \mapsto e_{t}$ is injective.

2.1givenF8F10F11F12F13step 1.1

Put $W = {span}_{C} (E_{λ})$ . Garnir straightening [F10] expresses every $e_{u}$ as a finite complex linear combination of members of $E_{λ}$ , so [F11] gives $e_{u} \in W$ . Since $W$ is a subspace [F12] containing all these generators, [F13] and [F8] give $S^{λ} \subseteq W$ ; conversely, step 1.1 gives $E_{λ} \subseteq S^{λ}$ , so [F13] gives $W \subseteq S^{λ}$ . Hence $W = S^{λ}$ .

3.1givenF14step 1.2step 2.1

By [F14], steps 1.2 and 2.1 show that $E_{λ}$ is a basis of $S^{λ}$ .

4.1givenF1F3F4F8F10F15step 1.2step 3.1∎

By [F1], standard tableaux form a finite set, and by [F4] it has $f^{λ}$ members; step 1.2 makes $t \mapsto e_{t}$ injective, so $∣ E_{λ} ∣ = f^{λ}$ . Thus [F15] and step 3.1 give $\dim_{C} S^{λ} = f^{λ}$ . If $λ = \emptyset$ , [F3] gives the unique empty standard tableau and [F8] gives its nonzero polytabloid and $S^{\emptyset} = C$ , hence the same singleton-basis argument gives $\dim_{C} S^{\emptyset} = 1$ . All sums in [F10] are finite; no RSK identity or axiom of choice is used.

Depends on

Used by

All three Specht modules of S₃ Example
Polytabloids of shape (2,1) Example

Dependency tree · two levels

37 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

Charlotte Chan, Representation Theory of Symmetric Groups, Theorem 4.11 and proof, Remark 4.13, printed pp. 16-17; the local spanning proof uses Garnir straightening instead of Chan's later RSK count (standard reference, not scraped)
Mark Wildon, Representation Theory of the Symmetric Group, Theorem 6.2, Proposition 6.5, Theorem 6.8, Definition 6.9 and Lemma 6.10 with proof, printed pp. 26-31 (standard reference, not scraped)