Finite groups are surjunctive

Disclosure — non-blind read-back. This read-back is not independent testimony. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, with full knowledge of the source material and of the intended meaning. It was not produced by a blind auditor, and reviewers should not treat it as an independent check of faithfulness.

For every group $G$ in universe $0$ that is finite, $G$ is surjunctive. Here a group $G$ is called surjunctive when the following holds: for every finite, nonempty set $A$ (a type in the lowest universe, equipped with a chosen finite enumeration and with a topology that is assumed to be discrete), and for every map $\tau : A^G \to A^G$ (where $A^G$ is the set of all functions $G \to A$, carrying the product topology), if $\tau$ is continuous, shift-equivariant and injective, then $\tau$ is surjective. Shift-equivariant means $\tau(g\cdot x) = g\cdot \tau(x)$ for every $g \in G$ and every $x \in A^G$, where the left shift is $(g\cdot x)(h) = x(g^{-1}h)$ for $h \in G$.