Proofs of the Frobenius characteristic map Let $\mathfrak{S}_n$ be the symmetric group on $n$ letters, $\mathsf{Rep}(\mathfrak{S}_n)$ be the abelian category of finite dimensional complex representations of $\mathfrak{S}_n$. A classical result of Frobenius asserts that there is an isomorphism of algebras
$$\bigoplus_{n\geq0}K_0(\mathsf{Rep}(\mathfrak{S}_n))\otimes\mathbb{C}\simeq\mathbb{C}[X_1,X_2,\cdots]^{\mathfrak{S}_\infty}.$$
Here $K_0$ means taking the Grothendieck group, and the multiplication of LHS is determined by
$$V\times W=\operatorname{Ind}_{\mathfrak{S}_n\times\mathfrak{S}_m}^{\mathfrak{S}_{n+m}}(V\boxtimes W)$$
for $V\in\mathsf{Rep}(\mathfrak{S}_n),W\in\mathsf{Rep}(\mathfrak{S}_m)$. The RHS is the ring of symmetric polynomials on countable variables.
In modern terminology, this isomorphism is called the Frobenius characteristic map.
The original proof of this theorem given by Frobenius is based on the explicit construction of Specht modules and many concrete computations of symmetric polynomials. I want to collect as many as possible proofs of this beautiful theorem. Techniques from any branch of mathematics (say, combinatorics, vertex algebra, geometric representation theory, etc.) are welcome.
 A: $\def\one{\mathbb{1}}$ Here is a direct attack. First, we give a concise definition of the Frobenius character map, then we check that it is a map of rings.
Let $(\alpha_1, \alpha_2, \dotsc)$ be any sequence of nonnegative integers, all but finitely many of which are $0$. Define $\lvert\alpha\rvert = \sum \alpha_i$ and $x^{\alpha}=\prod x_i^{\alpha_i}$. For $\alpha$ with $\lvert\alpha\rvert =m$, define $S_{\alpha}$ to be the subgroup $\prod S_{\alpha_i}$ of $S_{m}$, embedded in the obvious way. (Note that there is no problem with the $\alpha_i=0$ terms; $S_0$ is the trivial group.)
For a representation $V$ of $S_m$, we define the Frobenius character of $S_m$ as
$$\sum_{\lvert\alpha\rvert=m} \dim V^{S_{\alpha}} x^{\alpha}.$$
(Here $V^{S_{\alpha}}$ is the $S_{\alpha}$-invariants in $V$.)
This is clearly additive. Also, permuting the elements of $\alpha$ conjugates the group $S_{\alpha}$, so this is a symmetric polynomial.
It remains to check multiplicativity.
In other words, let $V$ and $W$ be representations of $S_m$ and $S_n$ and let $\lvert\gamma\rvert = m+n$. Comparing the coefficient of $x^{\gamma}$ on both sides, we must check that
$$\dim \left(\operatorname{Ind}_{S_m \times S_n}^{S_{m+n}} V \boxtimes W \right)^{S_{\gamma}} = \sum_{\lvert\alpha\rvert = m,\ \lvert\beta\rvert = n,\ \alpha+\beta = \gamma} (\dim V^{S_{\alpha}}) (\dim W^{S_{\beta}}).\tag{$\ast$}\label{ast}$$
We write $\one$ for the trivial representation of any group. So, for $H \subset G$ and $V$ a representation of $G$, we have $\dim V^H = \dim \operatorname{Hom}_H(\one,\ \operatorname{Res}^G_H V)$. So the left hand side of \eqref{ast} is
$$\dim \operatorname{Hom}_{S_{\gamma}}\left(\one,\ \operatorname{Res}^{S_{m+n}}_{S_{\gamma}} \operatorname{Ind}_{S_m \times S_n}^{S_{m+n}} (V \boxtimes W) \right).$$
By Mackey's formula, the restriction–induction can be written as a sum over double cosets $S_{\gamma} \backslash S_{m+n} / (S_m \times S_n)$. In other words, we take permutation matrices of size $m+n$, break them into blocks where the row blocks have sizes given by $\gamma$ and column blocks have sizes $m$ and $n$, and quotient by permutation of rows and columns within blocks. It isn't hard to see that the double cosets are determined by how many ones are in each block. Letting $\alpha_i$ be the number of ones in the left block of the $i$-th row, and $\beta_i$ the number of ones in the right block of the $i$-th row, the double cosets are indexed by $(\alpha, \beta)$ with $\lvert\alpha\rvert = m$, $\lvert\beta\rvert = n$ and $\alpha+\beta = \gamma$.
The contribution of $(\alpha, \beta)$ is
$$\dim \operatorname{Hom}_{S_{\alpha} \times S_{\beta}} \left( \one, \operatorname{Res}_{S_{\alpha} \times S_{\beta}} (V \boxtimes W) \right) = \dim (V \boxtimes W)^{S_{\alpha} \times S_{\beta}}.$$
Of course one needs to check that all the confusing conjugacies in Mackey's formula simply say to let $S_{\alpha}$ and $S_{\beta}$ act in the obvious ways but, really, what else could they do?
We have $(V \boxtimes W)^{S_{\alpha} \times S_{\beta}} = V^{S_{\alpha}} \boxtimes W^{S_{\beta}}$ so the dimensions multiply. Thus, the $(\alpha, \beta)$ coset contributes exactly the $(\alpha, \beta)$ summand in \eqref{ast}, and we win. $\square$
No symmetric polynomial theory, no construction of Specht modules, just chasing induction and restriction!
A: $\newcommand\Schur{\mathrm{Schur}}\newcommand\op{^\text{op}}\newcommand\FinVect{\mathrm{FinVect}}\DeclareMathOperator\Rep{Rep}\newcommand\Vect{\mathrm{Vect}}\DeclareMathOperator\GL{GL}\DeclareMathOperator\ch{ch}$Let $S$ be the category of finite sets and bijections; this is equivalent to $\bigsqcup_n BS_n$. Let $\Schur$ be the category of presheaves $S\op \to \FinVect$ with finite support, meaning that they assign the zero vector space to all but finitely many finite sets; $\Schur$ is equivalent to the direct sum $\bigoplus_{n \ge 0} \Rep(S_n)$ of the categories of finite-dimensional representations of the symmetric groups $S_n$, and accordingly its $K_0$ is exactly the LHS.
$\Schur$ admits a symmetric monoidal product given by Day convolution with respect to the symmetric monoidal product on $S$ given by disjoint union; you can verify from here that this reproduces the induction product, but thinking about it this way makes associativity etc. automatic.
$\Schur$ also admits a canonical action on $\Vect$ (and even on $\FinVect$) by Schur functors, as follows: if $F : S^\text{op} \to \FinVect$ assigns to the finite set of size $n$ the $S_n$-representation $F_n$, then it assigns to the vector space $V$ the vector space
$$F(V) = \bigoplus_{n \ge 0} F_n \otimes_{S_n} V^{\otimes n}$$
which is finite-dimensional if $V$ is. If $V$ is finite-dimensional then $F(V)$ has a character as a $\GL(V)$-representation which can be identified with a symmetric polynomial in $\dim V$ variables; to get a symmetric polynomial in countably many variables we can take $V$ to be countable-dimensional and consider its "formal character," given by counting the dimensions of the weight spaces of $F(V)$ with respect to the action of diagonal matrices with respect to some choice of basis. (If the base field $k$ is too small we may need to extend scalars for this to make sense, or equivalently think of diagonal matrices as an affine group scheme.) We will take this as our definition of the Frobenius characteristic map
$$\ch : K_0(\Schur) \otimes k \to k[x_1, x_2, \dotsc ]^{S_{\infty}}$$
which is a priori only $k$-linear and graded, where the grading on the LHS has $\text{Rep}(S_n)$ in degree $n$ and the grading on the RHS is the usual. Next we want to show that the functor $F \mapsto (V \mapsto F(V))$ is symmetric monoidal in the sense that the Day convolution $F \otimes G$ is sent to the pointwise tensor product $V \mapsto F(V) \otimes G(V)$. This can be verified explicitly but it can also be done using abstract nonsense by thinking of $\Schur$ as the free symmetric monoidal $\FinVect$-tensored category with finite colimits (or something like that, anyway) on a point and using the fact that the map $F \mapsto (V \mapsto F(V))$ comes directly from this universal property. It follows that $\ch$ is a ring homomorphism.
So far so abstract nonsense. Now we need two computations:

*

*The Schur functor associated to the sign representation of $S_n$ is the $n^\text{th}$ exterior power $V \mapsto \bigwedge^k(V)$. It follows that the Frobenius characteristic of the sign representation of $S_n$ is the elementary symmetric polynomial $e_n$, and hence (by the fundamental theorem of symmetric functions) that $\ch$ is surjective.

*The dimension of the degree $n$ piece of both $K_0(\Schur)$ and the ring of symmetric functions is $p(n)$. It follows from surjectivity that $\ch$ is an isomorphism.

The dimension calculation can probably be avoided by giving a more direct proof of injectivity. I think we just need to show that if $F_n$ and $G_n$ are two non-isomorphic representations of $S_n$ then $F_n \otimes_{S_n} V^{\otimes n}$ and $G_n \otimes_{S_n} V^{\otimes n}$ have different formal characters. I can't think of anything at the moment but probably one of you can.
In any case this argument avoids the construction of Specht modules and uses only the fundamental theorem of symmetric functions on the symmetric function side. The category theory cleanly handles all the bookkeeping as it should. I should mention that I learned all this stuff from reading John Baez - "Schur functors".
