It can happen that two equivariant sets with atoms are related by a finitely supported bijection, but not by an equivariant bijection.
A set is orbit finite if and only if the number of its elements supported by atoms grows polynomially with .
In Automata theory in nominal sets (Thm. 9.3), we provided a necessary and sufficient criterion for the existence of least finite supports for arbitrary atoms. It was not clear whether the criterion could be significantly simplified for Fraisse atoms. I show that it cannot be made as simple as we originally conjectured.
Fix attention on equality atoms.
Given an orbit-finite, deterministic automaton on the alphabet of atoms, a Brzozowski phase amounts to:
- reversing the direction of all transition arrows and swapping initial and accepting states,
- determinising the result, and
- cutting to the reachable part.