ExampleConstruction: Literature-sourcedVerification: 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.

The row and column Specht modules

Statement

For every $n \geq 1$ , $S^{(n)}$ is the one-dimensional trivial complex representation of $S_{n}$ , while $S^{(1^{n})}$ is the one-dimensional sign representation. For $n = 0$ , $S^{\emptyset}$ is the one-dimensional trivial representation of $S_{0}$ .

Facts & Assumptions

Given: A natural number $n$ .

[F1]

The column antisymmetrizer is $κ_{t} = \sum_{γ \in C_{t}} sgn (γ) γ$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F2]

The polytabloid is $e_{t} = κ_{t} \cdot {t}$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F3]

The Specht space is the complex span of the polytabloids of shape $λ$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F4]

The diagram of $(n)$ has one box in each column, and the diagram of $(1^{n})$ has one column containing all $n$ boxes (Partitions, English diagrams, and conjugation).

[F5]

The column stabilizer consists of the permutations preserving each column set (Row and column stabilizers).

[F6]

Tabloids identify tableaux that have the same row sets (Young subgroups, tabloids, and permutation modules).

[F7]

Two tableaux are row-equivalent exactly when their row sets agree (Young subgroups, tabloids, and permutation modules).

[F8]

The tabloids form a basis of the tabloid module and the group action extends linearly (Young subgroups, tabloids, and permutation modules).

[F9]

The coefficient of ${t}$ in $e_{t}$ is $1$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F10]

The Specht space is generated by any one polytabloid (Polytabloid covariance and the column sign rule).

[F11]

The trivial representation is one-dimensional and every group element acts as the identity (The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

[F12]

The sign representation acts on $C$ by $σ \cdot a = sgn (σ) a$ (The sign representation of $S_{n}$ and the restriction ${Res}_{H}^{G} (V)$ of a representation to a subgroup).

[F13]

The sign function is a group homomorphism to ${+ 1, - 1}$ (The sign is a homomorphism $S_{n} \to {+ 1, - 1}$ , surjective exactly when $n \geq 2$ ).

[F14]

A tableau is a bijective filling of the boxes by $1, \dots, n$ (Tableaux and standard tableaux).

[F15]

At $n = 0$ , the row and column stabilizers of the empty tableau are $S_{0} = {1}$ (Row and column stabilizers).

[F16]

At $n = 0$ , the empty-tableau definition gives $e_{\emptyset} = {\emptyset}$ and $S^{\emptyset} = C$ (Column antisymmetrizers, polytabloids, and Specht modules).

Proof

technique · direct

1.1givenF1F2F3F4F5F6F8F11F14

Let $n \geq 1$ and take the row-filled tableau $t$ of shape $(n)$ . By [F4,F5], every tableau of this shape has singleton columns, so its antisymmetrizer is $1$ and every polytabloid is its tabloid. Every tableau has row set ${1, \dots, n}$ by [F14], so [F6] makes all tabloids equal; [F3] then gives $S^{(n)} = C e_{t}$ . The group fixes the sole tabloid by [F8], so $a e_{t} \mapsto a$ identifies the action with the trivial representation [F11].

1.2givenF1F4F5F7F8F9F14

Let $n \geq 1$ and take the tableau $t$ whose single column is filled by $1, \dots, n$ from top to bottom, which exists by [F14]. By [F4,F5], $C_{t} = S_{n}$ ; [F7,F8] make the tabloids ${σ \cdot t}$ distinct basis vectors, so $e_{t} = \sum_{σ \in S_{n}} sgn (σ) {σ \cdot t}$ has coefficient $1$ at ${t}$ by [F9] and is nonzero.

2.1step 1.2F10F12F13algebra

For $τ \in S_{n}$ , reindexing the sum of step 1.2 by $ρ = τ σ$ gives $τ \cdot e_{t} = \sum_{ρ \in S_{n}} sgn (τ^{- 1} ρ) {ρ \cdot t} = sgn (τ) e_{t}$ , since [F13] implies $sgn (τ^{- 1}) = sgn (τ)$ . By [F10], this orbit spans $S^{(1^{n})}$ , so step 1.2 gives $S^{(1^{n})} = C e_{t}$ ; the map $a e_{t} \mapsto a$ identifies its action with the sign representation [F12].

3.1givenF11F15F16∎

When $n = 0$ , [F16] gives $S^{\emptyset} = C e_{\emptyset} = C$ , and [F15] says $S_{0} = {1}$ acts as the identity; therefore this is the one-dimensional trivial representation [F11].

Depends on

Used by

All three Specht modules of S₃ Example

Dependency tree · two levels

22 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 - Definition 3.8, Lemma 3.11(b), and Example 3.14(a-b), printed pp. 12-14 (standard reference, not scraped)