Peter-Weyl for an infinite product of finite groups

The Axiom of Choice is inherited through the profinite compactness and Haar suppliers and through the representative and basis choices in the general Peter–Weyl coefficient family (The Axiom of Choice). No further choice is needed for the finite-coordinate factorization and pullback arguments.

The product $K={\prod }_{i\in I}{G}_i$ of finite discrete groups is the inverse limit of the finite groups $K_F$ over the directed set of finite subsets $F\subseteq I$, hence a profinite group: compact, Hausdorff, totally disconnected; it carries a normalized Haar probability $\mu$, and the kernels $\ker p_F$ form an open normal neighbourhood basis. (A profinite group is a topological group isomorphic to an inverse limit of finite discrete groups, Normalized Haar probability on a compact group, The product set ${\prod }_{i\in I}{X}_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Continuous finite-dimensional representations of a product of finite groups factor through a finite subproduct)

Every continuous finite-dimensional unitary representation $\rho$ of $K$ factors as $\rho ={\rho }_F\circ p_F$ through a finite subproduct, and every matrix coefficient of $\rho$ depends only on the coordinates in $F$. Conversely a representation ${\rho }_F$ of $K_F$ pulls back along the surjection $p_F$ to a continuous finite-dimensional unitary representation of $K$ with coefficients ${\rho }_F$-coefficients composed with $p_F$. (Continuous finite-dimensional representations of a product of finite groups factor through a finite subproduct, Matrix coefficient of a unitary representation)

Pullback along a surjective homomorphism preserves and reflects irreducibility: a closed invariant subspace of the pullback corresponds bijectively to a closed invariant subspace of the representation on the quotient, because the acting groups coincide, $\rho (K)={\rho }_F(K_F)$. (Strongly continuous unitary representations, invariant linear subspaces and intertwiners, Continuous finite-dimensional representations of a product of finite groups factor through a finite subproduct)

For the finite group $K_F$ the coefficient algebra $R(K_F)$ equals $C(K_F)$: $R(K_F)$ is a dense linear subspace of the finite-dimensional space $C(K_F)$ by the general density theorem, and a finite-dimensional subspace of a normed space is closed. (Uniform density of representative functions (topological Peter-Weyl theorem), A finite-dimensional normed subspace is closed)

The general compact-group theory applies to $K$: irreducible representations are finite dimensional, $R(K)$ is uniformly dense in $C(K)$, the normalized coefficient family is an orthonormal basis of $L^2(K)$, and the regular representation decomposes into the isotypic blocks. (Irreducible unitary representations of compact groups are finite dimensional, Uniform density of representative functions (topological Peter-Weyl theorem), The normalized matrix coefficients form an orthonormal basis of L2(K), Peter-Weyl decomposition of the regular representation, The unitary dual of a compact group, The normalized irreducible matrix coefficient family)

The functions $K\to \mathbb{C}$ depending on finitely many coordinates form a unital self-adjoint complex algebra containing the constants, and they separate points: distinct points differ in some coordinate $i$, and the function of that coordinate alone taking value $1$ at one coordinate and $0$ at the other is continuous because $G_i$ is discrete. (Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense, The product set ${\prod }_{i\in I}{X}_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Representative functions on a compact group)