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.

Complex Specht modules are irreducible

Statement

For every $n \geq 0$ and $λ ⊢ n$ , the nonzero complex $S_{n}$ -representation $S^{λ}$ is irreducible.

Facts & Assumptions

Given: $n \geq 0$ , $λ ⊢ n$ , and a nonzero $S_{n}$ -subrepresentation $U \subseteq S^{λ}$ .

[F1]

$S^{λ}$ is the complex span of its polytabloids, which lie in the tabloid module $M^{λ}$ (Column antisymmetrizers, polytabloids, and Specht modules).

[F2]

$M^{λ}$ is a finite-dimensional complex representation of $S_{n}$ (Young subgroups, tabloids, and permutation modules).

[F3]

$S^{λ}$ is an $S_{n}$ -subrepresentation of $M^{λ}$ (Polytabloid covariance and the column sign rule).

[F4]

For every $S_{n}$ -submodule $V \subseteq M^{λ}$ , either $S^{λ} \subseteq V$ or $V \subseteq (S^{λ})^{⊥}$ (James's submodule theorem over the complex numbers).

[F5]

$S^{λ} \neq 0$ and $S^{λ} \cap (S^{λ})^{⊥} = {0}$ (Complex Specht modules have nondegenerate Hermitian self-pairing).

[F6]

A subrepresentation is a linear subspace stable under every group element (Subrepresentations, direct sums of representations, and irreducibility).

[F7]

A representation is irreducible when it is nonzero and its only subrepresentations are $0$ and the whole representation (Subrepresentations, direct sums of representations, and irreducibility).

No form of the Axiom of Choice is used.

Proof

technique · direct

1.1givenF1F2F3F4F6

By [F1]-[F3], $S^{λ}$ is a finite-dimensional subrepresentation of $M^{λ}$ . Since the given $U$ is a subrepresentation of $S^{λ}$ , [F6] makes $U$ stable under every $σ \in S_{n}$ also as a subspace of $M^{λ}$ . Therefore [F4] applies to $U$ .

2.1givenF4F5step 1.1

If the second branch of [F4] holds, then the given $U \subseteq S^{λ}$ also satisfies $U \subseteq (S^{λ})^{⊥}$ . By [F5], this forces $U \subseteq {0}$ , contrary to the nonzero hypothesis. Thus the first branch gives $S^{λ} \subseteq U$ .

3.1givenstep 2.1

The given inclusion $U \subseteq S^{λ}$ and step 2.1 imply $U = S^{λ}$ .

4.1givenF5F7step 3.1∎

By [F5], $S^{λ}$ is nonzero, and step 3.1 shows that every nonzero subrepresentation equals $S^{λ}$ . Thus [F7] gives that $S^{λ}$ is irreducible.

Depends on

Used by

Specht modules classify the complex irreducibles of Sₙ Theorem

Dependency tree · two levels

18 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.4(b) and proof, printed p. 16; Theorem 9.4 and complete proof of the submodule dichotomy, printed pp. 31-32 (standard reference, not scraped)