Fact. Suppose that is a one-orbit set and
is an equivariant function. Then is a bijection.
Proof. Let be the set of equivariant endomorphisms from to . This is a finite monoid, which contains . By a standard result on finite monoids, there must be some natural number such that is idempotent, i.e.
Let be any element in the range of . By idempotency of , this is a fixpoint, i.e.
By equivariance of , it follows that
holds for every atom automorphism , and therefore is the identity on by the assumption that has one orbit. Since is the identity, it follows that has to be a bijection.
Comment. The fact also follows from the representation theorem, but we do not know if the representation theorem always holds.