Let us fix an infinite set , which we will call the atoms. Consider the set of all permutations of the atoms, which is a group. An action of the group of permutations of atoms on a set
is a function
which is consistent with the group structure in the sense that
Given such an action, we say that a set of atoms supports some
if
is uniquely determined by the values of
on atoms from
. In other words,
Define a set with atoms to be a set equipped with an action of permutations of atoms such that every element
has some finite support.
Equivariance. If is a set with atoms, call a subset
equivariant if the subset is invariant under renaming atoms, i.e.
holds for every and every permutation of the atoms
. A function
is called equivariant if
holds for every and every permutation of the atoms
. These definitions are compatible in the sense that: a subset is equivariant if and only if its characteristic function is equivariant, and a function is equivariant if and only if its graph is an equivariant relation.
Orbit-finiteness. If is a set with atoms, we say that
are in the same orbit if some permutation of the atoms takes
to
. This is an equivalence relation, and its equivalence classes are called orbits. A set with atoms is called orbit-finite if it has finitely many orbits. The motivation for this notion is that the state space, input alphabet and all other components in a register automaton are orbit-finite sets with atoms.
Lemma 1. Let be an equivariant function. If a set of atoms supports
, then it also supports
.
Proof. From the definition: if is a permutation of atoms which fixes
, then it also fixes
by equivariance.
A representation theorem.
Let us write for the set of non-repeating
-tuples of atoms. This is a single-orbit set with atoms. On the set
, we can define an action of permutations of
as follows:
Note that we have two groups acting on , permutations of the atoms, and permutations of the coordinates. These actions commute with each other in the following sense: if
is a permutation of the coordinates and
is a permutation of the atoms, then
If is a subgroup of all permutations of
, then we define
to be modulo the equivalence relation which identifies two tuples if they are in the same orbit with respect to the action of
. The following theorem shows that this is essentially the only possible construction for sets with atoms.
Theorem 1. Every set with atoms is isomorphic (where isomorphisms are equivariant bijections) to a disjoint union of sets of the form
where is a natural number and
is a subgroup of the permutation group on
.
Proof. It suffices to prove the theorem for single orbit sets, because every set with atoms is isomorphic to the disjoint union of its orbits. Let then be a single-orbit set. Choose some
, and let
be the least support of
, in some order. Consider the relation
which is equivariant by definition. Because supports
, the above is actually an equivariant function, call it
Consider the inverse image , and define
to be the permutations of
such that
The set is easily seen to be a subgroup. To conclude the proof, we make the following claim, which implies that
is isomorphic to
.
Claim. The following conditions are equivalent for every :
1)
2) there is some such that
.
2) implies 1) Assume 2) holds for some . By definition of
, we have
Let be some permutation of the atoms such that
, which exists because there is only one orbit of non-repeating tuples. Applying
to both sides of the equality above, we get
By equivariance of , we have
Because permutations with atoms commute with permutations of coordinates, we have
By choice of , the above is
1) implies 2) Suppose . Let
be some permutation of the atoms such that
. By equivariance of
, we have
By Lemma 1, the tuple supports
. By the least support theorem, the set of atoms in
must be equal to
, i.e. there must be some permutation
of coordinates such that
Since has the same image under
as
, it follows that
. Therefore,
which completes the proof of the claim and therefore also of the theorem.
Leave a Reply