Abstract
In this paper we show duality results between categories of equations and categories of coequations. These dualities are obtained as restrictions of dualities between categories of algebras and coalgebras, which arise by lifting contravariant adjunctions on the base categories. By extending this approach to (co)algebras for (co)monads, we retrieve the duality between equations and coequations for automata proved by Ballester-Bolinches, Cosme-Llópez and Rutten, and generalize it to dynamical systems.
J. Salamanca—The research of this author is funded by the Dutch NWO project 612.001.210.
J. Rot—Supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
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, 21–23]).
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 L, B 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:
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:
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:
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:
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:
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
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
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
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 F, G 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.
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:
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.
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.
If F, G 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:
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\):
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:
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:
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:
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:
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:
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
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:
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:
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
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:
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.
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.
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:
-
(i)
\((X,\alpha )\,\models \, e_P\) if and only if \(\widehat{G}(X,\alpha )\mid \models \widehat{G}(e_P)\).
-
(ii)
\(\widehat{F}(Y,\beta )\,\models \, \widehat{F}(m_Q)\) if and only if \((Y,\beta )\mid \models m_Q\).
-
(i)
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:
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:
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:
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:
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
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:
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:
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.
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.
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:
-
(i)
\((X,\alpha )\,\models \, e_P\) if and only if \(\widehat{G}(X,\alpha )\mid \models \widehat{G}(e_P)\).
-
(ii)
\(\widehat{F}(Y,\beta )\,\models \, \widehat{F}(m_Q)\) if and only if \((Y,\beta )\mid \models m_Q\).
-
(i)
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:
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:
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:
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:
and let \(\mathsf {B}=(B,\epsilon , \delta )\) be the comonad on \(\mathrm{CABA}\) defined as:
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:
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
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:
-
(i)
\((X,\alpha )\,\models \, e_C\).
-
(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:
where \(FY=\mathrm{At}(Y)\), \(GX=2^X\), and \(\mathsf {L}\) is the monad given by:
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:
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:
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:
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.
Notes
- 1.
\(P\subseteq 2^{A^*}\) is closed under right (left) derivatives if for every \(L\in P\) and \(a\in A\), \(L_a\in P\) (\(_aL\in P\)). Here \(L_a(w)=L(aw)\), and \(_aL(w)=L(wa)\), \(w\in A^*\).
References
Adámek, J.: A logic of coequations. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 70–86. Springer, Heidelberg (2005)
Adámek, J.: Birkhoff’s covariety theorem without limitation. Comment. Math. Univ. Carolinae 46(2), 197–215 (2005)
Adámek, J., Milius, S., Myers, R.S.R., Urbat, H.: Generalized eilenberg theorem I: local varieties of languages. In: FoSSaCS 2014, pp. 366–380 (2014)
Adámek, J., Milius, S., Myers, R.S.R., Urbat, H.: Varieties of languages in a category. In: Proceedings of LICS 2015. IEEE (2015)
Awodey, S., Hughes, J.: Modal operators and the formal dual of Birkhoff’s completeness theorem. Math. Struct. CS 13(2), 233–258 (2003)
Awodey, S.: Category Theory. Oxford University Press, Oxford (2006)
Ballester-Bolinches, A., Cosme-Llópez, E., Rutten, J.J.M.M.: The dual equivalence of equations and coequations for automata. Inf. Comput. 244, 49–75 (2015)
Bonsangue, M.M., Kurz, A.: Duality for logics of transition systems. In: Sassone, V. (ed.) FOSSACS 2005 and ETAPS 2005. LNCS, vol. 3441, pp. 455–469. Springer, Heidelberg (2005)
Clouston, R., Goldblatt, R.: Covarieties of coalgebras: comonads and coequations. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 288–302. Springer, Heidelberg (2005)
Gehrke, M., Grigorieff, S., Pin, J.É.: Duality and equational theory of regular languages. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 246–257. Springer, Heidelberg (2008)
Gumm, H.P.: Birkhoff’s variety theorem for coalgebras. Contrib. Gen. Algebra 13, 159–173 (2000)
Gumm, H.P., Schröder, T.: Covarieties and complete covarieties. ENTCS 11, 42–55 (1998)
Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998)
Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. J. Comput. Syst. Sci. 81(5), 859–879 (2015)
Jacobs, B., Sokolova, A.: Exemplaric expressivity of modal logics. J. Log. Comput. 20(5), 1041–1068 (2010)
Klin, B.: ENTCS 173, 177–201 (2007)
Klin, B., Rot, J.: Coalgebraic trace semantics via forgetful logics. In: Pitts, A. (ed.) FOSSACS 2015 and ETAPS 2015. LNCS, vol. 9034, pp. 151–166. Springer, Heidelberg (2015)
Kurz, A.: Logics for coalgebras and applications to computer science. Doctoral Thesis, Ludwigs-Maximilians-Universität München (2000)
Kurz, A., Rosický, J.: Operations and equations for coalgebras. Math. Struct. Comput. Sci. 15(1), 149–166 (2005)
Pavlovic, D., Mislove, M.W., Worrell, J.B.: Testing semantics: connecting processes and process logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 308–322. Springer, Heidelberg (2006)
Roşu, G.: Equational axiomatizability for coalgebra. Theoret. Comput. Sci. 260(1–2), 229–247 (2001)
Rutten, J.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249(1), 3–80 (2000)
Schwencke, D.: Coequational logic for accessible functors. Inf. Comput. 208(12), 1469–1489 (2010)
Salamanca, J., Ballester-Bolinches, A., Bonsangue, M.M., Cosme-Llópez, E., Rutten, J.J.M.M.: Regular varieties of automata and coequations. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 224–237. Springer, Heidelberg (2015)
Salamanca, J., Bonsangue, M., Rutten, J.: Equations and coequations for weighted automata. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 444–456. Springer, Heidelberg (2015)
Acknowledgements
We would like to thank Alexander Kurz for his valuable comments, and Jan Rutten for his support and suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 IFIP International Federation for Information Processing
About this paper
Cite this paper
Salamanca, J., Bonsangue, M., Rot, J. (2016). Duality of Equations and Coequations via Contravariant Adjunctions. In: Hasuo, I. (eds) Coalgebraic Methods in Computer Science. CMCS 2016. Lecture Notes in Computer Science(), vol 9608. Springer, Cham. https://doi.org/10.1007/978-3-319-40370-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-40370-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40369-4
Online ISBN: 978-3-319-40370-0
eBook Packages: Computer ScienceComputer Science (R0)