1 Introduction

Equations play a fundamental role in (universal) algebra. Their categorical dual in universal coalgebra is the notion of coequations. Coequations were studied extensively in the search for a dual of Birkhoff’s theorem and the specification of classes of coalgebras (see, e.g., [1, 2, 5, 9, 11, 12, 18, 19, 2123]).

The aim of the current paper is a different one: to relate equations to coequations and vice versa. Our starting point is the abstract definition of (co)equations on (co)algebras for an endofunctor. These definitions give rise to categories of equations and coequations; we seek sufficient conditions to obtain dual equivalences between such categories.

We start with a more general concept than a duality, namely, a contravariant adjunction. Our approach is to lift adjunctions to categories of algebras and coalgebras [13]. In the setting of a contravariant adjunction, and by using preservation of limits by adjoints, we have that sets of equations are sent to sets of coequations. To guarantee the converse, i.e., that coequations are also mapped to equations, we assume that the contravariant adjunction is a duality. This gives us a duality result between equations and coequations. We derive known dualities between equations and coequations for automata [7, 24, 25] as a special case of this abstract approach, and we generalize the duality shown in [7] to include (general) dynamical systems.

As a natural next step in this study we include monads and comonads into the picture and prove a lifting theorem to lift contravariant adjunctions to Eilenberg-Moore categories. From this lifting theorem we show the following results:

  • Dualities between equations and coequations for Eilenberg-Moore categories.

  • Lifting of contravariant adjunctions to Eilenberg-Moore categories where, given a contravariant adjunction and a comonad, we define a canonical monad.

  • Lifting of dualities to Eilenberg-Moore categories where, given a duality and a monad, we define a canonical comonad.

The paper is organized as follows. Section 2 is a preliminary section in which we introduce some notation we use in the paper. In Sect. 3 we introduce the abstract definitions of equations and coequations, satisfaction of equations for algebras and satisfaction of coequations for coalgebras. Section 4 introduces the notion of a contravariant adjunction. We state a theorem for lifting contravariant adjunctions (Theorem 3), which is essentially a special case of [13, 2.14.Theorem], and then illustrate this lifting theorem through several examples. In Sect. 5 we focus on the particular case that the contravariant adjunction is a duality to show a general duality result between equations and coequations. Further, we show how to get a canonical notion of satisfaction of equations for coalgebras. In Sect. 6 we include monads and comonads in our setting to prove a lifting theorem (Theorem 11) that allows us to lift contravariant adjunctions to a contravariant adjunction between Eilenberg-Moore categories. We show how to construct a comonad from a given monad and vice versa to get respective lifting theorems. Finally, in Sect. 7 we apply the lifting theorems (to Eilenberg-Moore) to the study of equations and coequations for dynamical systems and deterministic automata.

2 Preliminaries

In this section we introduce the notation for categories of algebras and coalgebras that we will use in the paper. We assume that the reader is familiar with basic concepts from category theory and coalgebra, see, e.g., [6, 22].

Given a category \(\mathcal {D}\) and an endofunctor \(L:\mathcal {D}\rightarrow \mathcal {D}\), we denote by \(\mathrm{alg}(L)\) the category of L-algebras and their homomorphisms, i.e., objects in \(\mathrm{alg}(L)\) are pairs \((X,\alpha )\) where X is an object in \(\mathcal {D}\) and \(\alpha \in \mathcal {D}(LX,X)\), and a homomorphism from an L-algebra \((X_1,\alpha _1)\) to an L-algebra \((X_2,\alpha _2)\) is a morphism \(h\in \mathcal {D}(X_1,X_2)\) such that \(h\circ \alpha _1=\alpha _2\circ Lh\).

Dually, for a given endofunctor \(B:\mathcal {C}\rightarrow \mathcal {C}\) on a category \(\mathcal {C}\), \(\mathrm{coalg}(B)\) denotes the category of B-coalgebras, i.e., objects in \(\mathrm{coalg}(B)\) are pairs \((Y,\beta )\) where Y is an object in \(\mathcal {C}\) and \(\beta \in \mathcal {C}(Y,BY)\), and a homomorphism from a B-coalgebra \((Y_1,\beta _1)\) to a B-coalgebra \((Y_2,\beta _2)\) is a morphism \(h\in \mathcal {C}(Y_1,Y_2)\) such that \(\beta _2 \circ h=Bh\circ \beta _1\).

In case that we have a monad \(\mathsf {L}=(L,\eta ,\mu )\), we let \(\mathrm{Alg}(\mathsf {L})\) denote the category of (Eilenberg-Moore) \(\mathsf {L}\)-algebras, i.e., algebras for the monad \(\mathsf {L}\). Similarly, for a comonad \(\mathsf {B}=(B,\epsilon ,\delta )\), the category \(\mathrm{Coalg}(\mathsf {B})\) consists of Eilenberg-Moore coalgebras for the comonad \(\mathsf {B}\). Notice that we use the notation \(\mathsf {L}, \mathsf {B}\) to refer to (co)monads, and LB to refer to the underlying functors.

Each of the categories \(\mathrm{alg}(L)\), \(\mathrm{Alg}(\mathsf {L})\), \(\mathrm{coalg}(B)\), and \(\mathrm{Coalg}(\mathsf {B})\) has a canonical forgetful functor into the underlying category. For instance, the forgetful functor for \(\mathrm{Alg}(\mathsf {L})\) is the functor \(U:\mathrm{Alg}(\mathsf {L})\rightarrow \mathcal {D}\) defined as \(U(X,\alpha )=X\) and \(Uf=f\) for any L-algebra morphism f. We will refer to those forgetful functors without giving them a specific name.

3 Equations and Coequations

We introduce the abstract definitions of equations and coequations. Let L be an endofunctor on \(\mathcal {D}\) and S be an object in \(\mathcal {D}\). The free L-algebra on S generators is an algebra \(\mathfrak {F}(S)=(\mathfrak {F}(S), \tau )\in \mathrm{alg}(L)\) together with a morphism \(\eta \in \mathcal {D}(S,\mathfrak {F}(S))\), called unit, satisfying the following universal property: for any L-algebra \(X=(X,\alpha )\) and any morphism \(f\in \mathcal {D}(S,X)\) there is a unique morphism \(f^\sharp \in \mathrm{alg}(L)(\mathfrak {F}(S),X)\) such that \(f^\sharp \circ \eta =f\), i.e., the following diagram commutes:

figure a

We define equations for L on S generators as epimorphisms with domain \(\mathfrak {F}(S)\), i.e., elements \(e_P\in \mathrm{alg}(L)(\mathfrak {F}(S),P)\) that are epimorphisms for some \(P=(P,\zeta )\in \mathrm{alg}(L)\). Observe that if L is a polynomial functor on \(\mathrm{Set}\) (see, e.g., [22, Section 10]) then equations can be identified with L-congruences C of \(\mathfrak {F}(S)\), since \(\mathfrak {F}(S)/C\cong P\) for \(C=\ker (e_P)\), and elements in C are pairs of terms with variables on the set S. This corresponds to the classical definition of equations in universal algebra. Finally, we say that an L-algebra \(X=(X,\alpha )\) satisfies the equation \(e_P\), denoted as \((X,\alpha )\,\models \, e_P\), if for any morphism \(f\in \mathcal {D}(S,X)\) the morphism \(f^\sharp \) factors through \(e_P\), i.e., there exists \(g_f\in \mathrm{alg}(L)(P,X)\) such that the following diagram commutes:

figure b

Now, assuming that the free L-algebra on S generators \(\mathfrak {F}(S)=(\mathfrak {F}(S),\tau )\) exists, we can define the category \(\mathrm{eq}(L,S)\) of equations for L on S generators as follows:

$$\begin{aligned} \text {Objects of } \mathrm{eq}(L,S)\!:&\text { epimorphisms } e_X\in \mathrm{alg}(L)( \mathfrak {F}(S), X) \text { for some }\\&X=(X,\alpha )\in \mathrm{alg}(L).\\ \text {Arrows of } \mathrm{eq}(L,S)\!:&\text { for }e_{X_i}\in \mathrm{eq}(L,S), i=1,2, \text { a morphism }\\&f\in \mathrm{eq}(L,S)(e_{X_1},e_{X_2}) \text { is a morphism }f\in \mathrm{alg}(L)(X_1,X_2)\\&\text { such that the following diagram commutes:} \end{aligned}$$
figure c

Notice that morphisms in \(\mathrm{eq}(L,S)\) are necessarily epimorphisms.

Example 1

Consider the \(\mathrm{Set}\) endofunctor L given by \(LX = A \times X\), where A is a fixed set, and the singleton set \(S = 1\) of generators. Then an L-algebra together with an assignment of the single generator is a pointed deterministic automaton, i.e., a triple \((X, \alpha , x)\) consisting of a set of states X, a transition function \(\alpha :A \times X \rightarrow X\) and an element \(x \in X\).

The free L-algebra on 1 is given by \(A^*=(A^*,\tau )\) where \(\tau :A\times A^*\rightarrow A^*\) is defined by \(\tau (a,w)=wa\) and the unit \(\eta :1\rightarrow A^*\) maps the single generator to the empty word \(\varepsilon \in A^*\), i.e., \(\eta =\varepsilon \). Given a pointed automaton \((X,\alpha ,x)\) we obtain a unique homomorphism \(r_x :A^* \rightarrow X\), given by \(r_x(\varepsilon )= x\) and \(r_x(wa) = \alpha (a,r_x(w))\). In the sequel we sometimes denote \(r_x(w)\) by w(x), the state we reach from the state x by processing the word w.

A right congruence on \(A^*\) is an equivalence relation \(C\subseteq A^*\times A^*\) such that for any \(a\in A\) and \((u,v)\in C\) we have that \((ua,va)\in C\). Right congruences C correspond to equations as defined above, by letting \(A^*/C=(A^*/C,[\tau ])\in \mathrm{alg}(L)\) where \([\tau ]\) is given by \([\tau ](a,[w])=[wa]\) and the epimorphism (equation) \(e_C\in \mathrm{alg}(L)(A^*,A^*/C)\) maps every word to its equivalence class.

An L-algebra \((X,\alpha )\) satisfies the equation \(e_C\), i.e., \((X,\alpha )\,\models \, C\), if and only if for every \((u,v)\in C\) and any \(x\in X\), we have \(r_x(u)=r_x(v)\). This coincides with satisfaction of equations as defined in [7].

Notice that the function \(\tau ':A\times A^*\rightarrow A^*\) defined as \(\tau ' (a,w)=aw\) is such that the algebra \((A^*,\tau ')\) is also a free L-algebra, which gives us the notion of left congruence as a corresponding notion of equation.    \(\square \)

We dualize the definition of equations to obtain the definition of coequations, e.g., [18, 19, 22]. Let B be an endofunctor on \(\mathcal {C}\) and R be an object in \(\mathcal {C}\). The cofree B-coalgebra on R colours is a coalgebra \(\mathfrak {C}(R)=(\mathfrak {C}(R), \upsilon )\in \mathrm{coalg}(B)\) together with a morphism \(\epsilon \in \mathcal {C}(\mathfrak {C}(R),R)\), called counit, satisfying the following universal property: for any B-coalgebra \(Y=(Y,\beta )\) and any morphism (colouring) \(f\in \mathcal {C}(Y,R)\) there is a unique morphism \(f^\flat \in \mathrm{coalg}(L)(Y,\mathfrak {C}(R))\) such that \(\epsilon \circ f^\flat =f\), i.e., the following diagram commutes:

figure d

We define coequations for B on R colours as monomorphisms with codomain \(\mathfrak {C}(R)\), i.e., elements \(m_Q\in \mathrm{coalg}(B)(Q,\mathfrak {C}(R))\) that are monomorphisms for some \(Q=(Q,\delta )\in \mathrm{coalg}(B)\). We say that a B-coalgebra \(Y=(Y,\beta )\) satisfies the coequation \(m_Q\), denoted as \((Y,\beta )\mid \models m_Q\) (notice the difference between the symbols: \(\,\models \,\) for equations and \(\mid \models \) for coequations), if for any morphism (colouring) \(f\in \mathcal {C}(Y,R)\) the morphism \(f^\flat \) factors through \(m_Q\), i.e., there exists \(g_f\in \mathrm{coalg}(B)(Y,Q)\) such that the following diagram commutes:

figure e

Assuming that the cofree B-coalgebra on R colours \(\mathfrak {C}(R)=(\mathfrak {C}(R),\upsilon )\) exists, define the category \(\mathrm{coeq}(B,R)\) of coequations for B on R colours whose objects are monomorphisms \(m_Y\in \mathrm{coalg}(B)(Y,\mathfrak {C}(R))\) for some \(Y=(Y,\beta )\in \mathrm{coalg}(B)\), and, a morphism between two objects \(m_{Y_1}\) and \(m_{Y_2}\) in \(\mathrm{coeq}(B,R)\) is a morphism \(g\in \mathrm{coalg}(B)(Y_1,Y_2)\) such that \(m_{Y_2}\circ g=m_{Y_1}\). Notice that morphisms in \(\mathrm{coeq}(B,R)\) are necessarily monomorphisms.

Example 2

For a given set A, consider the \(\mathrm{Set}\) endofunctor B defined by \(BX = X^A\), and consider the two-element set \(R=2\) of colours. Then a B-coalgebra together with an assignment of colours to states is a coloured deterministic automaton: a triple \((Y, \beta , f)\) consisting of a set of states Y, a transition function \(\beta :Y \rightarrow Y^A\) and an assignment of final states \(f :Y \rightarrow 2\).

The cofree B-coalgebra on 2 colours is given by \(2^{A^*}=(2^{A^*}, \upsilon )\) where \(\upsilon :2^{A^*}\rightarrow (2^{A^*})^A\) is given by right derivative

$$ \upsilon (L)(a)=L_a = \{w \mid aw \in L\} $$

and the counit \(\epsilon :2^{A^*}\rightarrow 2\) is given by \(\epsilon (L)=L(\varepsilon )\). Given a coloured deterministic automaton \((Y, \beta , f)\), we obtain a unique B-coalgebra morphism \(l :Y \rightarrow 2^{A^*}\) that maps every state to the language it accepts, i.e., \(l(x)(\varepsilon ) = f(x)\) and \(l(x)(aw) = l(\beta (x)(a))(w)\).

Coequations for B on R correspond to subsets of \(2^{A^*}\) that are closed under right derivatives, i.e., subcoalgebras of \(2^{A^*}\). Given any monomorphism (coequation) \(m_Q\) with codomain \(2^{A^*}\) and a B-coalgebra \((Y,\beta )\), we have that \((Y,\beta )\mid \models m_Q\) if and only if for every 2-colouring \(f\in \mathrm{Set}(Y,2)\) the set of those languages accepted by the states of the coloured automaton \((Y,\beta ,f)\) is contained in \(\mathrm{Im}(m_Q)\). This coincides with satisfaction of coequations as defined in [7].

Similarly to the previous example, the function \(\upsilon ':2^{A^*}\rightarrow (2^{A^*})^A\) given by left derivative

$$ \upsilon ' (L)(a)={_a}L = \{w \mid wa \in L\} $$

is such that \((2^{A^*},\upsilon ')\) is also a cofree B-coalgebra for which the corresponding notion of coequations are subsets of \(2^{A^*}\) closed under left derivatives.    \(\square \)

4 Lifting Contravariant Adjunctions

In this section we recall the notion of a contravariant adjunction and how to lift it to categories of algebras and coalgebras, according to [13, 14]. We instantiate this abstract approach in examples of constructions on various kinds of automata.

Given two contravariant functors \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) (i.e., F and G reverse the direction of arrows), a contravariant adjunction between F and G, denoted by \(F \dashv \vdash G\), is a bijection

$$ \mathcal {D}(X,FY)\cong \mathcal {C}(Y,GX) $$

which is natural in both \(X\in \mathcal {D}\) and \(Y\in \mathcal {C}\). Observe that both F and G are on the codomain of the Hom-sets. Such a contravariant adjunction can be equivalently defined by two units \(\eta ^{FG}:Id_\mathcal {D}\Rightarrow FG\) and \(\eta ^{GF}:Id_\mathcal {C}\Rightarrow GF\) that satisfy the triangle identities \(G\eta ^{FG}\circ \eta ^{GF}_G=Id_{G}\) and \(F\eta ^{GF}\circ \eta ^{FG}_F=Id_F\). By standard preservation properties, both F and G map colimits to limits, in particular initial objects to final objects and epimorphisms to monomorphisms.

Given a contravariant adjunction as above, if \(\eta ^{GF}\) and \(\eta ^{FG}\) are isomorphisms then we say FG form a duality, and denote it by \(F \cong G\). In this case, limits are mapped to colimits and vice versa.

Our basic setting consists of a contravariant adjunction between F and G, an endofunctor B on \(\mathcal {C}\) and an endofunctor L on \(\mathcal {D}\), depicted in the diagram below. Throughout this paper we depict contravariant functors in diagrams with an ‘\(\times \)’ at the beginning of the arrow.

figure f

In this setting, we are interested in lifting the adjunction to a contravariant adjunction between lifted functors \(\widehat{F}:\mathrm{coalg}(B)\rightarrow \mathrm{alg}(L)\) and \(\widehat{G}:\mathrm{alg}(L)\rightarrow \mathrm{coalg}(B)\) of F and G, respectively, as in the following picture:

                           

figure g

where the vertical arrows are forgetful functors. An important consequence of such a lifting is that, if L has an initial algebra, then it is mapped by \(\widehat{G}\) to a final B-coalgebra.

In [13, 2.14.Theorem] it is shown that a sufficient condition for such a lifting is the existence of a natural isomorphism \(\gamma :GL\Rightarrow BG\). This is summarized by the theorem below.

Theorem 3

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a contravariant adjunction. Let B be an endofunctor on \(\mathcal {C}\) and L be an endofunctor on \(\mathcal {D}\). If there is a natural isomorphism \(\gamma :GL\Rightarrow BG\), then

  1. 1.

    The adjunction \(F \dashv \vdash G\) lifts to an adjunction as in Diagram (1), i.e., to a contravariant adjunction between functors \(\widehat{F}:\mathrm{coalg}(B) \rightarrow \mathrm{alg}(L)\) and \(\widehat{G}:\mathrm{alg}(L) \rightarrow \mathrm{coalg}(B)\).

  2. 2.

    If FG form a duality then \(\widehat{F}, \widehat{G}\) form a duality as well.

The functors \(\widehat{F}:\mathrm{coalg}(B) \rightarrow \mathrm{alg}(L)\) and \(\widehat{G}:\mathrm{alg}(L) \rightarrow \mathrm{coalg}(B)\) are defined on objects as:

$$\begin{aligned}&(Y\overset{\beta }{\longrightarrow } BY)\overset{\widehat{F}}{\longmapsto } (LFY\overset{\rho _Y}{\longrightarrow }FBY\overset{F\beta }{\longrightarrow }FY)\\&(LX\overset{\alpha }{\longrightarrow } X)\overset{\widehat{G}}{\longmapsto } (GX\overset{G\alpha }{\longrightarrow }GLX\overset{\gamma _X}{\longrightarrow }BGX) \end{aligned}$$

and on morphisms as \(\widehat{F}=F\) and \(\widehat{G}=G\). The natural transformation \(\rho :LF \Rightarrow FB\) in the definition of \(\widehat{F}\) is defined as the mate of the inverse \(\gamma ^{-1} :BG \Rightarrow GL\):

$$ \rho \overset{\text { def. }}{=}FB\eta ^{GF}\circ F\gamma ^{-1}F\circ \eta ^{FG}LF, $$

using the units \(\eta ^{GF}\) and \(\eta ^{FG}\) of the adjunction. Natural transformations of the form \(\rho :LF \Rightarrow FB\) and the definition of \(\widehat{F}\) form the heart of the approach to coalgebraic modal logic based on contravariant adjunctions/dualities (see, e.g., [8, 15, 16, 20]). There is a one-to-one correspondence between such natural transformations and those of the form \(BG \Rightarrow GL\), using the above construction. We are only interested in the case where the natural transformation \(BG \Rightarrow GL\) is an isomorphism, to lift adjunctions, as in [17]. For notational convenience, the direction in \(\gamma :GL \Rightarrow BG\) is reversed in the current paper.

In the rest of this section we provide examples and applications of Theorem 3 and the setting in Diagram (1).

Example 4

[17, Example 4] For a fixed set A consider the following situation:

figure h

Here L-algebras are pointed deterministic automata on A (Example 1) and B-coalgebras are two-coloured deterministic automata on A (Example 2). The contravariant functors F and G form a contravariant adjunction which, by Theorem 3, can be lifted to an adjunction between \(\widehat{F}\) and \(\widehat{G}\). The isomorphism \(\gamma :GL\Rightarrow BG\) is defined for any X as the function \(\gamma _X:2^{A\times X+1}\rightarrow 2\times (2^X)^A\) such that \(\gamma _X (f)=(f(\cdot ), \lambda a.\ \lambda x. f(a,x))\).

Given a B-coalgebra \((Y,\langle c,\beta \rangle )\) we have that \(\widehat{F} (Y,\langle c,\beta \rangle )=(2^Y,[\alpha ,i])\) where \(\alpha :A\times 2^Y\rightarrow 2^Y\) and \(i:1\rightarrow 2^Y\) are functions defined as follows:

$$\begin{aligned} i(\cdot )&=c^{-1}(\{1\})=\text { accepting states of }(Y,\langle c,\beta \rangle ),\\ \alpha (a,Z)&=\{y\in Y\ |\ \beta (y)(a)\in Z\}. \end{aligned}$$

Given an L-algebra \((X,[\alpha ,i])\) we have that \(\widehat{G}(X,[\alpha ,i])=(2^X,\langle c,\beta \rangle )\) where the functions \(c:2^X\rightarrow 2\) and \(\beta :2^X\rightarrow (2^X)^A\) are defined as:

$$\begin{aligned} c(Z)&=1 \text { iff }i(\cdot )\in Z\\ \beta (Z)(a)&=\{x\in X\ |\ \alpha (a,x)\in Z\} \end{aligned}$$

Recall from Example 1 that the initial L-algebra is given by \((A^*,[\eta ,\tau '])\), where \(A^*\) is the free monoid with generators A and identity element \(\varepsilon \), \(\eta :1\rightarrow A^*\) is the empty word \(\varepsilon \) and \(\tau ':A\times A^*\rightarrow A^*\) is the concatenation function given by \(\tau '(a,w)=aw\). Because of the contravariant adjunction, the initial L-algebra is sent by \(\widehat{G}\) to the final B-coalgebra, given by \(\widehat{G}(A^*,[\eta ,\tau '])=(2^{A^*},\langle \hat{\epsilon },\hat{\tau }\rangle )\) where \(\hat{\epsilon }(L)=L(\varepsilon )\) and \(\hat{\tau }(L)(a)(w)=L(aw)\). Note that the final B-coalgebra is not sent by \(\widehat{F}\) to the initial L-algebra.    \(\square \)

Example 5

Let \(\mathrm{CABA}\) be the category of complete atomic Boolean algebras whose morphisms are complete Boolean algebra homomorphisms. For a fixed set A consider the following situation:

figure i

Here \(\mathrm{At}(Y)\) denotes the set of atoms of the object Y in \(\mathrm{CABA}\). The contravariant functors F and G form a contravariant adjunction, in fact a duality, which, by Theorem 3, can be lifted to a duality between \(\widehat{F}\) and \(\widehat{G}\) if we consider the canonical natural isomorphism \(\gamma :GL\Rightarrow BG\) defined for every X as the morphism \(\gamma _X:2^{A\times X+1}\rightarrow 2\times (2^X)^A\) such that \(\gamma _X (f)=(f(\cdot ), \lambda a.\ \lambda x. f(a,x))\).

Given a B-coalgebra \((Y,\langle c,\beta \rangle )\), we have that \(\widehat{F} (Y,\langle c,\beta \rangle )=(\mathrm{At}(Y),[\alpha ,i])\) where the functions \(\alpha :A\times \mathrm{At}(Y)\rightarrow \mathrm{At}(Y)\) and \(i:1\rightarrow \mathrm{At}(Y)\) are defined as follows:

$$\begin{aligned} i(\cdot )&=\text { the unique element }y_0\in \mathrm{At}(Y) \text { s.t. } c(y_0)=1,\\ \alpha (a,y)&=\text { the unique element } y'\in \mathrm{At}(Y) \text { s.t. } \beta (y')(a)\ge y. \end{aligned}$$

In particular, if \(P\subseteq 2^{A^*}\) is a preformation of languages [7, Definition 11], i.e., \(P\in \mathrm{CABA}\) and it is closed under left and right derivativesFootnote 1, then \((P,\langle \hat{\epsilon },\hat{\tau }'\rangle )\in \mathrm{coalg}(B)\) where \(\hat{\epsilon }(L)=L(\varepsilon )\) and \(\hat{\tau }'(L)(a)={_a}L\). In this case, \(\widehat{F}(P,\langle \hat{\epsilon },\hat{\tau }'\rangle )=\mathbf {free}(P)\) which is the quotient \(A^*/C\) where C is the set, in fact congruence, of all equations satisfied by the automaton \((P,\hat{\tau })\), where \(\hat{\tau }(L)(a)=L_a\) (see [7]).

Given an L-algebra \((X,[\alpha ,i])\), we have that \(\widehat{G}(X,[\alpha ,i])=(2^X,\langle c,\beta \rangle )\) where the CABA morphisms \(c:2^X\rightarrow 2\) and \(\beta :2^X\rightarrow (2^X)^A\) are defined as

$$\begin{aligned} c(Z)&=1 \text { iff }i(\cdot )\in Z\\ \beta (Z)(a)&=\{x\in X\ |\ \alpha (a,x)\in Z\}. \end{aligned}$$

In particular, if C is a congruence of the monoid \(A^*\) then \((A^*/C,[[\tau '],[\varepsilon ]])\in \mathrm{alg}(L)\) where \([\tau '](a,[w])=[aw]\). In this case, \(\widehat{G}(A^*/C,[[\tau '],[\varepsilon ]])\cong \mathbf {cofree}(A^*/C)\) which is the minimum set of coequations that the automaton \((A^*/C,[\tau ])\) satisfies, where \([\tau ](a,[w])=[wa]\) (see [7]).

Similarly to the previous example, the initial L-algebra \(A^*=(A^*,[\eta ,\tau '])\), where \(\eta =\varepsilon \) and \(\tau '(a,w)=aw\), is sent by \(\widehat{G}\) to the final B-coalgebra \(2^{A^*}=(2^{A^*},\langle \hat{\epsilon },\hat{\tau }\rangle )\), where \(\hat{\epsilon }(L)=L(\varepsilon )\) and \(\hat{\tau }(L)(a)(w)=L(aw)\). Also, because the contravariant adjunction is a duality, the final B-coalgebra \(2^{A^*}\) is sent by \(\widehat{F}\) to the initial L-algebra \(A^*\). We will explore this case further in Sect. 5 to get dualities between sets of equations and sets of coequations.    \(\square \)

Example 6

For a fixed field \(\mathbb {K}\), let \(\mathrm{{Vec_\mathbb {K}}}\) be the category of vector spaces over \(\mathbb {K}\) with linear maps. Let A be a fixed set and consider the following situation:

figure j

Here \(X^\partial =\mathrm{{Vec_\mathbb {K}}}(X,\mathbb {K})\), the dual space of X, and \(A\times X:=\coprod _{a\in A}X\). We have that the contravariant functors F and G form a contravariant adjunction which, by Theorem 3, can be lifted to a contravariant adjunction between \(\widehat{F}\) and \(\widehat{G}\) if we consider the canonical natural isomorphism \(\gamma :GL\Rightarrow BG\) defined for every X as the map \(\gamma _X:(\mathbb {K}+A\times X)^\partial \rightarrow \mathbb {K}\times (X^\partial )^A\) such that \(\gamma _X (\varphi )=(\varphi (1), \lambda a.\ \lambda x. \varphi (a,x))\).

Given a B-coalgebra \((Y,\langle c,\beta \rangle )\), we have that \(\widehat{F} (Y,\langle c,\beta \rangle )=(Y^\partial ,[i,\alpha ])\) where \(i:\mathbb {K}\rightarrow Y^\partial \) and \(\alpha :A\times Y^\partial \rightarrow Y^\partial \) are linear maps which are defined on the canonical basis as:

$$\begin{aligned} i(1)(y)&=c(y)\\ \alpha (a,\varphi )(y)&=(\varphi \circ \beta (y))(a)=\varphi ( \beta (y)(a)) \end{aligned}$$

In particular, if \(S\subseteq \mathbb {K}^{A^*}\) is a subsystem such that for every \(f\in S\) and \(a\in A\), \(f_a,{_a}f\in S\), where \(f_a(w)=f(aw)\) and \({_a}f(w)=f(wa)\), \(w\in A^*\), then we have that \((S,\langle \hat{\epsilon },\hat{\tau }'\rangle )\in \mathrm{coalg}(B)\) where \(\hat{\epsilon }(f)=f(\varepsilon )\) and \(\hat{\tau }'(f)(a)={_a}f\). In this case, \(\widehat{F}(S,\langle \hat{\epsilon },\hat{\tau }'\rangle )\cong \mathbf {free}(S)\) which is the quotient \(V(A^*)/C\) where C is the set, in fact linear congruence, of all linear equations satisfied by the automaton \((S,\hat{\tau })\). Here \(V(A^*)=\{\phi :A^*\rightarrow \mathbb {K} \mid \mathrm{supp}(\phi ) \text { is finite}\}\), where \(\mathrm{supp}(\phi )=\{w\in A^*\mid \phi (w)\ne 0\}\) is the support of \(\phi \), and the function \(\hat{\tau }\) is defined as \(\hat{\tau }(f)(a)=f_a\) (see [25]).

Given an L-algebra \((X,[i,\alpha ])\), we have that \(\widehat{G}(X,[i,\alpha ])=(X^\partial ,\langle c,\beta \rangle )\) where the linear maps \(c:X^\partial \rightarrow \mathbb {K}\) and \(\beta :X^\partial \rightarrow (X^\partial )^A\) are defined as

$$\begin{aligned} c(\varphi )&=\varphi (i(1))\\ \beta (\varphi )(a)(x)&=\varphi (\alpha (a,x)) \end{aligned}$$

In particular, if \(C\subseteq V(A^*)\times V(A^*)\) is a linear congruence on \(V(A^*)\), then we have that \((V(A^*)/C,[[\tau '],[\varepsilon ]])\in \mathrm{alg}(L)\), where \([\tau '](a,[\phi ])=[a\phi ]\), and we have that \(\widehat{G}(V(A^*)/C,[[\tau '],[\varepsilon ]]) \cong \mathbf {cofree}(V(A^*)/C)\) which is the minimum set of coequations (power series) satisfied by the automaton \((V(A^*)/C,[\tau ])\), where \([\tau ](a,[\phi ])=[\phi a]\) (see [25]).

Notice that the contravariant adjunction is not a duality, but if we restrict to vector spaces of finite dimension then we get a duality. In the latter case there is no initial L-algebra or, equivalently, there is no final B-coalgebra.    \(\square \)

5 Duality Between Equations and Coequations

In Sect. 3, we defined equations as epimorphisms from an initial algebra and coequations as monomorphisms into a final coalgebra. In the previous section, we have seen how to relate initial algebras and final coalgebras by lifting contravariant adjunctions and dualities. Next, we describe how to apply these liftings to obtain a correspondence between equations and coequations.

If we lift the contravariant adjunction on the base categories to a contravariant adjunction \(\widehat{F} :\mathrm{coalg}(B) \rightarrow \mathrm{alg}(L)\) and \(\widehat{G} :\mathrm{alg}(L) \rightarrow \mathrm{coalg}(B)\) as in the previous section, then \(\widehat{G}\) sends the initial L-algebra to the final B-coalgebra, and \(\widehat{G}\) sends epimorphisms to monomorphisms. As a consequence, equations are sent by \(\widehat{G}\) to coequations. However, \(\widehat{F}\) does not map coequations to equations, in general.

In order to obtain a full correspondence between equations and coequations, suppose that the contravariant adjunction between F and G is a duality (and that there is a natural isomorphism \(\gamma :GL\Rightarrow BG\)). Then, by Theorem 3, the duality between F and G lifts to a duality between \(\widehat{F}\) and \(\widehat{G}\). In this case, we can add another level to the picture in (1), yielding a duality between equations and coequations:

                        

figure k

where \(\mathrm{eq}(L,S)\) and \(\mathrm{coeq}(B,G(S))\) are the categories of equations for L on S generators and coequations for B on G(S) colours respectively, as defined in Sect. 3, lower vertical arrows are forgetful functors, and upper vertical arrows are the canonical functors \(U:\mathrm{coeq}(B,G(S))\rightarrow \mathrm{coalg}(B)\) and \(V:\mathrm{eq}(L,S)\rightarrow \mathrm{alg}(S)\) which are defined as \(U(m_Y)=Y\) and \(V(e_X)=X\) on objects and \(Uf=f\) and \(Vg=g\) on morphisms.

Theorem 7

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a duality. Let B be an endofunctor on \(\mathcal {C}\), L be an endofunctor on \(\mathcal {D}\) with an object S in \(\mathcal {D}\) such that the free L-algebra \(\mathfrak {F}(S)\) on S generators exists. If there is a natural isomorphism \(\gamma :GL\Rightarrow BG\) then:

  1. 1.

    The duality between F and G lifts to a duality \(\widehat{F}:\mathrm{coeq}(B,G(S)) \rightarrow \mathrm{eq}(L,S)\) and \(\widehat{G}:\mathrm{eq}(L,S) \rightarrow \mathrm{coeq}(B,G(S))\), as in Diagram (2).

  2. 2.

    Given \(e_P\in \mathrm{eq}(L,S)\), \(m_Q\in \mathrm{coeq}(B,G(S))\), \((X,\alpha )\in \mathrm{alg}(L)\), and \((Y,\beta )\in \mathrm{coalg}(B)\) we have:

    1. (i)

      \((X,\alpha )\,\models \, e_P\) if and only if \(\widehat{G}(X,\alpha )\mid \models \widehat{G}(e_P)\).

    2. (ii)

      \(\widehat{F}(Y,\beta )\,\models \, \widehat{F}(m_Q)\) if and only if \((Y,\beta )\mid \models m_Q\).

As an application of the previous theorem we have the following.

Example 8

(cf. Example 5) For a fixed set A consider the following situation:

figure l

If we put \(S=1\), then we get a duality between \(\mathrm{eq}(L, 1)\), whose objects can be identified with right congruences of \(A^*\), and \(\mathrm{coeq}(B,2)\), whose objects can be identified with subalgebras \(Q\subseteq 2^{A^*}\) in \(\mathrm{CABA}\) that are closed under left derivatives. From this setting, if we consider congruences of \(A^*\) and subalgebras of \(2^{A^*}\) that are closed both under left and right derivatives, we can derive the duality between equations and coequations that was shown in [7, Theorem 22]. We will come back to this situation in a more general setting in Sect. 7.1 and also in a slightly different setting in Sect. 7.2.   \(\square \)

Example 9

In this example we explicitly show that if the contravariant adjunction is not a duality then sets of coequations are not always sent to sets of equations. For the set \(A=\{a,b\}\) consider the situation:

figure m

In this case, consider the set \(S=1\) of generators. The free L-algebra on S generators is given by \(A^*=(A^*,\tau ')\), where \(\tau '(a,w)=aw\), and unit \(\eta =\varepsilon \). The cofree B-coalgebra on \(G(S)=2\) colours is the coalgebra \(2^{A^*}=(2^{A^*},\upsilon )=\widehat{G}(A^*)\), where \(\upsilon (L)(a)(w)=L(aw)\), and counit \(\epsilon (L)=L(\varepsilon )\). Now, consider the element \(m_Q\in \mathrm{coeq}(B,2)\) where \(Q=\{\emptyset , A^*\}\) and \(m_Q\) is the inclusion map \(m_Q:Q\rightarrow 2^{A^*}\). Then the codomain of \(\widehat{F}(m_Q)\) is \((2^Q,\alpha )\) where \(\alpha (a,f)=\alpha (b,f)=f\) for all \(f\in 2^Q\) (this definition of \(\alpha \) follows from Example 4).

We have that \(2^Q=(2^Q,\alpha )\) cannot be a homomorphic image of \(A^*\). In fact, if there exists an epimorphism \(e\in \mathrm{alg}(L) (A^*, 2^Q)\) then there is a right congruence C of \(A^*\) such that \((A^*/C,[\tau '])\cong (2^Q,\alpha )\) which means that \(A^*/C\) has four equivalence classes and for each equivalence class \([w]\in A^*/C\) we have that \([w]=[aw]=[bw]\), which is a contradiction since the last equality implies that there is only one equivalence class.   \(\square \)

5.1 Equations for Coalgebras

In this section we show how to define equations for coalgebras by using liftings of contravariant adjunctions. The concepts presented here can be dualized to define coequations for algebras.

Assume that we have lifted a contravariant adjunction between functors \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) to a contravariant adjunction between \(\widehat{F}:\mathrm{coalg}(B)\rightarrow \mathrm{alg}(L)\) and \(\widehat{G}:\mathrm{alg}(L)\rightarrow \mathrm{coalg}(B)\) for an endofunctor B on \(\mathcal {C}\) and an endofunctor L on \(\mathcal {D}\). Given an equation \(e_P\in \mathrm{eq}(L,S)\) for some S in \(\mathcal {D}\), we define, for a given coalgebra \((Y,\beta )\) in \(\mathrm{coalg}(B)\), \((Y,\beta )\,\models \, e_P\), and say that the coalgebra \((Y,\beta )\) satisfies the equation \(e_P\), as:

$$ (Y,\beta )\,\models \, e_P\ \ \overset{def}{\Leftrightarrow }\ \ \widehat{F}(Y,\beta )\,\models \, e_P. $$

Notice that if \(\widehat{F}\) and \(\widehat{G}\) form a duality then \(\widehat{F}(Y,\beta )\,\models \, e_P\) is equivalent to \((Y,\beta )\mid \models \widehat{G}(e_P)\). One could be tempted to use \((Y,\beta )\mid \models \widehat{G}(e_P)\) as a definition for \((Y,\beta )\,\models \, e_P\) since \(\widehat{G}(e_P)\in \mathrm{coeq}(B, G(S))\) but we prefer to avoid this since the dual argument is not true in general, i.e., given \(m_Q\in \mathrm{coeq}(B,G(S))\), \(\widehat{F}(m_Q)\) is not always in \(\mathrm{eq}(L,S)\), as it was shown in Example 9.

Example 10

Consider the situation given in Example 4 and let \(S=\emptyset \). Then we have that for a B-coalgebra (deterministic automaton) \(Y=(Y,\langle c,\beta \rangle )\) and a right congruence C on \(A^*\):

In words, a right congruence C on \(A^*\) is satisfied by \(Y=(Y,\langle c,\beta \rangle )\) if for every pair \((u,v) \in C\) the set of states that accept u coincides with the set of states that accept v.

In Example 1 we also defined satisfaction of right congruences for deterministic automata, as the canonical notion that arises by viewing (the transition structure of) automata as algebras. According to this, if we consider \((Y,\beta )\) as an \(A\times Id_{\mathrm{Set}}\)-algebra, we have a direct definition for \((Y,\beta )\,\models \, C\). We conclude this example by showing the relation between \((Y,\langle c,\beta \rangle )\,\models \, C\) and \((Y,\beta )\,\models \, C\).

Consider the coloured automaton \((Y,\langle c,\beta \rangle )\) on \(A=\{a\}\) given by:

figure n

If we denote by \( \langle u=v\rangle \) the least right congruence containing the pair \((u,v)\in A^*\times A^*\), then we have that \((Y,\langle c,\beta \rangle )\,\models \, \langle a=aa\rangle \) since

$$ \{y\in Y\ |\ c(a(y))=1\}=\{r,s,t\}=\{y\in Y\ |\ c(aa(y))=1\} $$

but \((Y,\beta )\,\not \models \, \langle a=aa \rangle \) since \(a(r)=s\ne t=aa(r)\). One can prove that \((Y,\beta )\,\models \, \langle u=v\rangle \) implies \((Y,\langle c,\beta \rangle )\,\models \, \langle u=v\rangle \) and that the converse holds if \((Y,\langle c,\beta \rangle )\) is minimal.   \(\square \)

6 Lifting Contravariant Adjunctions to Eilenberg-Moore Categories

In this section we extend the results from the previous sections, on lifting adjunctions and dualities, to the case that the endofunctor L is a monad and the functor B is a comonad. We state the main theorem for lifting contravariant adjunctions to Eilenberg-Moore categories (Theorem 11), and obtain a theorem for dualities between equations and coequations as a consequence. Further, given either a monad or a comonad, we show how to derive a corresponding canonical comonad or monad, respectively.

Assume a contravariant adjunction between \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\), a monad \(\mathsf {L}=(L,\eta ,\mu )\) on \(\mathcal {D}\), and a comonad \(\mathsf {B}=(B,\epsilon ,\delta )\) on \(\mathcal {C}\), as summarized in the following picture:

figure o

Then we can ask under what conditions the contravariant adjunction can be lifted to functors \(\widehat{F}:\mathrm{Coalg}(\mathsf {B})\rightarrow \mathrm{Alg}(\mathsf {L})\) and \(\widehat{G}:\mathrm{Alg}(\mathsf {L})\rightarrow \mathrm{Coalg}(\mathsf {B})\) on the Eilenberg-Moore categories. Similar to the approach in Sect. 4, we require a natural isomorphism \(\gamma :GL\Rightarrow BG\), but for the current case we also require \(\gamma \) to satisfy certain conditions that relate the monad \(\mathsf {L}\) and the comonad \(\mathsf {B}\).

Theorem 11

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a contravariant adjunction. Let \(\mathsf {L}=(L,\eta ,\mu )\) be a monad on \(\mathcal {D}\), and \(\mathsf {B}=(B,\epsilon ,\delta )\) a comonad on \(\mathcal {C}\). If there is a natural isomorphism \(\gamma :GL\Rightarrow BG\) such that the following two diagrams commute:

figure p

then F lifts to a functor \(\widehat{F}:\mathrm{Coalg}(\mathsf {B})\rightarrow \mathrm{Alg}(\mathsf {L})\) and G lifts to a functor \(\widehat{G}:\mathrm{Alg}(\mathsf {L})\rightarrow \mathrm{Coalg}(\mathsf {B})\), such that \(\widehat{F}\) and \(\widehat{G}\) form a contravariant adjunction. Additionally, if F and G form a duality then \(\widehat{F}\) and \(\widehat{G}\) form a duality.

As an application of the previous theorem we can derive dualities between equations and coequations in Eilenberg-Moore categories, whose general result is obtained in a similar way as in Sect. 3. Notice that we do not need to explicitly assume the existence of free algebras since for any object S in \(\mathcal {D}\) the algebra \((LS,\mu _S)\in \mathrm{Alg}(\mathsf {L})\) has the universal property that characterizes free objects, with the unit given by \(\eta _S:S\rightarrow LS\).

Theorem 12

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a duality. Let \(\mathsf {L}=(L,\eta ,\mu )\) be a monad on \(\mathcal {D}\), and \(\mathsf {B}=(B,\epsilon ,\delta )\) a comonad on \(\mathcal {C}\). If there is a natural isomorphism \(\gamma :GL\Rightarrow BG\) making the diagrams (3) commute, then:

  1. 1.

    The duality between F and G lifts to a duality \(\widehat{F}:\mathrm{Coeq}(\mathsf {B},G(S)) \rightarrow \mathrm{Eq}(\mathsf {L},S)\) and \(\widehat{G}:\mathrm{Eq}(\mathsf {L},S) \rightarrow \mathrm{Coeq}(\mathsf {B},G(S))\).

  2. 2.

    Given \(e_P\in \mathrm{Eq}(\mathsf {L},S)\), \(m_Q\in \mathrm{Coeq}(\mathsf {B},G(S))\), \((X,\alpha )\in \mathrm{Alg}(\mathsf {L})\), and \((Y,\beta )\in \mathrm{Coalg}(\mathsf {B})\) we have that:

    1. (i)

      \((X,\alpha )\,\models \, e_P\) if and only if \(\widehat{G}(X,\alpha )\mid \models \widehat{G}(e_P)\).

    2. (ii)

      \(\widehat{F}(Y,\beta )\,\models \, \widehat{F}(m_Q)\) if and only if \((Y,\beta )\mid \models m_Q\).

We proceed with special cases of our setting where, given the contravariant adjunction and a comonad \(\mathsf {B}\) on \(\mathcal {C}\), we can canonically define a monad \(\mathsf {L}\) on \(\mathcal {D}\) such that the contravariant adjunction lifts (Sect. 6.1). We can also do it in the opposite way, i.e., define a comonad from a given monad, but in this case additional assumptions are required (Sect. 6.2).

6.1 Defining a Monad from a Comonad

In this part we start with a contravariant adjunction between contravariant functors \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) and a comonad \(\mathsf {B}=(B,\epsilon , \delta )\) on \(\mathcal {C}\). That is, we have the following setting:

figure q

The purpose is to find a canonical monad \(\mathsf {L}=(L,\eta ,\mu )\) on \(\mathcal {D}\) together with a lifting \(\widehat{F}:\mathrm{Coalg}(\mathsf {B})\rightarrow \mathrm{Alg}(\mathsf {L})\) and \(\widehat{G}:\mathrm{Alg}(\mathsf {L})\rightarrow \mathrm{Coalg}(\mathsf {B})\) of the contravariant adjunction. We choose \(L=FBG\), and define \(\eta :Id_\mathcal {D}\Rightarrow L\) and \(\mu :LL \Rightarrow L\) by:

(4)

where \(\eta ^{FG}\) and \(\eta ^{GF}\) are the units of the contravariant adjunction. With this choice of \((L,\eta ,\mu )\) we have the following result.

Proposition 13

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a contravariant adjunction. Let \(\mathsf {B}=(B,\epsilon , \delta )\) be a comonad on \(\mathcal {C}\). Then \((L,\eta , \mu )\) with \(L = FBG\) and \(\eta ,\mu \) defined as in (4) is a monad on \(\mathcal {D}\).

Additionally, if \(\eta ^{GF}\) is a natural isomorphism, then the contravariant adjunction between F and G lifts to a contravariant adjunction between \(\widehat{F}:\mathrm{Coalg}(\mathsf {B})\rightarrow \mathrm{Alg}(\mathsf {L})\) and \(\widehat{G}:\mathrm{Alg}(\mathsf {L})\rightarrow \mathrm{Coalg}(\mathsf {B})\). In this case, if F and G form a duality then the lifting \(\widehat{F}\) and \(\widehat{G}\) is also a duality.

6.2 Defining a Comonad from a Monad

We can dualize the previous proposition in order to define a comonad on \(\mathcal {C}\) if we have a monad on \(\mathcal {D}\). In order to do this we will assume that the contravariant adjunction is a duality so we can use the fact that the units of the contravariant adjunction are isomorphisms.

Assume that we have a contravariant adjunction between two contravariant functors \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\), and \(\mathsf {L}=(L,\eta ,\mu )\) a monad on \(\mathcal {D}\). Define the endofunctor B on \(\mathcal {C}\) as \(B=GLF\). Now, if we assume that the contravariant adjunction is a duality with units \(\eta ^{FG}:Id_\mathcal {D}\Rightarrow FG\) and \(\eta ^{GF}:Id_\mathcal {C}\Rightarrow GF\) that are natural isomorphisms. Then we can define natural transformations \(\epsilon :B\Rightarrow Id_\mathcal {C}\) and \(\delta :B\Rightarrow BB\) as:

(5)

Under the previous assumptions and choice of \((B,\epsilon ,\delta )\) we get:

Proposition 14

Let \(F:\mathcal {C}\rightarrow \mathcal {D}\) and \(G:\mathcal {D}\rightarrow \mathcal {C}\) be contravariant functors that form a duality. Let \(\mathsf {L}=(L,\eta , \mu )\) be a monad on \(\mathcal {D}\). Then \((B,\epsilon ,\delta )\), where \(B = GLF\) and \(\epsilon , \delta \) are defined as in (5), is a comonad on \(\mathcal {C}\). Further, the duality between F and G lifts to a duality between \(\widehat{F}:\mathrm{Coalg}(\mathsf {B})\rightarrow \mathrm{Alg}(\mathsf {L})\) and \(\widehat{G}:\mathrm{Alg}(\mathsf {L})\rightarrow \mathrm{Coalg}(\mathsf {B})\).

7 Applications

In this section we will apply results from the previous section to study equations and coequations for dynamical systems and deterministic automata.

7.1 Equations and Coequations for Dynamical Systems

Let \(M=(M,\cdot ,e)\) be a monoid, let \(\mathsf {L}=(L,\eta ,\mu )\) be the monad on \(\mathrm{Set}\) defined as:

figure r

and let \(\mathsf {B}=(B,\epsilon , \delta )\) be the comonad on \(\mathrm{CABA}\) defined as:

figure s

Consider the duality between \(\mathrm{CABA}\) and \(\mathrm{Set}\) given by the contravariant functors \(F:\mathrm{CABA}\rightarrow \mathrm{Set}\) and \(G:\mathrm{Set}\rightarrow \mathrm{CABA}\) defined as \(FY=\mathrm{At}(Y)\) and \(GX=2^X\), if we consider the natural isomorphism \(\gamma :GL\Rightarrow BG\) given by the canonical isomorphism \(\gamma _X:2^{X\times M}\rightarrow (2^{X})^M\) then we can easily verify the hypothesis of Theorem 11 to lift the duality between F and G from the following setting:

figure t

Observe that elements \((X,\alpha )\in \mathrm{Alg}(\mathsf {L})\) are dynamical systems (monoid actions) on \(\mathrm{Set}\), that is, an L-algebra is a set X together with a map \(\alpha :X \times M \rightarrow X\) that satisfies the properties \(\alpha (x,e)=x\) and \(\alpha (\alpha (x,m),n)=\alpha (x,m\cdot n)\). Further, a B-coalgebra is a set Y with a map \(\beta :Y \rightarrow Y^M\) such that \(\beta (x)(e)=x\) and \(\beta (\beta (x)(m))(n)=\beta (x)(n\cdot m)\).

We are going to consider equations and coequations for dynamical systems for the particular case that the set of generators is \(S=1\). We have that the free algebra \(\mathfrak {F}(1)\) in \(\mathrm{Alg}(\mathsf {L})\) on \(S=1\) generators is \(\mathfrak {F}(1)=(M,\tau )\) where \(\tau :M\times M\rightarrow M\) is given by \(\tau (m,n)=m\cdot n\) and the unit \(\eta :1\rightarrow M\) is given by \(\eta =e\), the identity element in M. On the other hand, the cofree coalgebra \(\mathfrak {C}(G(1))=\mathfrak {C}(2)\) in \(\mathrm{Coalg}(\mathsf {B})\) on 2 colours is \(\mathfrak {C}(2)=(2^M,\hat{\tau })\), where \(\hat{\tau }:2^M\rightarrow (2^M)^M\) is given by

$$ \hat{\tau }(f)(n)=\{m\in M\ |\ f(m\cdot n)=1\} $$

and the counit \(\epsilon :2^M\rightarrow 2\) is given by \(\epsilon (f)=f(e)\).

According to this, equations in \(\mathrm{Eq}(\mathsf {L},1)\) correspond to quotients \(M/C=(M/C,[\tau ])\) where \(C\subseteq M\times M\) is a right congruence on M, i.e. an equivalence relation such that for any \(p\in M\), \((m,n)\in C\) implies \((m\cdot p, n\cdot p)\in M\), and the function \([\tau ]:M/C\times M\rightarrow M/C\) is given by \([\tau ]([m],n)=[m\cdot n]\). On the other hand coequations in \(\mathrm{Coeq}(\mathsf {L},G(S))\) correspond to left-closed-subsystems \(Q=(Q,\hat{\tau })\), i.e. subalgebras Q of the complete atomic Boolean algebra \(2^M\) such that for any \(f\in Q\) and \(m\in M\), \(\hat{\tau }(f)(m)\in Q\).

Now, by using Theorem 12, we have as a consequence a correspondence between right congruences and left-closed-subsystems for dynamical systems.

Proposition 15

There is a duality between \(\mathrm{Eq}(\mathsf {L},1)\) and \(\mathrm{Coeq}(\mathsf {B},2)\) given by \(\widehat{F}\) and \(\widehat{G}\) that induces a duality between right congruences on M and left-closed-subsystems of \(2^M\).

Using this duality one can prove that right congruences on M and left-closed subsystems of \(2^M\) characterize the same classes of dynamical systems.

Proposition 16

For any dynamical system \((X,\alpha )\) on M and any right congruence C on M let \(e_C\in \mathrm{Alg}(\mathsf {L})(M,M/C)\) be the canonical epimorphism (equation) defined as \(e_C(m)=[m]\). The following are equivalent:

  1. (i)

    \((X,\alpha )\,\models \, e_C\).

  2. (ii)

    For every colouring \(c:X\rightarrow 2\) and any \(x\in X\) we have that

    $$ \{m\in M\ |\ c(\beta (x)(m))=1\}\in \mathrm{Im}(\widehat{G}(e_C)). $$

If M is the free monoid on A generators then we get [24, Corollary 14]. In this case, property ii) in the previous proposition is the definition for satisfaction of coequations given in [7] where the set of coequations considered is \(\mathrm{Im}(\widehat{G}(e_C))\).

7.2 Equations and Coequations for Automata

Consider the following setting:

figure u

where \(FY=\mathrm{At}(Y)\), \(GX=2^X\), and \(\mathsf {L}\) is the monad given by:

figure v

According to Proposition 14, as F and G form a duality, we get a comonad \(\mathsf {B}=(B,\epsilon ,\delta )\) on \(\mathrm{CABA}\) and a duality between \(\mathrm{Coalg}(\mathsf {B})\) and \(\mathrm{Alg}(\mathsf {L})\). Observe that \(\mathrm{Alg}(\mathsf {L})\) is isomorphic to the category of monoids.

For any set A, \(LA=A^*\) is the free monoid on A generators, with unit morphism \(\eta _A\) and multiplication \(\mu _A\). Now we will fix the set A and show how the notion of satisfaction of equations given in [7] for a deterministic automaton on A can be equivalently defined in this setting. In fact, given a deterministic automaton \((X,\alpha :X\times A\rightarrow A)\) on A we can use the correspondence:

$$\begin{aligned}&\underline{\alpha :X\times A\rightarrow X}\\&\alpha :A\rightarrow X^X \end{aligned}$$

to work with the monoid \(X^X=(X^X,\beta )\in \mathrm{Alg}(\mathsf {L})\) with composition of functions as multiplication \(\beta \). We have that homomorphic images of \(A^*\), i.e., elements in \(\mathrm{Eq}(\mathsf {L},A)\), correspond to congruences of the monoid \(A^*\). Given any congruence C of \(A^*\) we have that \((X,\alpha )\,\models \, A^*/C\), if the unique extension \(\alpha ^\sharp \in \mathrm{Alg}(\mathsf {L})(A^*, X^X)\) of \(\alpha \) factors through the canonical morphism \(e:A^*\rightarrow A^*/C\). That is, we have that \((X,\alpha )\,\models \, A^*/C\) if there exists \(g_\alpha \in \mathrm{Alg}(\mathsf {L})(A^*/C,X^X)\) such that the following diagram commutes:

figure w

this means that for any \((u,v)\in C\) the transition functions \(f_u,f_v\in X^X\), where \(f_w(x)=w(x)\), \(w\in A^*\), are the same. This is the notion of satisfaction of equations we previously defined in Example 1, and which appears in [7].

We apply G to the previous diagram to get the following diagram:

figure x

This means that \(\mathrm{Im}(2^{\alpha ^\sharp })\subseteq \mathrm{Im}(2^e)=\{L\in 2^{(A^*)}\ |\ \forall \ (u,v)\in C, L(u)=L(v)\}\), which is an object in \(\mathrm{CABA}\) and it is closed under left and right derivatives because C is a congruence.

By Theorem 12, we get a duality between \(\mathrm{Eq}(\mathsf {L},A)\) and \(\mathrm{Coeq}(\mathsf {B}, G(A))\) which is the duality between equations and coequations given in [7, Theorem 22]. Additionally, using the previous commutative diagrams, one can prove the equivalence between (i) and (ii) given in Proposition 16 for the case that \(M=A^*\), the congruences C are congruences of \(A^*\), and the coequations \(\mathrm{Im}(\widehat{G}(e_C))\) are subalgebras of \(2^M\) that are closed under left and right derivatives, cf. [24, Theorem 17].

8 Conclusions

We presented duality results between categories of equations and categories of coequations, Theorem 7. We started our approach by using a more general concept than a duality, namely, contravariant adjunctions. By using this setting we can employ algebraic techniques to study coalgebras as we showed by defining equations for coalgebras and we can also do it the opposite way, define coequations for algebras. Then we showed similar results if we add monads and comonads into our setting, to this end, we proved a lifting theorem to lift contravariant adjunctions to Eilenberg-Moore categories, Theorem 12.

The work here is aimed to understand the interaction between the algebraic and coalgebraic world, including the interpretation of coequations, and the study of comonads. In the future we would like to explore more the coalgebraic aspect, either with the aid of the algebraic side or not, in order to find applications to e.g., tree automata (cf. [17]). Because of limited space we have left out from our examples fundamental dualities such as Stone or Priestley dualities, which will possibly lead to a connection with the recent Eilenberg-type correspondences studied in [3, 4, 10]. We also leave open for future work the question if a converse of Theorem 11 holds.