Stone Coalgebras

Clemens Kupke

Institute for Logic, Language and Computation, University of Amsterdam, Plantage Muidergracht 24, NL–1018 TV Amsterdam, and Centrum voor Wiskunde en Informatica, P.O. Box 94079, NL–1090 GB

               Amsterdam. E-mail: ckupke@science.uva.nl.

Alexander Kurz^{1}

Department of Computer Science, University of Leicester, University Road, Leicester LE1 7RH, UK.

Yde Venema

Institute for Logic, Language and Computation, University of Amsterdam, Plantage Muidergracht 24, NL–1018 TV Amsterdam. E-mail:

                         yde@science.uva.nl.

Abstract

We argue that the category of Stone spaces forms an interesting base category for coalgebras, in particular, if one considers the Vietoris functor as an analogue to the power set functor on the category of sets.

We prove that the so-called descriptive general frames, which play a fundamental role in the semantics of modal logics, can be seen as Stone coalgebras in a natural way. This yields a duality between modal algebras and coalgebras for the Vietoris functor.

Building on this idea, we introduce the notion of a Vietoris polynomial functor over the category of Stone spaces. For each such functor T we provide an adjunction between T -sorted Boolean algebras with operators and the Stone coalgebras for T. We also identify the subcategory of algebras on which the adjunction restricts to an equivalence and show that the final T -coalgebra is the dual of the initial T -BAO.

Key words: coalgebra, Stone spaces, Vietoris topology, modal logic, descriptive general frames, Kripke polynomial functors

Preprint submitted to Elsevier Science 10 May 2004

1 Introduction

Every coalgebra is based on a carrier which is an object in the so-called base category. Most of the literature on coalgebras either focuses on Set as the base category, or takes a very general perspective, allowing arbitrary base categories (possibly restricted by some constraints). The aim of this paper is to argue that, besides Set, the category Stone of Stone spaces is an interesting base category. We have a number of reasons for believing that Stone coalgebras, that is, coalgebras based on Stone, are of relevance.

To start with, in Section 3 we discuss interesting examples of Stone coalgebras, namely the ones that are associated with the Vietoris functor 𝕍 : Stone → Stone, a topological analogue of the power set functor on Set. 𝕍 is a functorial extension of a well-known topological construction which associates with a topology its Vietoris topology [12]. This construction preserves a number of nice topological properties; in particular, it turns Stone spaces into Stone spaces [18]. As we will see further on, the category Coalg(𝕍) of coalgebras for the Vietoris functor is of interest because it is isomorphic to the category DGF of descriptive general frames. This category in its turn is dual to that of modal algebras, and hence, unlike Kripke frames, descriptive general frames form a mathematically adequate semantics for modal logics [8].

The connection with modal logic thus forms a second reason as to why Stone coalgebras are of interest. Since coalgebras can be seen as a very general model of state-based dynamics, and modal logic as a logic for dynamic systems, the relation between modal logic and coalgebras is rather tight. Starting with the work of Moss [25], this has been an active research area [28,17,6,27,15,9]. The relation between modal logic and coalgebras can be seen to dualise that between equational logic and algebra [20,19], an important difference being that the relation with Set-based coalgebras works smoothly only for modal languages that allow infinitary formulas. In the case of the Vietoris functor however, it follows from the duality between Coalg(𝕍) and the category MA of modal algebras, that Coalg(𝕍) provides an adequate semantics for finitary modal logics. Although probably not widely known, this insight is in fact due to Abramsky [1].

In Sections 4 and 5 we further substantiate our case for Stone spaces as a coalgebraic base category by considering so-called Vietoris polynomial functors as the Stone-based analogues of Kripke polynomial functors over Set [28]. Transferring the work of Jacobs [17] from the setting of Set-coalgebras to Stone-coalgebras, we establish, for each such functor T, a link between the category BAO_{T} of T -sorted Boolean algebras with operators and the category Coalg(T) of Stone coalgebras for T. In Section 4 we lay the foundations of this work, introducing the notions of a Vietoris polynomial functor

1 Partially supported by NWO/British Council.

(VPF), the algebraic and coalgebraic categories, and functors between these categories. Section 5 shows that these functors form an adjunction between the categories BAO_{T} and Coalg(T), for any VPF T. Although this adjunction is not a dual equivalence in general, we will see that each coalgebra can be represented by an algebra, more precisely, Coalg(T)^{op} is (isomorphic to) a full coreflective subcategory of BAO_{T}. We identify the full subcategory of BAO_{T} on which the adjunction restricts to an equivalence and show that the initial T -BAO is dual to the final T -coalgebra.

Let us add two more observations on Stone-coalgebras. First, the duality of descriptive general frames and modal algebras shows that the (trivial) duality between the categories Coalg(T) and Alg(T^{op}) has non-trivial instances. Second, it might be interesting to note that Stone provides a meaningful example of a base category for coalgebras which is not locally finitely presentable.

Related Work The study of coalgebras over topological spaces is closely related to existing work in denotational semantics. One of the main concerns of denotational semantics is to find, for a given type constructor T : X → X, solutions to the equation X ≅ T X. The typical situation is the following. X is a category of topological spaces as, for example, domains (see e.g. [4]) or (ultra)metric spaces (see e.g. [11,32]), T is a functor, and the favoured solution of X ≅ T X is the final T -coalgebra X → T X. The Vietoris functor is known in domain theory as the Plotkin powerdomain and its version on Stone has been considered in Abramsky [1]. The category of Stone spaces with a countable base and their connection to SFP-domains have been investigated by Alessi, Baldan, and Honsell [5]. Compared to Abramsky [2], our work might be seen as a variation based on the use of Stone spaces instead of SFP-domains. Motivated by a different perspective, coalgebras over Stone spaces have been considered recently also by Davey and Galati [10].

Acknowledgements We would like to thank the participants of the ACG-meetings at the Amsterdam Centrum voor Wiskunde en Informatica (CWI); we benefited in particular from discussions with Marcello Bonsangue, Alessandra Palmigiano, and Jan Rutten. We also greatly appreciated the comments by Samson Abramsky. Special thanks are due to one of the anonymous referees who provided us with very interesting comments, some of which have been incorporated in the Remarks 4.5, 4.15 and 5.9.

2 Preliminaries

We presuppose some familiarity with category theory, general topology, the (duality) theory of Boolean algebras, and universal coalgebra. The main purpose of this section is to fix our notation and terminology.

Definition 2.1 Let C be a category and T : C → C an endofunctor. Then a T - coalgebra is a pair (X, ξ : X → T X) where X denotes an object of C and ξ a morphism of C. A T -coalgebra morphism h : (X_{1}, ξ_{1}) → (X_{2}, ξ_{2}) is a C-morphism h : X_{1} → X_{2} satisfying ξ_{2} ∘ h = T h ∘ ξ_{1}. The category Coalg(T) has T -coalgebras as its objects and T -coalgebra morphisms as arrows. Dually, we define a T -algebra to be a T^{op}-coalgebra and Alg(T) = (Coalg(T^{op}))^{op}. ⊲

Example 2.2 A Kripke frame is a structure 𝔽 = (X, R) such that R is a binary relation on X. Kripke frames can be seen as coalgebras for the power set functor P over Set: replace the binary relation R of a frame 𝔽 = (X, R) with the map R[ ] : X → P(X) given by R[s] := {t ∈ X | Rst}. In fact, Kripke frames (and models) form some of the prime examples of coalgebras; in particular, bounded morphisms between Kripke frames coincide with P-coalgebra morphisms.

Definition 2.3 A topological space 𝕏 = (X, τ) is a Stone space if it is compact Hausdorff and has a basis of clopen sets. Clp_{𝕏} will denote the set of clopen subsets of X. The category Stone has Stone spaces as objects and continuous functions as morphisms. ⊲

We now turn to Stone duality.

Definition 2.4 The category of Boolean algebras and homomorphisms between them is denoted as BA. The Stone space (Sp 𝔹, τ_{𝔹}) corresponding to a Boolean algebra 𝔹 is given by the collection Sp 𝔹 of ultrafilters of 𝔹 and the topology τ_{𝔹} generated by basic opens of the form {u ∈ Sp 𝔹 | b ∈ u} for any b in 𝔹. We let 𝕊p denote the functor that associates with a Boolean algebra its corresponding Stone space, and with a Boolean homomorphism h : 𝔹_{1} → 𝔹_{2} the restriction of the inverse image function h^{−1} to Sp 𝔹_{2}. That is, 𝕊p(h): u ↦ {b ∈ 𝔹_{1} | h(b) ∈ u}. Conversely, the functor mapping a Stone space 𝕏 to the Boolean algebra Clp_{𝕏} of its clopens, and a continuous morphism to its inverse image function, is denoted as ℂlp. Furthermore, for any Boolean algebra 𝔹 we define a map i_{𝔹} : 𝔹 → ℂlp 𝕊p 𝔹 given by i_{𝔹}(b) = b̂ := {u ∈ Sp 𝔹 | b ∈ u}, and for any Stone space 𝕏 we define a map ϵ_{𝕏} : 𝕏 → 𝕊p ℂlp𝕏 fixed by ϵ_{𝕏}(x) := {U ∈ Clp_{𝕏} | x ∈ U}. ⊲

Theorem 2.5 The families of morphisms (i_{𝔹})_{𝔹∈BA} and (ϵ_{𝕏})_{𝕏∈Stone} are natural isomorphisms. Hence, the functors 𝕊p : BA → Stone^{op} and ℂlp : Stone^{op} → BA induce a dual equivalence

BA ≃ Stone^{op}.

Definition 2.6 Let 𝕏 = (X, τ) be a topological space. We let K(𝕏) denote the collection of all closed subsets of X. Define the operations [∋], ⟨∋⟩ : P(X) → P(K(𝕏)) by

\begin{aligned}[∋]U & := & \{F ∈ K(𝕏) | F ⊆ U\} , \\ ⟨∋⟩U & := & \{F ∈ K(𝕏) | F ∩ U ≠ ∅\} . \end{aligned}

Given a subset Q ⊆ P(X), define

V_{Q} := {[∋]U | U ∈ Q} ∪ {⟨∋⟩U | U ∈ Q} .

The Vietoris space 𝕍(𝕏) associated with 𝕏 is given by the topology υ_{𝕏} on K(𝕏) which is generated by V_{τ} as subbasis. ⊲

In case the original topology is compact, then we might as well have generated the Vietoris topology in other ways. This has nice consequences for the case that the original topology is a Stone space.

Lemma 2.7 Let 𝕏 = (X, τ) be a compact topological space and let B be a basis of τ that is closed under finite unions. Then the set V_{B} forms a subbasis for υ_{𝕏}. In particular, if 𝕏 is a Stone space, then the set V_{Clp_{𝕏}} forms a subbasis for υ_{𝕏}.

The Vietoris construction preserves various nice topological properties; proofs of this can be found in for instance [24].

Lemma 2.8 Let 𝕏 = (X, τ) be a topological space.

(1) If 𝕏 is compact then (K(𝕏), υ_{𝕏}) is compact.

(2) If 𝕏 is compact and Hausdorff, then (K(𝕏), υ_{𝕏}) is compact and Hausdorff.

(3) If 𝕏 is a Stone space, then so is (K(𝕏), υ_{𝕏}).

3 General frames as coalgebras

In this section we discuss what are probably the prime examples of Stone coalgebras, namely those for the Vietoris functor 𝕍. As we will see, the importance of these structures lies in the fact that the category Coalg(𝕍) is isomorphic to the category of so-called descriptive general frames, and hence, dual to the category of modal algebras (all these notions will be defined below). We hasten to remark that when it comes down to the technicalities, this section contains little news; most of the results in this section can be obtained by exposing existing material from Esakia [13], Goldblatt [16], Johnstone [18], and Sambin and Vaccaro [31] in a new coalgebraic light. Moreover, it will turn out that the duality of descriptive general frames and modal algebras is an instance of the general relationship between syntax and semantics as laid out by Abramsky in his domain theory in logical form [3]. He was also the first to observe the duality of Coalg(𝕍) and modal algebras in [1].

Modal algebras and (descriptive) general frames play a crucial role in the theory of modal logic, providing an important class of structures interpreting modal languages. From a mathematical perspective they display much better behaviour than Kripke frames, since the latter provide too poor a tool to make the required distinctions between modal logics (in the technical sense, see for instance [8], Chapter 4). The algebraic semantics for modal logic does not suffer from this fundamental incompleteness result: every modal logic is determined by the class of modal algebras on which it is valid.

Definition 3.1 Let 𝔹 and 𝔹′ be Boolean algebras; an operation g : B → B′ on their carriers is said to preserve finite meets if g(⊤) = ⊤′ and g(b_{1} ∧ b_{2}) = g(b_{1}) ∧′ g(b_{2}). A modal algebra is a structure 𝔸 = (A, ∧, −, ⊥, ⊤, g) such that the reduct (A, ∧, −, ⊥, ⊤) of 𝔸 is a Boolean algebra, and g : A → A preserves finite meets. The category of modal algebras (with homomorphisms) is denoted by MA. ⊲

The intended meaning of g is to provide an interpretation of the modal operator □. Thinking of a ∈ A as the interpretation of a modal formula φ, g(a) provides the interpretation of □φ.

Example 3.2 (1) If (X, R) is a Kripke frame then (PX, ∩, −, ∅, X, [R]) is a modal

algebra where [R](a) = {x ∈ X | ∀y. Rxy ⇒ y ∈ a},

(2) Let Prop be a set of propositional variables and L(Prop) be the set of modal formulas over Prop quotiented by φ ≡ ψ ⇔ ⊢_{K} φ ↔ ψ where ⊢_{K} denotes derivability in the basic modal logic K (see eg [8]). Then L(Prop)—equipped with the obvious operations—is a modal algebra. In fact, L(Prop) is the free modal algebra over Prop and is called the Lindenbaum-Tarski algebra (over Prop).

Remark 3.3 Although not needed in the following, we indicate how modal formulas are evaluated in modal algebras. Let φ be a modal formula taking propositional variables from Prop and let 𝔸 = (A, ∧, −, ⊥, ⊤, g) be a modal algebra. Employing the freeness of the modal algebra L(Prop) we can identify valuations of variables v : Prop → A with algebra morphisms L(Prop) → 𝔸 and define 𝔸 ⊧ φ if v([φ]_{≡}) = ⊤ for all morphisms v : L(Prop) → 𝔸.

Modal algebras are fairly abstract in nature and many modal logicians prefer the intuitive, geometric appeal of Kripke frames. General frames, unifying the algebraic and the Kripke semantics in one structure, provide a nice compromise.

Definition 3.4 A general frame is a structure 𝔾 = (G, R, A) such that (G, R) is a Kripke frame and A is a collection of so-called admissible subsets of G that is closed under the Boolean operations and under the operation ⟨R⟩ : P(G) → P(G) given by: ⟨R⟩X := {y ∈ G | Ryx for some x ∈ X}. A general frame 𝔾 = (G, R, A) is called differentiated if for all distinct s_{1}, s_{2} ∈ G there is a ‘witness’ a ∈ A such that s_{1} ∈ a while s_{2} ∉ a; tight if whenever t is not an R-successor of s, then there is a ‘witness’ a ∈ A such that t ∈ a while s ∉ ⟨R⟩a; and compact if ⋂ A_{0} ≠ ∅ for every subset A_{0} of A which has the finite intersection property. A general frame is descriptive if it is differentiated, tight and compact. ⊲

The term ‘admissible’ subset is explained by the semantic restriction that allows only those Kripke models on a general frame for which the extensions of the atomic formulae are admissible sets.

Example 3.5 (1) Any Kripke frame (X, R) can be considered as a general frame

(X, R, PX).

(2) If 𝔸 = (A, ∧, −, ⊥, ⊤, g) is a modal algebra then (Sp 𝔸, R, Â) where R = {(u, v) | a ∈ u ⇒ g(a) ∈ v} and Â = {{u ∈ Sp 𝔸 | a ∈ u} | a ∈ A} is a descriptive general frame, where the admissible sets are the clopen basis of Sp 𝔸.

(3) If 𝔾 = (G, R, A) is a general frame then (A, ∩, −, ∅, G, [R]) is a modal algebra (where [R]X = {y ∈ G | Ryx ⇒ x ∈ X}).

The last two examples form the basis of the dual equivalence

MA ≃ DGF^{op}

between the categories of modal algebras and descriptive general frames where the latter category is defined as follows.

Definition 3.6 (GF, DGF) A morphism θ : (G, R, A) → (G′, R′, A′) is a function from G to G′ such that (i) θ : (G, R) → (G′, R′) is a bounded morphism (see Example 2.2) and (ii) θ^{−1}(a′) ∈ A for all a′ ∈ A′. We let GF (DGF) denote the category with general frames (descriptive general frames, respectively) as its objects, and the general frame morphisms as the arrows. ⊲

Since Kripke frames (and models) form prime examples of coalgebras, the question naturally arises whether (descriptive) general frames can be seen as coalgebras as well. Our positive answer to this question is based on two crucial observations. First, the admissible sets of a descriptive frame form a basis for a Stone topology because descriptive general frames are compact, differentiated and the admissible sets are closed under Boolean operations. Second, the tightness condition of descriptive general frames can be reformulated as the requirement that the relation is point-closed; that is, the successor set of any point is closed in the Stone topology. This suggests that if we are looking for a coalgebraic counterpart of a descriptive general frame 𝔾 = (G, R, A), it should be of the form R[ ] : (G, τ) → (K(G), τ?) where K(G) is the collection of closed sets in the Stone topology τ on G and τ? is some suitable topology on K(G), which turns K(G) again into a Stone space. A good candidate is the Vietoris topology: it is based on the closed sets of τ and it yields a Stone space if we started from one. Moreover, as we will see, choosing the Vietoris topology for τ?, continuity of the map R[ ] corresponds to the admissible sets being closed under ⟨R⟩.

We will prove that the category of descriptive general frames and the category Coalg(𝕍) of coalgebras for the Vietoris functor are in fact isomorphic. We first note that [12, Theorem 3.1.8] whenever f : 𝕏 → 𝕏′ is a continuous map between compact Hausdorff spaces, then the image map f[ ] sends closed sets to closed sets. This motivates defining 𝕍(f) : K(𝕏) → K(𝕏′) by

𝕍(f)(F) := f[F] (= {f(x) | x ∈ F }).  (1)

Definition 3.7 The Vietoris functor on the category of Stone spaces is given on objects as in Definition 2.6 and on morphisms as in (1). ⊲

We now turn to the isomorphism between the categories DGF and Coalg(𝕍). It is straightforward to verify that the following definition is correct, that is, it indeed defines two functors.

Definition 3.8 We define the functor ℂ : DGF → Coalg(𝕍) via

(G, R, A) ↦ (G, σ_{A}) ⟶^{R[ ]} 𝕍(G, σ_{A})

Here σ_{A} denotes the Stone topology generated by taking A as a basis. Conversely, there is a functor 𝔻 : Coalg(𝕍) → DGF given by

(𝕏, γ) ↦ (X, R_{γ}, Clp_{𝕏})

where R_{γ} is defined by R_{γ}s_{1}s_{2} iff s_{2} ∈ γ(s_{1}). On morphisms both functors act as the identity with respect to the underlying Set-functions. ⊲

Theorem 3.9 The functors ℂ and 𝔻 form an isomorphism between the categories DGF and Coalg(𝕍).

Proof. The theorem can be easily proven by just spelling out the definitions. qed Remark 3.10 (Propositional Variables) For a set-coalgebra (X, ξ), a valuation of propositional variables p ∈ Prop is a function X → ∏_{Prop} 2 where 2 is the twoelement set of truth-values. For a Stone-coalgebra (𝕏, ξ), a valuation is a continuous map v : 𝕏 → ∏_{Prop} 2 where 2 is taken with the discrete topology. The continuity of v is equivalent to the statement that the propositional variables take their values in admissible sets. Indeed, writing π_{p} : ∏_{Prop} 2 → 2 (p ∈ Prop) for the projections, continuity of v is equivalent to v^{−1}(π_{p}^{−1}({1})) clopen for all p ∈ Prop. Observing that v^{−1}(π_{p}^{−1}({1})) = {x ∈ X | v(x)_{p} = 1} is the extension of p, the claim now follows from the fact that the clopens coincide with the admissible sets.

Let us note two corollaries of Theorem 3.9. Using MA ≃ DGF^{op} and (Coalg(𝕍))^{op} = Alg(𝕍^{op}), it follows that MA ≃ Alg(𝕍^{op}). With Stone^{op} ≃ BA we obtain the following.

Corollary 3.11 There is a functor H : BA → BA such that the category of modal algebras MA is equivalent to the category Alg(H) of algebras for the functor H.

Proof. Using ℂlp : Stone → BA and 𝕊p : BA → Stone, we let H = ℂlp𝕍 𝕊p. The claim now follows from the observation that Alg(H) is dual to Coalg(𝕍): An algebra HA ⟶^{α} A corresponds to the coalgebra 𝕊p A ⟶^{𝕊pα} 𝕊p HA ≅ 𝕍 𝕊p A and a coalgebra 𝕏 ⟶^{ξ} 𝕍𝕏 corresponds to the algebra Hℂlp𝕏 ≅ ℂlp𝕍𝕏 ⟶^{ℂlpξ} ℂlp𝕏 . qed

An explicit description of H not involving the Vietoris functor is given by the following proposition.

Proposition 3.12 Let H : BA → BA be the functor that assigns to a Boolean algebra the free Boolean algebra over its underlying meet-semilattice. Then Alg(H) is isomorphic to the category of modal algebras MA.

Proof. We use the well-known fact that MA is isomorphic to the category MPF which is defined as follows. An object of MPF is an endofunction A →^{m} A on a Boolean algebra A that preserves finite meets (i.e. binary meets and the top-element). A morphism f : (A →^{m} A) ⟶ (A′ →^{m′} A′) is a Boolean algebra morphism f : A → A′ such that m′ ∘ f = f ∘ m. We also write BA_{∧} for the category with Boolean algebras as objects and finite meet preserving functions as morphisms. To prove that Alg(H) and MPF are isomorphic categories, we first show that BA(HA, A) ≅ BA_{∧}(A, A), or slightly more general and precise, BA(HA, B) ≅ BA_{∧}(IA, IB) where I : BA ↪ BA_{∧}. (Here we denote, for a category C and objects A, B in C, the set of morphisms between A and B by C(A, B).) Indeed, consider the forgetful functors U : BA → SL, V : BA_{∧} → SL to the category SL of meet-semilattices with top element, and the left adjoint F of U. Using our assumption H = F U, we calculate BA(HA, B) = BA(F UA, B) ≅ SL(UA, UB) ≅ SL(V IA, V IB) ≅ BA_{∧}(IA, IB). The isomorphisms φ_{A} : BA(HA, A) → BA_{∧}(A, A), A ∈ BA, give us an isomorphism φ between the objects of Alg(H) and MPF. On morphisms, we define φ to be the identity. This is well-defined because the isomorphisms BA(HA, B) ≅ BA_{∧}(IA, IB) are natural in A and B. qed

Remark 3.13 Detailing the construction of a free Boolean algebra over its underlying meet-semilattice, we see that, given a Boolean algebra 𝔸 = (A, ∧, −, ⊥, ⊤), H𝔸 is the free Boolean algebra generated by {□a | a ∈ A} (the insertion of generators being □ : 𝔸 → H𝔸, a ↦ □a) and satisfying the equations □⊤ = ⊤, □(a ∧ b) = □a ∧ □b. That is, the functor H describes how to obtain modal logic by adding an operator to Boolean logic. As observed above this functor is the Stone dual of the Vietoris functor. This observation was made earlier by Abramsky in [1] and is an instance of the general relationship between syntax and semantics as laid out in his domain theory in logical form [3].

As another corollary to the duality we obtain that Coalg(𝕍) has cofree coalgebras.

Corollary 3.14 The forgetful functor Coalg(𝕍) → Stone has a right adjoint.

Proof. Consider the forgetful functors R : MA → BA, U : MA → Set, V : BA → Set. Since U and V are monadic, R has a left adjoint. Hence, by duality, Coalg(𝕍) → Stone has a right adjoint. qed

Finally, let us see how arbitrary general general frames can be seen as coalgebras.

Remark 3.15 (General Frames as Coalgebras) Stone spaces provide a convenient framework to study descriptive general frames since the admissible sets can be recovered from the topology: each Stone space 𝕏 = (X, τ) has a unique basis that is closed under the Boolean operations. Making a generalisation to arbitrary general frames, we can still work in a coalgebraic framework, but we have to make two adjustments. First, we work directly with admissible sets instead of with topologies: the category RBA (represented Boolean algebras) has objects (X, A) where X is a set and A a set of subsets of X closed under Boolean operations. It has morphisms f : (X, A) → (Y, B) where f is a function X → Y such that f^{−1}(b) ∈ A for all b ∈ B. And second, in the absence of tightness, the relation of the general frame will no longer be point-closed. Hence, its coalgebraic version has the full power set as its codomain. For 𝕏 = (X, A) ∈ RBA let 𝕎(𝕏) = (P(X), v_{𝕏}) where v_{𝕏} is the Boolean algebra generated by {{F ∈ PX | F ∩ a ≠ ∅} | a ∈ A}. On morphisms let 𝕎(f) = P(f). This clearly defines an endofunctor on the category RBA, and the induced category Coalg(𝕎) is the coalgebraic version of general frames:

There is an isomorphism between GF and Coalg(𝕎)  (2)

The crucial observation in the proof of (2) is that, for 𝕏 = (X, A) ∈ RBA and R a relation on X, we have that A is closed under ⟨R⟩ iff R[ ] : X → PX is a RBA-morphism 𝕏 → 𝕎(𝕏). This follows from the fact that ⟨R⟩a = (R[ ])^{−1}({F ∈ PX | F ∩ a ≠ ∅}).

4 Vietoris Polynomial Functors: from coalgebras to algebras and back

In this section we introduce the notion of a Vietoris polynomial functor (VPF) as a natural analogue for the category Stone of Stone spaces of the so-called Kripke polynomial functors [28,17] on Set. This section can be therefore seen as a first application of the observation that coalgebras over Stone can be used as semantics for (coalgebraic) modal logics. Much of the work in this section consists of transferring the work by Jacobs in [17] to the topological setting. After introducing the Vietoris polynomial functors, we define, for each VPF, the category BAO_{T} of T -sorted Boolean algebras with operators and their morphisms. We then link the categories BAO_{T} and Coalg(T) by functors A : Coalg(T)^{op} → BAO_{T} and C : BAO_{T} → Coalg(T)^{op}.

Definition 4.1 The collection of Vietoris polynomial functors, in brief: VPFs, over Stone is inductively defined as follows:

T ::= 𝕀 | 𝕂 | T_{1} + T_{2} | T_{1} × T_{2} | T^{D} | 𝕍T.

Here 𝕀 is the identity functor on the category Stone; 𝕂 denotes a finite Stone space (that is, the functor 𝕂 is a constant functor); ‘+’ and ‘×’ denote disjoint union and binary product, respectively; and, for an arbitrary set D, T^{D} denotes the functor sending a Stone space 𝕏 to the D-fold product of T (𝕏). Associated with this we inductively define the notion of a path:

p ::= ⟨⟩ | π_{1} · p | π_{2} · p | κ_{1} · p | κ_{2} · p | ev(d) · p | 𝕍 · p.

By induction on the complexity of paths we now define when two VPFs T_{1} and T_{2} are related by a path p, notation: T_{1} ⇝^{p} T_{2}:

T ⇝^{⟨⟩} T
T_{1} × T_{2} ⇝^{π_{i}·p} T′ if T_{i} ⇝^{p} T′
T_{1} + T_{2} ⇝^{κ_{i}·p} T′ if T_{i} ⇝^{p} T′
T^{D} ⇝^{ev(d)·p} T′ if T ⇝^{p} T′ and d ∈ D
𝕍T ⇝^{𝕍·p} T′ if T ⇝^{p} T′.

Finally, for a VPF T we define the category Ing(T) of ingredients of T to be the category with the set Ing(T) := {S | ∃p.T ⇝^{p} S} ∪ {𝕀} as the set of objects and the paths as morphisms between them. ⊲

Remark 4.2 All of our results could have been generalised to a setting that allows infinite constants and infinite topologised sums as in Gehrke [14]. We confine ourselves to the functors of Definition 4.1 in order to stay as close as possible to existing work on Kripke polynomial functors.

We will now define the Boolean algebras with operators associated with a VPF. The definition of a so-called T -BAO may look slightly involved, but it is based on a simple generalisation of the concept of a modal algebra. The generalisation is that instead of dealing with a single Boolean algebra, we will be working with a family (Φ(S))_{S∈Ing(T)} of Boolean algebras. As before, we let BA_{∧} denote the category with Boolean algebras as objects and finite-meet preserving functions as morphisms.

Definition 4.3 (T -BAO) Let T be a VPF. A T -sorted Boolean algebra with operators, T -BAO, consists of a functor Φ : Ing(T)^{op} ⟶ BA_{∧}, together with an additional map next : Φ(T) → Φ(𝕀) which preserves all Boolean operations. This functor is required to meet the conditions (1) Φ(𝕂) = ℂlp𝕂, (2) the functions Φ(π_{i}) and Φ(ev(d)) are Boolean homomorphisms, and (3) the functions Φ(κ_{i}) induced by the injection paths satisfy (3a) Φ(κ_{1})(⊥) = −Φ(κ_{2})(⊥) and (3b) −Φ(κ_{i})(⊥) ≤ (Φ(κ_{i})(−α) ↔ −Φ(κ_{i})(α)).

Example 4.4 Let 𝔸 = (A, ∧, −, ⊥, ⊤, g) be a modal algebra, cf. Definition 3.1. This algebra can be represented by two different 𝕍𝕀-BAOs. Note that Ing(𝕍𝕀) = {𝕀, 𝕍𝕀} and

𝕍𝕀 ⇝^{𝕍} 𝕀.

(1) Φ(𝕀) := 𝔸 , Φ(𝕍𝕀) := 𝔸, Φ(𝕍) := g, and next = id.

(2) Φ′(𝕀) := 𝔸, Φ′(𝕍𝕀) := H𝔸 (cf. Proposition 3.12), Φ′(𝕍) : Φ′(𝕀) ↪ Φ′(𝕍𝕀) the (meet-preserving) inclusion of generators, and next′ the unique Boolean algebra morphism satisfying next′ ∘ Φ′(𝕍) = g.

We will see that (Φ′, next′) is the 𝕍𝕀-BAO obtained by considering the algebra (Φ, next) from (1) as a 𝕍𝕀-coalgebra and translating it back to an algebra, that is, in the notation we are about to introduce, (Φ′, next′) = AC(Φ, next).

Remark 4.5 (T -BAOs as Many-Sorted Algebras) The definition of a T -BAO as a functor Φ : Ing(T)^{op} → BA_{∧} reminds one of Lawvere’s functorial semantics and, indeed, as suggested by a referee, T -BAOs can be represented as many-sorted algebras (this point of view will be applied in Remarks 4.10, 4.15, 5.9, 5.12). The following description can be read as an unfolding of Definitions 4.3 and 4.1. The sorts are the ingredients S of T. There are unary operation symbols [π_{i}], [κ_{i}], [ev(d)], [𝕍], next of type S_{i} → S_{1} × S_{2}, S_{i} → S_{1} + S_{2}, S → S^{D}, S → 𝕍S, T → 𝕀, respectively, constants q ∈ 𝕂, and Boolean operation symbols for each sort. The equations are: for the q ∈ 𝕂 all equations that hold in 𝕂; for the Boolean operations of each sort the equations of Boolean algebra; equations forcing all unary operation symbols (apart from Boolean complementation) to preserve finite meets; equations expressing that [π_{i}], [ev(d)], next preserve all Boolean structure; and finally, [κ_{1}]⊥ = −[κ_{2}]⊥ and −[κ_{i}]⊥ ≤ ([κ_{i}]−v ↔ −[κ_{i}]v), v a variable.

Remark 4.6 (Many-Sorted Coalgebraic Modal Logic) From the perspective of modal logic, what we are dealing with here is a sorted modal language, the formulas of which coincide with the set of terms described in the previous remark. Whereas the T -BAOs can be seen to give the algebraic semantics for this language, we can also provide it with a more standard semantics (from the point of view of modal logic) in which the intended general frames are derived from T -coalgebras. The idea is very simple: a T -coalgebra (𝕏, c) is represented as a sorted frame 𝔽_{T} (𝕏, c). This frame has a domain 𝔽_{S} = S(𝕏) for each ingredient S of T, a point-closed relation (see page 8) R_{p} from S_{1}(𝕏) to S_{2}(𝕏) for each path S_{1} ⇝^{p} S_{2}, and, finally, a point-closed relation R_{next} from 𝕏 to T (𝕏). These relations are determined by the path and the coalgebra: for instance, for 𝕍(S) ⇝^{𝕍} S, the relation R_{𝕍} is simply the converse membership relation, the relation R_{π_{i}} is the graph of the i-th projection map, etc. Finally, the relation R_{next} is the graph of the coalgebra map c. It is then a natural question how to axiomatise the logic corresponding to this semantics, i.e. to generate the collection of formulas that are valid in the class of these coalgebraic frames. The system MSML_{τ} of Jacobs [17, Definition 3.2] aims at precisely this—for the set based coalgebras that is, but this makes no difference here. The link between Jacobs’s logic and the equational theory described in Remark 4.5 is very tight: the second is the algebraisation of the first one. This means, for instance, that as modal axioms for Jacobs’s logic we can take the formulas φ ↔ ψ such that φ = ψ is one of the equations given in the previous remark. This modal perspective provides another way of understanding these equations. Basically they try to grasp as many properties of the just described accessibility relations as is ‘modally possible’. For instance, requiring a modality to preserve all Boolean structure forces the accessibility relation to be functional. The axioms for the coproduct modalities [κ_{i}] are modal/equational ways of saying that each point in the coproduct has an R_{κ_{i}}-successor for exactly one i, and that this successor is unique.

The following is the natural generalisation of the notion of a homomorphism between modal algebras.

Definition 4.7 (BAO_{T}) A morphism between T -BAOs (Φ′, next′) → (Φ, next) is a natural transformation t : Φ′ → Φ such that for each ingredient S of T the component t_{S} : Φ′(S) → Φ(S) preserves the Boolean structure, t_{𝕂} = id_{Clp_{𝕂}} for all constants 𝕂 ∈ Ing(T), and t_{𝕀} and t_{T} satisfy next ∘ t_{T} = t_{𝕀} ∘ next′. This yields the category BAO_{T}. ⊲ It is not difficult to transform a T -coalgebra into a T -BAO; basically, we are dealing with a sorted version of Stone duality, together with a path-indexed predicate lifting. We omit the fairly straightforward proofs.

Definition 4.8 Let T be a VPF and let 𝕏 = (X, τ) be a Stone space. Then the following definition on the complexity of paths

α^{⟨⟩} := α
α^{π_{1}·p} := π_{1}^{−1} (α^{p})
α^{π_{2}·p} := π_{2}^{−1} (α^{p})
α^{κ_{1}·p} := κ_{1} (α^{p}) ∪ κ_{2}S_{2}(X)  for T_{2} = S_{1} + S_{2}
α^{κ_{2}·p} := κ_{1}S_{1}(X) ∪ κ_{2} (α^{p})  for T_{2} = S_{1} + S_{2}
α^{ev(d)·p} := π_{d}^{−1} (α^{p})
α^{𝕍·p} := {β | β ⊆ α^{p} and β closed } (= [∋]α)

provides, for any path T_{1} ⇝^{p} T_{2}, a so-called predicate lifting

( )^{p} : Clp_{T_{2}𝕏} → Clp_{T_{1}𝕏}.

Lemma and Definition 4.9 (A) For each Vietoris polynomial functor T, each T - coalgebra (𝕏, c) gives rise to a T -BAO, namely, the ‘complex algebra’ functor A(𝕏, c) : Ing(T)^{op} → BA_{∧} given by

\begin{matrix}S & ↦ & ℂlpS(𝕏) \\ (S_{1} ⇝^{p} S_{2}) & ↦ & (( )^{p} : ℂlpS_{2}(𝕏) → ℂlpS_{1}(𝕏)) , \end{matrix}

accompanied by the map next : ℂlp(T 𝕏) → ℂlp(𝕏) given by next := c^{−1}.

Remark 4.10 (Semantics of Many-Sorted Coalgebraic Modal Logic) Note that each path gives rise to a term for the many-sorted signature of Remark 4.5. Indeed, let ( )^{∗} be the mapping from paths to terms defined by ⟨⟩^{∗} = v for a variable v of appropriate type, (l · p)^{∗} = [l](p^{∗}) for l ∈ {π_{1}, π_{2}, κ_{1}, κ_{2}, ev(d), 𝕍}. In the light of Remark 4.6, the predicate lifting ( )^{p} corresponds to the operation [R_{p}] defined from the relation R_{p} as in Example 3.5(3). Dually, given a T -coalgebra (𝕏, c) and a path T_{1} ⇝^{p} T_{2} between two ingredients of T, ( )^{p} is nothing else but the interpretation of the term p^{∗} in the dual algebra A(𝕏, c). Since the semantics of modal operators is given by predicate liftings (cf. [17, Definition 3.4]), it is now clear that the semantics of formulae φ of sort 𝕀 in the coalgebraic frame semantics of Remark 4.6 amounts to

(𝕏, c), x ⊧ φ ⇔ x ∈ φ^{A(𝕏,c)}

where x is an element of 𝕏 and φ^{A(𝕏,c)} is the interpretation of the term φ in the algebra A(𝕏, c). It follows (𝕏, c) ⊧ φ ⇔ A(𝕏, c) ⊧ φ = ⊤. This is in line with the duality theory of modal logics, see e.g. [8, Section 5.2]. The name ‘complex algebra’ stems from this tradition.

Conversely, with each T -BAO Φ we want to associate a T -coalgebra C(Φ). Assume that T has the identity functor as an ingredient; given our results in the previous section, it seems fairly obvious that we should take the dual Stone space 𝕊p Φ(𝕀) as the carrier of this dual coalgebra. It remains to define a T -coalgebra structure on this. Applying duality theory to the Boolean algebras obtained from Φ only seems to provide information on the spaces 𝕊p Φ(S), whereas we need to work with S(𝕊p Φ(𝕀)) in order to define a T -coalgebra. Fortunately, in the next lemma and definition we show that there exists a map r which produces the S-structure (see Remark 4.15 for an alternative way). The definition of r is as in [17]; what we have to show is that it works also in the topological setting.

Lemma and Definition 4.11 (r_{Φ}) Let T be a VPF and let (Φ, next) be a T -BAO. Then the following definition by induction on the structure of ingredient functors of T

r_{Φ}(𝕀)(U) := U
r_{Φ}(𝕂)(U) := (ϵ_{𝕂})^{−1} (cf. Def. 2.4)
r_{Φ}(S_{1} × S_{2})(U) := ⟨r_{Φ}(S_{1})(Φ(π_{1})^{−1}(U)), r_{Φ}(S_{2})(Φ(π_{2})^{−1}(U))⟩
r_{Φ}(S_{1} + S_{2})(U) := \{ \begin{matrix}κ_{1}r_{Φ}(S_{1})(Φ(κ_{1})^{−1}(U)) if & −Φ(κ_{1})(⊥) ∈ U \\ κ_{2}r_{Φ}(S_{2})(Φ(κ_{2})^{−1}(U)) if & −Φ(κ_{2})(⊥) ∈ U \end{matrix}
r_{Φ}(S^{D})(U) := λd ∈ D. r_{Φ}(S)(Φ(ev(d))^{−1}(U))
r_{Φ}(𝕍S)(U) := {r_{Φ}(S)(V) | V ∈ Sp Φ(S) and Φ(𝕍)^{−1}(U) ⊆ V }

defines, for every S ∈ Ing(T) a continuous map

r_{Φ}(S) : 𝕊p(Φ(S)) ⟶ S(𝕊p(Φ(𝕀))).

Furthermore, the inverse image map next^{−1} is a continuous map

next^{−1} : 𝕊p(Φ(𝕀)) ⟶ T (𝕊p(Φ(𝕀))).

Remark 4.12 Perhaps this definition makes somewhat more sense when seen from the modal perspective of Remark 4.6. Suppose that we allow ‘non-standard’ T -coalgebras in the semantics of our modal language. These would be many-sorted frames 𝔽 as well, with a Stone space 𝔽_{S} for each ingredient functor S, point-closed relations R_{p} from 𝔽_{S_{1}} to 𝔽_{S_{2}} for each path S_{1} ⇝^{p} S_{2}, and a point-closed relation R_{next} from 𝔽_{𝕀} to 𝔽_{T}. Let us agree to call such structures pseudo-coalgebras if they validate the (modal versions of the) axioms of Definition 4.4. Note that we may extract such a pseudo-coalgebra from every T -BAOs, simply by taking Stone duals ingredientwise, and defining point-closed relations between the sorts as in Example 3.5(3). It then follows from the standard modal theory of canonicity and correspondence, that pseudo-coalgebras are rather similar to real coalgebraic frames; for instance, while 𝔽_{S_{1}×S_{2}} need not be the product in Stone of 𝔽_{S_{1}} and 𝔽_{S_{1}}, it will certainly be the case that each R_{π_{i}} is a functional relation between 𝔽_{S_{1}×S_{2}} and 𝔽_{S_{i}}. It is this pseudo-coalgebraic structure that allows the definition of the maps r(S) : 𝔽_{S} → S(𝕏). For instance, suppose that r has been defined for S_{1} and S_{2}; then we define it for S_{1} × S_{2} by putting r(S_{1} × S_{2})(U) := (r(S_{1})(U_{1}), r(S_{2})(U_{2})) where each U_{i} is the unique element of 𝔽_{S_{i}} such that R_{π_{i}}UU_{i}. The family r of maps can thus be seen as the natural attempt to link the pseudo-coalgebra to a proper coalgebra over 𝔽_{𝕀}.

Proof. Let S ∈ Ing(T). Both claims (i.e. the one on well-definedness and the one on the continuity of r_{Φ}(S)) are proven simultaneously by induction on S. We only consider the case of the Vietoris functor: assume that S = 𝕍S′. In order to show that r_{Φ}(S) is well-defined, take an arbitrary U ∈ Sp Φ(𝕍S′) and consider the set F := {V | V ∈ Sp Φ(S′) and Φ(𝕍)^{−1}(U) ⊆ V }. F is closed in S′(Sp Φ(𝕀)), because for any V′ ∈ S′(Sp Φ(𝕀))\F there is an a ∈ Φ(𝕍)^{−1}(U) such that a ∉ V′, whence F ⊆ â and V′ ∉ â: for every V′ ∉ F we can find an open set containing V′ and disjoint from F. But from F being closed and the inductive hypothesis on r_{Φ}(S′) it follows that r_{Φ}(S′)[F] is closed as well, so by definition, r_{Φ}(S)(U) = r_{Φ}(S′)[F] belongs to K(S′(Sp Φ(𝕀))). This proves that r_{Φ}(S) is well-defined. We now turn to the continuity of r_{Φ}(S). It suffices to show that for an arbitrary clopen set O ⊆ S′(Sp Φ(𝕀)), all sets of the form r_{Φ}(𝕍S′)^{−1}([∋](O)) and r_{Φ}(𝕍S′)^{−1}(⟨∋⟩(O)) are clopen. We only consider sets of the first kind:

r_{Φ}(𝕍S′)^{−1}([∋](O)) = {U ∈ Sp Φ(𝕍S′) | r_{Φ}(𝕍S′)(U) ∈ [∋](O)}
= {U | {r_{Φ}(S′)(V) | Φ(𝕍)^{−1}(U) ⊆ V } ⊆ O}
= {U | {V | Φ(𝕍)^{−1}(U) ⊆ V } ⊆ r_{Φ}(S′)^{−1}(O)}

According to the induction hypothesis, r_{Φ}(S′)^{−1}(O) is a clopen set, say with b ∈ Φ(S′) such that r_{Φ}(S′)^{−1}(O) = b̂. This leads us to

r_{Φ}(𝕍S′)^{−1}([∋](O)) = {U | {V | Φ(𝕍)^{−1}(U) ⊆ V } ⊆ b̂}
= {U | ∀V ∈ Sp Φ(S′). (Φ(𝕍)^{−1}(U) ⊆ V → b ∈ V)}
=^{(!)} {U | Φ(𝕍)(b) ∈ U}

which shows that r_{Φ}(𝕍S′)^{−1}([∋](O)) is clopen. The proof of (!) is standard in the representation theory of modal algebras.

Finally, the claim on the map next^{−1} is a simple consequence of Stone duality. qed

The above lemma allows us to define a T -coalgebra for a given T -BAO.

Definition 4.13 (C) Let T be a VPF and let (Φ, next) be a T -BAO. We define the coalgebra C(Φ, next) as the structure (𝕊p(Φ(𝕀)), r_{Φ}(T) ∘ 𝕊p(next)). ⊲

The maps A and C that allow us to move from a given T -BAO to a T -coalgebra and vice versa, can be extended to functors. Fix a Vietoris polynomial functor T, and let f : (𝕏, c) → (𝕏′, c′) be a Coalg(T)-morphism. Then we define A(f) : A(𝕏′, c′) → A(𝕏, c) as follows. For each S ∈ Ing(T) let A(f)(S) := ℂlp(S(f)). Naturality of A(f) can be proven by induction on paths and the additional condition in Definition 4.7 concerning the next functions is fulfilled because f is a T -coalgebra homomorphism.

Conversely, given a BAO_{T} -morphism t : (Φ, next) → (Φ′, next′), define the map C(t) : Sp(Φ′(𝕀)) → Sp(Φ(𝕀)) to be the inverse image map of t_{𝕀} : Φ(𝕀) → Φ′(𝕀). We leave it to the reader to verify that C(t) is in fact a Coalg(T) morphism between C(Φ, next) and C(Φ′, next′) (cf. the proof of Proposition 5.3 in [17]).

Proposition 4.14 If we extend A and C as described above we obtain functors

A : Coalg(T)^{op} → BAO_{T} and C : BAO_{T} → Coalg(T)^{op}.

Remark 4.15 As pointed out by a referee, an alternative construction of the coalgebra C(Φ) can be given which avoids reasoning element-wise about ultrafilters. It uses that each of the type constructors ×, +, (−)^{D}, 𝕍 has a dual on Boolean algebras that can be described by generators and relations, see Vickers [33]. For example, 𝕍^{∂}𝔸 is generated by symbols [𝕍]a, a ∈ A, and relations expressing that the insertion of generators [𝕍] : 𝔸 → 𝕍^{∂}𝔸 preserves finite meets (𝕍^{∂} is the H of Remark 3.13 where we write now [𝕍]a instead of □a to emphasise the connection with Definition 4.1 and Remark 4.5); the dual ×^{∂} of × is the coproduct of algebras, that is, 𝔸_{1} ×^{∂} 𝔸_{2} is generated by symbols [π_{i}]a, a ∈ A_{i}, i = 1, 2, and relations expressing that the insertion of generators [π_{i}] :

𝔸_{i} → 𝔸_{1} ×^{∂} 𝔸_{2} are algebra morphisms; etc. For a VPF T, let T^{∂} be the dual functor constructed from ×^{∂}, +^{∂}, ((−)^{D})^{∂}, 𝕍^{∂}. From the presentation of a T -BAO Φ as a manysorted algebra (Remark 4.5) and the fact that each of the constructions 𝕍^{∂}, ×^{∂}, … used in T^{∂} is a free algebra modulo equations satisfied by Φ we obtain, by induction on the ingredients S of T, a family of morphisms

q_{Φ}(S) : S^{∂}(Φ(𝕀)) → Φ(S).

q_{Φ} allows us to transform T -BAOs Φ into T^{∂}-algebras T^{∂}(Φ(𝕀)) ⟶^{q_{Φ}(T)} Φ(T) ⟶^{next} Φ(𝕀) whose dual then is C(Φ).^{2} Conversely, to define the T -BAO Φ = A(𝕏, c) as a manysorted algebra, we let Φ(S) = ℂlpS(𝕏) and the interpretation of the operation symbols is given by the insertion of generators, e.g. Φ(S) = ℂlpS(𝕏) ⟶^{[𝕍]} 𝕍^{∂}(ℂlpS(𝕏)) ≅ Φ(𝕍S) is the interpretation of the operation symbol [𝕍] in Φ. Finally, note that the description of the dual type constructors ×^{∂}, +^{∂}, ((−)^{D})^{∂}, 𝕍^{∂} by generators and relations also offers an explanation of the notion of a T -BAO. Indeed, the operations and equations defining T -BAOs in Remark 4.5 correspond to the generators and relations describing the dual type constructors.

5 Vietoris Polynomial Functors: representation and duality theorems

In the previous section we encountered functors

A : Coalg(T)^{op} → BAO_{T}  and  C : BAO_{T} → Coalg(T)^{op}.

Here we will study these functors in more detail, and show that in fact they provide an adjunction between the categories BAO_{T} and Coalg(T). We will define two families of morphisms, α_{Φ} : ACΦ → Φ in BAO_{T}, and γ_{(𝕏,c)} : (𝕏, c) → CA(𝕏, c) in Coalg(T)^{op}; and prove that these are the unit and counit witnessing the fact that A is left adjoint to C. Since the γ’s will turn out to be isomorphisms, this will then show that Coalg(T)^{op} is (isomorphic to) a full coreflective subcategory of BAO_{T}. In contrast to the classical case of the duality MA ≃ DGF^{op}, we do not obtain a dual equivalence between BAO_{T} and Coalg(T). This is due to the fact, which the reader might have noticed already, that the axiomatic definition of T -BAOs does not force a T -BAO Φ to respect T -structure. We take a closer look at this, characterising the largest full subcategory of BAO_{T} on which the adjunction restricts to an equivalence. By

2 The map r_{Φ} which is used to construct C(Φ) in Definition 4.13 arises from the dual of q_{Φ} as r_{Φ}(T) = 𝕊p(Φ(T)) ⟶^{𝕊p(q_{Φ}(T))} 𝕊p T^{∂}(Φ(𝕀))) ⟶^{≅} T 𝕊p(Φ(𝕀).

showing that the initial algebra of BAO_{T} is exact, that is, belongs to this subcategory, we obtain the final T -coalgebra as its dual.

We start by proving that every T -coalgebra has an ‘ultrafilter representation’: it is isomorphic to its double dual. Recall from Definition 2.4 that for a Stone space 𝕐, ϵ_{𝕐} : 𝕐 → 𝕊p ℂlp𝕐 denotes the homeomorphism fixed by ϵ_{𝕐}(y) := {a ∈ Clp_{𝕐} | y ∈ a}.

Theorem 5.1 Let T be a Vietoris polynomial functor, and let (𝕏, c) be a T -coalgebra. Then the map ϵ_{𝕏} : 𝕏 → 𝕊p(ℂlp(𝕏)) is a Coalg(T)-isomorphism witnessing that

(𝕏, c) ≅ C(A(𝕏, c)).

Proof. We first show that for each sort S ∈ Ing(T) the following diagram commutes:

𝕊p A(𝕏, c)(S) ^{r_{A(𝕏,c)}(S)} S(𝕊p A(𝕏, c)(𝕀)) S𝕏_{ϵ_{S𝕏}}  _{S(ϵ_{𝕏})}

The proof is by induction on S. We will only treat the Vietoris functor, since all other cases work exactly as in the proof of Lemma 5.6 in [17]. In order to prove the commutativity of the above diagram for S = 𝕍S′, take an arbitrary F ∈ 𝕍S′(𝕏). Then, unravelling the definitions of r, A and of (·)^{𝕍}, we find

r_{A(𝕏,c)}(S)(ϵ_{S𝕏}(F)) = r_{A(𝕏,c)}(S′) [{V | A(𝕏, c)(𝕍)^{−1}(ϵ_{S𝕏}(F)) ⊆ V }]
= r_{A(𝕏,c)}(S′) [{V | {α ∈ Clp_{S′𝕏} | (α)^{𝕍} ∈ ϵ_{S𝕏}(F)} ⊆ V }]
= r_{A(𝕏,c)}(S′) [{V | {α ∈ Clp_{S′𝕏} | F ⊆ α} ⊆ V }]
=^{(!)} {S′(ϵ_{𝕏})(u) | u ∈ F }
= S(ϵ_{𝕏})(F).

It is left to prove (!). For (⊇), take an arbitrary u ∈ F, and define V_{u} := ϵ_{S′𝕏}(u). Then for all a ∈ Clp_{S′𝕏} it holds that F ⊆ a implies u ∈ a, which is equivalent to a ∈ ϵ_{𝕏}(u) = V_{u}; in other words,V_{u} satisfies the condition {α | F ⊆ α} ⊆ V_{u}. Also, by the inductive hypothesis we have that S′(ϵ_{𝕏})(u) = r_{A(𝕏,c)}(S′)(ϵ_{S_{1}𝕏}(u)). Taking these observations together we see that S′(ϵ_{𝕏})(u) ∈ r_{A(c)}(S′) [{V | {α ∈ Clp_{S′𝕏} | F ⊆ α} ⊆ V }]. For (⊆), let V ∈ Sp A(𝕏, c)(S′) be such that {α ∈ Clp_{S′𝕏} | F ⊆ α} ⊆ V. By Stone duality we know that ⋂_{α∈V} α = {u} for exactly one u ∈ S′𝕏. This u must be an element of F, because ⋂_{α∈V} α ⊆ ⋂{α | F ⊆ α} = F and we get ϵ_{S′𝕏}(u) = V. By the induction hypothesis this is the same as saying r_{A(𝕏,c)}(S′)(V) = S′(ϵ_{X})(u), which proves the inclusion.

Now we proceed to prove the theorem: we calculate

\begin{aligned}C(A(𝕏, c)) ∘ ϵ_{𝕏} & = & (r_{A(𝕏,c)}(T) ∘ 𝕊p ℂlp(c)) ∘ ϵ_{𝕏} & = & r_{A(𝕏,c)}(T) ∘ (𝕊p ℂlp(c) ∘ ϵ_{𝕏}) \\ & = & r_{A(𝕏,c)}(T) ∘ (ϵ_{T 𝕏} ∘ c) & = & (r_{A(𝕏,c)}(T) ∘ ϵ_{T 𝕏}) ∘ c, \end{aligned}

where the third step is by naturality of ϵ. Now by commutativity of the above diagram for T we find that C(A(𝕏, c)) ∘ ϵ_{𝕏} = T (ϵ_{𝕏}) ∘ c, which is nothing but stating that ϵ_{𝕏} is a coalgebra homomorphism. But then since ϵ_{𝕏} is an isomorphism between Stone spaces we may conclude that it is also an isomorphism between the two given coalgebras. qed

The functor C is not faithful in general; however, when it comes to morphisms having a complex algebra A(𝕏, c) as their domain, we can prove the following.

Proposition 5.2 Let (𝕏, c) be a T -coalgebra and Φ be a T -BAO. Furthermore let v, v′ : A(𝕏, c) → Φ be morphisms in BAO_{T}. Then C(v) = C(v′) implies v = v′.

Proof. Let (𝕏, c), Φ, v and v′ be as in the statement of the Proposition, and assume that C(v) = C(v′). Then it is clear that we have v_{𝕀} = v′_{𝕀}. With the help of Lemma 5.3 below we therefore get v = v′. qed

The following lemma, which forms the heart of the proof of Proposition 5.2, is stated separately because we need it again further on.

Lemma 5.3 Let (𝕏, c) be a T -coalgebra and Φ a T -BAO. Furthermore let v, v′ : A(𝕏, c) → Φ be natural transformations whose components preserve all the Boolean structure, v_{𝕀} = v′_{𝕀} and v_{𝕂} = v′_{𝕂} for all constants 𝕂 ∈ Ing(T). Then v = v′.

Proof. Assume that we have two natural transformations v, v′ : A(𝕏, c) → Φ as required in the lemma. In order to prove that v = v′, it suffices to show that

v_{S} = v′_{S} for all S ∈ Ing(T).  (3)

We will prove (3) by induction on S. In the base case (S = 𝕀 or S = 𝕂 for some constant functor 𝕂), it follows immediately that v_{S} = v′_{S}. For the inductive step of the proof, we confine ourselves to a rough sketch of the proof idea. In each case, in order to show that v_{S}(U) = v_{S′}(U) for every clopen U of S𝕏, we try and find a clopen subbasis B such that v_{S}(W) = v′_{S}(W) for all subbasic W. For instance, in the case that S = 𝕍S′, put

B := {W | W ∈ ( )^{𝕍}[Clp_{S′𝕏}]} ∪ {−W | W ∈ ( )^{𝕍}[Clp_{S′𝕏}]} ,

and let W ∈ B. Then one can easily check that we have v_{S}(W) = v′_{S}(W) for all W ∈ B and by the fact that B is a clopen subbasis of the Vietoris topology one can use a straightforward argument to show that v_{S} = v′_{S}. qed

We are now ready to show that the functors C : BAO_{T} → Coalg(T)^{op} and A : Coalg(T)^{op} → BAO_{T} form a so-called dual representation. That is, C is right adjoint to A and the unit of the adjunction is an isomorphism. We first define the unit γ and the counit α of the adjunction. Recall that we proved in Theorem 5.1 that ϵ is an isomorphism; for r_{Φ} see Definition 4.11 and for i_{Φ(S)} Definition 2.4.

Definition 5.4 (α, γ) For a T -BAO (Φ, next) and a S ∈ Ing(T) we define

α_{Φ} : AC(Φ) → Φ

via α_{Φ}(S) := j_{Φ(S)} ∘ ℂlp(r_{Φ}(S)), where j_{Φ(S)} denotes the inverse of the isomorphism i_{Φ(S)} : Φ(S) → ℂlp 𝕊p Φ(S).

For a T -coalgebra (𝕏, c), we define

γ_{(𝕏,c)} : (𝕏, c) → CA(𝕏, c) in Coalg(T)^{op}

as the inverse γ_{(𝕏,c)} : CA(𝕏, c) → (𝕏, c) of the morphism ϵ_{(𝕏,c)} : (𝕏, c) → CA(𝕏, c) in Coalg(T). ⊲

Intuitively, the next theorem establishes a duality between Coalg(T) and BAO_{T} in which every coalgebra (𝕏, c) can be represented in a canonical way by the algebra A(𝕏, c).

Theorem 5.5 Let T be a VPF. Then A : Coalg(T)^{op} → BAO_{T} is a full embedding and has C : BAO_{T} → Coalg(T)^{op} as a right adjoint with γ and α as unit and counit. That is, Coalg(T)^{op} is (isomorphic to) a full coreflective subcategory of BAO_{T}.

Before we turn to the proof of this theorem, we first show that α is indeed a morphism of T -BAOs.

Lemma 5.6 The family of maps α_{Φ}( ) : ACΦ → Φ is a morphism of T -BAOs.

Proof. We have to show that α_{Φ}( ) is a natural transformation and that α_{Φ}( ) fulfils an additional naturality condition with respect to the next-operator. Concerning the first claim we must prove that for all S ⇝^{p} S′ in Ing(T) we have

Φ(p) ∘ α_{Φ(S′)} = α_{Φ(S)} ∘ ( )^{p}.

It suffices to show, by a case distinction, that this equation holds for paths of length at most one. As all of these proofs boil down to a tedious but straightforward unravelling of definitions, we confine ourselves to the case that p = 𝕍 and S = 𝕍S_{1}. Take an arbitrary U ∈ Clp_{S_{1} 𝕊pΦ(𝕀)} and let a ∈ Φ(S_{1}) be such that ℂlp(r_{Φ}(S_{1}))(U) = â. Then

α_{Φ}(S)((U)^{𝕍}) = (j_{Φ(S)} ∘ ℂlp(r_{Φ(S)}))((U)^{𝕍})
= (j_{Φ(S)} ∘ r_{Φ(S)}^{−1})({β ⊆ U | β ⊆ S_{1} 𝕊p Φ(𝕀) closed})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | r_{Φ(S)}(u) ⊆ U})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | {r_{Φ(S_{1})}(v) | Φ(𝕍)^{−1}(u) ⊆ v} ⊆ U})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | {v | Φ(𝕍)^{−1}(u) ⊆ v} ⊆ ℂlp(r_{Φ(S_{1})})(U)})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | {v | Φ(𝕍)^{−1}(u) ⊆ v} ⊆ â})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | Φ(𝕍)^{−1}(u) ⊆ v ⇒ a ∈ v})
= j_{Φ(S)} ({u ∈ Sp Φ(S) | Φ(𝕍)(a) ∈ u})
= Φ(𝕍)(a)
= Φ(𝕍) (j_{Φ(S_{1})} ∘ ℂlp(r_{Φ(S_{1})})(U))
= (Φ(𝕍) ∘ α_{Φ}(S_{1})) (U)

and we get α_{Φ}(S) ∘ ( )^{𝕍} = Φ(𝕍) ∘ α_{Φ}(S_{1}), as required. Now we turn to the second claim. The ‘additional naturality condition with respect to the next-operator’ is the following: next ∘ α_{Φ}(T) = α_{Φ}(𝕀) ∘ ℂlp(r_{Φ}(T) ∘ 𝕊p next). This is easily shown to hold (the second identity being due the naturality of j).

α_{Φ}(𝕀) ∘ ℂlp(r_{Φ}(T) ∘ 𝕊p(next)) = j_{Φ(𝕀)} ∘ ℂlp(𝕊p(next)) ∘ ℂlp(r_{Φ(T)})
= next ∘ j_{Φ(T)} ∘ ℂlp(r_{Φ}(T))
= next ∘ α_{Φ}(T).

qed

Proof of Theorem 5.5. For the adjunction it suffices to show ([23], p. 81) that for all (𝕏, c) ∈ Stone and for all u : C(Φ) → (𝕏, c) there is a unique v : A(𝕏, c) → Φ such that the following diagram in Coalg(T) commutes:

CA(𝕏, c) ^{γ_{𝕏}} (𝕏, c) CΦ_{C(v)}  _{u}

Indeed, defining v = α_{Φ} ∘ A(u), we calculate

γ_{𝕏} ∘ C(α_{Φ} ∘ A(u)) = γ_{𝕏} ∘ 𝕊p (α_{Φ}(𝕀) ∘ A(u)(𝕀))
= γ_{𝕏} ∘ 𝕊p(j_{Φ(𝕀)} ∘ r_{Φ}(𝕀) ∘ ℂlp(u))
= γ_{𝕏} ∘ 𝕊p(ℂlp(u)) ∘ 𝕊p(j_{Φ(𝕀)})
= u ∘ γ_{𝕊p(Φ(𝕀))} ∘ 𝕊p(j_{Φ(𝕀)})
= u

The last two steps use the fact that 𝕊p and ℂlp are adjoint with (co)units j and γ, see Definitions 2.4 and 5.4. Uniqueness of v is Proposition 5.2. To conclude the proof, recall that a left-adjoint is full and faithful iff the unit is an isomorphism ([23], p. 88). Hence A is full and faithful by Theorem 5.1. qed

We now turn to a characterisation of the largest subcategory of BAO_{T} on which the adjunction from Theorem 5.5 restricts to a dual equivalence. The reader might have noticed already that our adjunction is not a dual equivalence since the definition of T -BAOs does not force a T -BAO Φ to respect T -structure. For example, if S_{1} × S_{2} is an ingredient of T then it may well be that Φ(S_{1} × S_{2}) ≠ Φ(S_{1}) + Φ(S_{2}).

Definition 5.7 Let S be a functor Stone → Stone. Then

Ŝ := ℂlp ∘ S ∘ 𝕊p .

defines a corresponding functor Ŝ on the category BA. ⊲

The following definition introduces exact T -BAOs, that is, those T -BAOs which do respect T -structure.

Definition 5.8 (Exact T -BAO) A T -BAO Φ is called exact if there is a family of isomorphisms

τ_{S} : Ŝ(Φ(𝕀)) → Φ(S)

with the following properties:

• τ : ˆ( )(Φ(𝕀)) → Φ is a natural transformation, where ˆ( )(Φ(𝕀)) : Ing(T)^{op} → BA_{∧} is defined on objects as in Definition 5.7 and on paths p : S_{1} ⇝^{p} S_{2} as ( )^{p} in Definition 4.8 (with 𝕏 here being Φ(𝕀)).

• τ_{𝕀} = j_{Φ(𝕀)}, where again j_{Φ(𝕀)} denotes the inverse of the isomorphism i_{Φ(𝕀)} : Φ(𝕀) → ℂlp 𝕊p Φ(𝕀)

• τ_{𝕂} = id_{Clp_{𝕂}} for every constant 𝕂 ∈ Ing(T).

BAO_{T}^{e} is the full subcategory of BAO_{T} consisting of the exact T -BAOs. ⊲ Remark 5.9 In terms of Remark 4.5, as noted by a referee, the exact T -BAOs are those that are freely generated by Φ(𝕀). Indeed, comparing, on the one hand, the definition of T -BAOs via operations and equations (Remark 4.5) and, on the other hand, the definition of the dual functors S^{∂} by generators and relations (Remark 4.15), we see that a T -BAO Φ is freely generated by Φ(𝕀) iff Φ(S) ≅ S^{∂}(Φ(𝕀)). It remains to notice S^{∂} ≅ Ŝ.

We will now see that exact T -BAOs are precisely those T -BAOs Φ for which the component α_{Φ} of the counit of the adjunction is an isomorphism.

Theorem 5.10 Let T be a VPF. The category BAO_{T}^{e} is the largest subcategory of BAO_{T} on which the adjunction of Theorem 5.5 restricts to a dual equivalence to Coalg(T).

Proof. Let B be the largest subcategory of BAO_{T} on which the adjunction A ⊣ C restricts to an equivalence. Then for any Φ ∈ B the map α_{Φ} : ACΦ → Φ consists of a family of isomorphisms going from ACΦ(S) = Ŝ(Φ)(𝕀) to Φ(S). Therefore we can define a family of isomorphisms τ_{S} : Ŝ(Φ)(𝕀) → Φ(S) by letting τ = α_{Φ}. It is straightforward to check that this family satisfies the conditions in Definition 5.8. Hence Φ ∈ BAO_{T}^{e}. Now let Φ ∈ BAO_{T}^{e}. We have to show that the counit α_{Φ} is an isomorphism. As Φ ∈ BAO_{T}^{e} there is a family of isomorphisms

τ_{S} : (ACΦ)(S) → Φ(S).

which is natural in S and for which we have τ_{𝕀} = j_{Φ(𝕀)} = α_{Φ}(𝕀) and τ_{𝕂} = id_{Clp_{𝕂}} = α_{Φ}(𝕂) for all constants 𝕂 ∈ Ing(T). Using Lemma 5.3 one can therefore show that τ_{S} = α_{S} for all S ∈ Ing(T). But this means in particular that α_{Φ} is an isomorphism. qed

We now show that the final object in Coalg(T) is obtained as the dual of the initial object in BAO_{T}. This is a direct consequence of Theorem 5.5 and a special case of the more general fact that the right adjoint C preserves colimits of diagrams that take values in the A-image of Coalg(T)^{op}.

Theorem 5.11 Let T be a VPF and L_{T} be the initial object in BAO_{T}. Then CL_{T} is final in Coalg(T).

Proof. We prove the theorem by showing that α_{L_{T}} is an isomorphism, i.e. L_{T} ∈ BAO_{T}^{e}. Finality of CL_{T} follows then immediately from the duality between Coalg(T) and BAO_{T}^{e}. Since L_{T} is initial there is a morphism m : L_{T} → ACL_{T}. Since id_{L_{T}} is the unique morphism L_{T} → L_{T} it follows that α_{L_{T}} ∘ m = id_{L_{T}}. We want to show that m ∘ α_{L_{T}} : ACL_{T} → ACL_{T} is in fact the identity on ACL_{T}. Since A is full (cf. Theorem 5.5) there is f : CL_{T} → CL_{T} in Coalg(T) such that A(f) = m ∘ α_{L_{T}}. We obtain α_{L_{T}} ∘ A(f) = α_{L_{T}} ∘ m ∘ α_{L_{T}} = α_{L_{T}} = α_{L_{T}} ∘ A(id_{CL_{T}}) and the universal property of the coreflection tells us that f = id_{CL_{T}}, hence, id_{ACL_{T}} = m ∘ α_{L_{T}} and α_{L_{T}} is iso. qed

Remark 5.12 (Completeness of Many-Sorted Coalgebraic Modal Logic) We can now use the standard Stone duality approach to prove soundness and completeness of Jacobs’s logic MSML_{T} (Remark 4.6) with respect to the coalgebraic semantics. Soundness is immediate. To show completeness, assume that / ⊢ φ in L, i.e. φ ≠ ⊤ in the initial T -BAO L_{T}, i.e. L_{T} \begin{matrix}/ \\ ⊧ \end{matrix} φ = ⊤. Since L_{T} ≅ AC(L_{T}) by the theorem, it follows from C(L_{T}) ⊧ φ ⇔ AC(L_{T}) ⊧ φ = ⊤ (Remark 4.10) that C(L_{T}) \begin{matrix}/ \\ ⊧ \end{matrix} φ. To conclude this remark, let us note that completeness w.r.t. set coalgebras as in Jacobs [17] is an immediate consequence of completeness w.r.t. Stone coalgebras, since every Stone coalgebra is a set coalgebra (for example, 𝕍-coalgebras are also P-coalgebras). Moreover, for Stone coalgebras, as a further consequence of Stone duality, we also get an expressiveness result: If two states of two Stone coalgebras are not bisimilar then they can be separated by some formula.

Remark 5.13 In [17], Jacobs states a similar final coalgebra theorem for set-based Kripke polynomial functors. Unfortunately, there is a defect in his proof. The problem involves his functor C_{J} : BAO_{T_{J}} → Coalg(T_{J})^{op}. Note that Jacobs’s functor T_{J} is the set-based analogue of our T. (To obtain T_{J} from ours, simply replace all occurrences of the Vietoris functor with the power set functor P, and interpret all polynomial functors occurring in T in the standard way.) Thus Jacobs studies the relation between T_{J}-BAOs and set-based T_{J}-coalgebras. However, as mentioned already, on the algebraic side, we may identify T_{J}-BAOs with T -BAOs. Thus we may compare Jacobs’s way of relating BAO_{T} with the Set-based Coalg(T_{J}) to our way of relating BAO_{T} to the Stone-based Coalg(T). Jacobs assigns a modal logic MSML_{T} to each Kripke polynomial functor (Remark 4.6) and he proves that the coalgebras for these functors form a sound and complete semantics for these logics. In order to obtain the final coalgebra for a so-called finite KPF T, that is, a KPF that may only contain the finite-power set functor, he maps the Lindenbaum-Tarski algebra L_{T} to its corresponding coalgebra C_{J}(L_{T}), using the abovementioned functor C_{J}. This construction works when C_{J} maps T -BAOs to T -coalgebras. This is, however, only the case for functors T not containing the finite power set functor P_{ω} (since a (P_{ω}𝕀)-BAO is mapped to a P-coalgebra and not to a P_{ω}-coalgebra). This means that Jacobs’s construction of final objects in Coalg(T) works only for Kripke polynomial functors that do not contain the power set functor or its finitary version. Moving from the category of sets to Stone enables us to repair this defect.

6 Conclusions

What we have done so far can be viewed from various perspectives. Here we summarise some of these, indicating possible future research directions.

Stone Coalgebras and Modal Logic Research on the relation between coalgebras and modal logic started with Moss [25] although earlier work, e.g. by Rutten [29] already showed that Kripke frames and models are instances of coalgebras. [20,19] showed that modal logic for coalgebras dualises equational logic for algebras, the idea being that equations describe quotients of free algebras and modal formulae describe subsets of final (or cofree) coalgebras. Another account of the duality has been given in [22] where it was shown that modalities dualise algebraic operations. But whereas, usually, any quotient of a free algebra can be defined by a set of ordinary equations, one needs infinitary modal formulae to define all subsets of a final coalgebra. As a consequence, while we have a satisfactory description of the coalgebraic semantics of infinitary modal logics, we do not completely understand the relationship between coalgebras and finitary modal logic. The results in this paper show that Stone coalgebras provide a natural and adequate semantics for finitary modal logics, but there is ample room for clarification here.

Another approach to a coalgebraic semantics for finitary modal logics was given in [21]. There, the idea is to modify coalgebra morphisms in such a way that they capture not bisimulation but only bisimulation up to rank ω. Since finitary modal logics capture precisely bisimulation up to rank ω, the resulting category Beh_{ω} provides a convenient framework to study the coalgebraic semantics of finitary modal logic. So an important next step is to understand the relation between both approaches.

Stone Coalgebras as Systems We investigated coalgebras over Stone spaces as models for modal logic. But what is the significance of Stone-coalgebras from the point of view of systems (that is, coalgebras over Set, cf. Rutten [30])? What is the relationship between Set-coalgebras and Stone-coalgebras? An interesting observation is here that their notions of behavioural equivalence coincide. Recall that two elements of two coalgebras are behaviourally equivalent iff they can be identified by some coalgebra morphisms. Since Stone-coalgebra morphisms have to be continuous, we expect that fewer states are identified under Stone-behavioural equivalence than under Set-behavioural equivalence. But the following holds.

Consider a Vietoris polynomial functor T : Stone → Stone and its corresponding (Kripke polynomial) functor T̆ : Set → Set. There is an obvious functor F : Coalg(T) → Coalg(T̆). Now let (𝕏_{1}, c_{1}), (𝕏_{2}, c_{2}) be two T -coalgebras and x_{1}, x_{2} be two elements in 𝕏_{1}, 𝕏_{2}, respectively. Then ((𝕏_{1}, c_{1}), x_{1}) and ((𝕏_{2}, c_{2}), x_{2}) are behaviourally equivalent iff (F (𝕏_{1}, c_{1}), x_{1}) and (F (𝕏_{2}, c_{2}), x_{2}) are behavioural equivalent. — Proof: ‘only if’ is immediate. The converse follows from the fact that the final T -coalgebra appears as the ω-limit of the terminal sequence (see Worrell [34]) of T̆.

Generalising Stone Coalgebras Coalgebras over Stone spaces can be generalised in different ways. We have seen that replacing the topologies by represented Boolean algebras leads to general frames. But it will also be of interest to consider other topological spaces as base categories.

From the point of view of modal logic, it will be interesting to investigate the Vietoris functors on other base categories. For example, Palmigiano [26] shows that the Vietoris functor can be defined on Priestley spaces, leading to an adequate semantics for positive modal logic.

From the point of view of the theory of coalgebras, the value of the move from Set to Stone as a base category can be explained as follows. For a functor on Set the notion of behavioural equivalence is, in general, characterised by the whole terminal sequence running through all ordinals. But often, one is interested only in finitary approximations. In the examples considered in this paper, the move from a functor on Set to its version on Stone has the consequence that the final coalgebra is the limit of the finitary approximants of the terminal sequence (and, therefore, behavioural equivalence is completely characterised by the finitary approximants of the terminal sequence). We expect that this idea of topologising a functor T in order to tailor the behaviour of T -coalgebras to meet a specific notion of observable behaviour will have further applications to universal coalgebra.

Coalgebras and Duality Theory Whereas many, or most, common dualities are induced by a schizophrenic object (see Johnstone [18], Section VI.4.1), the duality of modal algebras and descriptive general frames is not. To see why this is so, write K : MA → DGF, L : DGF → MA for the contravariant functors witnessing the duality and suppose, for a contradiction that there is a schizophrenic object S. That is, assume that MA(𝔸, S) ≅ UK(𝔸) where U denotes the forgetful functor DGF → Set. Then Set(1, U𝔾) ≅ U𝔾 ≅ UKL𝔾 ≅ MA(L𝔾, S) ≅ DGF(KS, KL𝔾) ≅ DGF(KS, 𝔾), showing that KS is a free object over one generator in DGF. But since DGF-morphisms are also bisimulations it is not hard to see that such an object cannot exist.

On the other hand, this duality is an instance of the duality Alg(T^{op}) ≅ Coalg(T)^{op} of algebras and coalgebras, with the Vietoris functor 𝕍 as the functor T. It seems therefore of interest to explore which dualities are instances of the algebra/coalgebra duality. As a first step in this direction, Palmigiano [26] shows that the duality between positive modal algebras and K^{+}-spaces can be described in a similar way as in Section 3 (although the technical details are substantially more complicated).

References

[1] S. Abramsky. A Cook’s Tour of the Finitary Non-Well-Founded Sets. Invited Lecture at BCTCS 1988.

[2] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92(2):161–218, 1991.

[3] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1–77, 1991.

[4] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science Volume 3, pages 1–168. Oxford University Press, 1994.

[5] F. Alessi, P. Baldan, and F. Honsell. Partializing Stone Spaces Using SFP Domains (extended abstract). In M. Bidoit et al, editor, CAAP ’97, volume 1158 of LNCS, pages 478–489. Springer, 1997.

[6] A. Baltag. A logic for coalgebraic simulation. In H. Reichel, editor, Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of ENTCS, 2000.

[7] F. Bartels, A. Sokolova, and E. de Vink. A hierarchy of probabilistic system types. In H.P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), volume 86.1 of ENTCS, 2003.

[8] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001.

[9] C. Cîrstea. On specification logics for algebra-coalgebra structures: Reconciling reachability and observability. In M. Nielsen, editor, Proceedings of FoSSaCS 2002, volume 2303 of LNCS, pages 82–97. Springer, 2002.

[10] B. Davey and J. Galati. A coalgebraic view of Heyting duality. Studia Logica, 75:259–270, 2003.

[11] J. de Bakker and E. de Vink. Control Flow Semantics. MIT Press, 1996.

[12] R. Engelking. General Topology. Heldermann Verlag, 1989.

[13] L.L. Esakia. Topological Kripke models. Soviet Mathematics Doklady, 15:147–151, 1974.

[14] M. Gehrke. The order structure of stone spaces and the T_{d}-separation axiom. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 37:5–15, 1991.

[15] R. Goldblatt. A calculus of terms for coalgebras of polynomial functors. In A. Corradini, M. Lenisa, and U. Montanari, editors, Coalgebraic Methods in Computer Science (CMCS’01), volume 44 of ENTCS, 2001.

[16] R. Goldblatt. Metamathematics of modal logic I. Reports on Mathematical Logic, 6:41–78, 1976.

[17] B. Jacobs. Many-sorted coalgebraic modal logic: a model-theoretic study. Theoretical Informatics and Applications, 35(1):31–59, 2001.

[18] P. Johnstone. Stone Spaces. Cambridge University Press, 1982.

[19] A. Kurz. Logics for Coalgebras and Applications to Computer Science. PhD thesis, Ludwig-Maximilians-Universität München, 2000.

[20] A. Kurz. A co-variety-theorem for modal logic. In M. Zakharyaschev et alii, editor, Advances in Modal Logic 2. CSLI, Stanford University, 2001.

[21] A. Kurz and D. Pattinson. Coalgebraic modal logic of finite rank. Mathematical Structures in Computer Science. Forthcoming.

[22] A. Kurz and J. Rosický. Modal predicates and coequations. In L. Moss, editor, Coalgebraic Methods in Computer Science (CMCS’2002), volume 65 of ENTCS, 2002.

[23] S. Mac Lane. Category Theory for the Working Mathematician. Springer, 1971.

[24] E. Michael. Topologies on spaces of subsets. Transactions of the American Mathematical Society, 71:152–182, 1951.

[25] L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999.

[26] A. Palmigiano. Coalgebraic semantics for positive modal logic. In H.-P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), volume 82 of ENTCS, 2003.

[27] D. Pattinson. Semantical principles in the modal logic of coalgebras. In Proceedings of STACS 2001, volume 2010 of LNCS, pages 514–526, Springer, 2001.

[28] M. Rößiger. Coalgebras and modal logic. In H. Reichel, editor, Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of ENTCS, 2000.

[29] J. Rutten. A calculus of transition systems (towards universal coalgebra). In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal Logic and Process Algebra, volume 53 of CSLI Lecture Notes. CSLI, Stanford University, 1995.

[30] J. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3–80, 2000.

[31] G. Sambin and V. Vaccaro. Topology and duality in modal logic. Annals of Pure and Applied Logic, 37:249–296, 1988.

[32] D. Turi and J. Rutten. On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces. Mathematical Structures in Computer Science, 8, 1998.

[33] S. J. Vickers. Topology Via Logic. Cambridge University Press, 1989.

[34] J. Worrell. Terminal sequences for accessible endofunctors. In B. Jacobs and J. Rutten, editors, Coalgebraic Methods in Computer Science (CMCS’99), volume 19 of ENTCS, 1999.