Orbit-finite groups are finite, and therefore not very interesting from the perspective of sets with atoms. It turns out that orbit-finite groupoids form interesting structures. They will be useful in the study of orbit-finite semigroups in the following post.

The following lemma appears in On the use of guards for logics with data by Thomas Colcombet, Clemens Ley and Gabriele Puppis (with a different proof).

Lemma 1. Any orbit-finite group is finite.

Proof. For simplicity, assume that is equivariant. It follows that the neutral element of is equivariant and also the inversion mapping is equivariant.

Observe that for any . Fix  to be of maximal support cardinality. Choose any whose support is disjoint from the support of . It follows from the above equation that is contained in . But is disjoint from , so in fact, is contained in . By maximality, it follows that Assuming that is infinite, there are infinitely many elements whose support is disjoint from the support of , and for each of them, the above equality holds. However, in an orbit-finite set there are only finitely many elements whose support is equal to . It follows that for two distinct elements , we have a contradiction.

A groupoid is a small category whose morphisms (arrows) are isomorphisms. In other words, it is a set of objects , a set of arrows , together with two mappings and a partial composition function , such that  is defined if and only if , and such that natural axioms are satisfied:

• associativity: the result (or lack of thereof) of composing three arrows does not depend on the order of applying composition;
• neutrality: for every object there is an identity morphism which is the left identity for every morphism from and right identity for every morphism to ;
• invertibility: every morphism has an inverse in the other direction such that the two compositions yield the identities on the source and target.

If are two objects, then by we denote the set of arrows with domain and range .

An orbit-finite groupoid is a groupoid where all the components are orbit-finite. In the rest of this post we will assume that groupoids are equivariant, i.e., all the components are equivariant.

A groupoid is connected if for every two objects there is an arrow between them, i.e., is nonempty for any two objects .

Example. Fix a single orbit alphabet and define the groupoid whose objects are elements of , and whose arrows are triples such that and is a bijection such that for any atom permutation extending . Then is a connected orbit-finite groupoid. For example, if is the set of unordered pairs of atoms, then the morphisms of  are bijections between two-element sets of atoms, with the natural composition in case when the domain and range agree.

Lemma 2. Let be a connected groupoid and let for some fixed object . Then, is a group, and for any two objects , the set is in bijection with .

Corollary. In an orbit-finite groupoid, there are finitely many arrows between any two objects.

Lemma 3. In an orbit-finite groupoid, for any object , every arrow from to  has the same support as .

Proof. Let be an arrow from to . Then supports , since is the source of , i.e., can be obtained from by applying the equivariant source mapping. This shows that .

Suppose that . By applying to  any permutation which is the identity on we obtain an arrow  whose source and target is equal to . If  then we may obtain infinitely many distinct such arrows of the form , contradicting the above corollary which states that there are finitely many arrows from to .

Question 1. Is there a structure theorem for orbit-finite groupoids? In particular, is every connected orbit-finite groupoid is equivariantly isomorphic to , for some orbit-finite alphabet ? This is false – consider for instance a finite groupoid. Is every orbit-finite groupoid is equivariantly isomorphic to , where is a finite groupoid? This is also false, as witnessed by the following example.

Example. The groupoid here consists of directed matchings from an unordered pair of atoms to an unordered pair of atoms, where each edge is directed and labeled by or . Composition of two such matchings is defined if the target-set of is equal to the source-set of ; in this case, the resulting matching is obtained by composing the arrows and adding the labels modulo . This forms a groupoid.

Question 2. Can groupoids be straightened (see the previous post), i.e., is every groupoid a image of a straight groupoid (one whose set of objects and set of arrows is a straight set) under an equivariant groupoid homomorphism (a functor of categories)?

In the following post, we will argue that groupoids arise naturally in the study of orbit-finite semigroups.