Friedrich-Alexander-Universität Erlangen-Nürnberg,
Germanyhenning.urbat@fau.dehttps://orcid.org/0000-0001-5890-9485 Friedrich-
Alexander-Universität Erlangen-Nürnberg,
Germanyhenning.urbat@fau.dehttps://orcid.org/0000-0002-2021-1644 Friedrich-
Alexander-Universität Erlangen-Nürnberg,
Germanyhenning.urbat@fau.dehttps://orcid.org/0000-0002-3265-7168 Fabian
Birkmann, Stefan Milius and Henning Urbat[100]F.4.3 Formal LanguagesA full
version is available at https://arxiv.org/abs/2304.13337Deutsche
Forschungsgemeinschaft (DFG, German Research Foundation) – project number
470467389

# Nominal Topology for Data Languages

Fabian Birkmann  Stefan Milius  Henning Urbat

###### Abstract

We propose a novel topological perspective on data languages recognizable by
orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite
nominal topological spaces. Assuming globally bounded support sizes, they
coincide with nominal Stone spaces and are shown to be dually equivalent to a
subcategory of nominal boolean algebras. Recognizable data languages are
characterized as topologically clopen sets of pro-orbit-finite words. In
addition, we explore the expressive power of pro-orbit-finite equations by
establishing a nominal version of Reiterman’s pseudovariety theorem.

###### keywords:

Nominal sets, Stone duality, Profinite space, Data languages

##  1 Introduction

While automata theory is largely concerned with formal languages over finite
alphabets, the extension to _infinite alphabets_ has been identified as a
natural approach to modelling structures involving _data_ , such as nonces
[26], channel names [23], object identities [22], process identifiers [11],
URLs [5], or values in XML documents [31]. For example, if $\mathbb{A}$ is a
(countably infinite) set of data values, typical languages to consider might
be

$\displaystyle L_{0}$ $\displaystyle=\\{\,vaaw\mid
a\in\mathbb{A},\,v,w\in\mathbb{A}^{*}\,\\}$ $\displaystyle\text{(``some data
value occurs twice in a row'')},\text{ or}$ $\displaystyle L_{1}$
$\displaystyle=\\{\,avaw\mid a\in\mathbb{A},\,v,w\in\mathbb{A}^{*}\,\\}$
$\displaystyle\text{(``the first data value occurs again'')}.$

Automata for data languages enrich finite automata with register mechanisms
that allow to store data and test data values for equality (or more complex
relations, e.g. order) [24, 31]. In a modern perspective first advocated by
Bojańczyk, Klin, and Lasota [9], a convenient abstract framework for studying
data languages is provided by the theory of _nominal sets_ [36].

Despite extensive research in the past three decades, no universally
acknowledged notion of _regular_ data language has emerged so far. One reason
is that automata models with data notoriously lack robustness, in that any
alteration of their modus operandi (e.g. deterministic vs. nondeterministic,
one-way vs. two-way) usually affects their expressive power. Moreover,
machine-independent descriptions of classes of data languages in terms of
algebra or model theory are hard to come by. However, there is one remarkable
class of data languages that closely mirrors classical regular languages: data
languages recognizable by orbit-finite nominal monoids [7]. Originally
introduced from a purely algebraic angle, recognizable data languages have
subsequently been characterized in terms of _rigidly guarded
$\text{MSO}^{\sim}$_, a fragment of monadic second-order logic with equality
tests [13], _single-use register automata_ [10] (both one-way and two-way),
and _orbit-finite regular list functions_ [10]. In addition, several landmark
results from the algebraic theory of regular languages, namely the McNaughton-
Papert-Schützenberger theorem [41, 29], the Krohn-Rhodes theorem [25], and
Eilenberg’s variety theorem [14] have been extended to recognizable data
languages [7, 13, 45, 10].

In the present paper, we investigate recognizable data languages through the
lens of _topology_ , thereby providing a further bridge to classical regular
languages. The topological approach to the latter is closely tied to the
algebraic one, which regards regular languages as the languages recognizable
by finite monoids. Its starting point is the construction of the topological
space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
of _profinite words_. Informally, this space casts all information represented
by regular languages over $\Sigma$ and their recognizing monoids into a single
mathematical object. Regular languages can then be characterized by purely
topological means: they may be interpreted as precisely the clopen subsets of
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$,
in such way that algebraic recognition by finite monoids becomes a continuous
process. Properties of regular languages are often most conveniently
classified in terms of the topological concept of _profinite equations_ , that
is, equations between profinite words; see [3, 33, 4] for a survey of
profinite methods in automata theory. Moreover, since
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
forms a Stone space, the power of _Stone duality_ – the dual equivalence
between Stone spaces and boolean algebras – becomes available. This allows for
the use of duality-theoretic methods for the study of regular languages and
their connection to logic and model theory, which in part even extend to _non-
regular_ languages [35, 18, 19, 20, 21].

On a conceptual level, the topological view of regular languages rests on a
single category-theoretic fact: Stone spaces admit a universal property. In
fact, they arise from the category of finite sets as the free completion under
codirected limits, a.k.a. its _Pro-completion_ :

$\mathbf{Stone}\simeq\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}}).$ (1.1)

In the world of data languages, the role of finite sets is taken over by
orbit-finite nominal sets. This strongly suggests to base a topological
approach on their free completion
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})$. However, this turns out to
be infeasible: the category $\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})$
is not concrete over nominal sets (3.3), hence it cannot be described via any
kind of nominal topological spaces. This is ultimately unsurprising given that
the description (1.1) of Stone spaces as a free completion depends on the
axiom of choice, which is well-known to fail in the topos of nominal sets. As
a remedy, we impose _global bounds_ on the support sizes of nominal sets, that
is, we consider the categories $\mathbf{Nom}_{k}$ and
$\mathbf{Nom}_{\mathrm{of},k}$ of (orbit-finite) nominal sets where every
element has a support of size $k$, for some fixed natural number $k$. This
restriction is natural from an automata-theoretic perspective, as it
corresponds to imposing a bound $k$ on the number of registers of automata,
and it fixes exactly the issue making unrestricted nominal sets non-amenable
(3.5). Let us emphasize, however, that the category $\mathbf{Nom}_{k}$ is not
proposed as a new foundation for names and variable binding; for instance, it
generally fails to be a topos.

The first main contribution of our paper is a generalization of (1.1) to
$k$-bounded nominal sets. For this purpose we introduce _nominal Stone spaces_
, a suitable nominalization of the classical concept, and prove that
$k$-bounded nominal Stone spaces form the Pro-completion of the category of
$k$-bounded orbit-finite sets. We also derive a nominal version of Stone
duality, which relates $k$-bounded nominal Stone spaces to _locally $k$-atomic
orbit-finitely complete nominal boolean algebras_. Hence we establish the
following equivalences of categories:

$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\simeq^{\mathrm{op}}\mathbf{nStone}_{k}\simeq\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k}).$

The above equivalences are somewhat remarkable since even the category of
$k$-bounded nominal sets does not feature choice. They hold because the
presence of bounds allows us to reduce topological properties of nominal Stone
spaces, most notably compactness, to their classical counterparts.

Building on the above topological foundations, which we regard to be of
independent interest, we subsequently develop first steps of a topological
theory of data languages. Specifically, we introduce nominal Stone spaces of
(bounded) _pro-orbit-finite words_ and prove their clopen subsets to
correspond to data languages recognizable by bounded equivariant monoid
morphisms, generalizing the topological characterization of classical regular
languages (Theorem 5.4). Moreover, we investigate the expressivity of _pro-
orbit-finite equations_ and show that they model precisely classes of orbit-
finite monoids closed under finite products, submonoids, and _multiplicatively
support-reflecting quotients_ (Theorem 6.3). This provides a nominal version
of Reiterman’s celebrated pseudovariety theorem [37] for finite monoids.

#### Related work.

The perspective taken in our paper draws much of its inspiration from the
recent categorical approach to algebraic recognition based on monads [8, 43,
39]. The importance of Pro-completions in algebraic language theory has been
isolated in the work of Chen et al. [12] and Urbat et al. [43]. In the latter
work the authors introduce _profinite monads_ and present a general version of
Eilenberg’s variety theorem parametric in a given Stone-type duality. The
theory developed there applies to algebraic base categories, but not to the
category of nominal sets.

Our version of nominal Stone duality builds on the orbit-finite restriction of
the duality between nominal sets and complete atomic nominal boolean algebras
due to Petrişan [17]. It is fundamentally different from the nominal Stone
duality proposed by Gabbay, Litak, and Petrişan [16], which relates _nominal
Stone spaces with $\mathsf{N}$ _ to _nominal boolean algebras with
$\mathsf{N}$ _. The latter duality is not amenable for the theory of data
languages; see 11.

Reiterman’s pseudovariety theorem has recently been generalized to the level
of finite algebras for a monad [12, 1] and, in a more abstract disguise,
finite objects in a category [30]. For nominal sets, varieties of algebras
over binding signatures have been studied by Gabbay [16] and by Kurz and
Petrişan [27], resulting in nominal Birkhoff-type theorems [6]. Urbat and
Milius [45] characterize classes of orbit-finite monoids called _weak_
pseudovarieties by sequences of nominal word equations. This gives a nominal
generalization of the classical Eilenberg-Schützenberger theorem [15], which
in fact is a special case of the general HSP theorem in [30]. Nominal pro-
orbit-finite equations as introduced in the present paper are strictly more
expressive than sequences of nominal word equations (6.5), hence our nominal
Reiterman theorem is not equivalent to the nominal Eilenberg-Schützenberger
theorem. Moreover, we note that the nominal Reiterman theorem does not appear
to be an instance of any of the abstract categorical frameworks mentioned
above.

##  2 Preliminaries

We assume that readers are familiar with basic notions from category theory,
e.g. functors, natural transformations, and (co)limits, and from point-set
topology, e.g. metric and topological spaces, continuous maps, and
compactness. In the following we recall some facts about Pro-completions, the
key categorical concept underlying our topological approach to data languages.
Moreover, we give a brief introduction to the theory of nominal sets [36].

Pro-completions. A small category $I$ is _cofiltered_ if (i) $I$ is non-empty,
(ii) for every pair of objects $i,j\in I$ there exists a span $i\leftarrow
k\to j$, and (iii) for every pair of parallel arrows $f,g\colon j\to k$, there
exists a morphism $h\colon i\to j$ such that $f\cdot h=g\cdot h$. Cofiltered
preorders are called _codirected_ ; thus a preorder $I$ is codirected if
$I\neq\emptyset$ and every pair $i,j\in I$ has a lower bound $k\leq i,j$. For
instance, every meet-semilattice with bottom is codirected. A diagram $D\colon
I\rightarrow\mathbf{C}$ in a category $\mathbf{C}$ is _cofiltered_ if its
index category $I$ is cofiltered. A _cofiltered limit_ is a limit of a
cofiltered diagram. _Codirected limits_ are defined analogously. The two
concepts are closely related: a category has cofiltered limits iff it has
codirected limits, and a functor preserves cofiltered limits iff it preserves
codirected limits [2, Cor. 1.5]. The dual concept is that of a _filtered
colimit_ or a _directed colimit_ , respectively.

######  Example 2.1.

  1. 1.

In the category $\mathbf{Set}$ of sets and functions, every filtered diagram
$D\colon I\to\mathbf{Set}$ has a colimit cocone $c_{i}\colon
D_{i}\to\operatorname*{colim}D$ ($i\in I$) given by
$\operatorname*{colim}D=\big{(}\coprod_{i\in I}D_{i}\big{)}/{\sim}$ and
$c_{i}(x)=[x]_{\sim}$, where the equivalence relation $\sim$ on the coproduct
(i.e. disjoint union) $\coprod_{i\in I}D_{i}$ relates $x\in D_{i}$ and $y\in
D_{j}$ iff there exist morphisms $f\colon i\to k$ and $g\colon j\to k$ in $I$
such that $Df(x)=Dg(y)$.

  2. 2.

Every cofiltered diagram $D\colon I\rightarrow\mathbf{Set}$ has a limit whose
cone $p_{i}\colon\lim D\to D_{i}$ ($i\in I$) is given by the _compatible
families_ of $D$ and projection maps:

$\lim D=\\{(x_{i})_{i\in I}\mid x_{i}\in D_{i}\text{ and
}Df(x_{i})=x_{j}\text{ for all $f\colon i\to j$ in $I$}\\}\quad\text{and}\quad
p_{j}((x_{i})_{i\in I})=x_{j}.$

  3. 3.

In the category $\mathbf{Top}$ of topological spaces and continuous maps, the
limit cone of a cofiltered diagram $D\colon I\rightarrow\mathbf{Top}$ is
formed by taking the limit in $\mathbf{Set}$ and equipping $\lim D$ with the
_initial topology_ , viz. the topology generated by the basic open sets
$p_{i}^{-1}[U_{i}]$ for $i\in I$ and $U_{i}\subseteq D_{i}$ open.

An object $C$ of a category $\mathbf{C}$ is _finitely copresentable_ if the
contravariant hom-functor
$\mathbf{C}(-,C)\colon\mathbf{C}^{\mathrm{op}}\to\mathbf{Set}$ preserves
directed colimits. In more elementary terms, this means that for every
codirected diagram $D\colon I\to\mathbf{C}$ with limit cone $p_{i}\colon
L\rightarrow D_{i}$ ($i\in I$),

  1. 1.

every morphism $f\colon L\rightarrow C$ factorizes as $f=g\circ p_{i}$ for
some $i\in I$ and $g\colon D_{i}\to C$, and

  2. 2.

the factorization is essentially unique: given another factorization $f=h\cdot
p_{i}$, there exists $j\leq i$ such that $g\cdot D_{j,i}=h\cdot D_{j,i}$.

A _Pro-completion_ of a small category $\mathbf{C}$ is a free completion under
codirected (equivalently cofiltered) limits. It is given by a category
$\operatorname{Pro}(\mathbf{C})$ with codirected limits together with a full
embedding $E\colon\mathbf{C}\hookrightarrow\operatorname{Pro}(\mathbf{C})$
satisfying the following universal property:

  1. 1.

every functor $F\colon\mathbf{C}\rightarrow\mathbf{D}$, where $\mathbf{D}$ has
codirected limits, extends to a functor $\mathrlap{\hskip
2.5pt\overline{\scalebox{0.6}[1.0]{\phantom{$F$}}}}F\colon\operatorname{Pro}(\mathbf{C})\rightarrow\mathbf{D}$
that preserves codirected limits and satisfies $F=\mathrlap{\hskip
2.5pt\overline{\scalebox{0.6}[1.0]{\phantom{$F$}}}}F\circ E$;

  2. 2.

$\mathrlap{\hskip 2.5pt\overline{\scalebox{0.6}[1.0]{\phantom{$F$}}}}F$ is
essentially unique: For every functor $G$ that preserves codirected limits and
satisfies $F=G\circ E$, there exists a natural isomorphism
$\alpha\colon\mathrlap{\hskip
2.5pt\overline{\scalebox{0.6}[1.0]{\phantom{$F$}}}}F\cong G$ such that $\alpha
E=\mathrm{id}_{F}$.

${\mathbf{C}}$${\operatorname{Pro}(\mathbf{C})}$${\mathbf{D}}$$\scriptstyle{E}$$\scriptstyle{F}$$\scriptstyle{\mathrlap{\hskip
2.0pt\overline{\scalebox{0.6}[1.0]{\phantom{$\scriptstyle F$}}}}F}$
${\mathbf{C}}$${\operatorname{Pro}(\mathbf{C})}$${\mathbf{D}}$$\scriptstyle{E}$$\scriptstyle{F}$$\scriptstyle{G}$

The universal property determines $\operatorname{Pro}(\mathbf{C})$ uniquely up
to equivalence of categories. We note that every object $EC$
($C\in\mathbf{C}$) is finitely copresentable in
$\operatorname{Pro}(\mathbf{C})$, see e.g. [1, Thm A.4]. The dual of Pro-
completions are _Ind-completions_ : free completions under _directed
colimits_.

######  Example 2.2.

The Pro-completion $\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}})$ of the
category of finite sets is the full subcategory of $\mathbf{Top}$ given by
_profinite spaces_ (topological spaces that are codirected limits of finite
discrete spaces). Profinite spaces are also known as _Stone spaces_ or
_boolean spaces_ and can be characterized by topological properties: they are
precisely compact Hausdorff spaces with a basis of clopen sets. This
equivalent characterization depends on the axiom of choice (or rather the
ultrafilter theorem, a weak form of choice), as does _Stone duality_ , the
dual equivalence between the categories of Stone spaces and boolean algebras.
The duality maps a Stone space to its boolean algebra of clopen sets, equipped
with the set-theoretic boolean operations. Its inverse maps a boolean algebra
the set of ultrafilters (equivalently, prime filters) on it, equipped with a
suitable profinite topology.

#### Profinite words.

The topological approach to classical regular languages is based on the space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
of _profinite words_ over the alphabet $\Sigma$. This space is constructed as
the codirected limit of all finite quotient monoids of $\Sigma^{*}$, the free
monoid of finite words generated by $\Sigma$. Formally, let
${\Sigma^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}}{\mathbf{Mon}_{\mathrm{f}}}$
be the codirected poset of all surjective monoid morphisms
$e\colon\Sigma^{*}\twoheadrightarrow M$, where $M$ is a finite monoid; the
order on
${\Sigma^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}}{\mathbf{Mon}_{\mathrm{f}}}$
is defined by $e\leq e^{\prime}$ if $e^{\prime}=e\cdot h$ for some $h$. Then
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
is the limit of the diagram
$D\colon{\Sigma^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}}{\mathbf{Mon}_{\mathrm{f}}}\to\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}})$
sending $e\colon\Sigma^{*}\twoheadrightarrow M$ to the underlying set of $M$,
regarded as a finite discrete topological space. The space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
is completely metrizable; in fact, it is the Cauchy completion of the metric
space $(\Sigma^{*},d)$ where $d(v,w)=\sup\\{\,2^{-|M|}\mid\text{$M$ is a
finite monoid separating $v,w$}\,\\}$. Here a monoid $M$ _separates_
$v,w\in\Sigma^{*}$ if there exists a morphism $h\colon\Sigma^{*}\to M$ such
that $h(v)\neq h(w)$. Regular languages over $\Sigma$ correspond to clopen
subsets of
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$,
or equivalently to continuous maps
$L\colon\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}\to
2$ into the discrete two-element space.

#### Nominal Sets.

Fix a countable set $\mathbb{A}$ of _names_ , and denote by
$\operatorname{Perm}\mathbb{A}$ the group of finite permutations, i.e.
bijections $\pi\colon\mathbb{A}\to\mathbb{A}$ fixing all but finitely many
names. Given $S\subseteq\mathbb{A}$ write

$\operatorname{Perm}_{S}\mathbb{A}=\\{\pi\in\operatorname{Perm}\mathbb{A}\mid\pi(a)=a\text{
for all $a\in S$}\\}$

for the the subgroup of permutations fixing $S$. A
_$\operatorname{Perm}\mathbb{A}$ -set_ is a set $X$ with a group action, that
is, an operation $\cdot\colon\operatorname{Perm}\mathbb{A}\times X\rightarrow
X$ such that $\mathrm{id}\cdot x=x$ and $\pi\cdot(\sigma\cdot
x)=(\pi\circ\sigma)\cdot x$ for every $x\in X$ and
$\pi,\sigma\in\operatorname{Perm}\mathbb{A}$. The _trivial_ group action on
$X$ is given by $\pi\cdot x=x$ for all $x\in X$ and
$\pi\in\operatorname{Perm}\mathbb{A}$.

A subset $S\subseteq\mathbb{A}$ is a _support_ of $x\in X$ if every
permutation $\pi\in\operatorname{Perm}_{S}\mathbb{A}$ acts trivially on $x$,
that is, $\pi\cdot x=x$. The idea is that $x$ is some syntactic object (e.g. a
word, a tree, or a $\lambda$-term) whose free variables are contained in $S$.
A $\operatorname{Perm}\mathbb{A}$-set $X$ is a _nominal set_ if every element
$x\in X$ has a finite support. This implies that every $x\in X$ has a _least_
finite support, denoted by $\operatorname{supp}x\subseteq\mathbb{A}$.

For a nominal set $X$ its _nominal powerset_
$\mathcal{P}_{\text{fs}}X\subseteq\mathcal{P}X$ consists of all subsets of
$U\subseteq X$ which are finitely supported under the action $\pi\cdot
U\vcentcolon=\\{\pi\cdot x\mid x\in U\\}$. For example, for the nominal set
$\mathbb{A}$ of names with the action $\pi\cdot a=\pi(a)$, its nominal
powerset $\mathcal{P}_{\text{fs}}\mathbb{A}$ consists of all finite and
cofinite subsets of $\mathbb{A}$. A subset $U\subseteq X$ is _equivariant_ if
it has empty support. If there exists a finite subset $S\subseteq\mathbb{A}$
supporting every $x\in U$ then $U$ is _uniformly finitely supported_ , and $S$
also supports $U$. Given a finite set $S\subseteq\mathbb{A}$ of names and a
subset $U\subseteq X$, we define the _$S$ -hull_ of $U$ by
$\operatorname{hull}_{S}U=\\{\pi\cdot x\mid x\in
U,\pi\in\operatorname{Perm}_{S}\mathbb{A}\\}$. This is the smallest
$S$-supported subset of $X$ containing $U$.

For finite $S\subseteq\mathbb{A}$ the _$S$ -orbit_ of an element $x\in X$ is
the set $\operatorname{orb}_{S}x=\\{\pi\cdot
x\mid\pi\in\operatorname{Perm}_{S}\mathbb{A}\\}$. The $\emptyset$-orbit of $x$
is called its _orbit_ , denoted $\operatorname{orb}x$. We write
$\operatorname{orb}_{S}X=\\{\operatorname{orb}_{S}x\mid x\in X\\}$ for the set
of all $S$-orbits of $X$, and $\operatorname{orb}X$ for the set of all orbits.
The $S$-orbits form a partition of $X$. A finitely supported subset
$Y\subseteq X$ is _orbit-finite_ if it intersects only finitely many orbits of
$X$. In particular, the nominal set $X$ is _orbit-finite_ if
$\operatorname{orb}X$ is a finite set. This implies that for every finite
subset $S\subseteq\mathbb{A}$ the set $\operatorname{orb}_{S}X$ is finite.
Moreover, $X$ contains only finitely many elements with support $S$.

######  Example 2.3.

The set $\mathbb{A}^{*}$ of finite words over $\mathbb{A}$ forms a nominal set
with the group action $\pi\cdot(a_{1}\cdots
a_{n})=\pi(a_{1})\cdots\pi(a_{n})$. The languages
$L_{0},L_{1}\subseteq\mathbb{A}^{*}$ from the Introduction are equivariant
subsets. Given a fixed name $a\in\mathbb{A}$, the subset $L_{2}=\\{awa\mid
w\in\mathbb{A}^{*}\\}$ is finitely supported with
$\operatorname{supp}L_{2}=\\{a\\}$. All the above sets have an infinite number
of orbits. An example of an orbit-finite set is given by
$\mathbb{A}^{2}=\mathbb{A}\times\mathbb{A}\subseteq\mathbb{A}^{*}$; its two
orbits are $\\{aa\mid a\in\mathbb{A}\\}$ and $\\{ab\mid a\neq
b\in\mathbb{A}\\}$.

A map $f\colon X\rightarrow Y$ between nominal sets is _finitely supported_ if
there exists a finite set $S\subseteq\mathbb{A}$ such that $f(\pi\cdot
x)=\pi\cdot f(x)$ for all $x\in X$ and
$\pi\in\operatorname{Perm}_{S}\mathbb{A}$, and _equivariant_ if it is
supported by $S=\emptyset$. Equivariant maps satisfy
$\operatorname{supp}f(x)\subseteq\operatorname{supp}x$ for all $x\in X$.
Nominal sets and equivariant maps form a category $\mathbf{Nom}$, with the
full subcategory $\mathbf{Nom}_{\mathrm{of}}$ of orbit-finite nominal sets.
The category $\mathbf{Nom}$ is complete and cocomplete. Colimits and finite
limits are formed like in $\mathbf{Set}$; general limits are formed by taking
the limit in $\mathbf{Set}$ and restricting to finitely supported elements.
The category $\mathbf{Nom}_{\mathrm{of}}$ is closed under finite limits and
finite colimits in $\mathbf{Nom}$. _Quotients_ and _subobjects_ in
$\mathbf{Nom}$ are represented by surjective and injective equivariant maps.
Every equivariant map $f$ has an image factorization $f=m\cdot e$ with $m$
injective and $e$ surjective; we call $e$ the _coimage_ of $f$.

A nominal set is _strong_ if for all $x\in X$ and
$\pi\in\operatorname{Perm}\mathbb{A}$ one has $\pi\cdot x=x$ iff
$\pi\in\operatorname{Perm}_{S}\mathbb{A}$, where $S=\operatorname{supp}x$.
(Note that the “if” direction holds in every nominal set.) For example, the
nominal set $\mathbb{A}^{\\#n}=\\{f\colon n\rightarrow\mathbb{A}\mid\text{$f$
injective}\\}$ with pointwise action is strong and has a single orbit. Up to
isomorphism, (orbit-finite) strong nominal sets are precisely (finite)
coproducts of such sets.

##  3 Nominal Stone Spaces

In this section, we establish the topological foundations for our pro-orbit-
finite approach to data languages. We start by recalling the basic definitions
of nominal topology [17, 32].

######  Definition 1.

  1. 1.

A _nominal topology_ on a nominal set $X$ is an equivariant subset
$\mathcal{O}_{X}\subseteq\mathcal{P}_{\text{fs}}X$ closed under finitely
supported union (that is, if $\mathcal{U}\subseteq\mathcal{O}_{X}$ is finitely
supported then $\bigcup\mathcal{U}\in\mathcal{O}_{X}$) and finite
intersection. Sets $U\in\mathcal{O}_{X}$ are called _open_ and their
complements _closed_ ; sets that are both open and closed are _clopen_. A
nominal set $X$ together with a nominal topology $\mathcal{O}_{X}$ is a
_nominal topological space_. An equivariant map $f\colon X\rightarrow Y$
between nominal topological spaces is _continuous_ if for every open set $U$
of $Y$ its preimage $f^{-1}[U]$ is an open set of $X$. Nominal topological
spaces and continuous maps form the category $\mathbf{nTop}$.

  2. 2.

A _subbasis_ of a nominal topological space $(X,\mathcal{O}_{X})$ is an
equivariant subset $\mathcal{B}\subseteq\mathcal{O}_{X}$ such that every open
set of $X$ is a finitely supported union of finite intersections of sets in
$\mathcal{B}$. If additionally every finite intersection of sets in
$\mathcal{B}$ is a finitely supported union of sets in $\mathcal{B}$, then
$\mathcal{B}$ is called a _basis_. In this case, every open set of $X$ is a
finitely supported union of elements of $\mathcal{B}$.

######  Example 3.1.

  1. 1.

A topological space may be viewed as a nominal topological space equipped with
the trivial group action. Then every (open) subset has empty support and every
union is finitely supported, so we recover the axioms of classical topology.

  2. 2.

Every nominal set $X$ equipped with the _discrete topology_ , where all
finitely supported subsets are open, is a nominal topological space. It has a
basis given by all singleton sets.

  3. 3.

A _nominal(pseudo-)metric space_ is given by a nominal set $X$ with a
(pseudo-)metric111Recall that a pseudometric differs from a metric by not
requiring $d(x,y)\neq 0$ for $x\neq y$. $d\colon X\times
X\rightarrow\mathbb{R}$ which is equivariant as a function into the set
$\mathbb{R}$, regarded as a nominal set with the trivial group action. As
usual, the open ball around $x\in X$ with radius $r>0$ is given by
$B_{r}x=\\{y\in X\mid d(x,y)<r\\}$. Since $\pi\cdot B_{r}(x)=B_{r}(\pi\cdot
x)$ for all $\pi\in\operatorname{Perm}\mathbb{A}$ and $x\in X$, every nominal
(pseudo-)metric space carries a nominal topology whose basic opens are the
open balls.

######  Remark 2.

Every nominal topological space induces two families of ordinary topological
spaces, one by taking only opens with a certain support and the other by
forming orbits. In more detail, let $S\subseteq\mathbb{A}$ be a finite set of
names and let $X$ be a nominal topological space with topology $\mathcal{O}$.

  1. 1.

The underlying set of the nominal space $X$ carries a classical topology
$\mathcal{O}_{S}$ consisting of all $S$-supported open sets of $\mathcal{O}$.
We denote the resulting topological space by $|{X}|_{S}$.

  2. 2.

The set $\operatorname{orb}_{S}X$ of $S$-orbits can be equipped with the
quotient topology $\mathcal{O}_{\operatorname{orb}_{S}}$ induced by the
projection $X\twoheadrightarrow\operatorname{orb}_{S}X$ mapping each $x\in X$
to its $S$-orbit $\operatorname{orb}_{S}x$. In this topology, a set
$O\subseteq\operatorname{orb}_{S}X$ of $S$-orbits is open iff its union
$\bigcup O$ is open in $X$.

These constructions give rise to functors
$|{-}|_{S},\operatorname{orb}_{S}\colon\mathbf{nTop}\rightarrow\mathbf{Top}$.
They allow us to switch between nominal and classical topology.

As noted in 2.2, the Pro-completion of the category
$\mathbf{Set}_{\mathrm{f}}$ is the category of profinite spaces. One may
expect that the Pro-completion of $\mathbf{Nom}_{\mathrm{of}}$ analogously
consists of all _pro-orbit-finite_ spaces, that is, nominal topological spaces
that are codirected limits of orbit-finite discrete spaces. However, this
fails due to a simple fact: while codirected limits of non-empty finite sets
are always non-empty (which is a consequence of Tychonoff’s theorem, thus the
axiom of choice), codirected limits of non-empty orbit-finite nominal sets may
be empty.

######  Remark 3.

Similar to $\mathbf{Top}$, codirected limits in $\mathbf{nTop}$ are formed by
taking the limit in $\mathbf{Nom}$ equipping it with the initial topology.

######  Example 3.2.

Consider the $\omega^{\mathrm{op}}$-chain
$1\leftarrow\mathbb{A}\leftarrow\mathbb{A}^{\\#2}\leftarrow\mathbb{A}^{\\#3}\leftarrow\cdots$
in $\mathbf{Nom}_{\mathrm{of}}$ with connecting maps omitting the last
component. Its limit in $\mathbf{Set}$ (see 2.1) is given by
$\mathbb{A}^{\\#\omega}$, the set of all injective functions from $\omega$ to
$\mathbb{A}$. Clearly no such function has finite support, thus the limit in
$\mathbf{Nom}$ (and therefore also in $\mathbf{nTop}$) is empty.

This entails that it is in fact impossible to characterize
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}}$) by any sort of spaces. By
definition of the free completion
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})$, the inclusion functor
$I\colon\mathbf{Nom}_{\mathrm{of}}\hookrightarrow\mathbf{Nom}$ extends
uniquely to a functor
$\bar{I}\colon\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})\rightarrow\mathbf{Nom}$
preserving codirected limits. The analogous functor
$\bar{I}\colon\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}})\to\mathbf{Set}$ is
the forgetful functor of the category of profinite spaces. In contrast, we
have

######  Proposition 3.3.

The category $\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}}$) is _not_
concrete: the functor $\bar{I}$ is not faithful.

######  Proof 3.4.

Consider the chain
$1\leftarrow\mathbb{A}\leftarrow\mathbb{A}^{\\#2}\leftarrow\cdots$ of 3.2. Let
$D\colon\omega^{\mathrm{op}}\to\mathbf{Nom}_{\mathrm{of}}$ denote the
corresponding diagram, and let
$E\colon\mathbf{Nom}_{\mathrm{of}}\hookrightarrow\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})$
be the embedding. To prove that $\bar{I}$ is not faithful, we show that
$|{\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})(\lim
ED,E2)}|>|\mathbf{Nom}(\bar{I}(\lim ED),\bar{I}E2)|$, where $2$ is the two-
element nominal set. Indeed, we have

$\displaystyle\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})(\lim_{n<\omega}ED_{n},E2)$
$\displaystyle\cong\operatorname*{colim}_{n<\omega}\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})(ED_{n},E2)$
$E2$ finitely copresentable
$\displaystyle\cong\operatorname*{colim}_{n<\omega}\mathbf{Nom}_{\mathrm{of}}(D_{n},2)$
$\displaystyle E\text{ full embedding}$ $\displaystyle\cong 2$

because $\mathbf{Nom}_{\mathrm{of}}(D_{0},2)\cong 2$ and the two elements are
not merged by the colimit injection. However,

$\displaystyle\mathbf{Nom}(\bar{I}(\lim_{n<\omega}ED_{n}),\bar{I}E2)$
$\displaystyle\cong\mathbf{Nom}(\lim_{n<\omega}\bar{I}ED_{n},\bar{I}E2)$
$\bar{I}$ preserves codirected limits
$\displaystyle\cong\mathbf{Nom}(\lim_{n<\omega}ID_{n},2)$ $\displaystyle
I=\bar{I}E$ $\displaystyle\cong\mathbf{Nom}(\emptyset,2)$ $\displaystyle\cong
1.$

We thus restrict our focus to well-behaved subcategories of
$\mathbf{Nom}_{\mathrm{of}}$. We choose these subcategories in such way that
situations like in 3.2, where unrestricted accumulation of supports results in
empty codirected limits, are avoided.

######  Definition 4.

A nominal set $X$ is _$k$ -bounded_, for $k\in\mathbb{N}$, if
$|{\operatorname{supp}x}|\leq k$ for every $x\in X$.

For concrete categories $\mathbf{C}$ over $\mathbf{Nom}$ (or
$\mathbf{Nom}_{\mathrm{of}}$) we denote by $\mathbf{C}_{k}$ the full
subcategory of $\mathbf{C}$ whose underlying objects are $k$-bounded. For
instance, $\mathbf{Nom}_{k}$ is the category of $k$-bounded nominal sets, and
$\mathbf{nTop}_{k}$ is the category of $k$-bounded nominal topological spaces.

######  Remark 5.

  1. 1.

The full subcategories $\mathbf{Nom}_{k}\hookrightarrow\mathbf{Nom}$ and
$\mathbf{Nom}_{\mathrm{of},k}\hookrightarrow\mathbf{Nom}_{\mathrm{of}}$ are
coreflective [28, Section IV.3]: the coreflector (viz. the right adjoint of
the inclusion functor) sends a nominal set $X$ to its subset $X_{k}=\\{x\in
X\mid|{\operatorname{supp}x}|\leq k\\}$. Hence $\mathbf{Nom}_{k}$ is complete:
limits are formed by taking the limit in $\mathbf{Nom}$ and applying the
coreflector. Analogously, $\mathbf{Nom}_{\mathrm{of},k}$ is finitely complete.

  2. 2.

In contrast to $\mathbf{Nom}$, the category $\mathbf{Nom}_{k}$ generally fails
to be a topos because it is not cartesian closed. For instance, the functor
$\mathbb{A}^{\\#2}\times(-)$ on $\mathbf{Nom}_{2}$ does not preserve
coequalizers, hence it is not a left adjoint.

  3. 3.

The category $\mathbf{Nom}$ is known to be equivalent to the category of
pullback-preserving presheaves $\mathbb{I}\rightarrow\mathbf{Set}$, where
$\mathbb{I}$ is the category of finite sets and injective functions [36,
Theorem 6.8]. By inspecting the proof it is easy to see that this restricts to
an equivalence between $\mathbf{Nom}_{k}$ and the category of _$k$ -generated_
pullback-preserving presheaves $\mathbb{I}\rightarrow\mathbf{Set}$. Here a
presheaf $F\colon\mathbb{I}\rightarrow\mathbf{Set}$ is $k$-generated if for
every finite set $S$ and every $x\in FS$ there exists a set $S^{\prime}$ of
cardinality at most $k$ and an injective map $f\colon S^{\prime}\rightarrow S$
such that $x\in Ff[FS^{\prime}]$.

With regard to codirected limits, the restriction to bounded nominal sets
fixes the issue arising in 3.2:

######  Lemma 3.5.

Codirected limits in $\mathbf{Nom}_{k}$ are formed at the level of
$\mathbf{Set}$.

We proceed to give a topological characterization of
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k})$ in terms of nominal Stone
spaces, generalizing the corresponding result (1.1) for
$\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}})$. To this end, we introduce
suitable nominalizations of the three characteristic properties of Stone
spaces: compactness, Hausdorffness, and existence of a basis of clopens. The
nominal version of compactness comes natural and is compatible with the
functors $|{-}|_{S}$ and $\operatorname{orb}_{S}$ of 2.

######  Definition 6.

An _open cover_ of a nominal topological space $(X,\mathcal{O})$ is a finitely
supported set $\mathcal{C}\subseteq\mathcal{O}$ that covers $X$, i.e.
$\bigcup\mathcal{C}=X$. A _subcover_ of $\mathcal{C}$ is a finitely supported
subset of $\mathcal{C}$ that also covers $X$. A nominal topological space $X$
is _compact_ if every open cover $\mathcal{C}$ of $X$ has an orbit-finite
subcover: there exist $U_{1},\ldots,U_{n}\in\mathcal{C}$ such that
$X=\bigcup_{i=1}^{n}\bigcup\operatorname{orb}U_{i}$.

######  Lemma 3.6.

For every nominal topological space $X$ the following conditions are
equivalent:

  1. 1.

The space $X$ is compact.

  2. 2.

Every uniformly finitely supported open cover of $X$ has a finite subcover.

  3. 3.

For every finite set $S\subseteq\mathbb{A}$ the topological space $|{X}|_{S}$
is compact.

  4. 4.

For every finite set $S\subseteq\mathbb{A}$ the topological space
$\operatorname{orb}_{S}X$ is compact.

The Hausdorff property is more subtle: rather than just separation of points,
we require separation of $S$-orbits (“thick points”) by disjoint $S$-supported
open neighbourhoods.

######  Definition 7.

A nominal topological space $X$ is _(nominal) Hausdorff_ if for every finite
set $S\subseteq\mathbb{A}$ and every pair $x_{1},x_{2}\in X$ of points lying
in different $S$-orbits, there exist disjoint $S$-supported open sets
$U_{1},U_{2}\subseteq X$ such that $x_{i}\in U_{i}$ for $i=1,2$.

Note that the nominal Hausdorff condition is clearly equivalent to being able
to separate disjoint $S$-_orbits_ : If
$\operatorname{orb}_{S}x_{1}\neq\operatorname{orb}_{S}x_{2}$, then any two
disjoint open $S$-supported neighbourhoods $U_{1},U_{2}$ of $x_{1},x_{2}$
satisfy $\operatorname{orb}_{S}x_{i}\subseteq U_{i}$ for $i=1,2$. Note also
that $\operatorname{orb}_{S}x=\\{x\\}$ whenever $\operatorname{supp}x\subseteq
S$, hence the nominal Hausdorff condition implies the ordinary one. For
bounded nominal compact Hausdorff spaces, we have a codirected Tychonoff
theorem:

######  Proposition 3.7.

For every codirected diagram of non-empty $k$-bounded nominal compact
Hausdorff spaces, the limit in $\mathbf{nTop}$ is a non-empty $k$-bounded
nominal compact Hausdorff space.

Finally, having a basis of clopen sets is not sufficient in our setting. To
see this, note that in an ordinary topological space $X$ every clopen subset
$C\subseteq X$ can be represented as $C=f^{-1}[A]$ for some continuous map
$f\colon X\to Y$ into a finite discrete space $Y$ and some subset $A\subseteq
Y$. (In fact, one may always take $Y=2$ and $A=\\{1\\}$.) This is no longer
true in the nominal setting, see 9 below. Therefore, in lieu of clopens we
work with _representable_ subsets:

######  Definition 8.

A subset $R\subseteq X$ of a nominal space $X$ is _representable_ if there
exists a continuous map $f\colon X\rightarrow Y$ into an orbit-finite discrete
space $Y$ such that $R=f^{-1}[A]$ for some $A\in\mathcal{P}_{\text{fs}}Y$.

######  Remark 9.

  1. 1.

Every representable set is clopen, but the converse generally fails. To see
this, consider the discrete space $X=\coprod_{n<\omega}\mathbb{A}^{\\#n}$. We
show that for fixed $a\in\mathbb{A}$ the (clopen) subset $R=\\{x\mid
a\in\operatorname{supp}x\\}\subseteq X$ is not representable. Towards a
contradiction suppose that $R$ is represented by $f\colon X\rightarrow Y$ as
$R=f^{-1}[A]$ for some $A\in\mathcal{P}_{\text{fs}}Y$. Since $Y$ is orbit-
finite, we can choose $m$ large enough such that there exists some
$x\in\mathbb{A}^{\\#m}\setminus R\subseteq X$ for which
$\operatorname{supp}f(x)\subsetneq\operatorname{supp}x$. Choose a name
$b\in\operatorname{supp}x\setminus\operatorname{supp}f(x)$. Then
$a,b\not\in\operatorname{supp}f(x)$, and so we have

$f(({a}\,\,{b})\cdot x)=({a}\,\,{b})\cdot f(x)=f(x).$

Since $({a}\,\,{b})\cdot x\in R$, this shows $f(x)\in A$ and thus $x\in R$.
This contradicts the above choice of $x$.

  2. 2.

If a nominal space $X$ has a basis of representable sets, then we may assume
without loss of generality that the basic open sets are of the form
$f^{-1}[y]$ for some $f\colon X\rightarrow Y$ and $y\in Y$, where $Y$ is
orbit-finite and discrete. Indeed, if $R=f^{-1}[A]$ for
$A\in\mathcal{P}_{\text{fs}}Y$, then $R=\bigcup_{y\in A}f^{-1}[y]$. Moreover,
given representable sets $R_{i}=f_{i}^{-1}[y_{i}]$, $i=1,2$, the set
$R_{1}\cap R_{2}$ is equal to $\langle f_{1},f_{2}\rangle^{-1}(y_{1},y_{2})$
and therefore representable as well. Hence, to show that representable subsets
form a basis it suffices to check whether every open set is a finitely
supported union of subsets of the form $f^{-1}[y]$.

######  Definition 10.

A _nominal Stone space_ is a nominal compact Hausdorff space with a basis of
representables. We let $\mathbf{nStone}$ denote the full subcategory of
$\mathbf{nTop}$ given by nominal Stone spaces.

######  Remark 11.

Nominal Stone spaces as per 10 are conceptually very different from _nominal
Stone spaces with $\mathsf{N}$ _, introduced by Gabbay et al. [17] as the dual
of _nominal boolean algebras with $\mathsf{N}$ _. The latter are equipped with
a _restriction operator_ $\mathrm{\mathbf{n}}$ tightly related to the
freshness quantifier  $\mathsf{N}$ of nominal sets, which enables a nominal
version of the ultrafilter theorem and thus a represention of boolean algebras
with  $\mathsf{N}$ via spaces of ultrafilters. In nominal Stone spaces with
$\mathsf{N}$ , the Hausdorff property is implicit (but would be analogous to
that in standard topology), the basis is given by clopen rather than
representable sets, and the notion of compactness (called
_$\mathrm{\mathbf{n}}$ -compactness_) considers open covers closed under the
operator $\mathrm{\mathbf{n}}$, which are required to have a _finite_
subcover. By this definition, the orbit-finite discrete space $\mathbb{A}$
fails to be compact (the $\mathrm{\mathbf{n}}$-cover $\\{\\{a\\}\mid
a\in\mathbb{A}\\}\cup\\{\emptyset\\}$ has no finite subcover). Hence, given
that algebraic recognition is based on orbit-finite sets, nominal Stone spaces
with  $\mathsf{N}$ are not suitable for a topological interpretion of data
languages.

######  Example 3.8.

Every orbit-finite nominal set can be viewed as a nominal Stone space equipped
with the discrete topology. We thus regard $\mathbf{Nom}_{\mathrm{of}}$ as a
full subcategory of $\mathbf{nStone}$. Nontrivial examples of nominal Stone
spaces are given by the spaces of pro-orbit-finite words introduced later.

Within the class of nominal Stone spaces, representable and clopen subsets
coincide:

######  Lemma 3.9.

If $X$ is a nominal Stone space, then every clopen set $C\subseteq X$ is
representable.

The following theorem is the key result leading to our topological approach to
data languages.

######  Theorem 3.10.

For each $k\in\mathbb{N}$, the category of $k$-bounded nominal Stone spaces is
the Pro-completion of the category of $k$-bounded orbit-finite nominal sets:

$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k})=\mathbf{nStone}_{k}.$

Moreover, $k$-bounded nominal Stone spaces are precisely the nominal
topological spaces arising as codirected limits of $k$-bounded orbit-finite
discrete spaces.

For $k=0$, we recover the corresponding characterization of classical Stone
spaces.

##  4 Nominal Stone Duality

Next, we give a dual characterization of (bounded) nominal Stone spaces. It
builds on the known duality between nominal sets and complete atomic nominal
boolean algebras due to Petrişan [32].

######  Definition 12.

A _nominal boolean algebra_ is a nominal set equipped with the structure of a
boolean algebra such that all operations are equivariant. It is _(orbit-
finitely) complete_ if every (orbit-finite) finitely supported subset has a
supremum. A _subalgebra_ of an (orbit-finitely) complete nominal boolean
algebra is an equivariant subset closed under boolean operations and the
respective suprema. Let $\mathbf{nC_{\mathrm{of}}BA}$ and $\mathbf{nCBA}$
denote the categories of (orbit-finitely) complete nominal boolean algebras;
their morphisms are equivariant homomorphisms preserving (orbit-finite)
suprema.

######  Definition 13.

An element $x\in B$ of a nominal boolean algebra is an _atom_ if $x\neq\bot$
and $y<x$ implies $y=\bot$. The (equivariant) set of atoms of $B$ is denoted
$\operatorname{At}B$. The algebra $B$ is _atomic_ if every element is the
supremum of all atoms below it; if additionally
$\operatorname{At}B\in\mathbf{Nom}_{\mathrm{of},k}$ we call it _$k$ -atomic_.
If $A\subseteq B$ is a $k$-atomic subalgebra we write
$A\leq_{\mathrm{of},{k}}B$. An algebra $B\in\mathbf{nCBA}$ is called _locally
$k$-atomic_ if every element of $B$ is contained in some
$A\leq_{\mathrm{of},{k}}B$. We denote by
$\mathbf{nCA_{\mathit{k}}BA}\subseteq\mathbf{nCBA}$ the full subcategory of
all $k$-atomic complete nominal boolean algebras, and
$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\subseteq\mathbf{nC_{\mathrm{of}}BA}$
denotes the full subcategory of all locally $k$-atomic orbit-finitely complete
nominal boolean algebras.

######  Remark 14.

  1. 1.

Orbit-finite completeness is equivalent to the weaker condition that suprema
of $S$-orbits exist for all finite subsets $S\subseteq\mathbb{A}$. In fact,
every $S$-supported orbit-finite subset $X\subseteq B$ is a finite union
$X=\bigcup_{i=1}^{n}\operatorname{orb}_{S}x_{i}$ of $S$-orbits, whence
$\bigvee X=\bigvee_{i=1}^{n}\bigvee\operatorname{orb}_{S}x_{i}$.

  2. 2.

Every $k$-atomic orbit-finitely complete nominal boolean algebra is complete:
For every finitely supported subset $X\subseteq B$ we have $\bigvee
X=\bigvee\\{b\in\operatorname{At}(B)\mid\exists(x\in X).\ b\leq x\\}$, which
is a supremum of an orbit-finite subset.

######  Theorem 4.1.

For each $k\in\mathbb{N}$, the category of locally $k$-atomic orbit-finitely
complete nominal boolean algebras is the Ind-completion of the category of
$k$-atomic complete nominal boolean algebras:

$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\simeq\operatorname{Ind}(\mathbf{nCA_{\mathit{k}}BA}).$

######  Theorem 4.2 (Nominal Stone Duality).

For each $k\in\mathbb{N}$, the category of locally $k$-atomic orbit-finitely
complete nominal boolean algebras is dual to the category of $k$-bounded
nominal Stone spaces:

$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\simeq^{\mathrm{op}}\mathbf{nStone}_{k}.$

######  Proof 4.3.

The category $\mathbf{Nom}$ of nominal sets is dually equivalent to the
category $\mathbf{nCABA}$ of complete atomic nominal boolean algebras [32].
The duality sends a nominal set $X$ to the boolean algebra
$\mathcal{P}_{\text{fs}}X$, equippped with the set-theoretic boolean
structure. Conversely, a complete atomic nominal boolean algebra $B$ is mapped
to the nominal set $\operatorname{At}(B)$ of its atoms, and an
$\mathbf{nCABA}$-morphism $h\colon C\rightarrow B$ to the equivariant map
$\operatorname{At}(B)\rightarrow\operatorname{At}(C)$ sending
$b\in\operatorname{At}(B)$ to the unique $c\in\operatorname{At}(C)$ such that
$c\leq h(b)$. For every $k\in\mathbb{N}$ the duality clearly restricts to one
between $k$-bounded orbit-finite nominal sets and $k$-atomic complete nominal
boolean algebras. Thus Theorem 4.1 and Theorem 3.10 yield

$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\simeq\operatorname{Ind}(\mathbf{nCA_{\mathit{k}}BA})\simeq^{\mathrm{op}}\operatorname{Pro}(\mathbf{nCA_{\mathit{k}}BA}^{\mathrm{op}})\simeq\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k})\simeq\mathbf{nStone}_{k}.$

######  Remark 15.

We give an explicit description of the dual equivalence of Theorem 4.2.

  1. 1.

In the direction
$\mathbf{nStone}_{k}\rightarrow\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}$
it maps a $k$-bounded nominal Stone space $X$ to the nominal boolean algebra
$\operatorname{Clo}(X)$ of clopens (or representables, see 3.9). A continuous
map $f\colon X\rightarrow Y$ is mapped to the homomorphism
$f^{-1}\colon\operatorname{Clo}(Y)\rightarrow\operatorname{Clo}(X)$ taking
preimages.

  2. 2.

The direction
$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}\rightarrow\mathbf{nStone}_{k}$
requires some terminology. A finitely supported subset $F\subseteq B$ of an
algebra $B\in\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}$ is a
_nominal orbit-finitely complete prime filter_ if (i) $F\neq\emptyset$, (ii)
$F$ is upwards closed ($x\in F\land x\leq y\Rightarrow y\in F$), (iii) $F$ is
downwards directed ($x,y\in F\Rightarrow x\land y\in F$), and (iv) for every
finitely supported $k$-bounded orbit-finite subset $X\subseteq B$ such that
$\bigvee X\in F$, one has $X\cap F\neq\emptyset$. The equivalence now maps
$B\in\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}$ to the space
$\operatorname{\mathcal{F}_{np}}(B)$ of nominal orbit-finitely complete prime
filters of $B$, whose topology is generated by the basic open sets
$\\{F\in\operatorname{\mathcal{F}_{np}}(B)\mid b\in F\\}$ for $b\in B$. A
morphism $h\colon B\rightarrow C$ of
$\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}$ is mapped to the
continuous map
$h^{-1}\colon\operatorname{\mathcal{F}_{np}}(C)\rightarrow\operatorname{\mathcal{F}_{np}}(B)$
taking preimages.

In Theorem 4.2 we made the support bound $k$ explicit, but we can also leave
it implicit. A nominal Stone space is _bounded_ if it lies in
$\mathbf{nStone}_{k}$ for some natural number $k$; similarly, a _locally
bounded atomic orbit-finitely complete nominal boolean algebras_ is an element
of $\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}$ for some $k$.

######  Corollary 4.4.

The category of locally bounded atomic orbit-finitely complete nominal boolean
algebras is dual to the category of bounded nominal Stone spaces.

######  Remark 16.

For $k=0$ we recover the classical Stone duality between boolean algebras and
Stone spaces. Indeed, $0$-bounded nominal Stone spaces are precisely Stone
spaces, and locally $0$-atomic orbit-finitely complete nominal boolean
algebras are precisely boolean algebras

##  5 Pro-Orbit-Finite Words

In this section, we generalize the topological characterization of regular
languages to data languages recognizable by orbit-finite nominal monoids [7,
13, 10].

######  Definition 17.

A _nominal monoid_ $M$ is a monoid object in $\mathbf{Nom}$, that is, it is
given by nominal set $M$ equipped with an equivariant associative
multiplication $M\times M\rightarrow M$ and an equivariant unit $1\in M$.
Nominal monoids and equivariant monoid homomorphisms form a category
$\mathbf{nMon}$.

As for ordinary monoids, the _free monoid_ generated by
$\Sigma\in\mathbf{Nom}$ is the nominal set $\Sigma^{*}$ of finite words (with
pointwise group action); its multipliation is concatenation and its unit the
empty word.

######  Remark 18.

We emphasize the difference between $k$-bounded nominal monoids – nominal
monoids whose carrier is $k$-bounded – and monoid objects in
$\mathbf{Nom}_{k}$, which are partial nominal monoids where the product
$x\cdot y$ is defined iff
$|{\operatorname{supp}x}\cup\operatorname{supp}y|\leq k$.

######  Definition 19.

A _data language_ over $\Sigma\in\mathbf{Nom}_{\mathrm{of}}$ is a finitely
supported subset $L\subseteq\Sigma^{*}$. It is _recognizable_ if there exists
an equivariant monoid morphism $h\colon{\Sigma}^{*}\rightarrow M$ with $M$
orbit-finite and a finitely supported subset $P\subseteq M$ such that
$L=h^{-1}[P]$. In this case, we say that the morphism _$h$ recognizes $L$_.

For example, the equivariant language $L_{0}$ from the Introduction is
recognizable, while the language $L_{1}$ is not recognizable.

######  Remark 20.

  1. 1.

The morphism $h$ can be taken to be surjective; otherwise, take its coimage.

  2. 2.

Via characteristic functions, data languages correspond precisely to finitely
supported maps $L\colon{\Sigma}^{*}\rightarrow 2$, where $2$ is the two-
element nominal set. Recognizablity then states that $L$ factorizes through
some equivariant monoid morphism with orbit-finite codomain.

Recall from section 2 that the Stone space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
of profinite words over a finite alphabet $\Sigma$ is constructed as the limit
in $\mathbf{Stone}\simeq\operatorname{Pro}(\mathbf{Set}_{\mathrm{f}})$ of all
finite quotient monoids of $\Sigma^{*}$. The obvious generalization to a
_nominal_ alphabet $\Sigma\in\mathbf{Nom}_{\mathrm{of}}$, which constructs the
limit of all orbit-finite quotient monoids in
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of}})$, is unlikely to yield a
useful object since this category is not concrete (3.3); in fact, it is futile
from a language-theoretic perspective, cf. 28. Instead, our results of section
3 suggest to restrict the diagram scheme to
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}}{\mathbf{nMon}_{\mathrm{of},k}}$,
the poset of $k$-bounded orbit-finite quotient monoids (where $e\leq
e^{\prime}$ iff $e^{\prime}$ factorizes through $e$), and take the limit in
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k})=\mathbf{nStone}_{k}$.
However, this diagram is not codirected (37), so its limit may not be a
nominal Stone space. We again focus on well-behaved (i.e., codirected),
subcategories by introducing _support bounds_.

######  Definition 21.

A _support bound_ is a map
$s\colon{\Sigma}^{*}\rightarrow\mathcal{P}\mathbb{A}$ such that
$s[{\Sigma}^{*}]\subseteq\mathcal{P}_{k}\mathbb{A}$ for some $k\in\mathbb{N}$,
where $\mathcal{P}_{k}\mathbb{A}=\\{S\subseteq\mathbb{A}\mid|S|\leq k\\}$. We
usually identify $s$ with its codomain restrictions to
$\mathcal{P}_{k}\mathbb{A}$ for sufficiently large $k$. A morphism
$h\colon{\Sigma}^{*}\rightarrow M$ of nominal monoids is _$s$ -bounded_ if
$\operatorname{supp}h(w)\subseteq s(w)$ for all $w\in{\Sigma}^{*}$; we write
$h\colon{\Sigma}^{*}\rightarrow_{s}M$. We denote by
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$
the subposet of
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}}{\mathbf{nMon}_{\mathrm{of},k}}$
given by $s$-bounded quotient monoids.

######  Lemma 5.1.

For every support bound $s$, the poset
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$
is codirected.

######  Proof 5.2.

Let $h\colon{\Sigma}^{*}\rightarrow_{s}M_{h}$ and
$h^{\prime}\colon{\Sigma}^{*}\rightarrow_{s}M_{h^{\prime}}$ be two $s$-bounded
quotients in
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$.
Form the coimage $k\colon{\Sigma}^{*}\twoheadrightarrow M$ of their pairing
$\langle h,h^{\prime}\rangle\colon\Sigma^{*}\to M_{h}\times M_{h^{\prime}}$.
Then for all $w\in{\Sigma}^{*}$

$\operatorname{supp}k(w)=\operatorname{supp}(h(w),h^{\prime}(w))=\operatorname{supp}h(w)\cup\operatorname{supp}h^{\prime}(w)\subseteq
s(w).$

Hence, $k$ is a lower bound for $h,h^{\prime}$ in the poset
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$.

######  Definition 22.

For an orbit-finite nominal set $\Sigma$ and a support bound
$s\colon{\Sigma}^{*}\rightarrow\mathcal{P}_{k}\mathbb{A}$ we define the
nominal Stone space
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
to be the limit of the codirected diagram

$D\colon{{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}\to\mathbf{nStone}_{k},\qquad(e\colon{\Sigma}^{*}\twoheadrightarrow_{s}M)\;\mapsto\;|M|,$

where $|M|$ is the nominal set underlying $M$, regarded as a discrete nominal
topological space. The elements of
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
are called the _( $s$-bounded) pro-orbit-finite words over $\Sigma$_. We
denote by
$\hat{e}\colon\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\to
M$ the limit projection associated to
$e\colon{\Sigma}^{*}\twoheadrightarrow_{s}M$ in
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$.

######  Remark 23.

  1. 1.

One may equivalently define
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
as the limit of the larger cofiltered diagram $D^{\prime}$ given by

$D^{\prime}\colon{{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}\to\mathbf{nStone}_{k},\qquad(e\colon{\Sigma}^{*}\to_{s}M)\;\mapsto\;|M|,$

where ${{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$
is the category of all equivariant $s$-bounded monoid morphisms
$h\colon{\Sigma}^{*}\to_{s}M$ with $k$-bounded orbit-finite codomain; a
morphism from $h$ to $h^{\prime}\colon{\Sigma}^{*}\to_{s}M^{\prime}$ is an
equivariant monoid morphism $k\colon M\to M^{\prime}$ such that
$h^{\prime}=k\cdot h$. In fact, the inclusion
${{\Sigma}^{*}}\mathord{\mathbin{\rotatebox[origin={c}]{-90.0}{$\twoheadrightarrow$}}_{s}}{\mathbf{nMon}_{\mathrm{of},k}}\hookrightarrow{{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$
is an initial functor, hence the limits of $D$ and $D^{\prime}$ coincide.
Since the limit of $D^{\prime}$ is formed as in $\mathbf{Set}$ (3.5), the
space
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
is carried by the nominal set of compatible families $(x_{h})_{h}$ of
$D^{\prime}$, and the limit projection $\hat{h}$ associated to
$h\colon\Sigma^{*}\to_{s}M$ is given by $(x_{h})_{h}\mapsto x_{h}$.

  2. 2.

The forgetful functor $V\colon\mathbf{nStone}_{k}\rightarrow\mathbf{Nom}_{k}$
and the inclusion $I\colon\mathbf{Nom}_{k}\rightarrow\mathbf{Nom}$ both
preserve codirected limits. The morphisms
${{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$ viewed
as equivariant functions form a cone for the diagram $IVD^{\prime}$, so there
exists a unique equivariant map $\eta\colon{\Sigma}^{*}\rightarrow
IV\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
such that

$h=\big{(}\leavevmode\hbox to107.64pt{\vbox
to14.33pt{\pgfpicture\makeatletter\hbox{\hskip 53.82082pt\lower-7.77065pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-56.82082pt}{-7.6708pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
8.01111pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.01111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\Sigma}^{*}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.01111pt\hfil&\hfil\hskip 34.62917pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.62917pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${IV\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
14.62917pt\hfil&\hfil\hskip 34.18056pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.18056pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${IV\\!M}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
14.18056pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{2.79985pt,1.59991pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-40.5986pt}{-5.1708pt}\pgfsys@lineto{-21.39856pt}{-5.1708pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.19858pt}{-5.1708pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-32.53645pt}{-1.45695pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{\eta}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{8.65973pt}{-5.1708pt}\pgfsys@lineto{27.85977pt}{-5.1708pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.05975pt}{-5.1708pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.04932pt}{-2.81804pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{IV\hat{h}}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\big{)}\qquad\text{for
all
$h\in{{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$}.$

In more explicit terms, the map $\eta$ is given by $\eta(w)=(h(w))_{h}$ for
$w\in\Sigma^{*}$. For simplicity we omit $I$ and $V$ and write
$\eta\colon{\Sigma}^{*}\rightarrow\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
The image of $\eta$ forms a dense subset of
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
We note that $\eta$ is generally not injective since we restrict a subdiagram
${{\Sigma}^{*}}\mathord{\downarrow_{s}}{\mathbf{nMon}_{\mathrm{of},k}}$ of the
diagram ${{\Sigma}^{*}}\mathord{\downarrow}{\mathbf{nMon}_{\mathrm{of}}}$,

  3. 3.

The space
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
is a nominal monoid with product $\hat{h}(x\cdot y)=\hat{h}(x)\cdot\hat{h}(y)$
and unit $\eta(\varepsilon)$, with $\varepsilon$ the empty word. Since the
multiplication is readily seen to be continuous,
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
can be regarded as an object of $\mathbf{Mon}(\mathbf{nStone})$, the category
of nominal Stone spaces equipped with a continuous monoid structure and
continuous equivariant monoid morphisms.

Now recall from section 2 that the space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
can be constructed as the metric completion of $\Sigma^{*}$, where the metric
measures the size of separating monoids. We now investigate to what extent the
metric approach applies to the nominal setting, using nominal
(pseudo-)metrics; see 3.1.

######  Definition 24.

Let $s$ be a support bound on ${\Sigma}^{*}$. We say that a nominal monoid $M$
_$s$ -separates_ $v,w\in\Sigma^{*}$ if there exists an $s$-bounded equivariant
monoid morphism $h\colon\Sigma^{*}\to_{s}M$ such that $h(v)\neq h(w)$. We
define a nominal pseudometric $d_{s}$ on ${\Sigma}^{*}$ by setting

$d_{s}(v,w)=\sup\\{\,2^{-|\operatorname{orb}M|}\mid\text{the orbit-finite
nominal monoid $M$ $s$-separates $v,w$}\,\\}.$

We let ${\Sigma}^{*}/d_{s}$ denote the corresponding nominal metric space,
obtained as a quotient space of the pseudometric space $({\Sigma}^{*},d_{s})$
by identifying $v,w$ if $d_{s}(v,w)=0$.

######  Remark 25.

In contrast to the classical case, $d_{s}$ is generally not a metric: there
may exist words $v\neq w$ which are not $s$-separated by any orbit-finite
nominal monoids. For example, if $\Sigma=\mathbb{A}$ and $s(a_{1}\cdots
a_{n})=a_{1}$ for $a_{1},\ldots,a_{n}\in\Sigma$, then for every $s$-bounded
$h$ and distinct names $a,b,c\in\mathbb{A}$ we have $h(ab)=h(({b}\,\,{c})\cdot
ac)=({b}\,\,{c})\cdot h(ac)=h(ac)$ since $b,c\not\in
s(ac)\supseteq\operatorname{supp}h(ac)$. Therefore, the additional metrization
process is required.

For the next lemma we need some terminology. A nominal metric space is
_complete_ if every finitely supported Cauchy sequence has a limit. A nominal
topological space is _completely metrizable_ if its topology is induced by a
complete metric. A subset $D\subseteq X$ of a nominal metric space is
_(topologically) dense_ if every open neighbourhood of a point $x\in X$
contains an element of $D$.

######  Remark 26.

In contrast to classical metric spaces, density is not equivalent to
_sequential density_ (every point $x\in X$ is a limit of a finitely supported
sequence in $D$). To see this, consider the space $\mathbb{A}^{\omega}$ of
finitely supported infinite words with the prefix metric, that is,
$d(v,w)=2^{-n}$ if $n$ is the length of the longest common prefix of $v,w$.
Let $D\subseteq X$ be the equivariant subset given by

$D=\\{\,x\in\mathbb{A}^{\omega}\mid|{\operatorname{supp}x}|\geq 2\text{ and
}|{\operatorname{supp}x}|\geq|\mathrm{initialblock}(x)|\,\\},$

where $\mathrm{initialblock}(x)$ is the longest prefix of $x$ of the form
$a^{n}$ ($a\in\mathbb{A}$). The set $D$ is dense, but not sequentially dense:
$a^{\omega}\in\mathbb{A}^{\omega}$ is not the limit of any finitely supported
sequence in $D$.

######  Lemma 5.3.

  1. 1.

The space
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
is completely metrizable via the complete nominal metric

$\hat{d}_{s}(x,y)=\sup\\{\,2^{-|{\operatorname{orb}M}|}\mid\exists(h\colon{\Sigma}^{*}\rightarrow_{s}M)\colon\hat{h}(x)\neq\hat{h}(y)\,\\}.$
(5.1)

  2. 2.

The canonical map $\eta$ (23) yields a dense isometry
$\eta\colon({\Sigma}^{*},d_{s})\to(\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s},\hat{d}_{s})$.

######  Remark 27.

In classical topology, it would now be clear that
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
is the metric completion of the metric space ${\Sigma}^{*}/d_{s}$, i.e. it
satisfies the universal property that every uniformly continuous map from
${\Sigma}^{*}/d_{s}$ to a complete metric space has a unique uniformly
continuous extension to
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
However, this rests on the coincidence of topological and sequential density,
which fails over nominal sets as seen in 26. We therefore conjecture that
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
is not the nominal metric completion of ${\Sigma}^{*}/d_{s}$.

By using support bounds, we obtain a topological perspective on recognizable
data languages. Let $\operatorname{Rec}_{s}{\Sigma}$ denote the set of data
languages recognized by $s$-bounded equivariant monoid morphisms.

######  Theorem 5.4.

For every support bound
$s\colon{\Sigma}^{*}\rightarrow\mathcal{P}_{k}\mathbb{A}$, the $k$-bounded
nominal Stone space
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
of $s$-bounded pro-orbit-finite words is dual to the locally $k$-atomic orbit-
finitely complete boolean algebra $\operatorname{Rec}_{s}({\Sigma}^{*})$ of
$s$-recognizable languages. In particular, we have the isomorphism

$\operatorname{Rec}_{s}({\Sigma}^{*})\;\cong\;\operatorname{Clo}(\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s})\qquad\text{
in }\qquad\mathbf{nC_{\mathrm{of}}A_{\mathrm{l}\mathit{k}}BA}.$

######  Proof 5.5 (Proof (Sketch)).

The isomorphism is illustrated by the two diagrams below:

${\mathllap{L\phantom{])}}=h^{-1}[P]}$${{\Sigma}^{*}}$${M}$${P}$${\mathllap{\overline{\eta[L]}}=\hat{h}^{-1}[P]}$${\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}}$${\subseteq}$$\scriptstyle{h}$$\scriptstyle{\eta}$${\supseteq}$${\subseteq}$$\scriptstyle{\hat{h}}$
${\mathllap{\eta^{-1}[C]}=h^{-1}[P]}$${{\Sigma}^{*}}$${M}$${P\mathrlap{=p^{-1}[U]}}$${\mathllap{C\phantom{]}}=f^{-1}[U]}$${\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}}$${Y}$${U}$${\subseteq}$$\scriptstyle{h}$$\scriptstyle{\eta}$$\scriptstyle{\exists
p}$${\supseteq}$${\subseteq}$$\scriptstyle{\hat{h}}$$\scriptstyle{f}$${\supseteq}$

In more detail, if $L\subseteq\Sigma^{*}$ is $s$-recognizable, say
$L=h^{-1}[P]$ for an $s$-bounded morphism $h$, then its corresponding clopen
is the topological closure $\overline{\eta[L]}=\hat{h}^{-1}[P]$ represented by
the continuous extension $\hat{h}$. Conversely, every clopen
$C\subseteq\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
restricts to an $s$-recognizable language $\eta^{-1}[C]\subseteq{\Sigma}^{*}$.
We get $s$-recognizability of $\eta^{-1}[C]$ by factorizing a representation
$f\colon\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\to
Y$ of $C$ through a limit projection $\hat{h}$ as $f=p\cdot\hat{h}$, using
that $Y$ is finitely copresentable. Thus $h$ recognizes $\eta^{-1}[C]$.

######  Remark 28.

In the proof of Theorem 5.4, finite copresentability of orbit-finite sets is
crucial to recover recognizable languages from representable subsets,
highlighting the importance of working in the Pro-completion
$\operatorname{Pro}(\mathbf{Nom}_{\mathrm{of},k})=\mathbf{nStone}_{k}$. In a
naive approach one might instead want to consider the limit of the diagram
$D\colon{{\Sigma}^{*}}\mathord{\downarrow}{\mathbf{nMon}_{\mathrm{of}}}\to\mathbf{nTop}$
of _all_ equivariant morphisms from ${\Sigma}^{*}$ to orbit-finite monoids.
The resulting space
$\mathrlap{\widehat{\scalebox{1.0}[1.0]{\phantom{$\Sigma^{*}$}}}}\Sigma^{*}$
is still a nominal Hausdorff space with a basis of representables, but it
generally fails to be compact, and its representable subsets do not correspond
to recognizable data languages. To see this, consider the space
$\widehat{\mathbb{A}^{*}}$ and the orbit-finite nominal monoids
$\mathbb{A}^{\leq n}$ (words of length at most $n$) with multiplication
cutting off after $n$ letters. We denote by
$h_{n}\colon\mathbb{A}^{*}\rightarrow\mathbb{A}^{\leq n}$ and
$p_{k,n}\colon\mathbb{A}^{\leq k}\twoheadrightarrow\mathbb{A}^{\leq n}$,
$n\leq k$, the equivariant monoid morphisms given by projection to the first
$n$ letters. For every compatible family
$x=(x_{h})\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{$\mathbb{A}^{*}$}}}}\mathbb{A}^{*}$
its subfamily $(x_{h_{n}})_{n\in\mathbb{N}}$ corresponds to a (possibly
infinite) word over $\mathbb{A}$ with finite support. Hence there exists a
largest natural number $N=N(x)$ such that $|\operatorname{supp}x_{h_{N}}|=N$.
The subsets
$C_{n}=\\{x\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{$\mathbb{A}^{*}$}}}}\mathbb{A}^{*}\mid
N(x)=n\\}$, $n\in\mathbb{N}$, are equivariant clopens since
$C_{n}=\hat{h}_{n}^{-1}[\mathbb{A}^{\\#n}]\cap\hat{h}_{n+1}^{-1}[\mathbb{A}^{\leq
n+1}\setminus\mathbb{A}^{\\#(n+1)}]$. Thus each $C_{n}$ is representable (by a
continuous map into the two-element discrete space), non-empty (since
$\eta(w)=(h(w))_{h}\in C_{n}$ for every word
$w\in\mathbb{A}^{\\#n}\subseteq{\mathbb{A}}^{*}$ of pairwise distinct
letters), and pairwise disjoint. Hence they form a cover of
$\widehat{\mathbb{A}^{*}}$ that admits no orbit-finite (equivalently, finite)
subcover, showing that $\widehat{\mathbb{A}^{*}}$ is not compact. Moreover,
the sets $C_{M}=\bigcup_{m\in M}C_{m}$, where $M\subseteq\mathbb{N}$, are
equivariant clopens (hence representable) and pairwise distinct. Thus
$\widehat{\mathbb{A}^{*}}$ has uncountably many clopens. On the other hand,
there exist only countably many recognizable languages over $\mathbb{A}$
(using that, up to isomorphism, there exist only countably many orbit-finite
sets [36, Thm. 5.13] and thus countably many orbit-finite nominal monoids),
showing that there is no bijective correspondence between representable sets
in $\widehat{\mathbb{A}^{*}}$ and recognizable data languages over
$\mathbb{A}$.

##  6 A Nominal Reiterman Theorem

As an application of pro-orbit-finite methods, we present a nominal extension
of Reiterman’s classical pseudovariety theorem [37]. The latter characterizes
classes of finite algebras presentable by profinite equations as precisely
those closed under finite products, subalgebras, and homomorphic images. This
result has been generalized to first-order structures [34] and, recently, to
abstract categories [1, 30]. A key insight for the categorical perspective is
that equations should be formed over projective objects. (Recall that an
object $X$ in a category is projective w.r.t. a class $\mathcal{E}$ of
morphisms if for all cospans
$\cramped[\textstyle]{X\xrightarrow{f}Y\overset{e}{\leftarrow}Z}$ with
$e\in\mathcal{E}$ there exists a factorization of $f$ through $e$.) In
$\mathbf{Nom}$, one takes strong nominal sets, which are projective with
respect to support-reflecting quotients (see 29.2). For spaces of pro-orbit-
finite words we have the support bound as an additional constraint, which
makes the situation more complex: In a cospan
$\cramped{\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\xrightarrow{\hat{h}}N\overset{e}{\twoheadleftarrow}M}$
with $e$ support-reflecting, no $s$-bounded factorization of $\hat{h}$ through
$e$ may exist (section A). Surprisingly, there nonetheless exists a suitable
type of quotients for nominal monoids, called _MSR quotients_ , which is
_independent_ of the support bound $s$.

######  Definition 29.

A surjective equivariant morphism $e\colon M\twoheadrightarrow N$ of nominal
monoids is

  1. 1.

_support-preserving_ if $\operatorname{supp}e(x)=\operatorname{supp}x$ for
every $x\in X$;

  2. 2.

_support-reflecting_ if for every $y\in Y$ there exists $x\in e^{-1}[y]$ such
that $\operatorname{supp}x=\operatorname{supp}y$;

  3. 3.

_multiplicatively support-reflecting_ (_MSR_ for short) if there exists a
nominal submonoid $M^{\prime}\subseteq M$ such that the domain restriction
$e|_{M^{\prime}}\colon M^{\prime}\to N$ of $e$ is surjective and support-
preserving.

######  Remark 30.

Note that a surjective morphism $e$ is support-reflecting iff it restricts to
a support-preserving surjection $e|_{M^{\prime}}$ for some equivariant subset
$M^{\prime}\subseteq M$. For MSR morphisms one additionally requires that
$M^{\prime}$ may be chosen to form a submonoid. We thus have

$\text{support-preserving}\quad\Longrightarrow\quad\text{multiplicatively
support-reflecting}\quad\Longrightarrow\quad\text{support-reflecting}.$

None of the two converses holds in general; for the first one consider the
morphism $\mathbb{A}^{*}\twoheadrightarrow 1$ into the trivial monoid, and for
the second one see 6.5.

######  Proposition 6.1.

A surjective equivariant morphism $e\colon M\twoheadrightarrow N$ between
orbit-finite nominal monoids is MSR iff all the monoids
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
(where $\Sigma\in\mathbf{Nom}_{\mathrm{of}}$ is strong and
$s\colon\Sigma^{*}\to\mathcal{P}\mathbb{A}$ is a support bound) are projective
with respect to $e$ in $\mathbf{Mon}(\mathbf{nStone})$, with $M$ and $N$
regarded as discrete spaces.

######  Definition 31.

An _MSR-pseudovariety of nominal monoids_ is a class
$\mathcal{V}\subseteq\mathbf{nMon}_{\mathrm{of}}$ of orbit-finite nominal
monoids closed under

  1. 1.

finite products: if $M_{1},\ldots,M_{n}\in\mathcal{V}$, $n\in\mathbb{N}$, then
$M_{1}\times\cdots\times M_{n}\in\mathcal{V}$;

  2. 2.

submonoids: if $M\in\mathcal{V}$ and $N\subseteq M$ is a nominal submonoid,
then $N\in\mathcal{V}$:

  3. 3.

MSR quotients: if $M\in\mathcal{V}$ and $e\colon M\twoheadrightarrow N$ is an
MSR quotient, then $N\in\mathcal{V}$.

######  Definition 32.

Let $s\colon\Sigma^{*}\rightarrow\mathcal{P}\mathbb{A}$ be a support bound. A
_morphic pro-orbit-finite equation_ , or _morphic proequation_ for short, is a
surjective $\mathbf{nStone}$-morphism
$\varphi\colon\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\twoheadrightarrow
E$. An orbit-finite monoid $M$ _satisfies_ $\varphi$ if for every $s$-bounded
morphism $h\colon\Sigma^{*}\to M$, the limit projection
$\hat{h}\colon\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\rightarrow
M$ factorizes through $\varphi$ in $\mathbf{nStone}_{k}$, for some
$k\in\mathbb{N}$ such that $M\in\mathbf{Nom}_{\mathrm{of},k}$ and $s$
corestricts to $\mathcal{P}_{k}\mathbb{A}$:

$\hat{h}=\big{(}\leavevmode\hbox to80.77pt{\vbox
to12.44pt{\pgfpicture\makeatletter\hbox{\hskip 40.38608pt\lower-7.77074pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-43.38608pt}{-7.6708pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
8.01111pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.01111pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{${\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
8.01111pt\hfil&\hfil\hskip 26.97916pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.97916pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${E}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
6.97916pt\hfil&\hfil\hskip 28.39583pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.39583pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${M}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
8.39583pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.07997pt}{2.39995pt}\pgfsys@curveto{-1.69997pt}{0.95996pt}{-0.85316pt}{0.28pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85316pt}{-0.28pt}{-1.69997pt}{-0.95996pt}{-2.07997pt}{-2.39995pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{}{{}}\pgfsys@moveto{-27.16386pt}{-5.1708pt}\pgfsys@lineto{-7.96382pt}{-5.1708pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.24377pt}{-5.1708pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.76384pt}{-5.1708pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.65344pt}{-1.45695pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\varphi}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}\pgfsys@setdash{2.79985pt,1.59991pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{6.79445pt}{-5.1708pt}\pgfsys@lineto{25.99449pt}{-5.1708pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{26.19447pt}{-5.1708pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.65001pt}{-2.81804pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{$\scriptstyle{\exists}$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\big{)}.$

For a set $\mathcal{T}$ of morphic proequations, taken over possibly different
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$,
we denote by $\mathcal{V}(\mathcal{T})$ the class of orbit-finite monoids
satisfying all proequations in $\mathcal{T}$. A class $\mathcal{V}$ of orbit-
finite monoids is _presentable by morphic proequations_ if
$\mathcal{V}=\mathcal{V}(\mathcal{T})$ for some set $\mathcal{T}$ of morphic
proequations.

Note that proequations use support bounds, while the definition of an MSR-
pseudovariety does not.

######  Theorem 6.2 (Nominal Reiterman).

A class of orbit-finite nominal monoids is an MSR-pseudovariety iff it is
presentable by morphic proequations.

The main technical observations for the proof are that (i) every orbit-finite
set is $k$-bounded for some $k$, hence finitely copresentable in
$\mathbf{nStone}_{k}$, and (ii) there are “enough” proequations in the sense
that every orbit-finite nominal monoid is a quotient of some
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
The quotient is not necessarily MSR, which entails that abstract pseudovariety
theorems [30, 1] do not apply to our present setting.

We also give a syntactic version of our nominal Reiterman theorem, which uses
explicit proequations in lieu of morphic proequations.

######  Definition 33.

An _explicit proequation_ is a pair
$(x,y)\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}\times\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
for some strong $\Sigma\in\mathbf{Nom}_{\mathrm{of}}$ and some support bound
$s$, denoted by $x=y$. An orbit-finite monoid $M$ _satisfies_ the explicit
proequation $x=y$ if

$\hat{h}(x)=\hat{h}(y)\qquad\text{for every $s$-bounded equivariant monoid
morphism $h\colon\Sigma^{*}\to M$}.$

(Here choose a common support size bound $k$ for $M$ and $s$, so that
$\hat{h}$ lies in $\mathbf{nStone}_{k}$.)

######  Theorem 6.3 (Explicit Nominal Reiterman).

A class of orbit-finite nominal monoids is an MSR-pseudovariety iff it is
presentable by explicit proequations.

######  Example 6.4.

Recall that in a finite monoid $M$ every element $m$ has a unique idempotent
power, denoted by $m^{\omega}$. This holds analogously for orbit-finite
nominal monoids $M$ [7, Theorem 5.1]: one has $m^{\omega}=m^{(n\cdot k!)!}$
where $n$ is the number of orbits $M$ and $k$ is the maximum support size.
(The number $n\cdot k!$ is an upper bound on the number of elements of $M$
with any given finite support [36, Thm. 5.13], hence on the cardinality of the
set $\\{m^{i}\colon i\in\mathbb{N}\\}$.) The nominal monoid $M$ is _aperiodic_
if $m^{\omega}\cdot m=m^{\omega}$ for all $m\in M$. Languages recognizable by
aperiodic orbit-finite monoids are captured precisely by first-order logic on
data words [7, 13]. One readily verifies that the class of aperiodic orbit-
finite monoids forms an MSR-pseudovariety; in fact, it is closed under all
quotients. To present it by pro-orbit-finite equations, note that for every
$x\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
the family $x^{\omega}=(\hat{h}(x)^{\omega})_{h}$ is again compatible, hence
$x^{\omega}\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
If $s\colon\Sigma^{*}\to\mathcal{P}_{k}\mathbb{A}$ and
$h\colon\Sigma^{*}\to_{s}M$ is an $s$-bounded equivariant monoid morphism such
that $M$ has at most $n$ orbits, then
$\hat{h}(x^{\omega})=\hat{h}(x)^{\omega}=\hat{h}(x)^{(n\cdot
k!)!}=\hat{h}(x^{(n\cdot k!)!})$, hence $\hat{d}_{s}(x^{\omega},x^{(n\cdot
k!)!})<2^{-n}$ in the metric (5.1) on
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$.
This shows that $x^{\omega}$ is the limit of the sequence $(x^{(n\cdot
k!)!})_{n\in\mathbb{N}}$ in
$\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$,
and moreover that the pseudovariety of aperiodic orbit-finite monoids is
presented by the explicit proequations $x^{\omega}\cdot x=x^{\omega}$, where
$x\in\mathrlap{\widehat{\scalebox{0.95}[1.0]{\phantom{${\Sigma}^{*}_{s}$}}}}{\Sigma}^{*}_{s}$
and $s\colon{\Sigma}^{*}\rightarrow\mathcal{P}_{k}\mathbb{A}$ ranges over all
support bounds on strong orbit-finite alphabets. Restricting to $k=0$, we
recover the well-known description of aperiodic finite monoids by the (single)
profinite equation $x^{\omega}\cdot x=x^{\omega}$.

######  Remark 34.

  1. 1.

Pseudovarieties of finite monoids admit an alternative equational
characterization based on sequences of word equations rather than profinite
equations. A _word equation_ is a pair $(v,w)\in\Sigma^{*}\times\Sigma^{*}$ of
words over some finite alphabet $\Sigma$, denoted $v=w$; it is _satisfied_ by
a monoid $M$ if $h(v)=h(w)$ for every monoid morphism $h\colon\Sigma^{*}\to
M$. More generally, a sequence $(v_{0}=w_{0},v_{1}=w_{1},\ldots)$ of word
equations, taken over possibly different finite alphabets, is _eventually
satisfied_ by $M$ if it satisfies all but finitely many of the equations. As
shown by Eilenberg and Schützenberger [15], a class of finite monoids forms a
pseudovariety iff it is presentable by a (single) sequence of word equations.

  2. 2.

Urbat and Milius [45] recently established a nominal version of the Eilenberg-
Schützenberger theorem. They consider nominal word equations (defined as
above, where $\Sigma$ is now a strong orbit-finite nominal set) and show that
sequences of nominal word equations present precisely _weak pseudovarieties_ ,
i.e. classes of orbit-finite nominal monoids closed under finite products,
submonoids, and support-reflecting quotients. Clearly every MSR-pseudovariety
is weak, but the converse does not hold; hence over nominal sets, sequences of
word equations and pro-orbit-finite equations are of different expressivity.
The example below illustrates one source of additional expressivity of pro-
orbit-finite equations: The support bound $s$ can control how the support
changes during multiplication, which is not expressible by sequences of word
equations.

######  Example 6.5.

An example of an MSR-pseudovariety that is not a weak pseudovariety is given
by the class $\mathcal{V}$ of all orbit-finite nominal monoids $M$ such that

$\forall(m,n\in
M)\colon\quad\operatorname{supp}(mn)=\emptyset\quad\iff\quad\operatorname{supp}(m,n)=\emptyset.$
(6.1)

(Note that
$\operatorname{supp}(m,n)=\operatorname{supp}m\cup\operatorname{supp}n$ and
that “$\Leftarrow$” always holds by equivariance of the monoid
multiplication.) It is not difficult to prove that $\mathcal{V}$ is an MSR-
pseudovariety. To show that $\mathcal{V}$ is not a weak pseudovariety, we
construct a support-reflecting quotient under which $\mathcal{V}$ is not
closed. The nominal set
$\overline{1}+\overline{\mathbb{A}}=\\{\overline{1}\\}+\\{\overline{a}\mid
a\in\mathbb{A}\\}$ forms a nominal monoid with multiplication given by
projection on the first component and unit $\overline{1}$. We extend the
multiplication to the nominal set
$M=1+\mathbb{A}+\overline{1}+\overline{\mathbb{A}}$ by letting $1$ be the unit
and setting $x\cdot y=\overline{x}\cdot\overline{y}$ whenever $x,y\neq 1$;
here overlining is idempotent ($\overline{\overline{x}}:=\overline{x}$). This
makes the multiplication associative and equivariant. Thus, $M$ is a nominal
monoid. Now let $N=1+\mathbb{A}+0=\\{1\\}+\mathbb{A}+\\{0\\}$ be the nominal
monoid with multiplication $x\cdot y=0$ for $x,y\neq 1$. Thus $0$ is an
absorbing element. Letting
$\mathrm{const}_{0}\colon\overline{1}+\overline{\mathbb{A}}\to 0$ denote the
constant map, we have the equivariant surjective map

$e=\mathrm{id}_{1+\mathbb{A}}+\mathrm{const}_{0}\colon
M=(1+\mathbb{A})+(\overline{1}+\overline{\mathbb{A}})\twoheadrightarrow(1+\mathbb{A})+0=N.$

Note that $e$ is a monoid morphism: it maps $1$ to $1$ and if $x,y\neq 1$ then
$e(x),e(y)\neq 1$ and hence $e(x\cdot
y)=e(\overline{x}\cdot\overline{y})=0=e(x)\cdot e(y)$. The quotient $e$ is
support-reflecting, but it is not MSR: the subset
$1+\mathbb{A}+\overline{1}\subseteq M$ of support-preserving elements does not
form a submonoid of $M$. Finally, clearly $M$ satisfies (6.1) while $N$ does
not.

##  7 Conclusion and Future Work

We have introduced topological methods to the theory of data languages, and
also explored some of their subtleties and limitations. Following the spirit
of Marshall Stone’s slogan _“always topologize”_ , the core insight of our
paper may be summarized as:

_Data languages topologize for bounded supports._

In fact, by restricting to support-bounded orbit-finite nominal sets and
analyzing their Pro-completion, we have shown that fundamental results from
profinite topology (notably Stone duality and the equivalence between
profinite spaces and Stone spaces) generalize to the pro-orbit-finite world.
These results are of independent interest; in particular, they are potentially
applicable to data languages recognizable by all kinds of orbit-finite
structures. For the case of monoids, we derived a topological interpretation
of recognizable data languages via clopen sets of pro-orbit-finite words, as
well as a nominal version of Reiterman’s pseudovariety theorem characterizing
the expressive power of pro-orbit-finite equations.

The foundations laid in the present paper open up a number of promising
directions for future research. One first goal is to develop a fully fledged
duality theory for data languages along the lines of the work of Gehrke et al.
[18] on classical regular languages, based on an _extended nominal Stone
duality_ between pro-orbit-finite monoids and nominal boolean algebras with
operators.

Regarding specific applications, we aim to analyze further classes of orbit-
finite monoids in terms of pro-orbit-finite equations, following the lines of
6.4, in order to classify the corresponding data languages. One natural
candidate is the class of $\mathcal{J}$-trivial monoids, with the vision of a
nominal version of Simon’s theorem [42] relating $\mathcal{J}$-triviality to
existential first-order logic on data words.

Finally, we aim to extend our topological theory of recognizable data
languages, and the corresponding nominal Reiterman theorem, to algebraic
structures beyond orbit-finite monoids. Potential instances include algebras
for a signature $\Sigma$, which serve as recognizers for data tree languages,
infinitary structures such as nominal $\omega$-semigroups [46], modeling
languages of infinite data words, and algebraic structures with binders, which
we expect to bear interesting connections to data languages with binders and
their automata models [40, 44].

## References

  * [1] Jiří Adámek, Liang-Ting Chen, Stefan Milius, and Henning Urbat.  Reiterman’s theorem on finite algebras for a monad.  ACM Trans. Comput. Log., 22(4):23:1–23:48, 2021.
  * [2] Jiří Adámek and Jiří Rosický.  Locally Presentable and Accessible Categories.  London Mathematical Society Lecture Note Series. Cambridge University Press, 1994.
  * [3] Jorge Almeida.  Profinite semigroups and applications.  In Structural Theory of Automata, Semigroups, and Universal Algebra, pages 1–45. Springer Netherlands, 2005.
  * [4] Jorge Almeida and Alfredo Costa.  Profinite topologies.  In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 615–652. European Mathematical Society Publishing House, Zürich, Switzerland, 2021.
  * [5] Michał Bielecki, Jan Hidders, Jan Paredaens, Jerzy Tyszkiewicz, and Jan Van den Bussche.  Navigating with a browser.  In ICALP 2002, volume 2380 of LNCS, pages 764–775. Springer, 2002.
  * [6] Garrett Birkhoff.  On the Structure of Abstract Algebras.  Mathematical Proceedings of the Cambridge Philosophical Society, 31(4):433–454, 1935.
  * [7] Mikołaj Bojańczyk.  Nominal monoids.  Theory Comput. Syst., 53(2):194–222, 2013.
  * [8] Mikołaj Bojańczyk.  Recognisable languages over monads.  In DLT 2015, volume 9168 of LNCS, pages 1–13. Springer, 2015\.
  * [9] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Log. Methods Comput. Sci., 10(3), 2014.
  * [10] Mikołaj Bojańczyk and Rafał Stefański.  Single-use automata and transducers for infinite alphabets.  In ICALP 2020, volume 168 of LIPIcs, pages 113:1–113:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [11] Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege.  A robust class of data languages and an application to learning.  Log. Meth. Comput. Sci., 10(4:19):23pp., 2014.
  * [12] Liang-Ting Chen, Jiří Adámek, Stefan Milius, and Henning Urbat.  Profinite monads, profinite equations, and Reiterman’s theorem.  In FOSSACS 2019, volume 9634 of LNCS, pages 531–547. Springer, 2016.
  * [13] Thomas Colcombet, Clemens Ley, and Gabriele Puppis.  Logics with rigidly guarded data tests.  Log. Methods Comput. Sci., 11(3), 2015.
  * [14] Samuel Eilenberg.  Automata, Languages, and Machines.  Elsevier Science, 1974.
  * [15] Samuel Eilenberg and Marcel-Paul Schützenberger.  On pseudovarieties.  Advances Math., 10:413–418, 1976.
  * [16] Murdoch James Gabbay.  Nominal algebra and the HSP theorem.  J. Log. Comput., 19(2):341–367, 2009.
  * [17] Murdoch James Gabbay, Tadeusz Litak, and Daniela Petrisan.  Stone Duality for Nominal Boolean Algebras with

$\mathsf{N}$

.  In CALCO 2011, volume 6859 of LNCS, pages 192–207. Springer, 2011.

  * [18] Mai Gehrke, Serge Grigorieff, and Jean-Eric Pin.  Duality and equational theory of regular languages.  In ICALP 2008, volume 5126 of LNCS, pages 246–257. Springer, 2008.
  * [19] Mai Gehrke, Serge Grigorieff, and Jean-Eric Pin.  A topological approach to recognition.  In ICALP 2010, volume 6199 of LNCS, pages 151–162. Springer, 2010.
  * [20] Mai Gehrke, Daniela Petrişan, and Luca Reggio.  The Schützenberger product for syntactic spaces.  In ICALP 2016, volume 55 of LIPIcs, pages 112:1–112:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [21] Mai Gehrke, Daniela Petrişan, and Luca Reggio.  Quantifiers on languages and codensity monads.  In LICS 2017, pages 1–12. IEEE Computer Society, 2017.
  * [22] Radu Grigore, Dino Distefano, Rasmus Petersen, and Nikos Tzevelekos.  Runtime verification based on register automata.  In TACAS 2013, volume 7795 of LNCS, pages 260–276. Springer, 2013.
  * [23] Matthew Hennessy.  A fully abstract denotational semantics for the pi-calculus.  Theoret. Comput. Sci., 278:53–89, 2002.
  * [24] Michael Kaminski and Nissim Francez.  Finite-memory automata.  Theor. Comput. Sci., 134(2):329–363, 1994.
  * [25] Kenneth Krohn and John Rhodes.  Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines.  Trans. Am. Math. Soc., 116:450–464, 1965.
  * [26] Klaas Kürtz, Ralf Küsters, and Thomas Wilke.  Selecting theories and nonce generation for recursive protocols.  In FSME 2007, pages 61–70. ACM, 2007.
  * [27] Alexander Kurz and Daniela Petrisan.  On universal algebra over nominal sets.  Math. Struct. Comput. Sci., 20(2):285–318, 2010.
  * [28] Saunders MacLane.  Categories for the Working Mathematician.  Springer-Verlag, 1971.
  * [29] R. McNaughton and S. Papert.  Counter-free Automata.  M.I.T. Press research monographs. M.I.T. Press, 1971.
  * [30] Stefan Milius and Henning Urbat.  Equational axiomatization of algebras with structure.  In FOSSACS 2019, volume 11425 of LNCS, pages 400–417. Springer, 2019.
  * [31] Frank Neven, Thomas Schwentick, and Victor Vianu.  Finite state machines for strings over infinite alphabets.  ACM Trans. Comput. Log., 5(3):403–435, 2004.
  * [32] Daniela Petrişan.  Investigations into Algebra and Topology over Nominal Sets.  PhD thesis, University of Leicester, 2012.
  * [33] Jean-Eric Pin.  Profinite methods in automata theory.  In STACS 2009, volume 3 of LIPIcs, pages 31–50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009.
  * [34] Jean-Eric Pin and Pascal Weil.  A Reiterman theorem for pseudovarieties of finite first-order structures.  Algebra Universalis, 35(4):577–595, 1996.
  * [35] Nicholas Pippenger.  Regular languages and Stone duality.  Theory Comput. Syst., 30(2):121–134, 1997.
  * [36] Andrew M. Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge University Press, 2013.
  * [37] Jan Reiterman.  The Birkhoff theorem for finite algebras.  Algebra Universalis, 14(1):1–10, 1982.
  * [38] L. Ribes and P. Zalesskii.  Profinite Groups.  Springer, 2010.
  * [39] Julian Salamanca.  Unveiling eilenberg-type correspondences: Birkhoff’s theorem for (finite) algebras + duality.  CoRR, 2017.  arXiv:1702.02822.
  * [40] Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann.  Nominal automata with name binding.  In FOSSACS 2017, pages 124–142, 2017.
  * [41] Marcel Paul Schützenberger.  On finite monoids having only trivial subgroups.  Information and Control, 8(2):190–194, 1965.
  * [42] Imre Simon.  Piecewise testable events.  In H. Brakhage, editor, Automata Theory and Formal Languages, pages 214–222. Springer, 1975.
  * [43] Henning Urbat, Jiří Adámek, Liang-Ting Chen, and Stefan Milius.  Eilenberg theorems for free.  In MFCS 2017, volume 83 of LIPIcs, pages 43:1–43:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [44] Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder.  Nominal Büchi automata with name allocation.  In CONCUR 2021, pages 4:1–4:16, 2021.
  * [45] Henning Urbat and Stefan Milius.  Varieties of data languages.  In ICALP 2019, volume 132 of LIPIcs, pages 130:1–130:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [46] Thomas Wilke.  An Eilenberg theorem for infinity-languages.  In ICALP 1991, volume 510 of LNCS, pages 588–599. Springer, 1991.

##  A Appendix

This appendix provides full proofs of all results and technical statements
omitted for space reasons.

### Details for Example 3.1.3

We show that every nominal metric space carries a natural nominal topology
with basic open sets given by the open balls. First we show that taking open
balls is equivariant:

$\displaystyle\pi\cdot B_{r}(x)$ $\displaystyle=\\{\pi\cdot y\mid
d(x,y)<r,y\in X\\}$ $\displaystyle=\\{\pi\cdot(\pi^{-1}\cdot z)\mid
d(x,\pi^{-1}\cdot z)<r,z=\pi\cdot y\in\pi\cdot X=X\\}$
$\displaystyle=\\{z\mid\pi\cdot d(x,\pi^{-1}\cdot z)<r,z\in X\\}$
$\displaystyle=\\{z\mid d(\pi x,z)<r,z\in X\\}$ $\displaystyle=B_{r}(\pi x).$

Note that this implies that $B_{r}x$ is finitely supported by
$\operatorname{supp}x$. It remains to show that the open balls form a basis.
For two balls $B_{r}x,B_{r^{\prime}}x^{\prime}$ the union
$\bigcup\\{B_{s}y\mid B_{s}y\subseteq B_{r}x\cap B_{r^{\prime}}x^{\prime}\\}$
is finitely supported by
$\operatorname{supp}x\cup\operatorname{supp}x^{\prime}$ and equal to
$B_{r}x\cap B_{r^{\prime}}x^{\prime}$.

### Details for 5.2

We prove that the category $\mathbf{Nom}_{k}$ is not cartesian closed, and
consequently not a topos. Recall that finite products in $\mathbf{Nom}_{k}$
are induced by the coreflector
$(-)_{k}\colon\mathbf{Nom}\rightarrow\mathbf{Nom}_{k}$ sending a nominal set
to its nominal subset of $k$-bounded elements, so the product of
$X,Y\in\mathbf{Nom}_{k}$ is given by

$X\times_{k}Y:=(X\times
Y)_{k}=\\{\,(x,y)\mid|\operatorname{supp}x\cup\operatorname{supp}y|\leq
k\,\\}.$

It suffices to show that the functor $X\times_{k}(-)$ generally does not
preserve coequalizers; this implies that it is not a left adjoint, whence
$\mathbf{Nom}_{k}$ is not cartesian closed.

We set $k=2$ and $X=\mathbb{A}^{\\#2}$. Consider the parallel pair

$i_{0},i_{1}\colon\mathbb{A}^{\\#2}\rightrightarrows\mathbb{A}+\mathbb{A}\qquad\text{with}\qquad
i_{l}=\iota_{l}\cdot\pi_{l},$

where $\pi_{l}\colon\mathbb{A}^{\\#2}\to\mathbb{A}$ is the $l$-th projection
and $\iota_{l}\colon\mathbb{A}\to\mathbb{A}+\mathbb{A}$ is the $l$-th
coproduct injection; that is, $i_{0}(a,b)=\iota_{0}(a)$ and
$i_{1}(a,b)=\iota_{1}(b)$. Since colimits in $\mathbf{Nom}_{k}$ are formed in
$\mathbf{Nom}$, the coequalizer of $i_{0},i_{1}$ is $1$, i.e., the equivalence
relation on $\mathbb{A}+\mathbb{A}$ generated by $i_{0}(a,b)\sim i_{1}(a,b)$
identifies everything. To see this, consider two elements
$\iota_{l}(a),\iota_{m}(b)$ of $\mathbb{A}+\mathbb{A}$. They are clearly
identified whenever $l\neq m$ and $a\neq b$. If $l=m$ and $a=b$ they are
identified by reflexivity. If $l=m$ and $a\neq b$ we choose a fresh
$c\in\mathbb{A}$ and $n\neq l$ to get

$\iota_{l}(a)\sim\iota_{n}(c)\sim\iota_{l}(b)=\iota_{m}(b).$

Finally, if $l\neq m$ and $a=b$ we choose fresh names $c,d\in\mathbb{A}$ to
get

$\iota_{l}(a)\sim\iota_{m}(c)\sim\iota_{l}(d)\sim\iota_{m}(b).$

The parallel pair $i_{0},i_{1}$ is mapped under the functor
$\mathbb{A}^{\\#2}\times_{2}(-)$ to

$j_{0},j_{1}\colon\mathbb{A}^{\\#2}\times_{2}\mathbb{A}^{\\#2}\rightrightarrows\mathbb{A}^{\\#2}\times_{2}(\mathbb{A}+\mathbb{A})\qquad\text{where}\qquad
j_{l}=\mathrm{id}_{\mathbb{A}^{\\#2}}\times_{2}i_{l}.$

We observe that for every element
$(a,b,\iota_{l}(c))\in\mathbb{A}^{\\#2}\times_{2}(\mathbb{A}+\mathbb{A})$
either $c=a$ or $c=b$ by $2$-boundedness. Moreover, every such element has a
unique preimage under $j_{l}$ and no preimage under $j_{m}$ for $m\neq l$. For
example, the element $(a,b,\iota_{0}(a))$ has the preimage $(a,b,a,b)$ under
$j_{0}$ and no preimage under $j_{1}$. Therefore, the equivalence class of
that element is the two-element set
$\\{(a,b,\iota_{0}(a)),(a,b,\iota_{1}(b))\\}$. Similarly, the preimage of
$(a,b,\iota_{0}(b))$ under $j_{0}$ is $(a,b,b,a)$ and its equivalence class is
$\\{(a,b,\iota_{0}(b)),(a,b,\iota_{1}(a))\\}$. In particular,
$(a,b,\iota_{0}(a))$ and $(a,b,\iota_{0}(b))$ are not identified. This shows
that the coequalizer of $j_{0},j_{1}$ is given by

$c\colon\mathbb{A}^{\\#2}\times_{2}(\mathbb{A}+\mathbb{A})\twoheadrightarrow\mathbb{A}^{\\#2}\times
2,$

defined by $(a,b,\iota_{0}(x))\mapsto(a,b,\delta_{x=a})$ and
$(a,b,\iota_{1}(x))\mapsto(a,b,\delta_{x=b})$, where $\delta_{x=a}(a)=1$ and
$\delta_{x=a}(x)=0$ for $x\neq a$. This map is clearly not the image of
$\mathbb{A}+\mathbb{A}\twoheadrightarrow 1$ under
$\mathbb{A}^{\\#2}\times_{2}(-)$, which proves that this functor does not
preserve coequalizers.

### Proof of 3.5

Let $D\colon I\rightarrow\mathbf{Nom}_{k}$ be a codirected diagram, and let
$p_{i}\colon L\rightarrow|D_{i}|$ be the limit of the underlying diagram of
sets, that is, $L$ consists of all compatible tuples $(x_{i}\in D_{i})_{i\in
I}$. Suppose that for any tuple $(x_{i})_{i\in I}$ the union $S=\bigcup_{i\in
I}\operatorname{supp}x_{i}$ contains $k+1$ pairwise distinct names
$\\{a_{0},\ldots,a_{k}\\}\subseteq S$. Then every $a_{i}$ lies in the support
of some $x_{t_{i}}$. By codirectedness there exists $t\leq t_{0},\ldots,t_{k}$
in $I$, then $D_{t,t_{j}}(x_{t})=x_{t_{j}}$ and therefore, for all
$j=0,\ldots,k$,

$a_{j}\in\operatorname{supp}x_{t_{j}}=\operatorname{supp}D_{t,t_{j}}(x_{t_{j}})\subseteq\operatorname{supp}x_{t}.$

But this is a contradiction to our assumption that $D_{t}$ is $k$-bounded. So
$S$ is a finite support of $(x_{i})_{i\in I}$, and the limit of $D$ in
$\mathbf{Nom}$ hence consists of _all_ compatible families $(x_{i}\in
D_{i})_{i\in I}$. Moreover, for any such family its least support is of size
less or equal to $k$.

### Proof of 3.6

$\ref{lem:comp:def}\Rightarrow\ref{lem:comp:unif}$: Let $\mathcal{C}$ be an
open cover of $X$ that is uniformly supported by some finite subset
$S\subseteq\mathbb{A}$. Then there exists an orbit-finite finitely supported
subcover $\mathcal{C}_{0}\subseteq\mathcal{C}$. All sets in $\mathcal{C}_{0}$
are $S$-supported, but the orbit-finite set $\mathcal{C}_{0}$ contains
finitely many $S$-supported elements, proving that $\mathcal{C}_{0}$ is
finite.

$\ref{lem:comp:unif}\Rightarrow\ref{lem:comp:supp}$: By definition of
$|{X}|_{S}$.

$\ref{lem:comp:supp}\Rightarrow\ref{lem:comp:orb}$: The space
$\operatorname{orb}_{S}X$ is defined as a quotient of $|{X}|_{S}$ and
compactness of topological spaces is preserved under quotients.

$\ref{lem:comp:orb}\Rightarrow\ref{lem:comp:unif}$: Let
$\mathcal{C}=\\{U_{i}\\}_{i\in I}$ be an open cover of $X$ uniformly finitely
supported by $S\subseteq\mathbb{A}$. Let $V_{i}$ be the set of $S$-orbits
contained in $U_{i}$, then the sets $\\{V_{i}\\}_{i\in I}$ cover
$\operatorname{orb}_{S}X$: If $x\in U_{i}$ then the $S$-orbit
$\operatorname{orb}_{S}x$ is a subset of $U_{i}$ since the latter is
$S$-supported, so $\operatorname{orb}_{S}x\in V_{i}$. By compactness finitely
many such $V_{i}$ cover $\operatorname{orb}_{S}X$, so the sets $U_{i}=\bigcup
V_{i}$ give a finite cover of $X$.

$\ref{lem:comp:unif}\Rightarrow\ref{lem:comp:def}$: Let $\mathcal{C}$ be a
cover of $X$ that is finitely supported by $S\subseteq\mathbb{A}$. The set
$\mathcal{C}_{S}=\\{\operatorname{hull}_{S}U\mid U\in\mathcal{C}\\}$ then is a
uniformly finitely supported cover of $X$, so finitely many
$\operatorname{hull}_{S}U_{1},\dots,\operatorname{hull}_{S}U_{n}$ suffice to
cover $X$. The subset $\mathcal{C}^{\prime}=\\{\pi\cdot
U_{i}\mid\pi\in\operatorname{Perm}_{S}\mathbb{A},1\leq i\leq n\\}$ therefore
is an orbit-finite subcover $X$ finitely supported by $S$.

### Proof of 3.7

The proof of 3.7 requires some auxiliary statements.

######  Lemma A.1.

Let $D\colon I\rightarrow\mathbf{nTop}$ be a codirected diagram of nominal
spaces with limiting cone $p_{i}\colon L\rightarrow D_{i}$ for $i\in I$.

  1. 1.

The open sets $\\{p_{i}^{-1}[U]\mid i\in I,U\subseteq D_{i}\text{ open }\\}$
form a basis of $L$.

  2. 2.

For every finite subset $S\subseteq\mathbb{A}$ the set $\\{p_{i}^{-1}[U]\mid
i\in I,U\subseteq|{D_{i}}|_{S}\text{ open }\\}$ forms a basis of $|{L}|_{S}$.

######  Proof A.2.

  1. 1.

The set is closed under intersection. Given $i,j\in I$ with lower bound $k\leq
i,j$ and open sets $U\subseteq D_{i},V\subseteq D_{j}$, the intersection
$p_{i}^{-1}[U]\cap p_{j}^{-1}[V]$ is equal to $p_{k}^{-1}[D_{ki}^{-1}[U]\cap
D_{kj}^{-1}[V]]$ since the $p_{i}$ form a cone.

  2. 2.

We show that every $U\subseteq L$ supported by $S\subseteq\mathbb{A}$ is a
union of $S$-supported basic open sets. By definition $U$ is the union of all
basic open sets $p_{i}^{-1}[U_{i}]$ contained in $U$. The $S$-hull
$\operatorname{hull}_{S}(p_{i}^{-1}[U_{i}])$ of each of these sets is open,
supported by $S$ and satisfies

$p_{i}^{-1}[U_{i}]\subseteq\operatorname{hull}_{S}(p_{i}^{-1}[U_{i}])\subseteq\operatorname{hull}_{S}U=U,$

hence $U$ is also a union of the $S$-supported basic open sets
$\operatorname{hull}_{S}(p_{i}^{-1}[U_{i}])=p_{i}^{-1}[\operatorname{hull}_{S}U_{i}]$.

######  Lemma A.3.

Limits of codirected bounded diagrams of compact spaces are compact.

######  Proof A.4.

Let $D\colon I\rightarrow\mathbf{nTop}$ be a codirected diagram of $k$-bounded
compact spaces, and let $\left|-\right|\colon\mathbf{nTop}\to\mathbf{Set}$
denote the forgetful functor. From 3.5 we get $|\\!\lim D|\cong\lim|D|$, and
thus by A.1.2 also $|\\!\lim|{D}|_{S}|\cong|{\lim D}|_{S}$ as topological
spaces. All spaces $|{D}|_{S}$ are compact by 3.6.3, and limits of compact
spaces are compact, so every $|{\lim D}|_{S}\cong\lim|{D}|_{S}$ is compact.
Using 3.6 again, we get that $\lim D$ is nominally compact.

######  Lemma A.5.

For every nominal topological space $X$ the following statements are
equivalent:

  1. 1.

The space $X$ is Hausdorff.

  2. 2.

For every finite $S\subseteq\mathbb{A}$ the topological space
$\operatorname{orb}_{S}X$ is Hausdorff.

######  Proof A.6.

By definition of the topology of $\operatorname{orb}_{S}X$.

######  Lemma A.7.

Codirected limits of nominal Hausdorff spaces are nominal Hausdorff.

######  Proof A.8.

Let $D\colon I\rightarrow\mathbf{nTop}$ be a codirected diagram of nominal
Hausdorff spaces and take its limit $p_{i}\colon L\rightarrow D_{i}$. We fix a
finite subset $S\subseteq\mathbb{A}$ and prove that every pair of distinct
orbits $\operatorname{orb}_{S}x,\operatorname{orb}_{S}y\subseteq L$ with
$x=(x_{i})_{i\in I},y=(y_{i})_{i\in I}$ has disjoint $S$-supported open
neighbourhoods. To this end, it suffices to show that there exists an $i\in I$
such that $x_{i}$ and $y_{i}$ lie in different $S$-orbits: then there exist,
because $D_{i}$ is Hausdorff, disjoint open $S$-supported neighbourhoods
$U_{1},U_{2}\subseteq D_{i}$ of
$\operatorname{orb}_{S}x_{i},\operatorname{orb}_{S}y_{i}$ whose preimages
under $p_{i}$ are the desired disjoint $S$-supported open neighbourhoods of
$\operatorname{orb}_{S}x,\operatorname{orb}_{S}y$. Suppose the contrary, i.e.,
that $x_{i},y_{i}$ lie in the same $S$-orbit for all $i\in I$. Choose
$T\subseteq\mathbb{A}$ finite and disjoint from $S$ such that $S\cup T$
supports both $x,y$. We enumerate all permutations $\pi_{0},\ldots,\pi_{n}$
supported by $T$ and consider for each $\pi_{k}$ the set

$I_{k}=\\{i\in I\mid x_{i}=\pi_{k}\cdot y_{i}\\}\subseteq I.$

Then $I=\bigcup_{k=0}^{n}I_{k}$: For each $i\in I$ there exists some
$\pi\in\operatorname{Perm}_{S}\mathbb{A}$ such that $x_{i}=\pi\cdot y_{i}$,
and since $x_{i},y_{i}$ are supported by $S\cup T$ we may choose $\pi$ such
that it fixes all elements in $\mathbb{A}\setminus T$. We now show that some
$I_{k}$ forms a cofinal subset of the partial order $I$, that is, each element
of $I$ has a lower bound in $I_{k}$. Suppose the contrary. Then, for each
$k\in\\{0,\ldots,n\\}$ there exists $i_{k}\in I$ such that no $i\leq i_{k}$
lies in $I_{k}$. Since $I$ is codirected, there exists a lower bound $i\leq
i_{0},\ldots,i_{n}$. Thus $i\not\in I_{k}$ for any $k$, a contradiction.

Thus let $I_{k}$ be cofinal. Then for each $i\in I$ there exists $j\in I_{k}$
such that $j\leq i$, and so we compute

$x_{i}=D_{ji}(x_{j})=D_{ji}(\pi_{k}\cdot y_{j})=\pi_{k}\cdot
D_{ji}(y_{j})=\pi_{k}\cdot y_{i}$

for all $i\in I$. This contradicts our assumption of $x,y$ lying in different
$S$-orbits of $L$.

We are now ready to prove 3.7.

Let $D\colon I\rightarrow\mathbf{nTop}$ be a $k$-bounded non-empty diagram of
nominal compact Hausdorff spaces. Combining A.5
($\ref{lem:haus:haus}\Rightarrow\ref{lem:haus:orb}$) and 3.6.4 we get that the
codirected diagram $\operatorname{orb}_{\emptyset}\cdot D\colon
I\rightarrow\mathbf{nTop}\rightarrow\mathbf{Top}$ of non-empty compact
Hausdorff spaces, hence its limit $L$ is non-empty [38, Prop. 1.1.4]. This
limit contains a family of orbits $(O_{i}\subseteq D_{i})_{i\in I}$ that is
compatible, i.e., $D_{ij}[O_{i}]=O_{j}$ for all $i\leq j$ in $I$. Now fix an
arbitrary set $S\subseteq\mathbb{A}$ of size $k$. Then the set

$O_{i}^{S}=\\{x\in O_{i}\mid x\text{ is supported by }S\\}$

is non-empty: If $x\in O_{i}$ has support $T$ then $|T|\leq k$ by boundedness
of $D_{i}$, and $\pi\cdot x$ has support $\pi\cdot T=S$ for any permutation
$\pi$ mapping $T$ to $S$. The sets $O_{i}^{S}$ thus give a codirected diagram
of non-empty finite sets, so their limit in $\mathbf{Set}$ is itself non-
empty. Any element of this limit is supported by $S$ and hence an element in
$\lim D$. Moreover, the limit is a nominal compact Hausdorff space by A.7 and
A.3.

### Proof of 3.9

Let $C\subseteq X$ be clopen and let $S=\operatorname{supp}C$. Then $C$ is
equal to the uniformly finitely supported union of all $S$-supported basic
representables $p_{i}^{-1}[U_{i}]$ it contains (A.1.2). Since $C$ is compact,
being a closed subspace of the compact space $X$, finitely many representables
$p_{i}^{-1}[U_{i}]$ suffice to cover $C$. Take a lower bound $j$ of all these
$i$; then $C=p_{j}^{-1}[U]$ where $U=\bigcup_{i}D_{ji}^{-1}[U_{i}]$.

### Proof of Theorem 3.10

To prove that $\mathbf{nStone}_{k}$ is the Pro-completion of
$\mathbf{Nom}_{\mathrm{of},k}$, we make use of the following characterization
of Pro-completions of small categories.

######  Lemma A.9 ([1, Corollary A.5]).

If $\mathbf{C}$ is small, then $\operatorname{Pro}(\mathbf{C})$ is
characterized, up to equivalence, as a category $\mathbf{P}$ containing
$\mathbf{C}$ as a full subcategory such that

  1. 1.

the category $\mathbf{P}$ has codirected limits,

  2. 2.

every object in $\mathbf{P}$ is a codirected limit of objects in $\mathbf{C}$,
and

  3. 3.

every object in $\mathbf{C}$ is finitely copresentable in $\mathbf{P}$.

Our task is thus to show that $\mathbf{nStone}_{k}$ satisfies the above
conditions. Towards the proof of the second condition, we introduce the
canonical diagram of a space:

######  Construction 34.

To every $k$-bounded nominal Stone space $X$ we can construct a _canonical
diagram_ : The small category
${X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$ has as objects
continuous equivariant functions $f\colon X\rightarrow Y_{f}$ with
$Y_{f}\in\mathbf{Nom}_{\mathrm{of},k}$ (regarded as a discrete space), and
$h\colon Y_{f}\longrightarrow Y_{f^{\prime}}$ is a morphism from $f\colon
X\rightarrow Y_{f}$ to $f^{\prime}\colon X\rightarrow Y_{f^{\prime}}$ if
$hf=f^{\prime}$. The projection $f\mapsto Y_{f}$ gives a diagram in
$\mathbf{nStone}_{k}$, which by abuse of notation we also denote
${X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$.

######  Lemma A.10.

Every $k$-bounded nominal Stone space is the limit of its canonical diagram,
with limit cone $f\colon X\to Y_{f}$
($f\in{X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$).

######  Proof A.11.

Let $X$ be a $k$-bounded nominal Stone space. To prove that $X$ is isomorphic
to the limit of its canonical diagram
${X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$ we verify three
conditions, namely that (1) every pair of distinct points of $X$ can be
separated by some morphism in
${X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$; (2) for every
finitely supported compatible family $(y_{f})$ where $f$ ranges over
${X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$ there exists some
$x\in X$ with $f(x)=y_{f}$ for all $f$. Conditions (1) and (2) ensure that the
induced continuous equivariant map

$i\colon
X\rightarrow\lim({X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}})\qquad
x\mapsto(x_{f})_{f\in({X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}})}$

is a bijection (they are responsible for injectivity and surjectivity,
respectively). Moreover, since the representables $f^{-1}[y]$
($f\in{X}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}}$, $y\in Y_{f}$)
form a subbase of $X$, the inverse $i^{-1}$ is also continuous, hence $i$ is a
homeomorphism.

  1. 1.

Let $x,x^{\prime}\in X$ be distinct points. The space $X$ is Hausdorff, whence
for $x$ we get a basic clopen neighbourhood not containing $x^{\prime}$; this
neighbourhood is representable by $f\colon X\rightarrow Y_{f}$, and this
function clearly separates $x,x^{\prime}$.

  2. 2.

We need to prove that the finitely supported intersection
$\bigcap_{f}f^{-1}[y_{f}]$ is non-empty. Suppose the contrary. Then the open
sets $U_{f}=X\setminus f^{-1}[y_{f}]$ form a cover $\mathcal{C}$ of $X$,
uniformly finitely supported by any finite support $S$ of the family
$(y_{f})$. By compactness of $X$ finitely many such sets
$U_{f_{1}},\ldots,U_{f_{n}}\subseteq\mathcal{C}$ suffice to cover $X$; hence
$\bigcap_{i=1}^{n}f^{-1}[y_{f_{i}}]$ is empty. Let $f\colon
X\twoheadrightarrow Y_{f}$ be the subdirect product of the
$f_{i},i=1,\dots,n$, i.e., the coimage of the continuous equivariant map

$\langle f_{1},\ldots,f_{n}\rangle\colon X\rightarrow
Y_{f_{1}}\times\cdots\times Y_{f_{n}}.$

Note that $Y_{f}$ is $k$-bounded since $X$ is $k$-bounded and $f$ is
surjective. By surjectivity of $f$ there exists an $x\in X$ such that
$f(x)=y_{f}$; but then $x\in\bigcap_{i=1}^{n}f^{-1}[y_{f_{i}}]$, a
contradiction.

######  Construction 34.

For every codirected diagram $D\colon I\rightarrow\mathbf{nStone}_{k}$ one can
construct a diagram $D^{\prime}\colon
I^{\prime}\rightarrow\mathbf{Nom}_{\mathrm{of},k}$ of orbit-finite discrete
spaces: Let $I^{\prime}$ be the category with objects

$(i,f)\text{ with }i\in
I,f\in({D_{i}}\mathord{\downarrow}{\mathbf{Nom}_{\mathrm{of},k}})$

with arrows $(i,f)\rightarrow(j,g)$ those $h\colon Y_{f}\rightarrow Y_{g}$
making the following square commute:

${D_{i}}$${D_{j}}$${Y_{f}}$${Y_{g}}$$\scriptstyle{D_{ij}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{h}$

######  Lemma A.12.

Let $D\colon I\rightarrow\mathbf{nStone}_{k}$ be a codirected diagram. Then
the diagram from section A is cofiltered, and if $(p_{i}\colon\lim
D\rightarrow D_{i})_{i\in I}$ is a limiting cone for $D$, then $(f\cdot
p_{i}\colon\lim D\rightarrow D_{i}\rightarrow Y_{f})_{(i,f)\in I^{\prime}}$ is
a limiting cone for $D^{\prime}$.

######  Proof A.13 (Proof of A.12.).

We prove that $I^{\prime}$ is cofiltered. Firstly, given objects
$(i,f),(j,g)\in I^{\prime}$ there exists by codirectedness of $I$ a lower
bound $k\leq i,j$ in $I$. The coimage $h\colon D_{k}\twoheadrightarrow Y_{h}$
of $\langle f\cdot D_{ki},g\cdot D_{kj}\rangle$ has a $k$-bounded codomain and
the projections $p_{f}\colon Y_{h}\rightarrow Y_{f},p_{g}\colon
Y_{h}\rightarrow Y_{g}$ are morphisms in $I^{\prime}$. This makes $(k,h)$ a
span over $(i,f)$ and $(j,g)$ in $I^{\prime}$. Secondly, assume that
$h,h^{\prime}\colon(i,f)\rightarrow(j,g)$ are parallel arrows in $I^{\prime}$.
This in particular implies $h\cdot f=h^{\prime}\cdot f$, so by forming their
equalizer $e\colon E\rightarrowtail Y_{f}$ in $\mathbf{Nom}_{\mathrm{of},k}$
its universal property yields a morphism $\bar{f}\colon D_{i}\rightarrow E$
with $e\cdot\bar{f}=f$. Note that $\bar{f}$ is continuous, as it is just a
corestriction of the continuous map $f$. This is precisely the statement that
$(i,\bar{f})$ equalizes the morphisms $h,h^{\prime}$ in $I^{\prime}$.

Now we prove the rest of the statement. If $(p_{i}\colon\lim D\rightarrow
D_{i})_{i\in I}$ is a limiting cone for $D$ then the family $(f\cdot
p_{i}\colon\lim D\rightarrow D_{i}\rightarrow Y_{f})_{(i,f)\in D^{\prime}}$ is
clearly a cone for $D^{\prime}$, we just have to show it is universal. Suppose
$(a_{(i,f)}\colon A\rightarrow Y_{f})_{(i,f)\in I^{\prime}}$ is another cone
for $D^{\prime}$. If we restrict this cone to a fixed $i\in I$ we obtain a
cone over the canonical diagram of $D_{i}$. By A.10 every $D_{i}$ is the limit
of its canonical diagram, so we get a unique $a_{i}\colon A\rightarrow D_{i}$
satisfying $a_{(i,f)}=f\cdot a_{i}$ for $(i,f)\in I^{\prime}$. The family of
all $(a_{i})_{i\in I}$ is a cone over $D$: For $i\leq j$ and every $(j,g)\in
I^{\prime}$ we get the following diagram:

${D_{i}}$${D_{j}}$${A}$${Y_{g\cdot
D_{ij}}}$${Y_{g}}$$\scriptstyle{D_{ij}}$$\scriptstyle{g\cdot
D_{ij}}$$\scriptstyle{g}$$\scriptstyle{a_{i}}$$\scriptstyle{a_{j}}$$\scriptstyle{a_{(i,g\cdot
D_{ij})}}$$\scriptstyle{a_{(j,g)}}$$\scriptstyle{\mathrm{id}}$ (A.1)

The outer square and all but the upper triangle commute. The morphisms $(j,g)$
for fixed $j$ form the limiting cone of $D_{j}$ and thus are jointly monic, so
the upper triangle also commutes for all $i\leq j$. Since the family
$(a_{i})_{i\in i}$ is a cone for $D$ we get a unique $\alpha\colon
A\rightarrow\lim D$ with $a_{i}=p_{i}\cdot\alpha$, postcomposition yields
$f\cdot a_{i}=(f\cdot p_{i})\cdot\alpha$ for all $(i,f)\in I^{\prime}$.
Regarding uniqueness, let $f\cdot p_{i}\cdot\alpha=f\cdot p_{i}\cdot\beta$ for
all $(i,f)\in I^{\prime}$. First for every $i\in I$ we get
$p_{i}\cdot\alpha=p_{i}\cdot\beta$ as the $(i,f)\in I^{\prime}$ are jointly
monic, and second also $\alpha=\beta$ since the $p_{i}$ are jointly monic.

######  Theorem A.14.

For any $k$-bounded nominal space $X$ the following statements are equivalent:

  1. 1.

$X$ is a nominal Stone space.

  2. 2.

$X$ is the codirected limit of its canonical diagram.

  3. 3.

$X$ is a codirected limit of $k$-bounded orbit-finite discrete spaces.

######  Proof A.15 (Proof of Theorem A.14.).

$\ref{thm:pro-nom-equiv:pro}\Rightarrow\ref{thm:pro-nom-equiv:cof-canon}$:
A.10.

$\ref{thm:pro-nom-equiv:cof-canon}\Rightarrow\ref{thm:pro-nom-equiv:cod-
diag}$: This holds trivially.

$\ref{thm:pro-nom-equiv:cod-diag}\Rightarrow\ref{thm:pro-nom-equiv:pro}$: If
$X$ is a codirected limit of $k$-bounded orbit-finite discrete spaces then it
is nominal compact and Hausdorff by Lemma A.3 and A.7. It has a basis of
representable sets by A.1.1.

The following result critically depends on non-emptiness of codirected limits
of $k$-bounded compact Hausdorff codirected diagrams.

######  Lemma A.16.

Let $D\colon I\rightarrow\mathbf{Nom}_{\mathrm{of},k}$ non-empty codirected
diagram with limit cone $p_{i}\colon L\rightarrow D_{i}$. Then there exists
for every $i\in I$ some $j\leq i$ with

$D_{ji}[D_{j}]=p_{i}[\lim D].$

######  Proof A.17 (Proof of A.16.).

We fix $i\in I$. Note that for all $j\leq i$ already $p_{i}[\lim D]\subseteq
D_{ji}[D_{j}]$ since the $(p_{i})_{i\in I}$ form a cone, hence we only need to
prove the reverse inclusion. Suppose no $j\in I$ satisfies
$D_{ji}[D_{j}]\subseteq p_{i}[\lim D]$, then for all $j\in I^{\leq i}$ the
sets $D_{j}^{\prime}=D_{ji}^{-1}[D_{i}\setminus p_{i}[\lim D]]\subseteq D_{j}$
are non-empty (here $I^{\leq i}$ denotes the the downset $\\{j\in I\mid j\leq
i\\}$ of $i$ in $I$). The restriction $D^{\leq i}\colon I^{\leq
i}\rightarrowtail I\rightarrow\mathbf{Nom}_{\mathrm{of},k}$ of $D$ to $I^{\leq
i}$ is a non-empty codirected diagram in $\mathbf{Nom}_{\mathrm{of},k}$, of
which $D^{\prime}$ is a non-empty subdiagram. Its limit $\lim D^{\prime}$ is a
non-empty nominal space by 3.7, containing a compatible family $(x_{j})_{j\leq
i}\in\lim D^{\prime}$. By initiality of the inclusion functor $I^{\leq
i}\rightarrowtail I$ the limits of $D^{\leq i}$ and $D$ are isomorphic, hence
the family $(x_{j})_{j\leq i}$ extends by $\lim D^{\prime}\subseteq\lim
D^{\leq i}\cong\lim D$ to an element $(x_{i})_{i\in I}\in\lim D$. But this
element satisfies both $x_{i}=p_{i}(x)\in p_{i}[\lim D]$ and $x_{i}\in
D_{i}^{\prime}=X\setminus p_{i}[\lim D]$, a contradiction.

######  Lemma A.18.

Every $k$-bounded orbit-finite nominal set is finitely copresentable in
$\mathbf{nStone}_{k}$.

######  Proof A.19.

Let $Y$ be a $k$-bounded orbit-finite set, w.l.o.g. $Y\neq\emptyset$, and let
$D\colon I\rightarrow\mathbf{nStone}_{k}$ be a codirected diagram with
limiting cone $(p_{i}\colon\lim D\rightarrow D_{i})_{i\in I}$. We show that
every continuous, equivariant function $f\colon\lim D\rightarrow Y$ factors
essentially uniquely through some $p_{i}$.

  1. (1)

We first assume that all $D_{i}$ are orbit-finite discrete spaces.

  2. (1.i)

We prove that there exists some $i\in I$ and a continuous equivariant function
$g$ with $f=g\cdot p_{i}$. We may assume that $f$ is surjective; otherwise we
replace $f$ by its coimage. First, we choose representatives
$y_{i},\ldots,y_{m}$ of the orbits of $Y$ with (representable!) preimages
$Y_{i}=f^{-1}[y_{i}]$. Note that the sets $\pi\cdot
Y_{i},\pi\in\operatorname{Perm}\mathbb{A},$ form a partition of $L=\lim D$.
Let $S\subseteq\mathbb{A}$ be a finite set supporting all
$y_{i},i=1,\ldots,m$, then $S$ also supports all sets $Y_{i}$ due to
equivariance of $f$.

We first show that there exists some $j\in I$ such that

$Y_{i}=p_{j}^{-1}[p_{j}[Y_{i}]]\quad\text{ for all }i=1,\ldots,m.$ (A.2)

Fix $i\in\\{1,\ldots,m\\}$. The set $Y_{i}$ is a clopen (and hence compact)
subset of $|{L}|_{S}$. Recall that by A.1.2 the space $|{L}|_{S}$ has a basis
given by the sets $p_{l}^{-1}[U]$ where $l\in I$ and $U\subseteq D_{l}$ is an
$S$-supported set. So we can present $Y_{i}$ as a finite union of basic open
sets

$Y_{i}=\bigcup_{\alpha=1}^{n}p_{j_{\alpha}}^{-1}[U_{\alpha}],$ (A.3)

with $j_{\alpha}\in I$ and such that all $U_{\alpha}\subseteq D_{j_{\alpha}}$