key: cord-0060839-uynmsd71 authors: Nishizawa, Koki; Katsumata, Shin-ya; Komorida, Yuichi title: Stone Dualities from Opfibrations date: 2020-04-01 journal: Relational and Algebraic Methods in Computer Science DOI: 10.1007/978-3-030-43520-2_14 sha: 474bf0624b08cce50e67ae5f8f6bce2823ce56f2 doc_id: 60839 cord_uid: uynmsd71 Stone dualities are dual equivalences between certain categories of algebras and those of topological spaces. A Stone duality is often derived from a dual adjunction between such categories by cutting down unnecessary objects. This dual adjunction is called the fundamental adjunction of the duality, but building it often requires concrete topological arguments. The aim of this paper is to construct fundamental adjunctions generically using (co)fibered category theory. This paper defines an abstract notion of formal spaces (including ordinary topological spaces as the leading example), and gives a construction of a fundamental adjunction between the category of algebras and the category of corresponding formal spaces. Dual equivalences between categories of spaces and those of algebras are ubiquitous in mathematics -following the famous book by Johnstone [1] , they are collectively called Stone dualities after the Stone Representation Theorem of Boolean algebras. Technically, they often arise as the restriction of dual adjunctions called fundamental adjunctions. For example, the Stone duality between sober topological spaces and spatial frames is obtained by cutting down the fundamental adjunction between the category of topological spaces and that of frames, which is the heart of pointless topology [2] . Categorical settings to capture various fundamental adjunctions of Stone dualities has been studied in [3] [4] [5] [6] [7] [8] . The basic idea of these settings is to formulate fundamental adjunctions as dual adjunctions that are representable through functors to Set. The objects representing adjoint functors are called dualizing object [6] . In this paper, we give a new construction of fundamental adjunctions by (Grothendieck) opfibrations 1 . Roughly speaking, our construction takes a category of algebras equipped with an abstract notion of subalgebra, then derives both the category of spaces and a fundamental adjunction between them. Despite its abstract nature, the constructed fundamental adjunctions reflect several properties seen in concrete ones. One such property is that, in a certain setting, our construction yields fundamental adjunctions that enjoy representability. Another is the full-faithfulness of the algebra-to-space construction. It is characterized in terms of the mono-ness of the unit arrow X → Ω A(−,Ω) , where A is a category of algebras and Ω is the dualizing object. This generalizes the full-faithfulness argument of the constructions of topological spaces from Boolean algebras [1] . Our construction proceeds by taking the pullback of c along R (right of Fig. 1 ). We call (R * M ) op the category of formal spaces. The horizontal legR of the pullback has a left adjoint by Hermida's adjoint lift theorem [9] . The fundamental adjunction then appears as the composite adjunction between A and R * M . We will illustrate several examples of fundamental adjunctions arising from our construction. The one between the category Frm of frames and that of topological spaces, which is the standard example of Stone duality, is an immediate instance: take c to be the subobject opfibration c : Sub(Frm) → Frm and R to be the power functor 2 (−) : Set op → Frm with the Sierpinski frame 2. Related Work. Categorical formulations of fundamental adjunctions via dualizing objects were studied by many authors [3] [4] [5] [6] [7] [8] . For the formulation of representable dual adjunctions, see e.g. [5] , where Dimov and Tholen also showed a general condition to obtain fundamental adjunctions using the lift conditions. In [8] , Maruyama improved the lift conditions by (1) breaking the symmetry of Dimov and Tholen's framework, and (2) imposing different conditions on the algebraic and spatial categories. Categories of Chu spaces [10] are self-dual, and can accommodate various dualities in them. Pratt [11] demonstrates that the self-dual category Chu(Set, 2) can accommodate (1) sets and complete atomic Boolean algebras, (2) Stone spaces and Boolean algebras, and (3) sober spaces and spatial frames. We relate the category of Chu spaces and that of formal spaces in Sect. 4.1. However, our construction does not explain the self-duality. The theory of natural dualities [12] aims to go roughly the same way as us, to make a "category of spaces" from a given category of algebras. The scope of their theory is narrower than ours, while their theory brings finer results. It is a future work to find connections between their framework and ours. It seems that neither of them can derive the other. Organization. This paper is organized as follows. In Sect. 2, we define opfibered comprehensions, which is the input of our construction. In Sect. 3, we construct the category of formal spaces from an opfibered comprehension and derive the fundamental adjunction. In Sects. 4 and 5, we list various examples of our framework. In Sect. 6, we show how to relate two fundamental adjunctions. Section 7 summarizes this work and future work. Preliminaries. The identity functor on a category A is denoted by Id A , and the identity natural transformation on a functor f is denoted by id f . We write L R : B → A (or simply L R) to mean that the functor R : B → A has L as a left adjoint. Its unit and counit are denoted by η L R , L R , respectively. One of inputs to our construction of fundamental adjunction ( Fig. 1) is an opfibered comprehension. An opfibered comprehension is defined to be a tuple (c : M → A, i, d) of functors such that 1. c : M → A is an opfibration, 2. i : A → M is the right adjoint to c whose counit is the identity, and 3. d : M → A is the right adjoint to i whose unit is the identity. We here recall the definition of (Grothendieck) opfibration; a good reference is [13] . The conditions 2 and 3 imply several equalities between functors and natural transformations. The last one is proved in [14] . Perhaps the simplest example is the following: Example 1. We write A → for the arrow category of A: objects are arrows in A, and an arrow from f to g is a pair (p, q) of arrows such that p • f = g • q. The functors cod, dom : A → → A respectively map an object arrow f : a → a to a and a, and an arrow (p, q) to p and q. The functor : A → A → maps an object a to the identity arrow id a on a and an arrow f : a → a to (f, f ): id a → id a . It is easy to see that (cod : A → → A, , dom) is an opfibered comprehension; the cocartesian lifting of an A-arrow g : a →b with an A → -object f : a → a is given by g(f ) = (g, id a ): f → g • f . We call it the arrow opfibered comprehension. We can restrict the objects of A → to monomorphisms if A has a (strong epi, mono)-factorization system. This is our leading example of an opfibered comprehension. We call it the subobject opfibered comprehension. These two examples above are generalized to the following: Let (E, M ) be a factorization system on A in the sense of [15] . We obtain an opfibered comprehension in the same way as Example 2: the triple (cod : M → A, , dom) is an opfibered comprehension, where we regard M as the full subcategory of A → whose objects are arrows in M . We note that the unique diagonal fill-in property of the factorization system guarantees the uniqueness of the mediating morphism k in (1). In general, c fails to be an opfibration when (E, M ) is merely a weak factorization system in the sense of [16] . On the other hand, in any opfibered comprehension arrows are factored in the following sense. Consider the cocartesian lifting f (ia) of f with ia as above. From the universal property of the cocartesian arrow, we obtain a unique vertical arrow . This factorization of if in M yields the desired factorization of dif = f in A. Throughout this section, we fix an opfibered comprehension (c : M → A, i, d) and an adjunction L R : B → A. Our first step is to derive the category of spaces from the opfibered comprehension. For this, we take the pullback of c along R : B → A, as done in (2) . We identify the opposite of the vertex of this pullback as the category of formal spaces and formally continuous maps. Definition 2. We define the category FS(R, c) of formal spaces to be (R * M ) op , the opposite of the vertex category of the above pullback in the category Cat of locally small categories. We call objects and arrows in FS(R, c) formal spaces and formally continuous maps, respectively. We give the following concrete presentation of FS(R, c). We next construct the fundamental adjunction between FS(R, c) op and A. The pullback diagram induces two extra adjunctions. The first is a right adjoint of π : the universal property of the pullback yields the mediating functor ρ : We have an adjunction π ρ whose counit is the identity. Proof. We show that π ρ is the adjunction whose counit is The second is the left adjoint ofR : R * M → M . This is the keystone of the fundamental adjunction. The general result of Hermida shows that the horizontal leg of the change-of-base of any opfibration along right adjoint has a left adjoint: Theorem 1 (Corollary 3.2.5, [9] ). In (2),R : To summarize, we obtain the following sequence of adjunctions, which factors L R: Starting from an opfibered comprehension (c : M → A, i, d) and an adjunction L R : B → A, this factorization theorem yields an adjunction between FS(R, c) op and A. This is the main subject of this paper, the fundamental adjunction. Sp R,c L • i : A → FS(R, c) op , Al R,c d •R : FS(R, c) op → A. When the left fundamental adjoint Sp R,c is full faithful, it yields an equivalence between A and its full image. We here consider when Sp R,c is full faithful. As shown in Lemma 1, in any opfibered comprehension (c : Proof. The unit of the adjunction Next, we study the representability of the fundamental adjunction. We say that a dual adjunction L R : C op → D is representable through γ : C → Set and δ : D → Set if there is a pair Ω C ∈ C, Ω D ∈ D of objects such that Note that it follows γΩ C ∼ = δΩ D ; see e.g. [5, Lemma 2.3] . The fundamental adjunction enjoys this representability when it arises from the following situation. Let c : M → A be an opfibered comprehension and Ω ∈ A. We assume that (1) Proof. The first is by the factorization of A(−, Ω) (Theorem 2). We show the second. When the construction of the category of formal spaces is applied to some concrete arrow opfibered comprehension cod : A → → A, derived concepts of formal space coincide with existing structures. We illustrate two such examples: one is Chu spaces [10] and the other is topological systems introduced by Vickers [18] . These suggests that, for the arrow opfibered comprehension, our construction can be regarded as a "non-symmetric" generalization of Chu construction. Let (A, I, ⊗, [−, −]) be a symmetric monoidal closed category, and Σ ∈ A be an object. It plays the role of a dualizing object. In [19] , Pavlovic showed that a category of Chu spaces can be obtained as the comma category of In [18] , Vickers introduces the category of topological system to model state spaces paired with notions of observations. This category is defined by the following data, and has a similar flavor to the category of Chu spaces. -A topological system is a tuple (x, a, s : x × a → 2) of a set, a frame, and a function such that, for each p ∈ x, the function s(p, −): a → 2 preserves finite meets and arbitrary unions. -A map from a topological system (x , a , s ) to another one (x, a, s) is a tuple (f, g) such that f : x → x is a function, g : a → a is a frame homomorphism and they satisfy s •(f × a) = s •(x × g). We can easily see that it is isomorphic to the category FS(2 (−) , cod) of formal spaces, where cod : Frm → → Frm is the arrow opfibered comprehension and 2 (−) : Set op → Frm is the power functor to 2. The left fundamental adjoint Sp 2 (−) ,cod : Frm → FS(2 (−) , cod) op sends each frame to the corresponding locale as defined in [18] . By Proposition 2 we can see that the functor is fully faithful, which implies that the definition of the category of locales there is indeed equivalent to the more common definition: Loc = Frm op . Let U : A → Set be a monadic functor and Ω ∈ A. Then (1) U has a left adjoint, (2) A admits powers of Ω since A has small limits, and (3) A admits a strong epi-mono factorization. Therefore from such U and Ω, we obtain two ingredients needed for constructing the category of formal spaces and the fundamental adjunction: (1) Then it returns the formal space (A(X, Ω), Im(η From Theorem 3, the fundamental adjunction is representable, and from Corollary 2, the left fundamental adjoint Sp Ω (−) ,cod is fully faithful if and only if the unit η : X → Ω A(X,Ω) of the hom-power adjunction is mono. We demonstrate that some known fundamental adjunctions between categories of algebras and those of spaces are instances of the above fundamental adjunction. To save space, we write FS(Ω, A), Sp Ω,A and Al Ω,A to mean FS(Ω (−) , cod), Sp Ω (−) ,cod and Al Ω (−) ,cod , respectively. Let us introduce various categories by Table 1 . These categories have the special object 2 = ({⊥, }, ⊥ ≤ ). In particular, FS(2, BA) is isomorphic to the category Fld of fields of sets and Boolean homomorphisms [20] , and FS(2, Frm) ∼ = Top as in Example 4. Since the lattice 2 X and its sublattices are always distributive, we have FS(2, DLat) ∼ = FS(2, Lat). Example 6. When A = BA, SLat, DLat, or CSLat, L = A(−, 2) is faithful and the left fundamental adjoint Sp 2,A is fully faithful by Proposition 2. On the other hand, when A = Lat, L is not faithful, since components for non distributive bounded lattices of the unit η Lat(−,2) 2 (−) are monomorphisms [21] . When A = Frm, L is not faithful and Sp 2,Frm is not fully faithful, since components for non spatial frames of the unit η Sp 2,Frm Al 2,Frm are not isomorphisms [1] . is called an ideal [21] in X, if it is down-closed and finite join closed. The set of all ideals in X forms a complete join semilattice, where for a set α of ideals, its join α is given not by its union α, but by {x | ∃β ⊆ α, β is finite, x ≤ β}. This construction gives adjunctions ideals forget : CSLat → SLat and ideals forget : Frm → DLat. Therefore, we have the following extended fundamental adjunctions. such that (c, c ) is a map of adjunction (see [17, Section IV.7] ) from F M U M to F A U A , that is, the following equalities hold: Then there is an adjunction F * U * : Since (R * M , π , R ) is the pullback of R and c in Cat, there exists the unique U * satisfying π • U * = π and R • U * = U M • R, where U * maps an object (b, m) to (b, U M m) and maps arrows similarly. To save notational burden, let η A and A be the unit and the counit of F A U A , and η M and M be the unit and the counit of holds. Thus, we have an arrow in the category R * M . We will show that this is a universal arrow from (b, m ) to U * . Assume that we have an arrow (f, g): The composite Thus, by the universality of cocartesian lifting, M m • (F M g) decomposes through e m . Combining this with the first decomposition yields the decomposition we want. Uniqueness can be shown by a similar means. Therefore, U * has a left adjoint F * satisfying F * (b, m ) = (b, ( A Rb ) * F M m ). By specializing Theorem 4, we have some more usable results. Proof. We can canonically obtain F A → U A → : A → → (A ) → by defining their object parts by the arrow parts of F A U A : A → A . These satisfy the conditions in Theorem 4, so we can apply it to obtain F * U * : The pushout in the construction in Theorem 4 turns out to coincide with postcomposition. This yields the equality for F * . By the assumption on the counit, the pushout in the construction in Theorem 4 turns out to coincide with postcomposition. This yields the equality for F * . Example 9. The leading example of Corollary 4 is the adjunction between Fld ∼ = FS(2, BA) and FS(2, DLat). The forgetful functor forget : BA → DLat has a right adjoint comp, which maps a distributive lattice (X, ∨, ∧, ⊥, ) to the Boolean algebra of its complemented elements [20] , that is to say, {x ∈ X | ∃x ∈ X, x ∨ x = , x ∧ x = ⊥}. Since this adjunction satisfies the condition of Corollary 4, we have the adjunction forget * comp * : FS(2, DLat) op We also have given the sufficient condition to construct different formal spaces FS(R, c) and FS(R , c ). Its leading example is the adjunction between FS(2, DLat) and FS(2, BA). It is future work to compare with other dualities, for example, Priestley duality [21] , algebra/coalgebra duality [22] , natural dualities [12] , and so on. Stone Spaces. Cambridge Studies in Advanced Mathematics The point of pointless topology General functorial semantics I A couple of triples Categorical Topology and Its Relation to Analysis Concrete dualities Categorical duality theory: with applications to domains, convexity, and the distribution monad Fibrations, logical predicates and related topics *-Autonomous Categories Chu spaces Natural Dualities for the Working Algebraist Categorical Logic and Type Theory Remarks on punctual local connectedness Handbook of Categorical Algebra Factorization, fibration and torsion Categories for the Working Mathematician Topology via Logic Chu I: cofree equivalences, dualities and *-autonomous categories Lattices and Ordered Algebraic Structures Introduction to Lattices and Order Computer Science Logic 2013 (CSL 2013) Acknowledgments. This work was the supported by JSPS KAKENHI Grant Number JP24700017. The second and third authors carried out this research under the support of JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).