remtheorem rem defntheorem defn Friedrich-Alexander-Universität Erlangen-
Nürnberg<EMAIL_ADDRESS>Friedrich-Alexander-Universität
Erlangen-Nürnberg<EMAIL_ADDRESS>H. Urbat and S.
Milius[100]F.4.3 Formal Languages Stefan Milius acknowledges support by
Deutsche Forschungsgemeinschaft (DFG) under project MI 717/5-1. Henning Urbat
acknowledges support by Deutsche Forschungsgemeinschaft (DFG) under project
SCHR 1118/8-2 Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and
Stefano Leonardi 4 46th International Colloquium on Automata, Languages, and
Programming (ICALP 2019) ICALP 2019 ICALP 2019 July 9–12, 2019 Patras, Greece
eatcs 132 125

# Varieties of Data Languages

Henning Urbat  Stefan Milius

###### Abstract

We establish an Eilenberg-type correspondence for data languages, i.e.
languages over an infinite alphabet. More precisely, we prove that there is a
bijective correspondence between varieties of languages recognized by orbit-
finite nominal monoids and pseudovarieties of such monoids. This is the first
result of this kind for data languages. Our approach makes use of nominal
Stone duality and a recent category theoretic generalization of Birkhoff-type
theorems that we instantiate here for the category of nominal sets. In
addition, we prove an axiomatic characterization of weak pseudovarieties as
those classes of orbit-finite monoids that can be specified by sequences of
nominal equations, which provides a nominal version of a classical theorem of
Eilenberg and Schützenberger.

###### keywords:

Nominal sets, Stone duality, Algebraic language theory, Data languages

##  1 Introduction

In the algebraic theory of formal languages, one studies automata and the
languages they represent in terms of associated algebraic structures. This
approach has been successfully implemented for numerous types of languages and
has proven extremely fruitful because it allows to import powerful algebraic
methods into the realm of automata theory. As a prime example, regular
languages can be described purely algebraically as the languages recognized by
finite monoids, and a celebrated result by McNaughton, Papert, and
Schützenberger [13, 21] asserts that a regular language is definable in first-
order logic if and only if its syntactic monoid is aperiodic (i.e. it
satisfies the equation $x^{n+1}=x^{n}$ for sufficiently large $n$). As an
immediate application, this algebraic characterization yields an effective
procedure for deciding first-order definability. The first systematic approach
to correspondence results of this kind was initiated by Eilenberg [7] who
proved that _varieties of languages_ (i.e. classes of regular languages closed
under the set-theoretic boolean operations, derivatives, and homomorphic
preimages) correspond bijectively to _pseudovarieties of monoids_ (i.e.
classes of finite monoids closed under quotients monoids, submonoids, and
finite products). Eilenberg’s result thus establishes a generic relation
between properties of regular languages and properties of finite monoids. In
addition, Eilenberg and Schützenberger [8] contributed a model-theoretic
description of pseudovarieties: they are those classes of finite monoids that
can be axiomatized by a sequence $(s_{n}=t_{n})_{n\in\mathds{N}}$ of
equations, interpreted as “$s_{n}=t_{n}$ holds for sufficiently large $n$”.
For instance, the pseudovariety of aperiodic finite monoids is axiomatized by
$(x^{n+1}=x^{n})_{n\in\mathds{N}}$.

The goal of our present paper is to study _data languages_ , i.e. languages
over an infinite alphabet, from the perspective of algebraic language theory.
Such languages have spurred significant interest in recent years, driven by
practical applications in various areas of computer science, including
efficient parsing of XML documents or software verification. Mathematically,
data languages are modeled using _nominal sets_. Over the years, several
machine models for handling data languages of different expressive power have
been proposed; see [23, 22] for a comprehensive survey. The focus of this
paper is on languages recognized by _orbit-finite nominal monoids_. They form
an important subclass of the languages accepted by Francez and Kaminski’s
_finite memory automata_ [11] (which are expressively equivalent to orbit-
finite automata in the category of nominal sets [5]) and have been
characterized by a fragment of monadic second-order logic over data words
called _rigidly guarded MSO_ [19]. In addition, Bojańczyk [6] and Colcombet,
Ley, and Puppis [19] established nominal versions of the McNaughton-Papert-
Schützenberger theorem and showed that the first-order definable data
languages are precisely the ones recognizable by aperiodic orbit-finite
monoids.

In the light of these results, it is natural to ask whether a generic variety
theory akin to Eilenberg’s seminal work can be developed for data languages.
As the main contribution of our paper, we answer this positively by
establishing nominal generalizations of two key results known from the
algebraic theory of regular languages. The first one is a counterpart of
Eilenberg’s variety theorem, which is the first result of this kind for data
languages:

######  Nominal Eilenberg Theorem.

Varieties of data languages correspond bijectively to pseudovarieties of
nominal monoids.

Here, the notion of a _pseudovariety of nominal monoids_ is as expected: a
class of orbit-finite nominal monoids closed under quotient monoids,
submonoids, and finite products. In contrast, the notion of a _variety of data
languages_ requires two extra conditions unfamiliar from other Eilenberg-type
correspondences, most notably a technical condition called _completeness_
(Definition 16). Like the original Eilenberg theorem, its nominal version
gives rise to a generic relation between properties of data languages and
properties of nominal monoids. For instance, the aperiodic orbit-finite
monoids form a pseudovariety, and the first-order definable data languages
form a variety, and thus the equivalence of these concepts can be understood
as an instance of the nominal Eilenberg correspondence.

On a conceptual level, our results crucially make use of _duality_ ,
specifically an extension of Petrişan’s [17] nominal version of Stone duality
which gives a dual equivalence between nominal sets and nominal complete
atomic boolean algebras. To derive the nominal Eilenberg correspondence, we
make two key observations. First, we show that varieties of data languages
dualize (under nominal Stone duality) to the concept of an _equational theory_
in the category of nominal sets. Second, we apply a recent categorical
generalization of Birkhoff-type variety theorems [16] to show that equational
theories correspond to pseudovarieties of nominal monoids. Our approach is
summarized by the diagram below:

Varieties of data languages Nominal Eilenberg
Theorem$\scriptstyle{\cong}$Nominal Stone duality$\scriptstyle{\cong}$
Equational theories Nom. Birkhoff Theorem$\scriptstyle{\cong}$ Pseudovarieties
of nominal monoids

The idea that Stone-type dualities play a major role in algebraic language
theory was firmly established by Gehrke, Grigorieff, and Pin [10]. It is also
at the heart of our recent line of work [1, 2, 24, 3], which culminated in a
uniform category theoretic proof of more than a dozen Eilenberg
correspondences for various types of languages. A related, yet more abstract,
approach was pursued by Salamánca [20]. The key insight of [24, 20] is that
Eilenberg-type correspondences arise by combining a Birkhoff-type
correspondence with a Stone-type duality. Our present approach to data
languages is an implementation of this principle in the nominal setting. Since
the existing categorical frameworks for algebraic language theory consider
algebraic-like base categories (which excludes nominal sets) and the
recognition of languages by finite structures, our Nominal Eilenberg Theorem
is not covered by any previous categorical work and requires new techniques.
However, our approach can be seen as an indication of the robustness of the
duality-based methodology for algebraic recognition.

As our second main contribution, we complement the Nominal Eilenberg Theorem
with a model-theoretic description of pseudovarieties of nominal monoids in
terms of sequences of _nominal equations_ , generalizing the classical result
of Eilenberg and Schützenberger for ordinary monoids. Our result applies more
generally to the class of _weak pseudovarieties_ of nominal monoids, which are
only required to be closed under support-reflecting (rather than arbitrary)
quotients. We then obtain the

######  Nominal Eilenberg-Schützenberger Theorem.

Weak pseudovarieties are exactly the classes of nominal monoids axiomatizable
by sequences of nominal equations.

While our main results apply to languages recognizable by orbit-finite
monoids, the underlying methods are of fairly general nature and can be
extended to other recognizing structures in the category of nominal sets. We
illustrate this in section 5 by deriving a (local) Eilenberg correspondence
for languages accepted by deterministic nominal automata.

##  2 Nominal Sets

We start by recalling basic definitions and facts from the theory of nominal
sets [18]. Some of the concepts considered in this paper are most clearly and
conveniently formulated in the language of category theory, but only very
basic knowledge of category theory is required from the reader. Fix a
countably infinite set $\mathbb{A}$ of _atoms_ , and denote by
$\mathrm{Perm}(\mathbb{A})$ the group of finite permutations of $\mathbb{A}$
(i.e. bijections $\pi\colon\mathbb{A}\to\mathbb{A}$ that move only finitely
many elements of $\mathbb{A}$). A _$\mathrm{Perm}(\mathbb{A})$ -set_ is a set
$X$ with an operation $\mathrm{Perm}(\mathbb{A})\times X\to X$, denoted as
$(\pi,x)\mapsto\pi\cdot x$, such that $(\sigma\pi)\cdot x=\sigma\cdot(\pi\cdot
x)$ and $\mathit{id}\cdot x$ for all $\sigma,\pi\in\mathrm{Perm}(\mathbb{A})$
and $x\in X$. If the group action is trivial, i.e. $\pi\cdot x=x$ for all
$\pi\in\mathrm{Perm}(\mathbb{A})$ and $x\in X$, we call $X$ _discrete_. For
any set $S\subseteq\mathbb{A}$ of atoms, denote by
$\mathrm{Perm}_{S}(\mathbb{A})\subseteq\mathrm{Perm}(\mathbb{A})$ the subgroup
of all finite permutations $\pi$ that fix $S$, i.e. $\pi(a)=a$ for all $a\in
S$. The set $S$ is called a _support_ of an element $x\in X$ if for every
$\pi\in\mathrm{Perm}_{S}(\mathbb{A})$ one has $\pi\cdot x=x$. The intuition is
that $x$ is some kind of syntactic object (e.g. a string, a tree, a term, or a
program) whose free variables are contained in $S$. Thus, a variable renaming
$\pi$ that leaves $S$ fixed does not affect $x$. A _nominal set_ is a
$\mathrm{Perm}(\mathbb{A})$-set $X$ such that every element of $X$ has a
finite support. This implies that every element $x\in X$ has a least support,
denoted by $\mathop{\mathsf{supp}}_{X}(x)\subseteq\mathbb{A}$. A nominal set
$X$ is _strong_ if, for every $x\in X$ and $\pi\in\mathrm{Perm}(\mathbb{A})$,
one has $\pi\cdot x=x$ if and only if $\pi(a)=a$ for all
$a\in\mathsf{supp}_{X}(x)$. The _orbit_ of an element $x$ of a nominal set $X$
is the set $\\{\pi\cdot x\;\mathrel{\mathop{\mathchar
58\relax}}\;\pi\in\mathrm{Perm}(\mathbb{A})\\}$. The orbits form a partition
of $X$. If $X$ has only finitely many orbits, then $X$ is called _orbit-
finite_. More generally, for any finite set $S\subseteq\mathbb{A}$ of atoms,
the _$S$ -orbit_ of an element $x\in X$ is the set $\\{\pi\cdot
x\;\mathrel{\mathop{\mathchar
58\relax}}\;\pi\in\mathrm{Perm}_{S}(\mathbb{A})\\}$, and the $S$-orbits form a
partition of $X$.

######  Lemma 2.1.

Let $S$ be a finite subset of $\mathbb{A}$. Then every orbit-finite nominal
set has only finitely many $S$-orbits.

A map $f\colon X\to Y$ between nominal sets is _equivariant_ if $f(\pi\cdot
x)=\pi\cdot f(x)$ for all $\pi\in\mathrm{Perm}(\mathbb{A})$ and $x\in X$, and
_finitely supported_ if there exists a finite set $S\subseteq\mathbb{A}$ such
that $f(\pi\cdot x)=\pi\cdot f(x)$ for all
$\pi\in\mathrm{Perm}_{S}(\mathbb{A})$ and $x\in X$. Equivariant maps do not
increase supports, i.e. one has
$\mathop{\mathsf{supp}}_{Y}(f(x))\subseteq\mathop{\mathsf{supp}}_{X}(x)$ for
all $x\in X$. We write $\mathbf{Nom}_{\mathsf{fs}}$ for the category of
nominal sets and finitely supported maps, and $\mathbf{Nom}$ for the (non-
full) subcategory of nominal sets and equivariant maps. We shall use the
following standard results about $\mathbf{Nom}$:

  1. (1)

$\mathbf{Nom}$ is complete and cocomplete. Finite limits and all colimits are
formed on the level of underlying sets. In particular, finite products of
nominal sets are given by cartesian products and coproducts by disjoint union.

  2. (2)

For every pair $X,Y$ of nominal sets, the _exponential_ $[X,Y]$ is the nominal
set consisting of all finitely supported maps $f\colon X\to Y$, with the group
action given by $(\pi\cdot f)(x)=\pi\cdot f(\pi^{-1}\cdot x)$. Moreover, for
every nominal set $X$, the _nominal power set_ $\mathcal{P}X$ is carried by
the set of all subsets $X_{0}\subseteq X$ with finite support; i.e. for which
there exists a finite set $S\subseteq\mathbb{A}$ of atoms such that $\pi\cdot
X_{0}=X_{0}$ for $\pi\in\mathrm{Perm}_{S}(\mathbb{A})$, where $\pi\cdot
X_{0}=\\{\pi\cdot x\;\mathrel{\mathop{\mathchar 58\relax}}\;x\in X_{0}\\}$. In
particular, every singleton $\\{x\\}$ is finitely supported by
$\mathop{\mathsf{supp}}_{X}(x)$. The group action on $\mathcal{P}X$ is given
by $X_{0}\mapsto\pi\cdot X_{0}$, and we have $\mathcal{P}X\cong[X,2]$, for the
discrete nominal set $2=\\{0,1\\}$.

  3. (3)

_Quotients_ and _subobjects_ in $\mathbf{Nom}$ are represented by epimorphisms
(= surjective equivariant maps) and monomorphisms (= injective equivariant
maps), respectively. $\mathbf{Nom}$ has image factorizations, i.e. every
equivariant map $f\colon X\to Y$ has a unique decomposition $f=m\cdot e$ into
a quotient $e\colon X\twoheadrightarrow I$ followed by a subobject $m\colon
I\rightarrowtail Y$. We call $e$ the _coimage_ of $f$.

  4. (4)

Orbit-finite nominal sets are closed under quotients, subobjects, and finite
products.

  5. (5)

For each $n\geq 0$, the nominal set
$\mathbb{A}^{\\#n}=\\{\,(a_{1},\ldots,a_{n})\in\mathbb{A}^{n}\;\mathrel{\mathop{\mathchar
58\relax}}\;a_{i}\neq a_{j}\text{ for $i\neq j$}\,\\}$ with group action
$\pi\cdot(a_{1},\ldots,a_{n})=(\pi(a_{1}),\ldots,\pi(a_{n}))$ is strong and
has a single orbit. More generally, the (orbit-finite) strong nominal sets are
up to isomorphism exactly the (finite) coproducts of nominal sets of the form
$\mathbb{A}^{\\#n}$.

##  3 Pseudovarieties of Nominal Monoids

In this section, we investigate classes of orbit-finite nominal monoids and
establish two characterizations of such classes: a categorical one, relating
pseudovarieties of nominal monoids to equational theories in the category of
nominal sets, and an axiomatic one, describing weak pseudovarieties in terms
of sequences of nominal equations. The first of these results is the algebraic
foundation of our subsequent treatment of varieties of data languages.

A _nominal monoid_ is a monoid $(M,\bullet,1_{M})$ in the category
$\mathbf{Nom}$; that is, $M$ is equipped with the structure of a nominal set
such that the multiplication $\bullet\colon M\times M\to M$ is an equivariant
map and the unit $1_{M}\in M$ has empty support, i.e. it corresponds to an
equivariant map $1\to M$, where $1$ is the nominal set with one element. We
write $\mathbf{nMon}$ for the category of nominal monoids and equivariant
monoid morphisms (usually just called _morphisms_), and
$\mathbf{nMon}_{\mathsf{of}}$ for the full subcategory of orbit-finite nominal
monoids. The forgetful functor from $\mathbf{nMon}$ to $\mathbf{Nom}$ has a
left adjoint assigning to each nominal set $\Sigma$ the free nominal monoid
$\Sigma^{*}$ of all words over $\Sigma$, with monoid multiplication given by
concatentation of words, unit $\varepsilon$ (the empty word) and group action
$\pi\cdot(a_{1}\cdots a_{n})=\pi(a_{1})\cdots\pi(a_{n})$ for
$\pi\in\mathrm{Perm}(\mathbb{A})$ and $a_{1}\cdots a_{n}\in\Sigma^{*}$. The
category $\mathbf{nMon}$ has products (formed on the level of $\mathbf{Nom}$),
image factorizations, and surjective and injective morphisms represent
_quotients_ and _submonoids_ of nominal monoids. A quotient $q\colon
M\twoheadrightarrow M^{\prime}$ is called _support-reflecting_ if for every
$x^{\prime}\in M^{\prime}$ there exists an $x\in M$ with $q(x)=x^{\prime}$ and
$\mathop{\mathsf{supp}}_{M}(x)=\mathop{\mathsf{supp}}_{M^{\prime}}(x^{\prime})$.
The following result characterizes the quotient monoids of $\Sigma^{*}$ in
terms of unary operations:

######  Proposition 3.1 (Unary presentation for nominal monoids).

For every nominal set $\Sigma$ and every surjective equivariant map
$e\colon\Sigma^{*}\twoheadrightarrow M$, the following statements are
equivalent:

  1. (1)

$e$ carries a quotient monoid of $\Sigma^{*}$, i.e. there exists a nominal
monoid structure $(M,\bullet,1_{M})$ on $M$ such that
$e\colon\Sigma^{*}\twoheadrightarrow(M,\bullet,1_{M})$ is a morphism of
nominal monoids;

  2. (2)

the maps $\Sigma^{*}\xrightarrow{w\cdot\mathord{-}}\Sigma^{*}$ and
$\Sigma^{*}\xrightarrow{\mathord{-}\cdot w}\Sigma^{*}$ $(w\in\Sigma^{*})$ lift
along $e$, i.e. there exist (necessarily unique) maps $l_{w}$ and $r_{w}$
making the following squares commute:

$\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
9.25938pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{e}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-21.65132pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\lower-1.99997pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
12.65706pt\raise 4.55556pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.55556pt\hbox{$\scriptstyle{w\cdot\mathord{-}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.78055pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
32.78055pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
40.79166pt\raise-15.74231pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{e}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
40.79166pt\raise-21.65132pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern
0.0pt\lower-1.99997pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.797pt\raise-37.34573pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.0pt\hbox{$\scriptstyle{l_{w}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
32.39583pt\raise-31.48463pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern
32.39583pt\raise-31.48463pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{M}$}}}}}}}\ignorespaces}}}}\ignorespaces}\qquad\qquad\vbox{
\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
9.25938pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{e}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-21.65132pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\lower-1.99997pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
12.65706pt\raise 4.55556pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.55556pt\hbox{$\scriptstyle{\mathord{-}\cdot w}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 32.78055pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
32.78055pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
40.79166pt\raise-15.74231pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{e}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
40.79166pt\raise-21.65132pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern
0.0pt\lower-1.99997pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.23392pt\raise-36.42213pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.07639pt\hbox{$\scriptstyle{r_{w}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
32.39583pt\raise-31.48463pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern
32.39583pt\raise-31.48463pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{M}$}}}}}}}\ignorespaces}}}}\ignorespaces}\qquad\qquad\text{for
every $w\in\Sigma^{*}$}.$

In general, the maps $w\cdot\mathord{-}$ and $\mathord{-}\cdot w$ are not
equivariant, but finitely supported (with support contained in the one of
$w$). This implies that also $l_{w}$ and $r_{w}$ in (2) are finitely
supported.

###  3.1 Equational Theories

In previous work [16] we studied varieties of objects in a general category
and their relation to an abstract form of equations. In the following, we
instantiate these concepts to the category of nominal sets to derive a
characterization of pseudovarieties of orbit-finite monoids.

######  Definition 1.

Let $\Sigma$ be a nominal set. A _$\Sigma$ -generated nominal monoid_ is a
nominal quotient monoid $e\colon\Sigma^{*}\twoheadrightarrow M$ of the free
monoid $\Sigma^{*}$. We denote by
$\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}$
the poset of $\Sigma$-generated orbit-finite nominal monoids, ordered by
$e\leq e^{\prime}$ iff $e^{\prime}$ factorizes through $e$.

######  Definition 2.

A _local pseudovariety of $\Sigma$-generated nominal monoids_ is a filter
$\mathscr{T}_{\Sigma}\subseteq\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}$
in the poset of $\Sigma$-generated orbit-finite nominal monoids; that is,
$\mathscr{T}_{\Sigma}$ is

  1. (1)

_upwards closed:_ $e\in\mathscr{T}_{\Sigma}$ and $e\leq e^{\prime}$ implies
$e^{\prime}\in\mathscr{T}_{\Sigma}$, and

  2. (2)

_downwards directed:_ for each pair $e_{0},e_{1}\in\mathscr{T}_{\Sigma}$ there
exists $e\in\mathscr{T}_{\Sigma}$ with $e\leq e_{0},e_{1}$.

If we replace (1) by the weaker condition

  1. (1’)

for each $e\colon\Sigma^{*}\twoheadrightarrow M$ in $\mathscr{T}_{\Sigma}$ and
each support-reflecting $q\colon M\twoheadrightarrow N$ one has $q\cdot
e\in\mathscr{T}_{\Sigma}$,

then $\mathscr{T}_{\Sigma}$ is called a _weak local pseudovariety of
$\Sigma$-generated nominal monoids_.

######  Remark 3.

By 3.1, the definition of local pseudovariety can be equivalently stated as
follows:

  1. (1)

$\mathscr{T}_{\Sigma}$ is a filter in the poset of orbit-finite quotients of
$\Sigma^{*}$ in $\mathbf{Nom}$;

  2. (2)

for every $e\in\mathscr{T}_{\Sigma}$ and $w\in\Sigma^{*}$, the unary
operations $w\cdot\mathord{-}$ and $\mathord{-}\cdot w$ on $\Sigma^{*}$ lift
along $e$.

Let $\mathbf{Nom}_{\mathsf{of,s}}$ denote the full subcategory of
$\mathbf{Nom}$ on orbit-finite strong nominal sets.

######  Definition 4 (Equational Theory).

A _(weak) equational theory_ is a family

$\mathscr{T}=(\,\mathscr{T}_{\Sigma}\subseteq\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}}$

of (weak) local pseudovarieties with the following two properties (see the
diagrams below):

  1. (1)

_Substitution invariance._ For each equivariant monoid morphism
$h\colon\Delta^{*}\to\Sigma^{*}$ with
$\Delta,\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}$ and each
$e_{\Sigma}\colon\Sigma^{*}\twoheadrightarrow M_{\Sigma}$ in
$\mathscr{T}_{\Sigma}$, the coimage $e_{\Delta}$ of $e_{\Sigma}\cdot h$ lies
in $\mathscr{T}_{\Delta}$.

  2. (2)

_Completeness._ For each $\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}$ and each
quotient $e\colon\Sigma^{*}\twoheadrightarrow M_{\Sigma}$ in
$\mathscr{T}_{\Sigma}$, there exists $\Delta\in\mathbf{Nom}_{\mathsf{of,s}}$
and a support-reflecting quotient
$e_{\Delta}\colon\Delta^{*}\twoheadrightarrow M_{\Delta}$ in
$\mathscr{T}_{\Delta}$ with $M_{\Delta}=M_{\Sigma}$.

$\textstyle{\Delta^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
h}$$\scriptstyle{e_{\Delta}}$$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
e_{\Sigma}}$$\textstyle{M_{\Delta}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M_{\Sigma}}$
$\textstyle{\Delta^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists
e_{\Delta}}$$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
e_{\Sigma}}$$\textstyle{M_{\Delta}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{M_{\Sigma}}$

######  Remark 5.

  1. (1)

Local pseudovarieties were previously called _equations_ [16]. In fact, in
many instances of the framework in _op. cit._ , a filter of quotients can be
represented as a single quotient of a free algebra on an object $\Sigma$,
which in turn corresponds to a set of pairs of terms given by the kernel of
the quotient, i.e. to the usual syntactic concept of an equation.

  2. (2)

The restriction to _strong_ nominal sets $\Sigma$ as generators reflects that
the latter are the “free” nominal sets [12], a property crucial for the proof
of Theorem 3.2 below. More precisely, letting $\mathcal{P}_{f}\mathbb{A}$
denote the set of finite subsets of $\mathbb{A}$, the forgetful functor
$U\colon\mathbf{Nom}\to\mathbf{Set}^{\mathcal{P}_{f}\mathbb{A}}$ mapping a
nominal set $X$ to the presheaf $S\mapsto\\{\,x\in
X\;\mathrel{\mathop{\mathchar
58\relax}}\;\mathop{\mathsf{supp}}_{X}(x)\subseteq S\,\\}$ has a left adjoint
$F$, and strong nominal sets are exactly the nominal sets of the form $FP$ for
$P\in\mathbf{Set}^{\mathcal{P}_{f}\mathbb{A}}$.

  3. (3)

The somewhat technical completeness property cannot be avoided, i.e. a
substitution-invariant family of local pseudovarieties is generally
incomplete. Indeed, consider the family

$\mathscr{T}=(\,\mathscr{T}_{\Sigma}\subseteq\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}},$

where $\mathscr{T}_{\Sigma}$ consists of all $\Sigma$-generated orbit-finite
nominal monoids $e\colon\Sigma^{*}\twoheadrightarrow M$ such that $e$ maps
each element of $\Sigma^{*}$ with a support of size $1$ to $1_{M}$.

To see that $\mathscr{T}_{\Sigma}$ is a filter, suppose that
$e\colon\Sigma^{*}\twoheadrightarrow M$ and
$e^{\prime}\colon\Sigma^{*}\twoheadrightarrow M^{\prime}$ are two quotients in
$\mathscr{T}_{\Sigma}$. Form their subdirect product $q$, viz. the coimage of
the morphism $\langle e,e^{\prime}\rangle\colon\Sigma^{*}\to M\times
M^{\prime}$. Each $w\in\Sigma^{*}$ with a support of size $1$ is mapped by $q$
to $(e(w),e^{\prime}(w))=(1_{M},1_{M^{\prime}})=1_{M\times M^{\prime}}$. Thus
$q\in\mathscr{T}_{\Sigma}$ and $q\leq e,e^{\prime}$, i.e.
$\mathscr{T}_{\Sigma}$ is downwards directed. Clearly, $\mathscr{T}_{\Sigma}$
is also upwards closed.

For substitution invariance, let $h\colon\Delta^{*}\to\Sigma^{*}$ be a
morphism and $e_{\Sigma}\colon\Sigma^{*}\twoheadrightarrow M_{\Sigma}$ a
quotient in $\mathscr{T}_{\Sigma}$. Then $e_{\Sigma}\cdot h$ maps each element
with a support of size $1$ to $1_{M_{\Sigma}}$ since $e_{\Sigma}$ does and the
equivariant map $h$ does not increase supports. Thus, the coimage of
$e_{\Sigma}\cdot h$ lies in $\mathscr{T}_{\Delta}$.

Finally, we show that $\mathscr{T}$ is not complete. Fix an arbitrary orbit-
finite nominal monoid $M$ containing an element $m$ with
${|\mathop{\mathsf{supp}}_{M}{m}|}=1$. Note that $m\neq 1_{M}$ because $1_{M}$
has empty support. Moreover, choose an orbit-finite strong nominal set
$\Sigma$ such that all elements of $\Sigma$ have least support of size at
least $2$, and $M$ can be expressed as a quotient
$e\colon\Sigma^{*}\twoheadrightarrow M$. (For instance, one may take
$\Sigma=\coprod_{i<k}\mathbb{A}^{\\#n}$ where $k$ is the number of orbits of
$M$ and
$n=\max\\{2,{|\mathop{\mathsf{supp}}_{M}(x)|}\mathrel{\mathop{\mathchar
58\relax}}x\in M\\}$.) Since all nonempty words in $\Sigma^{*}$ have a least
support of size at least $2$, one has $e\in\mathscr{T}_{\Sigma}$. For every
$\Delta\in\mathbf{Nom}_{\mathsf{of,s}}$ and every quotient
$q\colon\Delta^{*}\twoheadrightarrow M$ in $\mathscr{T}_{\Delta}$, the set
$q^{-1}[\\{m\\}]\subseteq\Delta^{*}$ contains no element with least support of
size $1$, since such elements are mapped by $q$ to $1_{M}\neq m$.
Consequently, $q$ is not support-reflecting. This shows that $M$ is not the
codomain of any support-reflecting quotient in $\mathscr{T}_{\Delta}$.

######  Definition 6 (Pseudovariety and Weak Pseudovariety).

A _pseudovariety of nominal monoids_ is a nonempty class $\mathscr{V}$ of
orbit-finite nominal monoids closed under finite products, submonoids, and
quotient monoids. That is,

  1. (1)

for each $M,N\in\mathscr{V}$ one has $M\times N\in\mathscr{V}$;

  2. (2)

for each $M\in\mathscr{V}$ and each nominal submonoid $N\rightarrowtail M$ one
has $N\in\mathscr{V}$;

  3. (3)

for each $M\in\mathscr{V}$ and each nominal quotient monoid
$M\twoheadrightarrow N$ one has $N\in\mathscr{V}$.

A _weak pseudovariety of nominal monoids_ is a nonempty class of orbit-finite
nominal monoids closed under finite products, submonoids, and support-
reflecting quotient monoids.

The following result is a special case of the Generalized Variety Theorem [16,
Theorem 3.15]. It asserts that equational theories and pseudovarieties are
equivalent concepts. Note that (weak) equational theories form a poset ordered
by $\mathscr{T}\leq\mathscr{T}^{\prime}$ iff
$\mathscr{T}_{\Sigma}\leq\mathscr{T}^{\prime}_{\Sigma}$ for all
$\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}$, where
$\mathscr{T}_{\Sigma}\leq\mathscr{T}^{\prime}_{\Sigma}$ holds iff for every
$e^{\prime}\in\mathscr{T}^{\prime}_{\Sigma}$ there exists an
$e\in\mathscr{T}_{\Sigma}$ with $e\leq e^{\prime}$. Similarly, (weak)
pseudovarieties of nominal monoids form a poset w.r.t. the inclusion ordering.

######  Theorem 3.2.

(Weak) equational theories and (weak) pseudovarieties of nominal monoids form
dually isomorphic complete lattices.

The isomorphism maps a (weak) equational theory $\mathscr{T}$ to the (weak)
pseudovariety $\mathscr{V}(\mathscr{T})$ of all orbit-finite monoids $M$ such
that each morphism $h\colon\Sigma^{*}\to M$ with
$\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}$ factorizes through some
$e_{\Sigma}\in\mathscr{T}_{\Sigma}$. The inverse maps a (weak) pseudovariety
$\mathscr{V}$ to the (weak) equational theory $\mathscr{T}(\mathscr{V})$ where
$\mathscr{T}(\mathscr{V})_{\Sigma}$ consists of all quotients
$e\colon\Sigma^{*}\twoheadrightarrow M$ with codomain $M\in\mathscr{V}$.

###  3.2 The Nominal Eilenberg-Schützenberger Theorem

In addition to their abstract category theoretic characterization in Theorem
3.2, weak pseudovarieties of nominal monoids admit an axiomatic description in
terms of sequences of equations, analogous to the classical result of
Eilenberg and Schützenberger [8] for pseudovarieties of ordinary monoids. The
appropriate concept of equation is as follows:

######  Definition 7.

  1. (1)

An _equation_ is a pair $(s,t)\in X^{*}\times X^{*}$, denoted as $s=t$, where
$X$ is an orbit-finite strong nominal set. A nominal monoid $M$ _satisfies_
$s=t$ if for every equivariant map $h\colon X\to M$ one has
$\widehat{h}(s)=\widehat{h}(t)$, where $\widehat{h}\colon X^{*}\to M$ denotes
the unique extension of $h$ to an equivariant monoid morphism.

  2. (2)

Given a sequence $E=(s_{n}=t_{n})_{n\in\mathds{N}}$ of equations (possibly
taken over different orbit-finite strong nominal sets $X$ of generators), a
nominal monoid $M$ _eventually satisfies_ $E$ if there exists an index
$n_{0}\in\mathds{N}$ such that $M$ satisfies all the equations $s_{n}=t_{n}$
with $n\geq n_{0}$. We denote by $\mathscr{V}(E)$ the class of all orbit-
finite nominal monoids that eventually satisfy $E$.

######  Remark 8.

Equations can be presented syntactically as expressions of the form

$y_{1}\mathrel{\mathop{\mathchar
58\relax}}S_{1},\ldots,y_{n}\mathrel{\mathop{\mathchar 58\relax}}S_{n}\vdash
u=v,$ (1)

where $Y=\\{y_{1},\ldots,y_{n}\\}$ is a finite set of variables,
$S_{1},\ldots,S_{n}\subseteq\mathbb{A}$ are finite sets of atoms, and $u,v$
are words in $(\mathrm{Perm}(\mathbb{A})\times Y)^{*}$. A nominal monoid $M$
is said to _satisfy_ (1) if for every _variable interpretation_ , i.e. every
map $h\colon Y\to M$ with $\mathop{\mathsf{supp}}_{M}(h(y_{i}))\subseteq
S_{i}$ for $i=1,\ldots,n$, one has $\overline{h}(u)=\overline{h}(v)$. Here,
$\overline{h}\colon(\mathrm{Perm}(\mathbb{A})\times Y)^{*}\to M$ is the unique
monoid morphism mapping $(\pi,y_{i})$ to $\pi\cdot h(y_{i})$. Every equation
can be transformed into an expressively equivalent syntactic equation, and
vice versa [15, Lemma B.31].

######  Theorem 3.3 (Nominal Eilenberg-Schützenberger Theorem).

A class $\mathscr{V}$ of orbit-finite nominal monoids forms a weak
pseudovariety iff $\mathscr{V}=\mathscr{V}(E)$ for some sequence $E$ of
equations.

######  Proof 3.4 (Proof sketch).

The proof proceeds along the lines of the one for ordinary monoids [8],
although some subtle modifications are required. The “if” direction is a
routine verification. For the “only if” direction, let $\mathscr{V}$ be a weak
pseudovariety. Using that there are only countably many orbit-finite monoids
up to isomorphism, one can construct a sequence $M_{0},M_{1},M_{2},\ldots$ of
nominal monoids in $\mathscr{V}$ such that each $M\in\mathscr{V}$ is a
quotient of all but finitely many $M_{n}$’s. Let $X_{0},X_{1},X_{2},\ldots$ be
the sequence of all (countably many) strong orbit-finite nominal sets up to
isomorphism, and consider the equivariant congruence relation on $X_{n}^{*}$
given by

$s\equiv_{n}t\quad\text{iff}\quad\text{$M_{n}$ satisfies the equation $s=t$.}$

One then shows that the congruence $\equiv_{n}$ is generated by a finite
subset $W_{n}\subseteq\mathord{\equiv_{n}}$, and that
$\mathscr{V}=\mathscr{V}(E)$ for every sequence $E$ that lists all equations
in the countable set $\bigcup_{n}W_{n}$.

######  Example 3.5.

An orbit-finite nominal monoid $M$ is called _aperiodic_ [6, 19] if there
exists a natural number $n\geq 1$ such that $x^{n+1}=x^{n}$ for all $x\in M$.
The class of all orbit-finite aperiodic nominal monoids forms a pseudovariety.
Taking the set $Y=\\{y\\}$ of variables, it is not difficult to see that this
pseudovariety is specified by the sequence of syntactic equations

$y\mathrel{\mathop{\mathchar 58\relax}}S_{n}\vdash
y^{n+1}=y^{n}\qquad(n\in\mathds{N}),$

where $S_{n}=\\{a_{0},a_{1},\ldots,a_{n-1}\\}$ is the set of the first $n$
atoms in the countably infinite set $\mathbb{A}=\\{a_{0},a_{1},a_{2}\ldots\\}$
of all atoms, and we write $y$ for
$(\mathit{id},y)\in\mathrm{Perm}(\mathbb{A})\times Y$.

##  4 Duality and the Nominal Eilenberg Correspondence

In this section, we establish our nominal version of Eilenberg’s variety
theorem. It is based on a dual interpretation of the concepts of a (local)
pseudovariety of nominal monoids and of an equational theory, introduced in
the previous section, under _nominal Stone duality_.

###  4.1 Nominal Stone Duality

A classical result from duality theory, known as _discrete Stone duality_ ,
states that the category of sets is dually equivalent to the category of
complete atomic boolean algebras, i.e. complete boolean algebras in which
every non-zero element is above some atom. An analogous duality holds for the
category $\mathbf{Nom}_{\mathsf{fs}}$ of nominal sets and finitely supported
maps.

######  Definition 9.

A _nominal complete atomic boolean algebra_ (_ncaba_) is a boolean algebra
$(B,\vee,\wedge,\neg,\bot,\top)$ in $\mathbf{Nom}$ such that every finitely
supported subset of $B$ has a supremum, and for every element $b\in
B\setminus\\{\bot\\}$ there exists an atom (i.e. a minimal element) $a\in B$
with $a\leq b$. Here, the partial order $\leq$ is defined as usual by $a\leq
b$ iff $a\wedge b=a$. We denote by $\mathbf{nCABA}_{\mathsf{fs}}$ the category
of ncabas and finitely supported morphisms (i.e. finitely supported maps
preserving all the boolean operations and suprema of finitely supported
subsets), and by $\mathbf{nCABA}$ the (non-full) subcategory of ncabas and
_equivariant_ morphisms.

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

The categories $\mathbf{nCABA}_{\mathsf{fs}}$ and $\mathbf{Nom}_{\mathsf{fs}}$
are dually equivalent. The duality restricts to one between the subcategories
$\mathbf{nCABA}$ and $\mathbf{Nom}$.

The restricted duality is due to Petrişan [17, Prop. 5.3.11].

######  Remark 10.

  1. (1)

The equivalence functor
$\mathbf{Nom}_{\mathsf{fs}}\xrightarrow{\simeq}\mathbf{nCABA}_{\mathsf{fs}}^{\mathsf{op}}$
maps a nominal set $X$ to the ncaba $\mathcal{P}X$ of finitely supported
subsets of $X$ (equipped with the set-theoretic boolean operations), and a
finitely supported map $f\colon X\to Y$ to the morphism
$f^{-1}\colon\mathcal{P}Y\to\mathcal{P}X$ taking preimages. The inverse
equivalence functor
$\mathbf{nCABA}_{\mathsf{fs}}^{\mathsf{op}}\xrightarrow{\simeq}\mathbf{Nom}_{\mathsf{fs}}$
maps an ncaba $B$ to the equivariant subset $\mathsf{At}(B)$ of its atoms,
with group action restricting the one of $B$.

  2. (2)

The dual equivalence restricts to one between the full subcategories of orbit-
finite nominal sets and _atom-finite_ ncabas, i.e. ncabas whose set of atoms
is orbit-finite. For atom-finite ncabas the property that every finitely
supported subset has a supremum is equivalent to the weaker requirement that
for every finite set $S\subseteq\mathbb{A}$, every $S$-orbit has a supremum.
Indeed, given a finitely supported subset $X\subseteq B$ (say with finite
support $S\subseteq\mathbb{A}$), put $X^{\prime}\mathrel{\mathop{\mathchar
58\relax}}=\\{\,a\in\mathsf{At}(B)\mathrel{\mathop{\mathchar 58\relax}}a\leq
x\text{ for some $x\in X$}\,\\}$. Since $\leq$ is an equivariant relation,
$X^{\prime}\subseteq\mathsf{At}(B)$ is a subset with finite support $S$. Since
$\mathsf{At}(B)$ is orbit-finite and thus has only finitely many $S$-orbits by
2.1, we can express $X^{\prime}$ as a finite union
$X^{\prime}=X_{1}^{\prime}\cup\ldots\cup X_{n}^{\prime}$ of $S$-orbits. Using
that every element of $B$ is the join of the finitely supported set of all
atoms below it, it follows that $\bigvee X=\bigvee X^{\prime}=\bigvee
X_{1}^{\prime}\vee\ldots\vee\bigvee X_{n}^{\prime}$, so $\bigvee X$ is a
finite join of joins of $S$-orbits.

###  4.2 Varieties of Data Languages

For the notion of a _language_ over an alphabet $\Sigma\in\mathbf{Nom}$ and
the corresponding concept of algebraic recognition by nominal monoids, there
are two natural choices: consider equivariant subsets $L\subseteq\Sigma^{*}$
and their recognition by equivariant monoid morphisms [5, 19], or consider
finitely supported subsets $L\subseteq\Sigma^{*}$ and their recognition by
finitely supported monoid morphisms [6]. For our duality-based approach to
data languages, it turns out that we need to work with an intermediate
concept: finitely supported languages recognizable by equivariant monoid
morphisms (see the discussion in Remark 15 below). That is, we work with the
following

######  Definition 11.

A _data language_ over the alphabet $\Sigma\in\mathbf{Nom}$ is a finitely
supported map $L\colon\Sigma^{*}\to 2$. It is _recognized_ by an equivariant
monoid morphism $e\colon\Sigma^{*}\to M$ if there exists a finitely supported
map $p\colon M\to 2$ with $L=p\cdot e$. In this case, we also say that $M$
_recognizes_ $L$. A data language is _recognizable_ if it recognized by some
orbit-finite nominal monoid.

######  Remark 12.

  1. (1)

Identifying finitely supported maps into $2$ with finitely supported subsets,
Definition 11 can be restated: an equivariant monoid morphism
$e\colon\Sigma^{*}\to M$ _recognizes_ a language $L\subseteq\Sigma^{*}$ if
there exists a finitely supported subset $P\subseteq M^{*}$ with
$L=e^{-1}[P]$.

  2. (2)

If $L$ is an equivariant recognizable language, then $p$ in Definition 11 is
also equivariant. Therefore, for equivariant languages we recover the notion
of recognition of [5, 19].

  3. (3)

If $\Sigma$ is a finite set (viewed as an orbit-finite discrete nominal set),
a data language is just an ordinary formal language over the alphabet
$\Sigma$. Indeed, the free nominal monoid $\Sigma^{*}$ is discrete, and thus
every subset of $\Sigma^{*}$ is finitely supported. Moreover, every orbit-
finite nominal quotient monoid of $\Sigma^{*}$ is discrete and finite. Hence,
the above notion of language recognition coincides with the classical
recognition by finite monoids. In particular, for finite $\Sigma$, a
recognizable data language is the same as a regular language.

######  Example 4.2.

Examples of recognizable data languages over the alphabet $\Sigma=\mathbb{A}$
include (1) every finite or cofinite subset $L\subseteq\mathbb{A}^{*}$ (see
Remark 14 below), (2) $a\mathbb{A}^{*}$ for a fixed atom $a\in\mathbb{A}$, and
(3) $\bigcup_{a\in\mathbb{A}}\mathbb{A}^{*}aa\mathbb{A}^{*}$. The languages
(4) $\\{a_{1}\ldots a_{n}\;\mathrel{\mathop{\mathchar 58\relax}}\;a_{i}\neq
a_{j}\text{ for }i\neq j\\}$, (5)
$\bigcup_{a\in\mathbb{A}}a\mathbb{A}^{*}a\mathbb{A}^{*}$, and (6)
$\mathbb{A}^{*}a\mathbb{A}^{*}$ for a fixed atom $a\in\mathbb{A}$ are not
recognizable. The equivariant examples (3)–(5) are taken from [6, 5].

In previous work [1] we have given a categorical account of _local varieties
of regular languages_ [10], i.e. sets of regular languages over a fixed finite
alphabet $\Sigma$ closed under the set-theoretic boolean operations (finite
union, finite intersection, complement) and derivatives. This concept can be
generalized to data languages. The _derivatives_ of a data language
$L\subseteq\Sigma^{*}$ with respect to a word $w\in\Sigma^{*}$ are given by

$w^{-1}L=\\{\,v\in\Sigma^{*}\;\mathrel{\mathop{\mathchar 58\relax}}\;wv\in
L\,\\}\quad\text{and}\quad
Lw^{-1}=\\{\,v\in\Sigma^{*}\;\mathrel{\mathop{\mathchar 58\relax}}\;vw\in
L\,\\}.$

Since
$\mathop{\mathsf{supp}}(w^{-1}L),\mathop{\mathsf{supp}}(Lw^{-1})\subseteq\mathop{\mathsf{supp}}(w)\cup\mathop{\mathsf{supp}}(L)$,
the derivatives are again data languages.

######  Definition 13 (Local Variety of Data Languages).

Let $\Sigma\in\mathbf{Nom}$. A _local variety of data languages over $\Sigma$_
is an equivariant set $\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}$ of
recognizable data languages closed under the set-theoretic boolean operations,
unions of $S$-orbits for every finite set $S\subseteq\mathbb{A}$ of atoms
(that is, for every $L\in\mathcal{V}_{\Sigma}$ the language
$\bigcup_{\pi\in\mathrm{Perm}_{S}(\mathbb{A})}\pi\cdot L$ lies in
$\mathcal{V}_{\Sigma}$), and derivatives.

######  Remark 14.

  1. (1)

If $\Sigma$ is a finite set (viewed as a discrete nominal set), then by Remark
12 a local variety $\mathcal{V}_{\Sigma}$ consists of regular languages, and
the closure under unions of $S$-orbits is trivial: since
$\mathcal{P}\Sigma^{*}$ is discrete, every $S$-orbit has a single element.
Thus, in this case, a local variety of data languages is precisely a local
variety of regular languages.

  2. (2)

However, in general the closedness under unions of $S$-orbits cannot be
dropped, as it is neither trivial nor implied by the other conditions. To see
this, consider the alphabet $\Sigma=\mathbb{A}$ and the equivariant set
$\mathcal{V}_{\mathbb{A}}\subseteq\mathcal{P}\mathbb{A}^{*}$ of all finite or
cofinite subsets of $\mathbb{A}^{*}$. Note that every finite language
$L\subseteq\mathbb{A}^{*}$ is recognizable: let $n\geq 1$ be an upper bound on
the length of words in $L$, and take the orbit-finite monoid
$M=\mathbb{A}^{\leq n}\cup\\{0\\}$ consisting of all words over $\mathbb{A}$
of length at most $n$, and a zero element $0$. The multiplication $\bullet$ is
defined as follows: given $v,w\in\mathbb{A}^{\leq n}$, if the word $vw$ has
length at most $n$, put $v\bullet w=vw$. Otherwise, put $v\bullet w=0$. Then
the equivariant monoid morphism $e\colon\mathbb{A}^{*}\to M$ extending
$a\mapsto a$ recognizes $L$ since $L=e^{-1}[L]$. It follows that also
$\mathbb{A}^{*}\setminus L=e^{-1}[M\setminus L]$. This shows that every
language in $\mathcal{V}_{\mathbb{A}}$ is recognizable. Moreover, clearly
$\mathcal{V}_{\mathbb{A}}$ is closed under the set-theoretic boolean
operations and derivatives. However, the languages $\\{a\\}$,
$a\in\mathbb{A}$, form an orbit in $\mathcal{V}_{\mathbb{A}}$, but their union
$\mathbb{A}=\bigcup_{a\in\mathbb{A}}\\{a\\}$ is not in
$\mathcal{V}_{\mathbb{A}}$. Thus $\mathcal{V}_{\mathbb{A}}$ is not a local
variety of data languages in the sense of Definition 13.

A local variety $\mathcal{V}_{\Sigma}$ is generally not a subobject of
$\mathcal{P}\Sigma^{*}$ in $\mathbf{nCABA}$, because it is not required to be
closed under unions of arbitrary finitely supported subsets and also not
necessarily atomic as a boolean algebra. However, if the atomic languages in
$\mathcal{V}_{\Sigma}$ form an orbit-finite subset and every language in
$\mathcal{V}_{\Sigma}$ contains some atomic language, then
$\mathcal{V}_{\Sigma}$ is an atom-finite subobject of $\mathcal{P}\Sigma^{*}$,
see Remark 10(2). In this case, we call $\mathcal{V}_{\Sigma}$ an _atom-
finite_ local variety.

######  Theorem 4.3 (Finite Local Variety Theorem).

The lattice of atom-finite local varieties of data languages over $\Sigma$ is
dually isomorphic to the lattice of $\Sigma$-generated orbit-finite monoids.

The isomorphism maps a $\Sigma$-generated orbit-finite monoid
$e\colon\Sigma^{*}\twoheadrightarrow M$ to the atom-finite local variety of
all data languages recognized by $e$.

######  Proof 4.4.

By the duality of $\mathbf{Nom}$ and $\mathbf{nCABA}$, orbit-finite
equivariant quotients $e\colon\Sigma^{*}\twoheadrightarrow M$ of $\Sigma^{*}$
in $\mathbf{Nom}$ correspond bijectively to atom-finite subobjects
$\mathcal{V}_{\Sigma}\rightarrowtail\mathcal{P}\Sigma^{*}$ in
$\mathbf{nCABA}$, i.e. atom-finite equivariant sets of languages closed under
the set-theoretic boolean operations and unions of $S$-orbits for every finite
$S\subseteq\mathbb{A}$. By 3.1 and the dual equivalence of
$\mathbf{Nom}_{\mathsf{fs}}$ and $\mathbf{nCABA}_{\mathsf{fs}}$, the map $e$
represents a nominal quotient monoid of $\Sigma^{*}$ if and only if
$\mathcal{V}_{\Sigma}$ is closed under derivatives, i.e. a local variety. The
closure under left derivatives is illustrated by the two dual commutative
squares below, where the left-hand one lives in $\mathbf{Nom}_{\mathsf{fs}}$
and the right-hand one in $\mathbf{nCABA}_{\mathsf{fs}}$.

$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{w\cdot\mathord{-}}$$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists}$$\textstyle{M}$
$\textstyle{\mathcal{P}\Sigma^{*}}$$\textstyle{\mathcal{P}\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{w^{-1}(\mathord{-})}$$\textstyle{\mathcal{V}_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq}$$\textstyle{\mathcal{V}_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists}$$\scriptstyle{\subseteq}$

The elements of $\mathcal{V}_{\Sigma}$ are precisely the languages recognized
by $e$. Indeed, the former correspond to the morphisms
$\mathds{1}\to\mathcal{V}_{\Sigma}$ in $\mathbf{nCABA}_{\mathsf{fs}}$, where
$\mathds{1}$ is the free boolean algebra on one generator, the latter to the
finitely supported maps $M\to 2$ in $\mathbf{Nom}_{\mathsf{fs}}$, and
$\mathds{1}$ and $2$ are dual objects.

Recall that an _ideal_ in a poset is a downwards closed and upwards directed
subset. For the lattice of local varieties of data languages over $\Sigma$
(ordered by inclusion), we obtain

######  Lemma 4.5.

The lattice of local varieties of data languages over $\Sigma$ is isomorphic
to the lattice of ideals in the poset of atom-finite local varieties over
$\Sigma$.

The isomorphism maps a local variety $\mathcal{V}_{\Sigma}$ to the ideal of
all atom-finite local subvarieties of $\mathcal{V}_{\Sigma}$. Its inverse maps
an ideal $\\{\,\mathcal{V}_{\Sigma,i}\mathrel{\mathop{\mathchar 58\relax}}i\in
I\,\\}$ in the poset of atom-finite local varieties to the local variety
$\bigcup_{i\in I}\mathcal{V}_{\Sigma,i}$. In order-theoretic terms, the above
lemma states that local varieties of data languages form the ideal completion
of the poset of atom-finite local varieties. Using Theorem 4.3, 4.5, and the
fact that ideals are dual to filters, we obtain

######  Theorem 4.6 (Local Variety Theorem).

For each $\Sigma\in\mathbf{Nom}$, the lattice of local varieties of data
languages over $\Sigma$ is dually isomorphic to the lattice of local
pseudovarieties of $\Sigma$-generated nominal monoids.

######  Remark 15.

  1. (1)

Since data languages are morphisms $L\colon\Sigma^{*}\to 2$ in
$\mathbf{Nom}_{\mathsf{fs}}$, the reader may wonder why we do not entirely
work in this category and use monoids with finitely supported multiplication
and finitely supported monoid morphisms (rather than the equivariant ones) for
the recognition of languages. The reason lies on the dual side: in the proof
of Theorem 4.3, we used that equivariant injective maps
$\mathcal{V}_{\Sigma}\rightarrowtail\mathcal{P}\Sigma^{*}$ can be uniquely
identified with equivariant subsets of $\mathcal{P}\Sigma^{*}$. In contrast,
finitely supported injective maps
$\mathcal{V}_{\Sigma}\rightarrowtail\mathcal{P}\Sigma^{*}$ do not correspond
to the finitely supported (or any other kind of) subsets of
$\mathcal{P}\Sigma^{*}$.

  2. (2)

Similarly, we cannot restrict ourselves to the category $\mathbf{Nom}$ and
only consider equivariant languages $L\subseteq\Sigma^{*}$ rather than
finitely supported ones. Indeed, the Finite Local Variety Theorem then fails:
the map sending a $\Sigma$-generated orbit-finite monoid
$e\colon\Sigma^{*}\twoheadrightarrow M$ to the set of equivariant languages it
recognizes is no longer bijective. To see this, consider the nominal monoids
$M=\mathbb{A}\cup\\{1\\}$ with $a\bullet b=a$ for $a,b\in\mathbb{A}$, and
$N=\\{0,1\\}$ with $0\bullet 0=0\bullet 1=1\bullet 0=0$. Then the two
surjective morphisms $e\colon\mathbb{A}^{*}\twoheadrightarrow M$, extending
$a\mapsto a$, and $f\colon\mathbb{A}^{*}\twoheadrightarrow N$, extending
$a\mapsto 0$, recognize the same equivariant languages, namely
$\mathbb{A}^{*}$, $\mathbb{A}^{*}\setminus\\{\varepsilon\\}$,
$\\{\varepsilon\\}$ and $\emptyset$.

In the following, we consider data languages whose alphabet $\Sigma$ is an
orbit-finite strong nominal set (see Remark 5(2)). By dualizing the concept of
an equational theory, we obtain

######  Definition 16 (Variety of data languages).

A _variety of data languages_ is a family

$\mathcal{V}=(\,\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}}$

of local varieties of data languages with the following two properties:

  1. (1)

_Closedness under preimages._ For each equivariant monoid morphism
$h\colon\Delta^{*}\to\Sigma^{*}$ with
$\Sigma,\Delta\in\mathbf{Nom}_{\mathsf{of,s}}$ and each
$L\in\mathcal{V}_{\Sigma}$, one has $h^{-1}[L]\in\mathcal{V}_{\Delta}$.

  2. (2)

_Completeness._ For each atom-finite local subvariety
$\mathcal{V}^{\prime}_{\Sigma}\rightarrowtail\mathcal{V}_{\Sigma}$, there
exists an equivariant monoid morphism $h\colon\Sigma^{*}\to\Delta^{*}$ and an
atom-finite local subvariety
$\mathcal{V}^{\prime}_{\Delta}\rightarrowtail\mathcal{V}_{\Delta}$ such that

    1. (a)

the map $L\mapsto h^{-1}[L]$ defines a bijection between
$\mathcal{V}^{\prime}_{\Delta}$ and $\mathcal{V}^{\prime}_{\Sigma}$, and

    2. (b)

every atomic language $L\in\mathcal{V}^{\prime}_{\Delta}$ contains a word
$w\in\Delta^{*}$ with
$\mathop{\mathsf{supp}}_{\mathcal{P}\Delta^{*}}(L)=\mathop{\mathsf{supp}}_{\Delta^{*}}(w)$.

######  Remark 17.

Except for the completeness condition, the above concept is analogous to
Eilenberg’s original notion of a variety of regular languages (i.e. a family
of local varieties of regular languages closed under preimages of monoid
morphisms). In fact, if $\Sigma$ is a finite alphabet, and thus
$\mathcal{V}_{\Sigma}$ is just a local variety of regular languages,
completeness is trivial: given any finite local subvariety
$\mathcal{V}^{\prime}_{\Sigma}$ of $\mathcal{V}_{\Sigma}$, choose
$\Delta=\Sigma$,
$\mathcal{V}^{\prime}_{\Delta}=\mathcal{V}^{\prime}_{\Sigma}$, and
$h=\mathit{id}\colon\Sigma^{*}\to\Delta^{*}$. Then (2)(a) is clear, and (2)(b)
holds because each $L\in\mathcal{P}\Sigma^{*}$ and each $w\in\Sigma^{*}$ has
empty support.

In general, however, the completeness property cannot be dropped. This follows
from Remark 5(3) and the observation that the completeness of a variety
dualizes to the completeness of the corresponding equational theory (see the
proof of Theorem 4.7).

We are ready to state the main result of our paper:

######  Theorem 4.7 (Nominal Eilenberg Theorem).

Varieties of data languages and pseudovarieties of nominal monoids form
isomorphic complete lattices.

The isomorphism maps a variety $\mathcal{V}$ of data languages to the
pseudovariety $\mathscr{V}$ of all orbit-finite nominal monoids that recognize
only languages from $\mathcal{V}$. Its inverse maps a pseudovariety
$\mathscr{V}$ to the variety $\mathcal{V}$ of all data languages recognized by
some monoid in $\mathscr{V}$.

######  Proof 4.8 (Proof sketch).

We observe that the concept of a variety is dual to that of an equational
theory. Indeed, by the Local Variety Theorem 4.6, a family
$\mathcal{V}=(\,\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}}$
of local varieties of data languages bijectively corresponds to a family
$\mathscr{T}=(\,\mathscr{T}_{\Sigma}\subseteq\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}}$
of local pseudovarieties of nominal monoids. One then shows that (1)
$\mathscr{T}$ is substitution-invariant if and only if $\mathcal{V}$ is closed
under preimages, and (2) $\mathscr{T}$ is complete if and only if
$\mathcal{V}$ is complete. In particular, $\mathscr{T}$ is a theory if and
only if $\mathcal{V}$ is a variety of data languages. Since theories
correspond to pseudovarieties by Theorem 3.2, this proves the theorem.

##  5 Adding Expressivity: Regular Data Languages

As recognizing structures for data languages, nominal monoids are of limited
expressivity; in particular, they are strictly weaker than deterministic
automata in the category of nominal sets [5, 6]. Therefore, we now show how to
extend our results for monoid-recognizable data languages and establish a
local variety theorem for languages accepted by nominal automata.

######  Definition 18.

Fix an input alphabet $\Sigma\in\mathbf{Nom}$. A _nominal $\Sigma$-automaton_
$A=(Q,\delta,q_{0})$ consists of a nominal set $Q$ of states, an equivariant
transition map $\delta\colon Q\times\Sigma\to Q$, and an initial state
$q_{0}\in Q$ with empty support. It is called _orbit-finite_ if $Q$ is orbit-
finite. A _morphism_ between nominal automata $A=(Q,\delta,q_{0})$ and
$A^{\prime}=(Q^{\prime},\delta^{\prime},q_{0}^{\prime})$ is an equivariant map
$h\colon Q\to Q^{\prime}$ such that $\delta(h(q),a)=h(\delta(q,a))$ for all
$q\in Q$ and $a\in\Sigma$, and $h(q_{0})=q_{0}^{\prime}$.

The _initial nominal $\Sigma$-automaton_ is given by
$I=(\Sigma^{*},\delta,\varepsilon)$ with transition map $\delta(w,a)=wa$ for
$w\in\Sigma^{*}$ and $a\in\Sigma$. It is characterized by the universal
property that for every nominal $\Sigma$-automaton $A=(Q,\delta,q_{0})$, there
exists a unique morphism $e_{A}\colon I\to A$, sending a word $w\in\Sigma^{*}$
to the state reached from $q_{0}$ after reading $w$. The automaton $A$ is
called _reachable_ if $e_{A}$ is surjective. A data language
$L\subseteq\Sigma^{*}$ is _accepted_ by $A$ if there exists a finitely
supported subset $F\subseteq Q$ with $L=e_{A}^{-1}[F]$. This corresponds to
the usual notion of acceptance of an automaton with final states $F$: the
language $L$ consists of all words $w\in\Sigma^{*}$ such that $A$ reaches a
state in $F$ after reading $w$. A data language $L\subseteq\Sigma^{*}$ is
called _regular_ if there exists an orbit-finite nominal automaton accepting
it. In analogy to 3.1, we get

######  Proposition 5.1 (Unary presentation for nominal automata).

For every surjective equivariant map $e\colon\Sigma^{*}\twoheadrightarrow Q$,
the following statements are equivalent:

  1. (1)

there exists a nominal automaton $A=(Q,\delta,q_{0})$ with states $Q$ such
that $e=e_{A}$;

  2. (2)

the maps $\Sigma^{*}\xrightarrow{\mathord{-}\cdot w}\Sigma^{*}$
$(w\in\Sigma^{*})$ lift along $e$, i.e. there exist (necessarly unique) maps
$r_{w}\colon Q\to Q$ such that $e\cdot(\mathord{-}\cdot w)=r_{w}\cdot e$ for
all $w\in\Sigma^{*}$.

Define a _local pseudovariety of nominal $\Sigma$-automata_ to be a class
$\mathscr{V}_{\Sigma}$ of orbit-finite reachable nominal $\Sigma$-automata
such that (1) $\mathscr{V}_{\Sigma}$ is closed under quotients (represented by
surjective automata morphisms), and (2) for every pair
$A,B\in\mathscr{V}_{\Sigma}$, the reachable part of the product $A\times B$
lies in $\mathscr{V}_{\Sigma}$. Here, the product of two nominal automata
$A=(Q,\delta,q_{0})$ and $B=(Q^{\prime},\delta^{\prime},q_{0}^{\prime})$ is
given by $A\times B=(Q\times Q^{\prime},\delta,(q_{0},q_{0}^{\prime}))$ with
$\delta((q,q^{\prime}),a)=(\delta(q,a),\delta^{\prime}(q^{\prime},a))$ for
$(q,q^{\prime})\in Q\times Q^{\prime}$ and $a\in\Sigma$, and the reachable
part $R$ of $A\times B$ is the coimage $e\colon\Sigma^{*}\twoheadrightarrow R$
of the unique morphism $e_{A\times B}\colon\Sigma^{*}\to A\times B$. Note that
a local pseudovariety corresponds precisely to a filter in the poset
$\Sigma^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\Sigma\text{-}\mathbf{nAut}_{\mathsf{of}}$
of orbit-finite reachable nominal $\Sigma$-automata. The dual version of this
concept is the one of a _local variety of regular data languages over
$\Sigma$_: an equivariant set
$\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}$ of such languages closed
under the set-theoretic boolean operations, unions of $S$-orbits for every
finite set $S\subseteq\mathbb{A}$ of atoms, and _right_ derivatives. The
following theorem, and its proof, are completely analogous to Theorem 4.6:

######  Theorem 5.2 (Local Variety Theorem for Regular Data Languages).

For each $\Sigma\in\mathbf{Nom}$, the lattice of local varieties of regular
data languages over $\Sigma$ is dually isomorphic to the lattice of local
pseudovarieties of nominal $\Sigma$-automata.

##  6 Conclusions and Future Work

We have demonstrated that two cornerstones of the algebraic theory of regular
languages, Eilenberg’s variety theorem and Eilenberg and Schützenberger’s
axiomatic characterization of pseudovarieties, can be generalized to data
languages recognizable by orbit-finite monoids. Our results are the first of
this type for data languages, and thus the present work makes a contribution
towards developing a fully fledged algebraic theory of such languages. In a
broader sense, the approach taken in this paper can be seen as a further
illustration of the power of duality in formal language theory: we believe
that without the guidance given by nominal Stone duality, it would have been
significantly harder to even come up with the suitable notion of a variety of
data languages that makes the nominal Eilenberg correspondence work. The
duality-based approach thus adds much conceptual clarity and simplicity. There
remain several research questions and interesting directions for future work.

As indicated in section 5, the techniques used in our paper can be adapted
without much effort to languages recognized by nominal algebraic structures
other than monoids, including deterministic nominal automata. As a first step,
we aim to extend the local variety theorem for regular data languages (Theorem
5.2) to a full Eilenberg correspondence. It remains an important goal to
further extend our results to more powerful classes of data languages.

Our proof of the (local) Eilenberg correspondence rests on the observation
that a local variety of data languages can be expressed as the directed union
of its atom-finite subvarieties. From a category theoretic perspective, this
suggests that local varieties are formed within the _$\mathsf{Ind}$
-completion_ (i.e. the free completion under directed colimits) of the
category of atom-finite nominal complete atomic boolean algebras. We
conjecture that this completion can be described as a category of nominal
boolean algebras with joins of $S$-orbits for each finite set $S$ of atoms. On
the dual side, we expect that the _$\mathsf{Pro}$ -completion_ (i.e. the free
completion under codirected limits) of the category of orbit-finite nominal
sets consists of some form of nominal Stone spaces. The approach of working
with free completions should lead to a topological version of nominal Stone
duality similar to the one established by Gabbay, Litak, and Petrişan [9].
More importantly, it might pave the way to the introduction of
pro-(orbit-)finite methods for the theory of data languages.

## References

  * [1] Jiří Adámek, Stefan Milius, Robert S.R. Myers, and Henning Urbat.  Generalized Eilenberg Theorem I: Local Varieties of Languages.  In Anca Muscholl, editor, Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of Lecture Notes Comput. Sci., pages 366–380. Springer, 2014.
  * [2] Jiří Adámek, Stefan Milius, Robert S.R. Myers, and Henning Urbat.  Varieties of languages in a category.  In Catuscia Palamidessi, editor, Proc. 30th Annual Symposium on Logic in Computer Science (LICS’15), pages 414–425. IEEE Computer Society, 2015\.
  * [3] Jiří Adámek, Stefan Milius, Robert S.R. Myers, and Henning Urbat.  Generalized Eilenberg theorem: Varieties of languages in a category.  ACM Trans. Comput. Log., 20(1):3:1–3:47, 2019.
  * [4] Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann.  On finitary functors and finitely presentable algebras.  Submitted; available online at https://arxiv.org/abs/1902.05788.
  * [5] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Log. Methods Comput. Sci., 10(3:4):44 pp., 2014.
  * [6] Mikołaj Bojańczyk.  Nominal monoids.  Theory of Computing Systems, 53(2):194–222, 2013.
  * [7] Samuel Eilenberg.  Automata, Languages, and Machines Vol. B.  Academic Press, 1976.
  * [8] Samuel Eilenberg and Marcel-Paul Schützenberger.  On pseudovarieties.  Advances Math., 10:413–418, 1976.
  * [9] Murdoch J. Gabbay, Tadeusz Litak, and Daniela Petrişan.  Stone duality for nominal boolean algebras with new.  In A. Corradini, B. Klin, and C. Cîrstea, editors, Proc. CALCO’11, volume 6859 of LNCS, pages 192–207. Springer, 2011.
  * [10] Mai Gehrke, Serge Grigorieff, and Jean-Éric Pin.  Duality and equational theory of regular languages.  In Proc. ICALP’08, Part II, volume 5126 of LNCS, pages 246–257. Springer, 2008.
  * [11] Michael Kaminski and Nissim Francez.  Finite-memory automata.  Theoret. Comput. Sci., 134(2):329 – 363, 1994.
  * [12] Alexander Kurz and Daniela Petrisan.  On universal algebra over nominal sets.  Mathematical Structures in Computer Science, 20(2):285–318, 2010\.
  * [13] Robert McNaughton and Seymour A. Papert.  Counter-Free Automata (M.I.T. Research Monograph No. 65).  The MIT Press, 1971.
  * [14] Stefan Milius, Lutz Schröder, and Thorsten Wißmann.  Regular behaviours with names.  Appl. Categ. Structures, 24(5):663–701, 2016.
  * [15] Stefan Milius and Henning Urbat.  Equational axiomatization of algebras with structure.  Full version; available online at http://arxiv.org/abs/1812.02016, 2018.
  * [16] Stefan Milius and Henning Urbat.  Equational axiomatization of algebras with structure.  In Proc. 22nd International Conference on Foundations of Software Science and Computation Structures, 2019.  To appear.
  * [17] Daniela Petrişan.  Investigations into Algebra and Topology over Nominal Sets.  PhD thesis, University of Leicester, 2012.
  * [18] Andrew M. Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge University Press, 2013.
  * [19] Gabriele Puppis, Thomas Colcombet, and Clemens Ley.  Logics with rigidly guarded data tests.  Log. Methods Comput. Sci., 11(3:10):56 pp., 2015.
  * [20] Julian Salamanca.  Unveiling Eilenberg-type Correspondences: Birkhoff’s Theorem for (finite) Algebras + Duality.  https://arxiv.org/abs/1702.02822, February 2017.
  * [21] Marcel-Paul Schützenberger.  On finite monoids having only trivial subgroups.  Inform. and Control, 8:190–194, 1965.
  * [22] Thomas Schwentick.  Automata for XML – a survey.  J. Comput. System Sci., 73(3):289–315, 2007.
  * [23] Luc Segoufin.  Automata and logics for words and trees over an infinite alphabet.  In Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, pages 41–57, 2006.
  * [24] Henning Urbat, Jiří Adámek, Liang-Ting Chen, and Stefan Milius.  Eilenberg theorems for free.  In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, Proc. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), volume 83 of LIPIcs. Schloss Dagstuhl, 2017.  EATCS Best Paper Award.

##  Appendix A Appendix: Omitted Proofs and Details

In this appendix, we provide full proofs of all our results and technical
details omitted due to space restrictions.

## Properties of nominal sets

We review some additional concepts from the theory of nominal sets that we
shall use in subsequent proofs.

######  Definition 19.

A _supported set_ is a set $X$ together with a map
$\mathop{\mathsf{supp}}_{X}\colon X\to\mathcal{P}_{f}\mathbb{A}$, where
$\mathcal{P}_{f}\mathbb{A}$ is the set of finite subsets of $\mathbb{A}$. A
_morphism_ between supported sets $X$ and $Y$ is a function $f\colon X\to Y$
with $\mathop{\mathsf{supp}}_{Y}(f(x))\subseteq\mathop{\mathsf{supp}}_{X}(x)$
for all $x\in X$. We denote by $\mathbf{SuppSet}$ the category of supported
sets and their morphisms.

Note that every nominal set $X$ is a supported set w.r.t. its least-support
function $\mathop{\mathsf{supp}}_{X}$, and that every equivariant map is a
morphism of supported sets. The following result is a reformulation of [14,
Prop. 5.10]:

######  Lemma A.1 ([15], Lemma B.25).

The forgetful functor from $\mathbf{Nom}$ to $\mathbf{SuppSet}$ has a left
adjoint.

The left adjoint $F\colon\mathbf{SuppSet}\to\mathbf{Nom}$ is constructed as
follows. Given a finite set $I$, let $\mathbb{A}^{I}=\prod_{i\in I}\mathbb{A}$
denote the $I$-fold power of $\mathbb{A}$, and consider the strong nominal set

$\mathbb{A}^{\\#I}=\\{\,a\in\mathbb{A}^{I}\;\mathrel{\mathop{\mathchar
58\relax}}\;\text{$a\colon I\to\mathbb{A}$ injective}\,\\},$

with group action given by $(\pi\cdot a)(i)\mathrel{\mathop{\mathchar
58\relax}}=\pi(a(i))$ for every $\pi\in\mathrm{Perm}(\mathbb{A})$. Then $F$
sends a supported set $X$ to the nominal set $FX=\coprod_{x\in
X}\mathbb{A}^{\\#{\mathop{\mathsf{supp}}_{X}(x)}}$, and the universal map
$\eta_{X}\colon X\to FX$ maps an element $x\in X$ to the inclusion map
$\mathop{\mathsf{supp}}_{X}(x)\rightarrowtail\mathbb{A}$ in
$\mathbb{A}^{\\#\mathop{\mathsf{supp}}_{X}(x)}$.

######  Lemma A.2 ([15], Lemma B.27).

  1. (1)

For each nominal set $Z$, there exists a strong nominal set $X$ and a
surjective equivariant map $e\colon X\twoheadrightarrow Z$ preserving least
supports, i.e. with
$\mathop{\mathsf{supp}}_{Z}(e(x))=\mathop{\mathsf{supp}}_{X}(x)$ for all $x\in
X$.

  2. (2)

Every strong nominal set is isomorphic to $FY$ for some
$Y\in\mathbf{SuppSet}$.

It follows from the proof that in the case where $Z$ above is orbit-finite,
one may choose $X$ to be orbit-finite (in fact, with the same number of orbits
as $Z$). In particular:

######  Corollary A.3 (Pitts [18], Exercise 5.1).

Every nominal set which has only a single orbit is a quotient of the nominal
set
$\mathbb{A}^{\\#n}=\\{(a_{1},\ldots,a_{n})\in\mathbb{A}^{n}\;\mathrel{\mathop{\mathchar
58\relax}}\;a_{i}\neq a_{j}\text{ for $i\neq j$}\\}$ for some $n\geq 0$.

######  Lemma A.4.

Every orbit-finite nominal set contains only finitely many elements of any
given support.

######  Proof A.5.

This is a consequence of the following facts:

  * •

Every nominal set is the disjoint union of its orbits.

  * •

Every single-orbit nominal set is a quotient of the nominal set
$\mathbb{A}^{\\#n}$ (see A.3).

  * •

Every $\mathbb{A}^{\\#n}$ satisfies the desired property and every equivariant
map $f\colon X\to Y$ satisfies
$\mathop{\mathsf{supp}}_{Y}(f(x))\subseteq\mathop{\mathsf{supp}}_{X}(x)$ for
every $x\in X$.

## Proof of 2.1

Clearly the nominal set $\mathbb{A}^{\\#n}$ has only finitely many $S$-orbits:
two tuples $(a_{1},\ldots,a_{n})$ and $(b_{1},\ldots,b_{n})$ in
$\mathbb{A}^{\\#n}$ lie in the same $S$-orbit if and only if for every
$i=1,\ldots,n$ one has $a_{i}\in S$ iff $b_{i}\in S$ and in this case
$a_{i}=b_{i}$. Thus, by A.3, every nominal set with a single orbit has
finitely many $S$-orbits (using that equivariant maps preserve $S$-orbits).
Since every orbit-finite nominal set is the finite coproduct of its orbits,
this proves the claim. ∎

## Proof of 3.1

The proof is analogous to the corresponding statement for ordinary monoids.
Given a nominal quotient monoid
$e\colon\Sigma^{*}\twoheadrightarrow(M,\bullet,1_{M})$ as in (1), choose
$l_{w}=e(w)\bullet\mathord{-}$ and $r_{w}=\mathord{-}\bullet e(w)$.
Conversely, if (2) holds, there is a unique monoid structure
$(M,\bullet,1_{M})$ on $M$ making $e$ a monoid morphism in $\mathbf{Set}$. It
is uniquely defined by

$ev\bullet ew\mathrel{\mathop{\mathchar 58\relax}}=e(vw)\text{ for
$v,w\in\Sigma^{*}$}\quad\text{and}\quad 1_{M}\mathrel{\mathop{\mathchar
58\relax}}=e(\varepsilon).$

Condition $(2)$ makes sure that $\bullet$ is well-defined, i.e. independent of
the choice of $v$ and $w$. Moreover, the multiplication $\bullet$ is
equivariant since, for every $\pi\in\mathrm{Perm}(\mathbb{A})$,

$\pi\cdot(ev\bullet ew)=\pi\cdot e(vw)=e(\pi\cdot(vw))=e((\pi v)(\pi w))=e(\pi
v)\cdot e(\pi w)=(\pi\cdot e(v))\bullet(\pi\cdot e(w)),$

using that $e$ and the monoid multiplication on $\Sigma^{*}$ are equivariant.
∎

## Proof of Theorem 3.2

This theorem can be derived as an instance of the Generalized Variety Theorem
established in our previous work [16, Theorem 3.15], which relates varieties
of objects in a category $\mathscr{A}$ with a categorical notion of equational
theory. For the convenience of the reader, we briefly recall this result. For
the statement of the theorem one fixes the following parameters:

  * •

a category $\mathscr{A}$ with a proper factorization system
$(\mathcal{E},\mathcal{M})$;

  * •

a full subcategory $\mathscr{A}_{0}\subseteq\mathscr{A}$;

  * •

a class $\Lambda$ of cardinal numbers;

  * •

a class ${\mathscr{X}}\subseteq\mathscr{A}$ of objects.

Recall that a factorization system $(\mathcal{E},\mathcal{M})$ is _proper_ if
all morphisms in $\mathcal{E}$ are epic and all morphisms in $\mathcal{M}$ are
monic. The idea is that $\mathscr{A}$ is some category of algebraic
structures, $\mathscr{A}_{0}$ is the subcategory in which varieties are
formed, $\Lambda$ specifies the arities of products under which varieties are
closed, and ${\mathscr{X}}$ is the class of algebras over which equations are
formed (thus, ${\mathscr{X}}$ is usually some class of free algebras).
_Quotients_ and _subobjects_ in $\mathscr{A}$ are taken w.r.t. the classes
$\mathcal{E}$ and $\mathcal{M}$. An object $A\in\mathscr{A}$ is called
_${\mathscr{X}}$ -generated_ if there exists a quotient $e\colon
X\twoheadrightarrow A$ for some $X\in{\mathscr{X}}$. An object
$X\in\mathscr{A}$ is _projective_ w.r.t. a morphism $e\colon A\to B$ if for
every morphism $f\colon X\to B$ there exists a morphism $g\colon X\to A$ with
$e\cdot g=h$. We define the subclass
$\mathcal{E}_{\mathscr{X}}\subseteq\mathcal{E}$ by

$\mathcal{E}_{\mathscr{X}}=\\{\,e\in\mathcal{E}\;\mathrel{\mathop{\mathchar
58\relax}}\;\text{every $X\in{\mathscr{X}}$ is projective
w.r.t.\leavevmode\nobreak\ $e$}\,\\}.$

Our data is required to satisfy the following assumptions:

  1. (A1)

$\mathscr{A}$ has $\Lambda$-products, i.e. for every $\lambda\in\Lambda$ and
every family $(A_{i})_{i<\lambda}$ of objects in $\mathscr{A}$, the product
$\prod_{i<\lambda}A_{i}$ exists.

  2. (A2)

$\mathscr{A}_{0}$ is closed under isomorphisms, $\Lambda$-products and
${\mathscr{X}}$-generated subobjects. The last statement means that for every
subobject $m\colon A\rightarrowtail B$ in $\mathcal{M}$ where
$B\in\mathscr{A}_{0}$ and $A$ is ${\mathscr{X}}$-generated, one has
$A\in\mathscr{A}_{0}$.

  3. (A3)

Every object of $\mathscr{A}_{0}$ is an $\mathcal{E}_{\mathscr{X}}$-quotient
of some object of ${\mathscr{X}}$, that is, for every object
$A\in\mathscr{A}_{0}$ there exists some $e\colon X\twoheadrightarrow A$ in
$\mathcal{E}_{\mathscr{X}}$ with domain $X\in{\mathscr{X}}$.

######  Definition 20.

A _(weak) variety_ is a full subcategory $\mathscr{V}\subseteq\mathscr{A}_{0}$
closed under ($\mathcal{E}_{\mathscr{X}}$-)quotients, subobjects, and
$\Lambda$-products. More precisely,

  1. (1)

for every ($\mathcal{E}_{\mathscr{X}}$-)quotient $e\mathrel{\mathop{\mathchar
58\relax}}A\twoheadrightarrow B$ in $\mathscr{A}_{0}$ with $A\in\mathscr{V}$
one has $B\in\mathscr{V}$,

  2. (2)

for every $\mathcal{M}$-morphism $m\mathrel{\mathop{\mathchar
58\relax}}A\rightarrowtail B$ in $\mathscr{A}_{0}$ with $B\in\mathscr{V}$ one
has $A\in\mathscr{V}$, and

  3. (3)

for every family of objects $A_{i}$ ($i<\lambda$) in $\mathscr{V}$ with
$\lambda\in\Lambda$ one has $\prod_{i<\lambda}A_{i}\in\mathscr{V}$.

Given an object $X\in\mathscr{A}$, we denote by
$X\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathscr{A}_{0}$
the poset of all quotients $e\colon X\twoheadrightarrow A$ with codomain
$A\in\mathscr{A}_{0}$, ordered by $e\leq e^{\prime}$ iff $e^{\prime}$
factorizes through $e$. A subset $\mathscr{T}_{X}\subseteq
X\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathscr{A}_{0}$
is called a _(weak) equation_ if it is downwards $\Lambda$-directed, i.e.
every subset of $S\subseteq\mathscr{T}_{X}$ with ${|S|}\in\Lambda$ has a lower
bound in $\mathscr{T}_{X}$, and closed under
($\mathcal{E}_{\mathscr{X}}$-)quotients, i.e. for every quotient $e\colon
X\twoheadrightarrow E$ in $\mathscr{T}_{X}$ and every
($\mathcal{E}_{\mathscr{X}}$-)quotient $q\colon E\twoheadrightarrow
E^{\prime}$ in $\mathscr{A}_{0}$, one has $q\cdot e\in\mathscr{T}_{X}$. An
object $A\in\mathscr{A}_{0}$ _satisfies_ the (weak) equation $\mathscr{T}_{X}$
if every morphism $h\colon X\to A$ factorizes through some quotient in
$\mathscr{T}_{X}$.

######  Definition 21.

A _(weak) equational theory_ is a family

$\mathscr{T}=(\,\mathscr{T}_{X}\subseteq
X\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathscr{A}_{0}\,)_{X\in{\mathscr{X}}}$

of (weak) equations with the following properties (illustrated by the diagrams
below):

  1. (1)

_Substitution invariance._ For every morphism $h\colon X\to Y$ with
$X,Y\in{\mathscr{X}}$ and every $e_{Y}\colon Y\twoheadrightarrow E_{Y}$ in
$\mathscr{T}_{Y}$, the coimage $e_{X}\colon X\twoheadrightarrow E_{X}$ of
$e_{Y}\cdot h$ lies in $\mathscr{T}_{X}$.

  2. (2)

_$\mathcal{E}_{\mathscr{X}}$ -completeness._ For every $Y\in{\mathscr{X}}$ and
every quotient $e\colon Y\twoheadrightarrow E_{Y}$ in $\mathscr{T}_{Y}$, there
exists an $X\in{\mathscr{X}}$ and a quotient $e_{X}\colon X\twoheadrightarrow
E_{X}$ in $\mathscr{T}_{X}\cap\mathcal{E}_{\mathscr{X}}$ with $E_{X}=E_{Y}$.

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
h}$$\scriptstyle{e_{X}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
e_{Y}}$$\textstyle{E_{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E_{Y}}$
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists
e_{X}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\forall
e_{Y}}$$\textstyle{E_{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E_{Y}}$

######  Remark 22.

We warn the reader about a clash of terminology: in our previous work [15],
weak equations, weak equational theories and weak varieties were called
equations, equational theories and varieties (without the adjective “weak”).
Our present non-weak notion of an equation, an equational theory, and variety
in Definition 20/21 was not considered in [15].

######  Remark 23.

  1. (1)

To every weak equational theory $\mathscr{T}$ one can associate the variety

$\mathscr{V}(\mathscr{T})=\\{\,A\in\mathscr{A}_{0}\;\mathrel{\mathop{\mathchar
58\relax}}\;\text{$A$ satisfies $\mathscr{T}_{X}$ for every
$X\in{\mathscr{X}}$}\,\\}.$

Equivalently, by [15, Lemma A.2] the variety $\mathscr{V}(\mathscr{T})$
consists of all objects $A\in\mathscr{A}_{0}$ such that, for some
$X\in{\mathscr{X}}$, there exists a quotient $e\colon X\twoheadrightarrow A$
in $\mathscr{T}_{X}$ with codomain $A$.

  2. (2)

Conversely, to every weak variety $\mathscr{V}$ one can associate a weak
equational theory $\mathscr{T}(\mathscr{V})$ where
$[\mathscr{T}(\mathscr{V})]_{X}$ consists of all quotients $e\colon
X\twoheadrightarrow A$ with $A\in\mathscr{V}$.

Given two weak equations $\mathscr{T}_{X}$ and $\mathscr{T}_{X}^{\prime}$ over
$X\in{\mathscr{X}}$, we put $\mathscr{T}_{X}\leq\mathscr{T}_{X}^{\prime}$ if
every quotient in $\mathscr{T}_{X}^{\prime}$ factorizes through some quotient
in $\mathscr{T}_{X}$. Weak theories form a poset with respect to the order
$\mathscr{T}\leq\mathscr{T}^{\prime}$ iff
$\mathscr{T}_{X}\leq\mathscr{T}_{X}^{\prime}$ for all $X\in{\mathscr{X}}$.
Similarly, weak varieties form a poset – in fact, a complete lattice – ordered
by inclusion. Then, we obtain the following correspondence:

######  Theorem A.6 ([16], Theorem 3.15).

The complete lattices of weak equational theories and weak varieties are
dually isomorphic. The isomorphism is given the maps

$\mathscr{T}\mapsto\mathscr{V}(\mathscr{T})\quad\text{and}\quad\mathscr{V}\mapsto\mathscr{T}(\mathscr{V}).$

Clearly, the above isomorphism restricts to one between equational theories
and varieties. Thus, we obtain

######  Corollary A.7.

The complete lattices of equational theories and varieties are dually
isomorphic.

Let us now instantiate these results to the setting of orbit-finite nominal
monoids. That is, we choose the parameters of the above categorical setting as
follows:

  * •

$\mathscr{A}=\mathbf{nMon}$;

  * •

$(\mathcal{E},\mathcal{M})$ = (surjective morphisms, injective morphisms);

  * •

$\mathscr{A}_{0}=\mathbf{nMon}_{\mathsf{of}}$;

  * •

$\Lambda=$ all finite cardinal numbers;

  * •

${\mathscr{X}}=$ all free nominal monoids $\Sigma^{*}$ with $\Sigma$ an orbit-
finite strong nominal set.

The class $\mathcal{E}_{\mathscr{X}}$ can be characterized as follows:

######  Lemma A.8 ([15], Lemma B.28).

A quotient $e\colon M\twoheadrightarrow N$ belongs to
$\mathcal{E}_{\mathscr{X}}$ if and only if $e$ is support-reflecting.

It is now easy to verify that the assumptions (A1)–(A3) are satisfied. For
(A1) use that products of nominal monoids are formed on the level of their
underlying nominal sets. For (A2), use that finite products and equivariant
subsets of orbit-finite nominal sets are again orbit-finite. For (A3), let $M$
be an orbit-finite nominal monoid. By A.2, we can express the underlying
nominal set of $M$ as a quotient $e\colon\Sigma\twoheadrightarrow M$ in
$\mathbf{Nom}$ of an orbit-finite strong nominal set $\Sigma$, where $e$
preserves least supports. Then the unique extension
$\widehat{e}\colon\Sigma^{*}\twoheadrightarrow M$ to an equivariant monoid
morphism is support-reflecting. Indeed, given $m\in M$, choose $a\in\Sigma$
with $e(a)=m$. Then $\widehat{e}(a)=m$ and
$\mathop{\mathsf{supp}}_{\Sigma^{*}}(a)=\mathop{\mathsf{supp}}_{\Sigma}(a)=\mathop{\mathsf{supp}}_{M}(e(a))=\mathop{\mathsf{supp}}_{M}(m)$.

Finally, observe that the above general concepts of a variety and of an
equational theory specialize to the ones of a pseudovariety of nominal monoids
and of an equational theory of nominal monoids, respectively. Thus, Theorem
3.2 is an instance of Theorem A.6 and A.7. ∎

## Proof of Theorem 3.3

The key ingredient of the proof is an observation about congruences. A
_congruence_ on a nominal monoid $M$ is an equivariant equivalence relation
$\mathord{\equiv}\subseteq M\times M$ such that, for $m,n\in M$,

$m\equiv n\quad{\text{implies}}\quad pmq\equiv pnq\text{ for all $p,q\in M$}.$

There is an isomorphism of complete lattices

$\text{congruences on $M$}\quad\cong\quad\text{nominal quotients monoids of
$M$}$

mapping a congruence $\equiv$ to the quotient monoid $e\colon
M\twoheadrightarrow M/\mathord{\equiv}$, where $M/\mathord{\equiv}$ is the
monoid of all $\equiv$-congruence classes (with multiplication
$[m]\bullet[n]=[mn]$ for $m,n\in M$ and unit $[1_{M}]$), and $e$ sends $m$ to
$[m]$. The inverse isomorphism maps a nominal quotient monoid $e\colon
M\twoheadrightarrow N$ to its _kernel_ , i.e. the congruence $\equiv_{e}$ on
$M$ given by $m\equiv_{e}m^{\prime}$ iff $e(m)=e(m^{\prime})$. As a
consequence, we get

######  Theorem A.9 (Homomorphism Theorem).

Given two equivariant monoid morphisms $e\colon M\twoheadrightarrow N$ and
$h\colon M\to P$ with $e$ surjective, there exists a morphism $g\colon N\to P$
with $g\cdot e=h$ if and only if the kernel of $e$ is contained in the kernel
of $h$.

A congruence $\mathord{\equiv}$ on $M$ is is called _orbit-finite_ if the
corresponding quotient monoid $M/\mathord{\equiv}$ is orbit-finite, and
_finitely generated_ if there is a finite subset $W\subseteq\mathord{\equiv}$
such that $\equiv$ is the least congruence on $M$ containing $W$.

######  Lemma A.10.

Let $X$ be an orbit-finite nominal set. Then every orbit-finite congruence on
the free nominal monoid $X^{*}$ is finitely generated.

######  Proof A.11.

Let $\equiv$ be an orbit-finite congruence on $X^{*}$. Since
$X^{*}/\mathord{\equiv}$ is orbit-finite, there exists a natural number $k>0$
such that each congruence class contains a word of length $<k$. Moreover,
there exists a natural number $n$ such that every word of length $\leq k$ in
$X^{*}$ has a support of size $\leq n$. This follows from the fact that (a)
the least support of a word $a_{1}\cdots a_{m}\in\Sigma^{*}$ is given by
$\mathop{\mathsf{supp}}_{X^{*}}(a_{1}\cdots
a_{m})=\bigcup_{i=1}^{m}\mathop{\mathsf{supp}}_{X}(a_{i})$, and (b) the size
of least supports of elements of $X$ has an upper bound because $X$ is orbit-
finite and for elements $x,x^{\prime}\in X$ in the same orbit we have
$|\mathop{\mathsf{supp}}_{X}(x)|=|\mathop{\mathsf{supp}}_{X}(x^{\prime})|$.

We now fix a list of $2n$ pairwise distinct atoms
$a_{1},\ldots,a_{2n}\in\mathbb{A}$, and consider the subset
$W\subseteq\mathord{\equiv}$ defined by

$W\mathrel{\mathop{\mathchar 58\relax}}=\\{\,(s,t)\;\mathrel{\mathop{\mathchar
58\relax}}\;s\equiv t,\,{|s|}<k,\,{|t|}\leq
k,\,\mathop{\mathsf{supp}}(s),\mathop{\mathsf{supp}}(t)\subseteq\\{a_{1},\ldots,a_{2n}\\}\,\\}.$

Here ${|\mathord{-}|}$ denotes the length of a word. The set $W$ is finite
because $X$ contains only finitely many elements with support
$\\{a_{1},\ldots,a_{2n}\\}$, see A.4. Let $\sim$ be the congruence on $X^{*}$
generated by $W$ (i.e. the intersection of all congruences containing $W$). We
claim that $\mathord{\sim}=\mathord{\equiv}$, which proves that $\equiv$ is
finitely generated.

  1. (1)

For every pair $s,t\in X^{*}$ with $s\equiv t$, ${|s|}<k$ and ${|t|}\leq k$,
one has $s\sim t$. Indeed, since $s$ and $t$ have supports of size $\leq n$,
there exist pairwise distinct atoms $b_{1},\ldots,b_{2n}$ such that
$\mathop{\mathsf{supp}}(s),\mathop{\mathsf{supp}}(t)\subseteq\\{b_{1},\ldots,b_{2n}\\}$.
Choose a finite permutation $\pi\in\mathrm{Perm}(\mathbb{A})$ with
$\pi(b_{i})=a_{i}$ for $i=1,\ldots,2n$. Then the pair $(\pi\cdot s,\pi\cdot
t)$ lies in $W$; indeed, we have

    1. (a)

$\pi\cdot s\equiv\pi\cdot t$ because $s\equiv t$ and $\equiv$ is equivariant;

    2. (b)

${|\pi\cdot s|}<k$ and ${|\pi\cdot t|}\leq k$ because ${|s|}<k$ and ${|t|}\leq
k$ and $\pi\cdot(\mathord{-})$ preserves the length of words;

    3. (c)

$\mathop{\mathsf{supp}}(\pi\cdot s),\mathop{\mathsf{supp}}(\pi\cdot
t)\subseteq\\{a_{1},\ldots,a_{2n}\\}$ because
$\mathop{\mathsf{supp}}(s),\mathop{\mathsf{supp}}(t)\subseteq\\{b_{1},\ldots,b_{2n}\\}$.

Since $(s,t)=\pi^{-1}\cdot(\pi\cdot s,\pi\cdot t)$ and $(\pi\cdot s,\pi\cdot
t)\in W$, we conclude that the pair $(s,t)$ lies in the congruence generated
by $W$, i.e. $s\sim t$.

  2. (2)

We claim that for every word $s\in X^{*}$, there exists a word $t\in X^{*}$ of
length $<k$ with $s\sim t$. The proof is by induction on ${|s|}$. If
${|s|}<k$, one may take $t=s$. Thus let ${|s|}\geq k$. Since $k>0$, we have
that $s=xs^{\prime}$ for some $x\in X$ and $s^{\prime}\in X^{*}$. Since
${|s^{\prime}|}<{|s|}$, we have that $s^{\prime}\sim t^{\prime}$ for some word
$t^{\prime}\in X^{*}$ of length $<k$ by induction. This implies
$s=xs^{\prime}\sim xt^{\prime}$ because $\sim$ is a congruence. By the choice
of the number $k$, there exists a word $t\in X^{*}$ of length $<k$ with
$t\equiv xt^{\prime}$. Since ${|t|}<k$ and ${|xt^{\prime}|}\leq k$, we have
$t\sim xt^{\prime}$ by Part (1). Therefore, $s\sim xt^{\prime}\sim t$, as
required.

  3. (3)

We are ready two prove that $\mathord{\sim}=\mathord{\equiv}$. The inclusion
$\subseteq$ is obvious. Conversely, suppose that $s\equiv t$. By Part (2),
there are words $s^{\prime}$ and $t^{\prime}$ of length $<k$ with $s\sim
s^{\prime}$ and $t\sim t^{\prime}$. Since
$\mathord{\sim}\subseteq\mathord{\equiv}$, we get $s^{\prime}\equiv s\equiv
t\equiv t^{\prime}$. Part (1) then shows that $s^{\prime}\sim t^{\prime}$.
Thus, we conclude $s\sim s^{\prime}\sim t^{\prime}\sim t$.

######  Remark 24.

As an important consequence of the previous lemma, we note that there are only
countably many orbit-finite nominal monoids up to isomorphism. This is because
(1) every orbit-finite nominal monoid is a quotient of $X^{*}$ for some orbit-
finite set $X$, (2) up to isomorphism, there are only countably many orbit-
finite sets $X$ (this follows from [18, Theorem 5.13]; see also [4, Lemma
A.1]), and (3) $X^{*}$ is countably infinite, and thus has only countably many
orbit-finite quotient monoids by A.10 and the coincidence between quotients
and congruences.

We are ready to prove Theorem 3.3.

### Proof of the “if” direction

Let $E=(s_{n}=t_{n})_{n\in\mathds{N}}$ be a sequence of nominal equations,
where $s_{n},t_{n}\in X_{n}^{*}$ for a strong orbit-finite nominal set
$X_{n}$. We need to show that $\mathscr{V}(E)$ forms a weak pseudovariety.

_Closedness under finite products._ Let $M,N\in\mathscr{V}(E)$. Then there
exists $n_{0}\in\mathds{N}$ such that both $M$ and $N$ satisfy the equations
$s_{n}=t_{n}$ for $n\geq n_{0}$. Let $h\colon X_{n}\to M\times N$ be an
equivariant map, and denote by $\pi_{M}\colon M\times N\to M$ and
$\pi_{N}\colon M\times N\to N$ the projections. Then, for every $n\geq n_{0}$,

$\pi_{M}\cdot\widehat{h}(s_{n})=\widehat{\pi_{M}\cdot
h}(s_{n})=\widehat{\pi_{M}\cdot h}(t_{n})=\pi_{M}\cdot\widehat{h}(t_{n})$

and analogously
$\pi_{N}\cdot\widehat{h}(s_{n})=\pi_{N}\cdot\widehat{h}(t_{n})$. This implies
$\widehat{h}(s_{n})=\widehat{h}(t_{n})$. Thus $M\times N$ satisfies
$s_{n}=t_{n}$ for $n\geq n_{0}$, whence $M\times N\in\mathscr{V}(E)$.

_Closedness under submonoids._ Let $M\in\mathscr{V}(E)$ and let $m\colon
N\rightarrowtail M$ be a nominal submonoid of $M$. Choose $n_{0}\in\mathds{N}$
such that $M$ satisfies all equations $s_{n}=t_{n}$ with $n\geq n_{0}$. Then,
for each equivariant map $h\colon X_{n}\to N$ and $n\geq n_{0}$, one has

$m\cdot\widehat{h}(s_{n})=\widehat{m\cdot h}(s_{n})=\widehat{m\cdot
h}(t_{n})=m\cdot\widehat{h}(t_{n}).$

Since $m$ is monomorphic, this implies that
$\widehat{h}(s_{n})=\widehat{h}(t_{n})$. Thus, $N$ satisfies $s_{n}=t_{n}$ for
$n\geq n_{0}$, whence $N\in\mathscr{V}(E)$.

_Closedness under quotient monoids._ Let $M\in\mathscr{V}(E)$ and let $e\colon
M\twoheadrightarrow N$ be a support-reflecting surjective equivariant monoid
morphism. Choose $n_{0}\in\mathds{N}$ such that $M$ satisfies all equations
$s_{n}=t_{n}$ with $n\geq n_{0}$. Given an equivariant map $h\colon X_{n}\to
N$, since $e$ is support-reflecting, there exists an equivariant map $g\colon
X_{n}\to M$ with $h=e\cdot g$, see A.8. It follows that, for each $n\geq
n_{0}$,

$\widehat{h}(s_{n})=\widehat{e\cdot
g}(s_{n})=e\cdot\widehat{g}(s_{n})=e\cdot\widehat{g}(t_{n})=\widehat{e\cdot
g}(t_{n})=\widehat{h}(t_{n}).$

Thus $N$ satisfies $s_{n}=t_{n}$ for $n\geq n_{0}$, whence
$N\in\mathscr{V}(E)$. ∎

### Proof of the “only if” direction

Let $\mathscr{V}$ be a weak pseudovariety of nominal monoids. We need to find
a sequence $E$ of equations with $\mathscr{V}=\mathscr{V}(E)$.

  1. (1)

First, we prove that there exists a sequence of monoids
$M_{0},M_{1},M_{2},\ldots\in\mathscr{V}$ such that every $M\in\mathscr{V}$ is
a support-reflecting quotient of $M_{n}$ for all but finitely many $n$. To see
this, let $S_{0},S_{1},S_{2},\ldots$ be the countably many elements of
$\mathscr{V}$ up to isomorphism (see Remark 24), and put

$M_{n}=S_{0}\times S_{1}\times\cdots\times S_{n}\quad\text{for $n\geq 0$}.$

For each $M\in\mathscr{V}$ one has $M\cong S_{m}$ for some $m\geq 0$. Then,
for $n\geq m$, we obtain the surjective morphism $M_{n}\twoheadrightarrow M$
given by the projection

$M_{n}=S_{0}\times S_{1}\times\cdots\times
S_{n}\xrightarrow{\pi_{n,m}}S_{m}\xrightarrow{\cong}M.$

Note that $\pi_{n,m}$ is support-reflecting: for each $s\in S_{m}$ one has

$\pi_{n,m}(1,\ldots,1,s,1,\ldots,1)=s,$

and since the unit $1$ of each nominal monoid has empty support, one has
$\mathop{\mathsf{supp}}_{M_{n}}(1,\ldots,1,s,1,\ldots,1)=\mathop{\mathsf{supp}}_{S_{m}}{s}$.
Thus, we have shown that $M$ is a support-reflecting quotient of $M_{n}$ for
each $n\geq m$.

  2. (2)

Let $X_{0},X_{1},X_{2},\ldots$ be a sequence that enumerates all orbit-finite
strong nominal sets (up to isomorphism); cf. Remark 24. For each $n\geq 0$,
consider the following congruence $\equiv_{n}$ on $X_{n}^{*}$:

$s\equiv_{n}t\quad\Leftrightarrow\quad h(s)=h(t)\text{ for all morphisms
$h\colon X_{n}^{*}\to M_{n}$}.$

In other words, $\equiv_{n}$ is the set of all equations over $X_{n}$
satisfied by $M_{n}$. We claim that

$X_{n}^{*}/\mathord{\equiv_{n}}\in\mathscr{V}\quad\text{for all
$n\in\mathds{N}$}.$

To see this, note first that there are only finitely many morphisms
$X_{n}^{*}\to M_{n}$: such a morphism bijectively corresponds to an
equivariant map $X_{n}\to M_{n}$, which in turn corresponds to a map of
supported sets $Y_{n}\to M_{n}$, where $Y_{n}$ is a finite supported set with
$X_{n}\cong F(Y_{n})$ (see A.1 and A.2). Since $M_{n}$ contains only finitely
many elements of any given support by A.4, there exist only finitely many such
maps.

Letting $h_{0},\ldots,h_{p}$ denote the morphisms from $X_{n}^{*}$ to $M_{n}$,
the induced morphism

$\langle h_{i}\rangle_{i\leq p}\colon X_{n}^{*}\to\prod_{i\leq p}M_{n}$

has kernel $\equiv_{n}$. Thus, we can conclude that
$X_{n}^{*}/\mathord{\equiv_{n}}$ is a submonoid of the finite product
$\prod_{i}M_{n}$, and therefore it lies in $\mathscr{V}$.

  3. (3)

Since $X^{*}_{n}/\mathord{\equiv_{n}}\in\mathscr{V}$ by part (2) above,
$\equiv_{n}$ is an orbit-finite congruence on $X_{n}^{*}$ for each $n\geq 0$.
Therefore, by A.10, there exists a finite generating subset $W_{n}$ of
$\equiv_{n}$. We may assume that $W_{n}$ is nonempty, so that
$\bigcup_{n}W_{n}$ is a countably infinite set of equations. Let
$E=(s_{k}=t_{k})_{k\in\mathds{N}}$ be a sequence that enumerates all equations
in $\bigcup_{n}W_{n}$. We claim that $\mathscr{V}=\mathscr{V}(E)$.

To prove “$\subseteq$”, let $M\in\mathscr{V}$. By Part (1), there exists
$m\geq 0$ such that $M$ is a support-reflecting quotient of $M_{n}$ for each
$n\geq m$. Since $M_{n}$ satisfies all equations in $W_{n}$, it follows that
also $M$ satisfies them for $n\geq m$ (using that satisfaction of equations is
preserved by support-reflecting quotients, as shown in the “only if” direction
of our proof). Thus $M$ satisfies all equations in $\bigcup_{n\geq m}W_{n}$,
i.e. it eventually satisfies $E$.

For the proof of “$\supseteq$”, let $M\in\mathscr{V}(E)$. Note that there are
infinitely many $n\in\mathds{N}$ such that a support-reflecting quotient
$h\colon X_{n}^{*}\twoheadrightarrow M$ exists (indeed, one may take any
orbit-finite strong nominal set $X_{n}$ of the form
$\mathbb{A}^{\\#k_{0}}+\cdots+\mathbb{A}^{\\#k_{m-1}}+\mathbb{A}^{\\#k}$,
where $m$ is the number of orbits of $M$, $k_{i}$ is the size of the least
support of any element of the $i^{\text{th}}$ orbit, and $k$ is any natural
number with $k\geq k_{0}$). In particular, since $M$ satisfies all but
finitely many of the equations in $E$, one can choose $n\in\mathds{N}$ such
that (a) $M$ satisfies the equations in $W_{n}$, and (b) a support-reflecting
quotient $h\colon X_{n}^{*}\twoheadrightarrow M$ exists. Then

$h(s)=h(t)\quad\text{for all $(s,t)\in W_{n}$},$

that is, $W_{n}$ is contained in the kernel of $h$. Since $W_{n}$ generates
$\equiv_{n}$, it follows that also $\equiv_{n}$ is contained in the kernel of
$h$. The Homomorphism Theorem A.9 then yields a morphism $e\colon
X_{n}^{*}/\mathord{\equiv_{n}}\twoheadrightarrow M$ with $h=e\cdot q$, where
$q$ is the quotient corresponding to $\equiv_{n}$:

$\textstyle{X_{n}^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{q}$$\textstyle{X_{n}^{*}/\mathord{\equiv_{n}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{M}$

Note that $e$ is support-reflecting because $h$ is. Since
$X_{n}^{*}/\mathord{\equiv_{n}}\in\mathscr{V}$ by part (2) and $\mathscr{V}$
is closed under support-reflecting quotients, we conclude that
$M\in\mathscr{V}$.∎

## Details for 3.5

We show that an orbit-finite nominal monoid $M$ is aperiodic if and only if it
eventually satisfies the equations

$y\mathrel{\mathop{\mathchar 58\relax}}S_{n}\vdash
y^{n+1}=y^{n}\qquad(n\in\mathds{N}),$ (2)

where $S_{n}=\\{a_{0},a_{1},\ldots,a_{n-1}\\}$ is the set of the first $n$
atoms in the countably infinite set $\mathbb{A}=\\{a_{0},a_{1},a_{2}\ldots\\}$
of all atoms, and we write $y$ for
$(\mathit{id},y)\in\mathrm{Perm}(\mathbb{A})\times Y$.

For the “if” direction, suppose that $M$ is aperiodic, i.e. there exists a
natural number $m\geq 1$ such that $x^{m+1}=x^{m}$ for every $x\in M$. This
implies that $x^{n+1}=x^{n}$ for all $n\geq m$ and $x\in M$. In particular,
this holds for all elements $x$ with support $S_{n}$, i.e. (2) is satisfied
for all $n\geq m$.

For the “only if” direction, suppose that $M$ eventually satisfies the
equations (2). Choose $n\in\mathds{N}$ such that $M$ satisfies the equation
$y\mathrel{\mathop{\mathchar 58\relax}}S_{n}\vdash y^{n+1}=y^{n}$ and every
element of $M$ has a support of size $n$. Given any element $x\in M$, choose a
finite permutation $\pi\in\mathrm{Perm}(\mathbb{A})$ that maps a support of
$x$ to $S_{n}$. The $\pi\cdot x$ is as element with support $S_{n}$, and thus
$(\pi\cdot x)^{n+1}=(\pi\cdot x)^{n}$ holds. This implies $x^{n+1}=x^{n}$
because the monoid multiplication on $M$ is equivariant. Thus, $M$ is
aperiodic.

## Proof of Theorem 4.1

Recall that $\mathbf{Nom}_{\mathsf{fs}}$ denotes the category of nominal sets
and finitely supported maps and $\mathbf{nCABA}_{\mathsf{fs}}$ the category of
ncabas and finitely supported boolean homomorphisms preserving suprema of
finitely supported subsets. We know from Petrişan [17, Prop. 5.3.11] that the
categories $\mathbf{nCABA}$ and $\mathbf{Nom}$ are dually equivalent with the
equivalence functors being the restrictions of the ones in Remark 10. Thus, in
order to obtain the desired result we prove the following

######  Proposition A.12.

The dual equivalence
$\mathbf{Nom}\xrightarrow{\simeq}\mathbf{nCABA}^{\mathsf{op}}$ extends to a
dual equivalence
$\mathbf{Nom}_{\mathsf{fs}}^{\mathsf{op}}\xrightarrow{\simeq}\mathbf{nCABA}_{\mathsf{fs}}$
given by $X\mapsto\mathcal{P}X$ and $f\mapsto f^{-1}$.

######  Proof A.13.

We first show that the above functor
$\mathbf{Nom}_{\mathsf{fs}}^{\mathsf{op}}\to\mathbf{nCABA}_{\mathsf{fs}}$ is
well-defined, that is, for every finitely supported map $f\colon Y\to X$ the
map $f^{-1}\colon\mathcal{P}X\to\mathcal{P}Y$ is also finitely supported. Let
$S\subseteq\mathbb{A}$ be a finite support of $f$. Then for every
$X_{0}\in\mathcal{P}X$ and $\pi\in\mathrm{Perm}_{S}(\mathbb{A})$ one has
$\pi\cdot f^{-1}[X_{0}]=f^{-1}[\pi\cdot X_{0}]$ since, for all $y\in Y$,

$\displaystyle y\in\pi\cdot f^{-1}[X_{0}]$
$\displaystyle\Leftrightarrow\pi^{-1}\cdot y\in f^{-1}[X_{0}]$
$\displaystyle\Leftrightarrow f(\pi^{-1}\cdot y)\in X_{0}$
$\displaystyle\Leftrightarrow\pi^{-1}\cdot f(y)\in X_{0}$
$\displaystyle\Leftrightarrow f(y)\in\pi\cdot X_{0}$
$\displaystyle\Leftrightarrow y\in f^{-1}[\pi\cdot X_{0}]$

This proves that $f^{-1}$ has support $S$.

It remains to verify that the functor
$\mathbf{Nom}_{\mathsf{fs}}^{\mathsf{op}}\to\mathbf{nCABA}_{\mathsf{fs}}$ is
(1) essentially surjective on objects, (2) faithful and (3) full. Point (1) is
clear because on objects the functor coincides with the equivalence functor
$\mathbf{Nom}\xrightarrow{\simeq}\mathbf{nCABA}^{\mathsf{op}}$. For (2),
suppose that $f\neq g\colon Y\to X$ are two distinct finitely supported maps.
Choose $y\in Y$ with $f(y)\neq g(y)$. Since the singleton $\\{f(y)\\}$ is
finitely supported, we may apply $f^{-1}$ and $g^{-1}$ to it, and we clearly
have $f^{-1}\\{f(y)\\}\neq g^{-1}\\{f(y)\\}$. Thus $f^{-1}\neq g^{-1}$. For
(3), let $g\colon\mathcal{P}X\to\mathcal{P}Y$ be a morphism in
$\mathbf{nCABA}_{\mathsf{fs}}$ with finite support $S\subseteq\mathbb{A}$.
Then the sets $g(\\{x\\})\subseteq Y$ ($x\in X$) form a partition of $Y$ since
$g$ is a homomorphism of boolean algebras, i.e. for every $y\in Y$ there
exists a unique $x_{y}\in X$ with $y\in g(\\{x_{y}\\})$. Consider the map
$f\colon Y\to X$ defined by $f(y)\mathrel{\mathop{\mathchar 58\relax}}=x_{y}$.
We claim that $f$ has support $S$. To see this, let
$\pi\in\mathrm{Perm}_{s}(\mathbb{A})$. Then we have $\pi\cdot
g(\\{x\\})=g(\\{\pi\cdot x\\})$ for every $x\in X$. Since $f(y)=x_{y}$ where
$y\in g(\\{x_{y}\\})$ we know $\pi\cdot y\in\pi\cdot
g(\\{x_{y}\\})=g(\\{\pi\cdot x_{y}\\})$, hence, $f(\pi\cdot y)=\pi\cdot
x_{y}=\pi\cdot f(y)$ as desired.

Finally, we show that $g=f^{-1}$. By the definition of $f$ the two maps agree
on singleton sets $\\{x\\}$. It follows that they agree on all finitely
supported subsets of $X$: every such set can be expressed as the finitely
supported union of its singleton subsets, and both $g$ and $f^{-1}$ preserve
that union.

## Details for 4.2

(1) See Remark 14.

(2) We prove that the language $L=a\mathbb{A}^{*}$ (for a fixed atom
$a\in\mathbb{A}$) is recognizable. Consider the orbit-finite monoid
$M=\\{1\\}+\mathbb{A}$ with multiplication given by

$b\bullet c=b\quad\text{for all $b,c\in\mathbb{A}$}.$

Let $e\colon\mathbb{A}^{*}\to M$ be the unique morphism given by $b\mapsto b$.
Thus $e$ maps $\varepsilon$ to $1$ and every word $bw$ ($w\in\Sigma^{*}$,
$b\in\mathbb{A}$) to $b$. It follows that

$L=e^{-1}[\\{a\\}].$

Since $\\{a\\}$ is a finitely supported subset of $\mathbb{A}$, this shows
that $e$ recognizes $L$.

(3)–(5) are equivariant languages and were treated in [5, 19].

(6) We prove that the language $L=\mathbb{A}^{*}a\mathbb{A}^{*}$ (for a fixed
atom $a\in\mathbb{A}$) is not recognizable. Suppose for the contrary that
there exists an equivariant monoid morphism $e\colon\mathbb{A}^{*}\to M$ into
an orbit-finite monoid $M$ that recognizes $L$. We claim that

$\mathop{\mathsf{supp}}(e(w))=\mathop{\mathsf{supp}}(w)\quad\text{for every
$w\in\mathbb{A}^{*}\setminus L$}.$

Since $\mathbb{A}^{*}$ contains words of arbitrarily large finite support,
this implies that also $M$ contains elements of arbitrarily large finite
support, contradicting the assumption that $M$ is orbit-finite.

To prove the above equation, note that
$\mathop{\mathsf{supp}}(e(w))\subseteq\mathop{\mathsf{supp}}(w)$ holds by
equivariance of $e$. For the reverse inclusion, let
$w\in\mathbb{A}^{*}\setminus L$ and $b\in\mathop{\mathsf{supp}}(w)$, i.e. $w$
contains the letter $b$ but not the letter $a$. Suppose for the sake of
contradiction that $b\not\in\mathop{\mathsf{supp}}(e(w))$. Then
$a,b\not\in\mathop{\mathsf{supp}}(e(w))$ and thus

$e(w)=(a\,b)\cdot e(w)=e((a\,b)\cdot w),$

where $(a\,b)\in\mathrm{Perm}(\mathbb{A})$ denotes the permutation that swaps
$a$ and $b$ and leaves all other atoms fixed. But we have $w\not\in L$ and
$(a\,b)\cdot w\in L$, which implies that $e(w)\neq e((a\,b)\cdot w)$.

## Proof of 4.5

For a given set $W\subseteq\mathcal{P}\Sigma^{*}$ of recognizable languages we
denote by $\langle W\rangle\subseteq\mathcal{P}\Sigma^{*}$ the subobject of
$\mathcal{P}\Sigma^{*}$ in $\mathbf{nCABA}$ generated by $W$, obtained by
closing $W$ under the group action, boolean operations, and unions of finitely
supported subsets. Note that if $W$ is closed under derivatives, then so is
$\langle W\rangle$, i.e. $\langle W\rangle$ is then a local variety. This
follows from the following identities:

$\displaystyle w^{-1}(K\cup L)$ $\displaystyle=w^{-1}K\cup w^{-1}L,$
$\displaystyle w^{-1}(K\cap L)$ $\displaystyle=w^{-1}K\cap w^{-1}L,$
$\displaystyle w^{-1}(\Sigma^{*}\setminus L)$
$\displaystyle=\Sigma^{*}\setminus w^{-1}L,$ $\displaystyle
w^{-1}(\bigcup_{j\in J}L_{j})$ $\displaystyle=\bigcup_{j\in J}L_{j},$
$\displaystyle w^{-1}(\pi\cdot L)$ $\displaystyle=\pi\cdot((\pi^{-1}\cdot
w)L),$

for all $w\in\Sigma^{*}$, languages $K,L,L_{j}\subseteq\Sigma^{*}$ and
$\pi\in\mathrm{Perm}(\mathbb{A})$.

  1. (1)

Given an ideal of atom-finite local varieties
$\mathcal{V}_{\Sigma,i}\subseteq\mathcal{P}\Sigma^{*}$ ($i\in I$), the
directed union $\mathcal{V}_{\Sigma}=\bigcup_{i}\mathcal{V}_{\Sigma,i}$ is a
local variety. Indeed, to see that $\mathcal{V}_{\Sigma}$ is closed under
unions of $S$-orbits for every finite $S\subseteq\mathbb{A}$, suppose that
$W\subseteq\mathcal{V}_{\Sigma}$ is an $S$-orbit. Then
$W\subseteq\mathcal{V}_{\Sigma,i}$ for some $i$ because every
$\mathcal{V}_{\Sigma,i}$ is an equivariant subset of $\mathcal{P}\Sigma^{*}$.
Since $\mathcal{V}_{\Sigma,i}$ is closed under unions $S$-orbits, we get
$\bigcup W\in\mathcal{V}_{\Sigma,i}\subseteq\mathcal{V}_{\Sigma}$. To show
that $\mathcal{V}_{\Sigma}$ is closed under finite union, let
$K,L\in\mathcal{V}_{\Sigma}$. Then, since the $\mathcal{V}_{\Sigma,i}$ form a
directed set, there exists $i\in I$ with $K,L\in\mathcal{V}_{\Sigma,i}$ Thus
$K\cup L\in\mathcal{V}_{\Sigma,i}\subseteq\mathcal{V}_{\Sigma}$ because
$\mathcal{V}_{\Sigma,i}$ is closed under finite union. That
$\mathcal{V}_{\Sigma}$ is closed under the remaining boolean operations,
derivatives, and the group action is shown in the same way.

  2. (2)

Given a local variety $\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}$,
form the family $\mathcal{V}_{\Sigma,i}\subseteq\mathcal{P}\Sigma^{*}$ ($i\in
I$) of all atom-finite local subvarieties of $\mathcal{V}_{\Sigma}$. We claim
that this family forms an ideal. Clearly, it is downwards closed. To show that
it is upwards directed, it suffices to verify that for every $i,j\in I$ the
local variety $\langle\mathcal{V}_{\Sigma,i}\cup\mathcal{V}_{\Sigma,j}\rangle$
is atom-finite. Let $e_{i}\colon\Sigma^{*}\twoheadrightarrow M_{i}$ and
$e_{j}\colon\Sigma^{*}\twoheadrightarrow M_{j}$ be the $\Sigma$-generated
orbit-finite quotient monoids corresponding to $\mathcal{V}_{\Sigma,i}$ and
$\mathcal{V}_{\Sigma,j}$ by the Finite Local Variety Theorem 4.3. Form their
subdirect product, i.e. the coimage $e\colon\Sigma^{*}\twoheadrightarrow M$ of
the map $\langle e_{i},e_{j}\rangle\colon\Sigma^{*}\to M_{i}\times M_{j}$.
Then $e$ is the infimum of $e_{i}$ and $e_{j}$ in the lattice of quotients (in
$\mathbf{Nom}$) of $\Sigma^{*}$. Thus $e$ dualizes to
$\langle\mathcal{V}_{\Sigma,i}\cup\mathcal{V}_{\Sigma,j}\rangle$, the supremum
of $\mathcal{V}_{\Sigma,i}$ and $\mathcal{V}_{\Sigma,j}$ in the lattice of
subobjects of $\mathcal{P}\Sigma^{*}$ in $\mathbf{nCABA}$. Moreover, since $M$
is orbit-finite,
$\langle\mathcal{V}_{\Sigma,i}\cup\mathcal{V}_{\Sigma,j}\rangle$ is atom-
finite.

  3. (3)

It remains to show that the constructions of (1) and (2) are mutually inverse.
First, given an ideal of atom-finite local varieties
$\mathcal{V}_{\Sigma,i}\subseteq\mathcal{P}\Sigma^{*}$ ($i\in I$) and an atom-
finite local subvariety
$\mathcal{W}_{\Sigma}\subseteq\bigcup_{i}\mathcal{V}_{\Sigma,i}$ we need to
prove that $\mathcal{W}_{\Sigma}=\mathcal{V}_{\Sigma,i}$ for some $i$. Let
$L_{1},\ldots,L_{n}$ be the finitely many atoms of $\mathcal{W}_{\Sigma}$ up
to application of the group action. By the ideal property, we may assume that
$L_{1},\ldots,L_{n}\in\mathcal{V}_{\Sigma,j}$ for some $j\in I$. Since every
element $L$ of the ncaba $\mathcal{W}_{\Sigma}$ can be expressed as the union
of all atoms below it, and the set of these atoms is a finite union of
$S$-orbits for some finite $S\subseteq\mathbb{A}$ (cf. Remark 10), one has
$\mathcal{W}_{\Sigma}=\langle
L_{1},\ldots,L_{n}\rangle\subseteq\mathcal{V}_{\Sigma,j}$ and thus
$\mathcal{W}_{\Sigma}=\mathcal{V}_{\Sigma,i}$ for some $i$ by down-closure.

  4. (4)

Conversely, let $\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}$ be a
local variety and let $\mathcal{V}_{\Sigma,i}$ $(i\in I)$ be the ideal of its
atom-finite local subvarieties. Clearly, we have
$\bigcup_{i}\mathcal{V}_{\Sigma,i}\subseteq\mathcal{V}_{\Sigma}$, so we only
need to show $\mathcal{V}_{\Sigma}\subseteq\bigcup_{i}\mathcal{V}_{\Sigma,i}$.
For every $L\in\mathcal{V}_{\Sigma}$, since $L$ is recognizable, there exists
an orbit-finite quotient monoid $e\colon\Sigma^{*}\twoheadrightarrow M$
recognizing $L$. By the Finite Local Variety Theorem 4.3, the quotient $e$
dualizes to an atom-finite local variety
$\mathcal{W}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}$ containing $L$. Then
$\mathcal{V}_{\Sigma,i}\mathrel{\mathop{\mathchar
58\relax}}=\mathcal{W}_{\Sigma}\cap\mathcal{V}_{\Sigma}$ is an atom-finite
local subvariety of $\mathcal{V}_{\Sigma}$ containing $L$, i.e.
$L\in\mathcal{V}_{\Sigma,i}\subseteq\bigcup_{i}\mathcal{V}_{\Sigma,i}$.∎

## Proof of Theorem 4.7

The proof boils down to the observation that varieties can be interpreted as
the dual concept of an equational theory. By the Local Variety Theorem, a
collection
$\mathcal{V}=(\,\mathcal{V}_{\Sigma}\subseteq\mathcal{P}\Sigma^{*}\,)_{\Sigma\in\mathbf{Nom}_{\mathsf{of,s}}}$
of local varieties of data languages corresponds bijectively to a collection
$\mathscr{T}=(\,\mathscr{T}_{X}\subseteq
X^{*}\mathord{\mathrel{\rotatebox[origin={c}]{90.0}{$\twoheadleftarrow$}}}\mathbf{nMon}_{\mathsf{of}}\,)_{X\in\mathbf{Nom}_{\mathsf{of,s}}}$
of local pseudovarieties of nominal monoids. We claim that

  1. (1)

$\mathscr{T}$ is substitution-invariant if and only if $\mathcal{V}$ is closed
under preimages, and

  2. (2)

$\mathscr{T}$ is complete if and only if $\mathcal{V}$ is complete.

In particular, $\mathscr{T}$ is an equational theory if and only if
$\mathcal{V}$ is variety. Together with Theorem 3.2, this proves the theorem.

_Proof of(1)._ By the Finite Local Variety Theorem 4.3 and 4.5, the
substitution invariance of $\mathscr{T}$ dualizes to the statement that for
every atom-finite local subvariety $\mathcal{V}^{\prime}_{\Sigma}$ of
$\mathcal{V}_{\Sigma}$ and every $h\colon\Delta^{*}\to\Sigma^{*}$, there
exists an atom-finite local subvariety $\mathcal{V}^{\prime}_{\Delta}$ of
$\mathcal{V}_{\Delta}$ that contains the preimage $h^{-1}[L]$ for each
$L\in\mathcal{V}^{\prime}_{\Sigma}$.

$\textstyle{\Delta^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{\Delta}}$$\scriptstyle{h}$$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{\Sigma}}$$\textstyle{M_{\Delta}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists}$$\textstyle{M_{\Sigma}}$
$\textstyle{\mathcal{P}\Delta^{*}}$$\textstyle{\mathcal{P}\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h^{-1}(\mathord{-})}$$\textstyle{\mathcal{V}^{\prime}_{\Delta}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq}$$\textstyle{\mathcal{V}^{\prime}_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists}$$\scriptstyle{\subseteq}$

By 4.5, every language in $\mathcal{V}_{\Sigma}$ is contained in some atom-
finite subvariety $\mathcal{V}^{\prime}_{\Sigma}$. Hence, the commutativity of
the right-hand diagram above implies that $\mathcal{V}$ is closed under
preimages. Conversely, suppose that $\mathcal{V}$ is closed under preimages,
and let $\mathcal{V}^{\prime}_{\Sigma}$ be an atom-finite local subvariety of
$\mathcal{V}_{\Sigma}$. Thus, there are atomic languages
$L_{1},\ldots,L_{n}\in\mathcal{V}^{\prime}_{\Sigma}$ such that every other
atomic language in $\mathcal{V}^{\prime}_{\Sigma}$ is of the form $\pi\cdot
L_{i}$ for some $\pi\in\mathrm{Perm}(\mathbb{A})$ and $i\in\\{1,\ldots,n\\}$.
By closure of $\mathcal{V}$ under preimages, one has
$h^{-1}[L_{i}]\in\mathcal{V}_{\Delta}$ for all $i$. Choose an atom-finite
local subvariety $\mathcal{V}^{\prime}_{\Delta,i}$ of
$\mathcal{V}^{\prime}_{\Delta}$ containing $L_{i}$. Since the atom-finite
local subvarieties of $\mathcal{V}^{\prime}_{\Delta}$ form an ideal (i.e. are
upwards directed), we can choose an atom-finite local subvariety
$\mathcal{V}^{\prime}_{\Delta}$ containing all
$\mathcal{V}^{\prime}_{\Delta,i}$’s. Thus
$h^{-1}[L_{i}]\in\mathcal{V}^{\prime}_{\Delta}$ for all $i$. By Remark 10,
every language $L\in\mathcal{V}^{\prime}_{\Sigma}$ can be expressed as a
finite union $L=K_{0}\cup\ldots\cup K_{m}$, where every $K_{i}$ is the union
of an $S$-orbit in $\mathcal{V}^{\prime}_{\Sigma}$. Since the equivariant map
$h^{-1}$ maps $S$-orbits to $S$-orbits, and $\mathcal{V}^{\prime}_{\Delta}$ is
closed under finite unions and unions of $S$-orbits, it follows that
$h^{-1}[L]=h^{-1}[K_{1}]\cup\ldots\cup h^{-1}[K_{m}]$ lies in
$\mathcal{V}^{\prime}_{\Delta}$.

_Proof of(2)._ Suppose that $\mathscr{T}$ is complete, let
$\mathcal{V}^{\prime}_{\Sigma}$ be an atom-finite local subvariety of
$\mathcal{V}_{\Sigma}$, and let $e_{\Sigma}\colon\Sigma^{*}\twoheadrightarrow
M_{\Sigma}$ be its dual quotient in $\mathscr{T}_{\Sigma}$. Then there exists
$\Delta\in\mathbf{Nom}_{\mathsf{of,s}}$ and a support-reflecting quotient
$e_{\Delta}\colon\Delta^{*}\twoheadrightarrow M_{\Delta}$ in
$\mathscr{T}_{\Delta}$ with $M_{\Delta}\cong M_{\Sigma}$. By projectivity (see
A.8), we can choose an equivariant monoid morphism
$h\colon\Sigma^{*}\to\Delta^{*}$ with $e_{\Delta}\cdot h=e_{\Sigma}$. Letting
$\mathcal{V}^{\prime}_{\Delta}$ denote the atom-finite local subvariety of
$\mathcal{V}_{\Delta}$ dual to $e_{\Delta}$, we thus obtain the two dual
commutative diagrams below:

$\textstyle{\Delta^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{\Delta}}$$\textstyle{\Sigma^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{e_{\Sigma}}$$\textstyle{M_{\Delta}}$$\textstyle{M_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$
$\textstyle{\mathcal{P}\Delta^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h^{-1}(\mathord{-})}$$\textstyle{\mathcal{P}\Sigma^{*}}$$\textstyle{\mathcal{V}^{\prime}_{\Delta}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq}$$\scriptstyle{\cong}$$\textstyle{\mathcal{V}^{\prime}_{\Sigma}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\subseteq}$

The right-hand diagram shows that the map $L\mapsto h^{-1}[L]$ from
$\mathcal{V}^{\prime}_{\Delta}$ to $\mathcal{V}^{\prime}_{\Sigma}$ is
bijective. Moreover, by Theorem 4.3, $M_{\Delta}$ is (up to isomorphism)
carried by the set of atomic languages in $\mathcal{V}^{\prime}_{\Delta}$, and
$e_{\Delta}$ is the morphism mapping every word $w\in\Delta^{*}$ to the unique
atomic language in $\mathcal{V}^{\prime}_{\Delta}$ containing $w$. That
$e_{\Delta}$ is support-reflecting thus means precisely that every atomic
language $L\in\mathcal{V}^{\prime}_{\Delta}$ contains a word $w\in L$ with
$\mathop{\mathsf{supp}}_{\mathcal{P}\Delta^{*}}(L)=\mathop{\mathsf{supp}}_{\Delta^{*}}(w)$.
This shows that $\mathcal{V}$ is complete.

Conversely, suppose that $\mathcal{V}$ is complete, and let
$e_{\Sigma}\colon\Sigma^{*}\twoheadrightarrow M_{\Sigma}$ be a quotient in
$\mathscr{T}_{\Sigma}$. Then, for its dual atom-finite local subvariety
$\mathcal{V}^{\prime}_{\Sigma}$ of $\mathcal{V}_{\Sigma}$, we have that there
exists a morphism $h\colon\Sigma^{*}\to\Delta^{*}$ and an atom-finite local
subvariety $\mathcal{V}^{\prime}_{\Delta}$ of $\mathcal{V}_{\Delta}$
satisfying the conditions (2)(a) and (2)(b) from Definition 16(2). Condition
(2)(a) means precisely that we have the right-hand commutative square above.
Thus, letting $e_{\Delta}\colon\Delta^{*}\twoheadrightarrow M_{\Delta}$ denote
the quotient in $\mathscr{T}_{\Delta}$ that dually corresponds to
$\mathcal{V}^{\prime}_{\Delta}$, we obtain the left-hand diagram above.
Moreover, condition (2)(b) states that $e_{\Delta}$ is support-reflecting.
Thus $\mathscr{T}$ is complete. ∎