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

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.

Young permutation modules are induced trivial modules

Statement

For every $n \geq 0$ and every partition $λ ⊢ n$ , the Young permutation module $M^{λ}$ is isomorphic, as a complex representation of $S_{n}$ , to the permutation representation of $S_{n}$ on the left coset set $S_{n} / S_{λ}$ , and hence to the induced representation ${Ind}_{S_{λ}}^{S_{n}} 1$ of the trivial complex representation of the standard Young subgroup $S_{λ}$ . This includes the case $n = 0$ , where $λ = \emptyset$ and $S_{\emptyset} = S_{0} = {1}$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , a partition $λ = (λ_{1}, \dots, λ_{k}) ⊢ n$ , the standard row-filled $λ$ -tableau $t_{0}$ , the standard Young subgroup $S_{λ} \leq S_{n}$ , and the Young permutation module $M^{λ}$ with tabloid basis $Ω_{λ}$ .

[L1]

The tabloids are the row-equivalence classes ${t} = {ρ \cdot t : ρ \in R_{t}}$ of $λ$ -tableaux, and $M^{λ} = C^{(Ω_{λ})}$ is the complex vector space with the tabloids as basis, on which $S_{n}$ acts by $σ \cdot {t} = {σ \cdot t}$ ; the stabilizer of the tabloid ${t}$ is the row stabilizer $R_{t}$ , the action on $Ω_{λ}$ is transitive, and for the standard row-filled tableau $t_{0}$ one has $R_{t_{0}} = S_{λ}$ , so the stabilizer of ${t_{0}}$ is $S_{λ}$ (Young subgroups, tabloids, and permutation modules).

[L2]

If $t \sim u$ are $λ$ -tableaux and $τ \in S_{n}$ , then $τ \cdot t \sim τ \cdot u$ ; this is the well-definedness of the tabloid action in [L1] (Young subgroups, tabloids, and permutation modules).

[L3]

Every $λ$ -tableau $t$ equals $σ \cdot t_{0}$ for a unique $σ \in S_{n}$ , because $σ (t_{0} (i, j)) : = t (i, j)$ defines a permutation of ${1, \dots, n}$ (Tableaux and standard tableaux).

[L4]

For a finite group $G$ and a subgroup $H \leq G$ , inducing the trivial complex representation of $H$ to $G$ gives the permutation representation of $G$ on the left coset set $G / H$ ; the cosets form the set $G / H = {g H : g \in G}$ with $G$ acting by $x \cdot (g H) = (x g) H$ , and the permutation representation has these cosets as a basis (Inducing the trivial representation gives the permutation representation on $G / H$ ).

Proof

technique · direct

1.1

Define $Φ : S_{n} / S_{λ} \to Ω_{λ}$ by $Φ (σ S_{λ}) : = {σ \cdot t_{0}}$ . This is well defined: if $σ S_{λ} = τ S_{λ}$ , then $τ^{- 1} σ \in S_{λ} = R_{t_{0}}$ , so $(τ^{- 1} σ) \cdot t_{0} \sim t_{0}$ by [L1], and applying $τ$ gives $σ \cdot t_{0} \sim τ \cdot t_{0}$ by [L2], that is ${σ \cdot t_{0}} = {τ \cdot t_{0}}$ .

givenL1L2construct

2.1

The map $Φ$ is injective: if ${σ \cdot t_{0}} = {τ \cdot t_{0}}$ , then $σ \cdot t_{0} \sim τ \cdot t_{0}$ , so $τ^{- 1} \cdot (σ \cdot t_{0}) \sim τ^{- 1} \cdot (τ \cdot t_{0}) = t_{0}$ by [L2]; hence $τ^{- 1} σ \cdot t_{0} \sim t_{0}$ , so $τ^{- 1} σ \in R_{t_{0}} = S_{λ}$ by [L1] and therefore $σ S_{λ} = τ S_{λ}$ .

L1L2step 1.1

2.2

The map $Φ$ is surjective: every tabloid is ${t}$ for some $λ$ -tableau $t$ by [L1], and $t = σ \cdot t_{0}$ for some $σ \in S_{n}$ by [L3], so ${t} = {σ \cdot t_{0}} = Φ (σ S_{λ})$ .

L1L3step 1.1

2.3

The map $Φ$ is $S_{n}$ -equivariant for the left actions of [L1] and [L4]: for $τ \in S_{n}$ one has $Φ (τ \cdot σ S_{λ}) = Φ ((τ σ) S_{λ}) = {(τ σ) \cdot t_{0}} = {τ \cdot (σ \cdot t_{0})} = τ \cdot {σ \cdot t_{0}} = τ \cdot Φ (σ S_{λ})$ , using that the action on tableaux and on tabloids is a left action and $σ \cdot {t} = {σ \cdot t}$ .

L1L3L4step 1.1algebra

3.1

Steps 2.1, 2.2 and 2.3 show that $Φ$ is an isomorphism of left $S_{n}$ -sets, hence extends to an isomorphism of complex representations $M^{λ} ≅ C [S_{n} / S_{λ}]$ , the permutation representation of $S_{n}$ on the coset set $S_{n} / S_{λ}$ ; this is the first isomorphism of the statement.

step 2.1step 2.2step 2.3L1

4.1

Applying [L4] to the finite group $G = S_{n}$ and the subgroup $H = S_{λ} \leq S_{n}$ identifies the permutation representation of $S_{n}$ on $S_{n} / S_{λ}$ with ${Ind}_{S_{λ}}^{S_{n}} 1$ ; composing with the isomorphism of step 3.1 gives $M^{λ} ≅ {Ind}_{S_{λ}}^{S_{n}} 1$ .

step 3.1L4

5.1

For $n = 0$ one has $λ = \emptyset$ and $S_{\emptyset} = S_{0} = {1}$ ; there is exactly one $\emptyset$ -tableau, the empty one, so $Ω_{\emptyset}$ has one element and $M^{\emptyset}$ is one-dimensional with trivial action, the coset set $S_{0} / S_{0}$ is a single point, and [L4] with $G = H = S_{0}$ gives the same one-dimensional trivial representation as the induced module; so steps 3.1 and 4.1 hold also in this case. ∎

step 3.1step 4.1L4given

Depends on

Used by

The two extreme Young permutation modules Example

Dependency tree · two levels

8 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.5, printed pp. 12-13 (standard reference, not scraped)
David Craven, Groups, Geometries and Representation Theory - Lemma 1.17 and Section 1.6, printed pp. 13-14 (standard reference, not scraped)