Proof of Lemma 4.8 — the regular representation of a quotient has no fixed zero-sum vector

Let $\phi : H \to T$ be a surjective homomorphism from a group $H$ onto a finite group $T$, and let $\pi$ be the left regular representation of $T$ by permutation matrices, $(\pi(t))_{w,u} = 1$ if $w u^{-1} = t$ and $0$ otherwise. Let $W = \{ v \in \mathbb{C}^T : \sum_{t\in T} v_t = 0 \}$. Then every nonzero $v \in W$ is moved by some element of $H$:

In other words the representation $\pi\cdot\phi$ of $H$, restricted to the invariant subspace $W$, is essentially nontrivial (Definition 4.5). This is the claim in the proof of Lemma 4.8 that lets Lemma 4.7 be applied to $W$.

Formalization Note The statement is phrased on the permutation matrices $\pi(\phi(h))$ acting on $\mathbb{C}^T$ rather than on a packaged unitary representation of $H$ in the Hilbert space $W$; the conclusion is exactly the defining condition of essential nontriviality for that representation.