Finite faithful representation from point-separating representations (source code)

= Finite faithful representation from point-separating representations

Suppose finite-dimensional <continuous> <group representations> separate points of a <compact Lie group>. Choose an identity neighborhood $U$ containing no nontrivial subgroup, using <Lie groups have no small subgroups>. For each $g\notin U$, choose a representation whose matrix at $g$ is not the identity. The corresponding open nonidentity sets cover the compact complement of $U$, so finitely many representations suffice there. Their <direct sum> has kernel inside $U$ and therefore trivial kernel. <Unitarization of a compact-group representation> makes it a finite-dimensional faithful <unitary representation>.