ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Schur-Weyl decomposition of (C^2)^tensor3

Statement

Let $V = C^{2}$ with fixed basis $e_{1}, e_{2}$ , let $E = V^{\otimes 3}$ carry the commuting left place action of $S_{3}$ and diagonal action of $GL (V)$ (Commuting symmetric-group and linear actions on a tensor power), and for $λ ⊢ 3$ put $M_{λ} : = {Hom}_{S_{3}} (S^{λ}, E)$ , with $GL (V)$ acting by postcomposition. Then:

(Decomposition.) There is an isomorphism of $(S_{3} \times GL (V))$ -modules $E ≅ S^{(3)} \otimes M_{(3)} \oplus S^{(2, 1)} \otimes M_{(2, 1)}$ , and $M_{(1, 1, 1)} = 0$ : the shape $(1, 1, 1)$ is absent, in agreement with the length cutoff $ℓ ((1, 1, 1)) = 3 > 2 = \dim V$ .
(The trivial factor.) $S^{(3)}$ is the one-dimensional trivial representation of $S_{3}$ , the fixed space $E^{S_{3}}$ is four-dimensional with basis $e_{1}^{\otimes 3}, \sum_{σ \in S_{3}} σ \cdot (e_{1} \otimes e_{1} \otimes e_{2}), \sum_{σ \in S_{3}} σ \cdot (e_{1} \otimes e_{2} \otimes e_{2}), e_{2}^{\otimes 3},$ and evaluation at a generator of $S^{(3)}$ identifies $M_{(3)} ≅ E^{S_{3}}$ as $GL (V)$ -modules. Writing ${Sym}^{3} (C^{2}) : = E^{S_{3}}$ with the corresponding basis $x^{3}, x^{2} y, x y^{2}, y^{3}$ , the decomposition reads $E ≅ S^{(3)} \otimes {Sym}^{3} (C^{2}) \oplus S^{(2, 1)} \otimes M_{(2, 1)}$ .
(Dimensions and highest weight.) $\dim_{C} M_{(3)} = 4$ and $\dim_{C} M_{(2, 1)} = 2$ , so $\dim_{C} E = 8 = 1 \cdot 4 + 2 \cdot 2$ ; the two standard $(2, 1)$ -tableaux give $\dim_{C} S^{(2, 1)} = 2$ , and $M_{(2, 1)}$ has highest weight $(2, 1)$ , while $M_{(3)}$ has highest weight $(3)$ .

Facts & Assumptions

Given: the complex vector space $V = C^{2}$ with basis $e_{1}, e_{2}$ , the module $E = V^{\otimes 3}$ with its commuting $S_{3}$ - and $GL (V)$ -actions, and the multiplicity spaces $M_{λ} = {Hom}_{S_{3}} (S^{λ}, E)$ for $λ ⊢ 3$ .

[F1]

The place action of $S_{3}$ on $E$ is a linear left action and $g \mapsto g^{\otimes 3}$ is the diagonal $GL (V)$ -action, which commutes with it; the diagonal infinitesimal operator is $Δ (X) = \sum_{a = 1}^{3} 1^{\otimes (a - 1)} \otimes X \otimes 1^{\otimes (3 - a)}$ (Commuting symmetric-group and linear actions on a tensor power).

[F2]

The eight elementary tensors $e_{i} \otimes e_{j} \otimes e_{k}$ with $i, j, k \in {1, 2}$ form a basis of $E$ , so $\dim_{C} E = 2^{3} = 8$ (The elementary tensors of two bases form the product basis of the tensor product, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[F3]

For $d = \dim_{C} V = 2$ the Schur-Weyl decomposition reads $E ≅ ⨁_{λ ⊢ 3, ℓ (λ) \leq 2} S^{λ} \otimes M_{λ}$ ; for every $λ ⊢ 3$ with $ℓ (λ) \leq 2$ the space $M_{λ}$ is nonzero and irreducible over $B = {span}_{C} {g^{\otimes 3}}$ and has highest weight $λ$ , while $ℓ (λ) > 2$ forces $M_{λ} = 0$ (Schur-Weyl decomposition and highest weights).

[F4]

For $λ ⊢ 3$ with $ℓ (λ) \leq 2$ , the multiplicity space $M_{λ}$ contains the nonzero map $φ = Φ ∣_{S^{λ}}$ with $Δ (E_{i i}) \circ φ = λ_{i} φ$ for every $i$ (with $λ_{i} : = 0$ for $i > ℓ (λ)$ ) and $Δ (E_{12}) \circ φ = 0$ ; if $M_{λ}$ is irreducible over $B$ , then $λ$ is its unique highest weight (The row-labelled polytabloid map has highest weight lambda).

[F5]

For every $λ ⊢ 3$ the standard polytabloids form a $C$ -basis of $S^{λ}$ , so $\dim_{C} S^{λ} = f^{λ}$ , the number of standard $λ$ -tableaux (Standard polytabloids form a basis of a complex Specht module, Tableaux and standard tableaux).

[F6]

For a partition $λ$ the tabloids of shape $λ$ form a basis of $M^{λ} = C^{(Ω_{λ})}$ on which $S_{n}$ acts by $σ \cdot {t} = {σ \cdot t}$ . For $λ = (3)$ the set $Ω_{(3)}$ has the single element ${t} = {1, 2, 3}$ , so $M^{(3)}$ is one-dimensional and every $σ \in S_{3}$ acts trivially (Young subgroups, tabloids, and permutation modules).

[F7]

The polytabloid of a tableau $t$ is $e_{t} = κ_{t} \cdot {t}$ with $κ_{t} = \sum_{γ \in C_{t}} sgn (γ) γ$ , and $S^{λ} = {span}_{C} {e_{s} : s$ a $λ$ -tableau $}$ ; the column stabilizer of a one-row tableau is trivial, so $e_{t} = {t}$ there (Column antisymmetrizers, polytabloids, and Specht modules).

[F8]

The standard tableaux of shape $(3)$ are the single tableau $1 2 3$ , and the standard tableaux of shape $(2, 1)$ are $\begin{matrix} 1 & 2 \\ 3 \end{matrix}$ and $\begin{matrix} 1 & 3 \\ 2 \end{matrix}$ ; hence $f^{(3)} = 1$ and $f^{(2, 1)} = 2$ (Tableaux and standard tableaux).

[F9]

The partitions of $3$ are $(3)$ with $ℓ = 1$ , $(2, 1)$ with $ℓ = 2$ and $(1, 1, 1)$ with $ℓ = 3$ (Partitions, English diagrams, and conjugation).

No form of the Axiom of Choice is used: the space $V$ has an explicit finite basis, the group $S_{3}$ is finite and explicit, and all decompositions below are finite.

Proof

technique · direct

1.1givenF1F2

By [F2] the elementary tensors $e_{i} \otimes e_{j} \otimes e_{k}$ form a basis of $E$ , so $\dim_{C} E = 8$ , and by [F1] the place action only permutes this basis: $σ \cdot (e_{i} \otimes e_{j} \otimes e_{k})$ is again an elementary tensor, with the three basis vectors permuted among the positions.

1.2F6F7given

For $λ = (3)$ the module $M^{(3)}$ has the single tabloid ${1, 2, 3}$ as basis, so it is one-dimensional and every $σ \in S_{3}$ fixes that tabloid; by [F7] the column stabilizer of the one-row tableau $t$ is trivial, so $e_{t} = {t}$ and $S^{(3)} = span {e_{s}} = C {t} = M^{(3)}$ . Hence $S^{(3)}$ is the one-dimensional trivial representation, and $e_{t}$ is a nonzero fixed vector that generates $S^{(3)}$ .

1.3F3F9given

By [F9] the partitions of $3$ with $ℓ (λ) \leq 2$ are $(3)$ and $(2, 1)$ , while $ℓ ((1, 1, 1)) = 3 > 2 = \dim V$ ; by [F3] therefore $E ≅ S^{(3)} \otimes M_{(3)} \oplus S^{(2, 1)} \otimes M_{(2, 1)}$ with $M_{(1, 1, 1)} = 0$ , and both $M_{(3)}$ and $M_{(2, 1)}$ are nonzero and irreducible over $B$ .

1.4F5F8

By [F5] and the standard tableaux enumerated in [F8], $\dim_{C} S^{(3)} = f^{(3)} = 1$ and $\dim_{C} S^{(2, 1)} = f^{(2, 1)} = 2$ ; the two standard $(2, 1)$ -tableaux of [F8] are the two ways $\begin{matrix} 1 & 2 \\ 3 \end{matrix}$ and $\begin{matrix} 1 & 3 \\ 2 \end{matrix}$ of placing the entries while increasing along rows and down columns, so $f^{(2, 1)} = 2$ is verified directly.

2.1step 1.1F1F2algebra

Compute the fixed space. An element $x = \sum_{i, j, k \in {1, 2}} c_{i j k} e_{i} \otimes e_{j} \otimes e_{k}$ is fixed by $S_{3}$ exactly when its coefficient function is constant on every orbit of $S_{3}$ acting by permutation of the three positions, because [F2] makes these basis vectors linearly independent; the orbits are the four multisets ${1, 1, 1}$ , ${1, 1, 2}$ , ${1, 2, 2}$ , ${2, 2, 2}$ , of sizes $1, 3, 3, 1$ . The sums of distinct basis tensors in these four orbits form a basis of $E^{S_{3}}$ , since the orbits are disjoint. The middle two sums over all $σ \in S_{3}$ displayed in the Statement are twice their distinct-orbit sums, because each of those tensors has a stabilizer of order two. As $2 \neq 0$ in $C$ , the four displayed vectors also form a basis, so $\dim_{C} E^{S_{3}} = 4$ .

2.2F4step 1.3

For the highest weight, $ℓ ((2, 1)) = 2 = d$ and $ℓ ((3)) = 1 \leq d$ , and $M_{(2, 1)}$ , $M_{(3)}$ are irreducible over $B$ by step 1.3; the highest-weight lemma [F4] therefore provides a nonzero $φ \in M_{(2, 1)}$ with $Δ (E_{11}) \circ φ = 2 φ$ , $Δ (E_{22}) \circ φ = φ$ and $Δ (E_{12}) \circ φ = 0$ , so $M_{(2, 1)}$ has highest weight $(2, 1)$ , unique up to scalar; for $(3)$ the padded weight is $(3, 0)$ , so the same lemma gives eigenvalues $3$ and $0$ for $Δ (E_{11})$ and $Δ (E_{22})$ , respectively, and annihilation by $Δ (E_{12})$ .

3.1step 1.2step 2.1F1algebra

Since $S^{(3)} = C e_{t}$ with $e_{t}$ fixed and nonzero by step 1.2, the evaluation map $e v (φ) : = φ (e_{t})$ is a $C$ -linear bijection ${Hom}_{S_{3}} (S^{(3)}, E) \to E^{S_{3}}$ : a homomorphism takes the fixed generator $e_{t}$ to a fixed vector, and conversely a fixed vector $v$ defines the well-defined $S_{3}$ -linear map $λ e_{t} \mapsto λ v$ . For $g \in GL (V)$ postcomposition gives $e v (g \cdot φ) = g^{\otimes 3} φ (e_{t}) = (g^{\otimes 3}) \cdot e v (φ)$ , so the bijection is $GL (V)$ -equivariant; hence $M_{(3)} = {Hom}_{S_{3}} (S^{(3)}, E) ≅ E^{S_{3}}$ as $GL (V)$ -modules, of dimension $4$ .

4.1step 3.1step 1.3step 1.4algebra

Reading dimensions in the isomorphism of step 1.3 and using steps 3.1 and 1.4: $8 = \dim_{C} E = 1 \cdot \dim_{C} M_{(3)} + 2 \cdot \dim_{C} M_{(2, 1)} = 1 \cdot 4 + 2 \dim_{C} M_{(2, 1)}$ , so $\dim_{C} M_{(2, 1)} = 2$ .

5.1F2F3step 2.1step 1.3step 4.1step 2.2given∎

Substituting the identification $M_{(3)} ≅ E^{S_{3}} = {Sym}^{3} (C^{2})$ of step 3.1 into step 1.3 gives the decomposition $E ≅ S^{(3)} \otimes {Sym}^{3} (C^{2}) \oplus S^{(2, 1)} \otimes M_{(2, 1)}$ . All three partitions of $3$ have been accounted for: $(3)$ and $(2, 1)$ occur with the multiplicities $\dim M_{(3)} = 4$ and $\dim M_{(2, 1)} = 2$ just computed, while $(1, 1, 1)$ is excluded exactly by the length cutoff $ℓ ((1, 1, 1)) = 3 > d = 2$ ; the dimension count $8 = 4 + 4$ closes, and the enumeration uses only the finite sets ${1, 2}^{3}$ , $S_{3}$ and the partitions of $3$ , so no choice principle is invoked. This proves the Statement.

Remarks

Why the shape $(1, 1, 1)$ is absent. Its three boxes form one column, so a nonzero column-antisymmetrized tensor in $V^{\otimes 3}$ would need three distinct basis vectors, and $V = C^{2}$ supplies only two: this is the length cutoff $ℓ (λ) \leq d$ in the smallest nontrivial case, and it is exactly the criterion applied in step 1.3.
The classical shape of the answer. $E ≅ {Sym}^{3} (C^{2}) \oplus (M_{(2, 1)})^{\oplus 2}$ with $\dim {Sym}^{3} (C^{2}) = 4$ and $\dim M_{(2, 1)} = 2$ : the degree-three piece of the symmetric algebra of $C^{2}$ has the monomial basis $x^{3}, x^{2} y, x y^{2}, y^{3}$ , and the remaining two copies of the two-dimensional module $M_{(2, 1)}$ of highest weight $(2, 1)$ exhaust the dimension count $4 + 2 \cdot 2 = 8$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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

Pavel Etingof et al., Introduction to Representation Theory, MIT 18.712 Chapter 4, Sections 4.18-4.21, PDF pp. 18-21 (standard reference, not scraped)
Hsueh-Yung Lin, Modern Algebra I, Section 27, printed pp. 71-74 (standard reference, not scraped)