[proofplan] We use the standard Specht-module construction together with the seminormal form of the Specht modules over $\mathbb C$. The standard polytabloid basis identifies $\dim_{\mathbb C} S^\lambda$ with the number $f_\lambda$ of standard Young tableaux of shape $\lambda$. Irreducibility follows because the Jucys-Murphy family separates the seminormal basis vectors and the adjacent transpositions connect the standard tableaux of a fixed shape. Completeness follows by comparing the sum of squares of these dimensions with the dimension of the regular representation of $S_n$. [/proofplan]

[step:Fix the complex Specht modules and their standard bases]Fix a partition $\lambda \vdash n$. Let $M^\lambda$ denote the complex permutation module on $\lambda$-tabloids, and for a Young tableau $t$ of shape $\lambda$, let $e_t \in M^\lambda$ denote its polytabloid. The complex Specht module $S^\lambda$ is the $\mathbb C$-subspace of $M^\lambda$ spanned by all such polytabloids $e_t$. By the polytabloid realization theorem [citetheorem:8441], this subspace is stable under the natural action of $S_n$, so $S^\lambda$ is a left $\mathbb C[S_n]$-module. By the [standard polytabloid basis theorem](/theorems/8442) [citetheorem:8442], the set $\{e_t : t \text{ is a standard Young tableau of shape } \lambda\}$ is a $\mathbb C$-basis of $S^\lambda$. Define \begin{align*} f_\lambda := |\{t : t \text{ is a standard Young tableau of shape } \lambda\}|. \end{align*} Therefore \begin{align*} \dim_{\mathbb C} S^\lambda = f_\lambda. \end{align*}[/step]

[guided]The first point is to be explicit about which Specht module is being used. We are working over $\mathbb C$, not over an arbitrary field. For a partition $\lambda \vdash n$, let $M^\lambda$ be the complex permutation module whose basis consists of $\lambda$-tabloids. For each Young tableau $t$ of shape $\lambda$, the associated polytabloid is denoted by $e_t \in M^\lambda$, and $S^\lambda$ is defined to be the $\mathbb C$-span of all such $e_t$. The action of $S_n$ on entries of tableaux induces an action on tabloids and hence on $M^\lambda$. The polytabloid realization theorem [citetheorem:8441] says that the span of the polytabloids is stable under this action, so $S^\lambda$ is a left $\mathbb C[S_n]$-module. Now we need a dimension count. The standard polytabloid basis theorem [citetheorem:8442] states that the polytabloids indexed by standard Young tableaux of shape $\lambda$ form the basis $\{e_t : t \text{ is a standard Young tableau of shape } \lambda\}$. Thus if \begin{align*} f_\lambda := |\{t : t \text{ is a standard Young tableau of shape } \lambda\}|, \end{align*} then the basis has exactly $f_\lambda$ elements. Hence \begin{align*} \dim_{\mathbb C} S^\lambda = f_\lambda. \end{align*} This is the numerical input needed later when we compare the Specht modules with the regular representation.[/guided]

[step:Use seminormal form to prove irreducibility]Define the Jucys-Murphy elements $X_1,\dots,X_n \in \mathbb C[S_n]$ by $X_1:=0$ and, for $2\le k\le n$, \begin{align*} X_k := \sum_{j=1}^{k-1} (j\ k), \end{align*} where $(j\ k)\in S_n$ denotes the transposition exchanging $j$ and $k$. The module $S^\lambda$ is a complex Specht module by the previous step, so the Young seminormal form theorem [citetheorem:8448] applies to this constructed module and gives a seminormal basis $(v_T)$ indexed by standard Young tableaux $T$ of shape $\lambda$. This cited seminormal form theorem is used only for the explicit action formulas on the constructed Specht module and not for irreducibility, so the argument below is not assuming the conclusion. In that basis each $X_k$ acts by \begin{align*} X_k v_T = c_k(T)v_T. \end{align*} Here $c_k(T)$ denotes the content of the box containing $k$ in $T$. The simple spectrum theorem for the Jucys-Murphy family [citetheorem:8449] applies to the same complex Specht module $S^\lambda$ in its seminormal representation; hence each simultaneous eigenspace for $X_1,\dots,X_n$ in $S^\lambda$ is one-dimensional, namely the line $\mathbb C v_T$ for a unique standard tableau $T$. Let $0 \ne U \subset S^\lambda$ be a $\mathbb C[S_n]$-submodule. Because each $X_k$ lies in $\mathbb C[S_n]$, the subspace $U$ is stable under every $X_k$. Choose $0 \ne u \in U$ and write \begin{align*} u=\sum_T a_T v_T, \end{align*} where the sum ranges over standard tableaux of shape $\lambda$ and at least one coefficient $a_T \in \mathbb C$ is nonzero. Choose a standard tableau $T_0$ with $a_{T_0}\ne 0$. For every standard tableau $T\ne T_0$, content separation gives an index $k(T)\in\{1,\dots,n\}$ with $c_{k(T)}(T)\ne c_{k(T)}(T_0)$. By the Jucys-Murphy commutativity theorem [citetheorem:8446], the elements $X_1,\dots,X_n$ commute pairwise in $\mathbb C[S_n]$. Hence the operator \begin{align*} \Pi_{T_0}:=\prod_{T\ne T_0}\frac{X_{k(T)}-c_{k(T)}(T)\operatorname{id}_{S^\lambda}}{c_{k(T)}(T_0)-c_{k(T)}(T)} \end{align*} is a well-defined polynomial in the commuting operators $X_1,\dots,X_n$ and therefore preserves $U$. Applying it to $u$ gives $\Pi_{T_0}u=a_{T_0}v_{T_0}\in U$, so $v_{T_0}\in U$. For standard tableaux of the same fixed shape, the graph whose edges join $T$ to $s_iT$ whenever $s_iT$ is standard is connected. The Young seminormal form theorem [citetheorem:8448] gives the action of each adjacent transposition $s_i=(i\ i+1)$ on the span of $v_T$ and $v_{s_iT}$; whenever $s_iT$ is standard, there are scalars $a\in\mathbb C$ and $b\in\mathbb C\setminus\{0\}$ such that $s_i v_T=a v_T+b v_{s_iT}$. If $v_T\in U$, then $s_i v_T\in U$ because $U$ is a $\mathbb C[S_n]$-submodule, and hence $b v_{s_iT}=s_i v_T-a v_T\in U$. Since $b\ne 0$, this gives $v_{s_iT}\in U$. Following a path in the connected tableau graph gives $v_{T'}\in U$ for every standard tableau $T'$ of shape $\lambda$. Thus $U$ contains the whole seminormal basis, so $U=S^\lambda$. Therefore $S^\lambda$ is irreducible.[/step]

[guided]We want to prove irreducibility without assuming the conclusion. The replacement for the circular submodule argument is the seminormal form. Define $X_1,\dots,X_n\in\mathbb C[S_n]$ by $X_1:=0$ and, for $2\le k\le n$, \begin{align*} X_k:=\sum_{j=1}^{k-1}(j\ k), \end{align*} where $(j\ k)$ is the transposition in $S_n$ exchanging $j$ and $k$. These are the Jucys-Murphy elements. The previous step has constructed $S^\lambda$ as the complex Specht module of shape $\lambda$, so the Young seminormal form theorem [citetheorem:8448] applies to this module. In this proof, that theorem is being used for its explicit seminormal basis and action formulas on the constructed Specht module; irreducibility is proved below from those formulas. It gives a basis $(v_T)$ indexed by standard Young tableaux $T$ of shape $\lambda$ such that \begin{align*} X_k v_T = c_k(T)v_T \end{align*} for every $1\le k\le n$. The scalar $c_k(T)$ is the content of the box containing the entry $k$ in $T$. Now let $0\ne U\subset S^\lambda$ be a $\mathbb C[S_n]$-submodule. Since each $X_k$ belongs to the group algebra $\mathbb C[S_n]$, the submodule $U$ is stable under all $X_k$. Choose $0\ne u\in U$ and expand it in the seminormal basis: \begin{align*} u=\sum_T a_T v_T. \end{align*} At least one coefficient $a_T$ is nonzero. The simple spectrum theorem for the Jucys-Murphy family [citetheorem:8449] applies to this same complex Specht module in its seminormal representation and says that the simultaneous eigenspaces are the one-dimensional lines $\mathbb C v_T$. Choose $T_0$ with $a_{T_0}\ne 0$. For each $T\ne T_0$, content separation gives some $k(T)$ with $c_{k(T)}(T)\ne c_{k(T)}(T_0)$. By the Jucys-Murphy commutativity theorem [citetheorem:8446], the elements $X_1,\dots,X_n$ commute pairwise in $\mathbb C[S_n]$. Therefore the finite product \begin{align*} \Pi_{T_0}:=\prod_{T\ne T_0}\frac{X_{k(T)}-c_{k(T)}(T)\operatorname{id}_{S^\lambda}}{c_{k(T)}(T_0)-c_{k(T)}(T)} \end{align*} is a well-defined polynomial in the commuting operators $X_1,\dots,X_n$. It acts as the identity on $v_{T_0}$ and kills every other basis vector appearing in the seminormal basis. Since $\Pi_{T_0}$ is a polynomial in elements of $\mathbb C[S_n]$, it preserves $U$. Thus $\Pi_{T_0}u=a_{T_0}v_{T_0}\in U$, and because $a_{T_0}\ne 0$, we get $v_{T_0}\in U$. It remains to propagate from one seminormal basis vector to all of them. Standard tableaux of a fixed shape form a connected graph under adjacent swaps $T\mapsto s_iT$ whenever the result is again standard. The Young seminormal form theorem [citetheorem:8448] gives the action of $s_i=(i\ i+1)$ on the two-dimensional span of $v_T$ and $v_{s_iT}$. When $s_iT$ is standard, there are scalars $a\in\mathbb C$ and $b\in\mathbb C\setminus\{0\}$ such that $s_i v_T=a v_T+b v_{s_iT}$. If $v_T\in U$, then $s_i v_T\in U$ because $U$ is a $\mathbb C[S_n]$-submodule, so $b v_{s_iT}=s_i v_T-a v_T\in U$. Since $b\ne 0$, this implies $v_{s_iT}\in U$. Following paths in the connected tableau graph shows that $v_{T'}\in U$ for every standard tableau $T'$ of shape $\lambda$. Hence $U$ contains the entire seminormal basis, so $U=S^\lambda$. This proves that $S^\lambda$ is irreducible.[/guided]

[step:Separate Specht modules attached to different partitions]Let $\lambda,\mu \vdash n$ be partitions. Suppose that $S^\lambda \cong S^\mu$ as $\mathbb C[S_n]$-modules. The isomorphism intertwines the action of every element of $\mathbb C[S_n]$, hence it identifies the simultaneous spectra of the Jucys-Murphy family $X_1,\dots,X_n$ on $S^\lambda$ and on $S^\mu$. By the content eigenvalue theorem [citetheorem:8447], the joint eigenvalue vectors on $S^\lambda$ are exactly \begin{align*} (c_1(T),\dots,c_n(T)) \end{align*} as $T$ ranges over standard Young tableaux of shape $\lambda$, and similarly for $\mu$. Each partition of $n$ has at least one standard tableau, obtained by filling the boxes row by row from left to right and top to bottom. Hence the common joint spectrum is nonempty. Choose a vector in this common spectrum. It equals the content vector of some standard tableau $T$ of shape $\lambda$ and also of some standard tableau $T'$ of shape $\mu$. By content separation of standard tableaux [citetheorem:8445], $T=T'$ as standard tableaux of size $n$. Therefore their shapes are equal, so $\lambda=\mu$. Hence the family \begin{align*} \{S^\lambda : \lambda \vdash n\} \end{align*} is a pairwise non-isomorphic family of irreducible complex representations of $S_n$.[/step]

[guided]The point of this step is to show that two different shapes cannot give isomorphic modules. Assume $S^\lambda \cong S^\mu$ as $\mathbb C[S_n]$-modules. Such an isomorphism commutes with the action of every element of the group algebra, in particular with the Jucys-Murphy elements $X_1,\dots,X_n$. By the content eigenvalue theorem [citetheorem:8447], the simultaneous eigenvalue vector attached to a seminormal basis vector $v_T\in S^\lambda$ is \begin{align*} (c_1(T),\dots,c_n(T)), \end{align*} where $c_k(T)$ is the content of the box containing $k$. Therefore an isomorphism $S^\lambda\cong S^\mu$ identifies the set of content vectors coming from standard tableaux of shape $\lambda$ with the corresponding set for shape $\mu$. Each partition of $n$ has at least one standard tableau, for instance the tableau obtained by filling boxes row by row from left to right and top to bottom, so the joint spectra are nonempty. Choose one content vector in the common spectrum. It comes from a standard tableau $T$ of shape $\lambda$ and also from a standard tableau $T'$ of shape $\mu$. Content separation of standard tableaux [citetheorem:8445] says that a standard tableau is determined by the full list of contents of its entries, so $T=T'$. A tableau has a unique shape, hence $\lambda=\mu$. Therefore distinct partitions give non-isomorphic Specht modules.[/guided]

[step:Count the dimensions contributed by all Specht modules]For each partition $\lambda \vdash n$, the previous basis computation gives $\dim_{\mathbb C} S^\lambda=f_\lambda$. Let $\operatorname{SYT}_n$ denote the set of all standard Young tableaux with $n$ boxes. Define the RSK insertion map \begin{align*} P:S_n\to\operatorname{SYT}_n \end{align*} by sending $w\in S_n$ to its RSK insertion tableau $P(w)$, and define the RSK recording map \begin{align*} Q:S_n\to\operatorname{SYT}_n \end{align*} by sending $w\in S_n$ to its RSK recording tableau $Q(w)$. By the RSK bijection theorem [citetheorem:8435], $P(w)$ and $Q(w)$ are standard Young tableaux of the same shape. Define $\operatorname{sh}:S_n\to\{\text{partitions of }n\}$ by letting $\operatorname{sh}(w)$ be this common shape of the pair $(P(w),Q(w))$. By the [RSK shape count](/theorems/8451) [citetheorem:8451], \begin{align*} |\{w \in S_n : \operatorname{sh}(w)=\lambda\}| = (f_\lambda)^2. \end{align*} The sets $\{w \in S_n : \operatorname{sh}(w)=\lambda\}$, as $\lambda$ ranges over all partitions of $n$, form a disjoint partition of $S_n$, because every permutation has exactly one RSK shape. Summing the displayed identity over all $\lambda \vdash n$ gives \begin{align*} \sum_{\lambda \vdash n} (\dim_{\mathbb C} S^\lambda)^2 = \sum_{\lambda \vdash n} (f_\lambda)^2 = |S_n| = n!. \end{align*}[/step]

[guided]The purpose of this step is to prove that the Specht modules have the right total size to account for every irreducible representation. For each $\lambda \vdash n$, the standard polytabloid basis gives \begin{align*} \dim_{\mathbb C} S^\lambda=f_\lambda, \end{align*} where $f_\lambda$ is the number of standard Young tableaux of shape $\lambda$. Now we use RSK. Let $\operatorname{SYT}_n$ denote the set of all standard Young tableaux with $n$ boxes. Define the RSK insertion map \begin{align*} P:S_n\to\operatorname{SYT}_n \end{align*} by sending a permutation $w\in S_n$ to its RSK insertion tableau $P(w)$, and define the RSK recording map \begin{align*} Q:S_n\to\operatorname{SYT}_n \end{align*} by sending $w\in S_n$ to its RSK recording tableau $Q(w)$. By the RSK bijection theorem [citetheorem:8435], these are standard Young tableaux of the same shape. Define $\operatorname{sh}:S_n\to\{\text{partitions of }n\}$ by letting $\operatorname{sh}(w)$ be that common shape. The RSK shape count [citetheorem:8451] says that the number of permutations whose RSK shape is $\lambda$ is \begin{align*} |\{w \in S_n : \operatorname{sh}(w)=\lambda\}| = (f_\lambda)^2. \end{align*} Why does summing this identity count all of $S_n$ exactly once? Every permutation $w \in S_n$ has a unique RSK insertion-recording pair, hence a unique common shape $\operatorname{sh}(w)$. Therefore the subsets \begin{align*} \{w \in S_n : \operatorname{sh}(w)=\lambda\} \end{align*} are pairwise disjoint as $\lambda$ varies and their union is all of $S_n$. Thus \begin{align*} \sum_{\lambda \vdash n} (f_\lambda)^2 = |S_n|. \end{align*} Since $|S_n|=n!$ and $\dim_{\mathbb C}S^\lambda=f_\lambda$, this becomes \begin{align*} \sum_{\lambda \vdash n} (\dim_{\mathbb C} S^\lambda)^2 = n!. \end{align*} This is exactly the numerical equality needed for the exhaustion argument.[/guided]

[step:Use semisimplicity and the sum of squares formula to exhaust all irreducibles]Since $\mathbb C$ has characteristic zero, the characteristic of $\mathbb C$ does not divide $|S_n|=n!$. By [Maschke's theorem](/theorems/2409) [citetheorem:8439], every finite-dimensional complex representation of $S_n$ is completely reducible. In particular, the left regular representation $\mathbb C[S_n]$ decomposes as a direct sum of irreducible complex representations. We use the standard sum-of-squares theorem for finite groups over $\mathbb C$: if $V_1,\dots,V_r$ are representatives for the isomorphism classes of irreducible complex representations of a finite group $G$, then \begin{align*} |G|=\sum_{i=1}^{r}(\dim_{\mathbb C} V_i)^2. \end{align*} Apply this with $G=S_n$. The pairwise non-isomorphic irreducible modules $S^\lambda$ already contribute \begin{align*} \sum_{\lambda \vdash n}(\dim_{\mathbb C} S^\lambda)^2=n!. \end{align*} Since $|S_n|=n!$, no additional irreducible complex representation can occur: any further irreducible would add a positive square to the sum. Therefore every irreducible finite-dimensional complex representation of $S_n$ is isomorphic to $S^\lambda$ for some partition $\lambda \vdash n$. The uniqueness of $\lambda$ follows from pairwise non-isomorphism proved above. Hence the complex Specht modules $S^\lambda$, indexed by partitions $\lambda \vdash n$, form a complete set of pairwise non-isomorphic irreducible complex representations of $S_n$.[/step]

[guided]The last step is an exhaustion argument. Since $\mathbb C$ has characteristic zero, its characteristic does not divide $|S_n|=n!$. Maschke's theorem [citetheorem:8439] therefore applies and says that every finite-dimensional complex representation of $S_n$ is completely reducible. In particular, the regular representation $\mathbb C[S_n]$ decomposes into irreducible summands. For a finite group $G$ over $\mathbb C$, the sum-of-squares theorem says that if $V_1,\dots,V_r$ are representatives of all irreducible complex representations of $G$, then \begin{align*} |G|=\sum_{i=1}^{r}(\dim_{\mathbb C}V_i)^2. \end{align*} Applying this theorem to $G=S_n$ gives a total available square-dimension budget of $|S_n|=n!$. The Specht modules are already pairwise non-isomorphic irreducible modules, and the RSK count proved above gives \begin{align*} \sum_{\lambda\vdash n}(\dim_{\mathbb C}S^\lambda)^2=n!. \end{align*} Thus the Specht modules already use the entire sum allowed by the sum-of-squares theorem. If there were another irreducible representation not isomorphic to any $S^\lambda$, its positive square dimension would have to be added to the sum, contradicting the equality above. Hence every irreducible finite-dimensional complex representation of $S_n$ is isomorphic to some $S^\lambda$. Finally, the partition $\lambda$ is unique because the previous step proved that $S^\lambda\cong S^\mu$ implies $\lambda=\mu$. Therefore the Specht modules indexed by partitions of $n$ form a complete set of pairwise non-isomorphic irreducible complex representations of $S_n$.[/guided]