The Double Category of Paired Dialgebras on the Chu Category
Aydin Manzouri

TL;DR
This paper introduces a new double category framework on the Chu category that unifies various mathematical structures, demonstrating self-duality properties and exploring categorical products and coproducts.
Contribution
It develops a novel formalism combining double categories, dialgebras, and Chu construction to unify diverse mathematical formalisms within a single framework.
Findings
The double category exhibits horizontal and vertical self-duality.
It investigates the existence of binary horizontal products and coproducts.
Provides foundational insights for future categorical unification efforts.
Abstract
The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of providing common languages and frameworks to be utilized by professionals from different fileds in solving interdisciplinary and challenging problems. The present thesis is done in the same direction. Here, we develop a new formalism with the central idea of "unification of various mathematical branches". For this purpose, we utilize three major tools from today's mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of "double cateogries", the theory of "universal dialgebra", and the "Chu construction". With the aid of these tools, we define and study a double category that subsumes a significant…
| Statement | Dual Statement |
|---|---|
| is monic | is epic |
| is an isomorphism | is an isomorphism |
| is initial | is terminal |
| etc. | etc. |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topics in Algebra · Algebraic structures and combinatorial models
\MakePerPage
footnote [intoc]
The Double Category of Paired Dialgebras on the Chu Category
(English Translation)
Aydin Manzouri
May 2017
A Thesis Submitted in Partial Fulfillment of
the Requirements for the Degree of
Master of Science in Pure Mathematics
Faculty of Mathematical Sciences
Shahid Beheshti University
Tehran, Iran
Supervisor:
Professor Mojgan Mahmoudi
Advisors:
Professor Mohammad-Mehdi Ebrahimi
Professor Amir Daneshgar, Sharif University of Technology
**Abstract
The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of providing common languages and frameworks to be utilized by professionals from different fileds in solving interdisciplinary and challenging problems.
The present thesis is done in the same direction. Here, we develop a new formalism with the central idea of “unification of various mathematical branches”. For this purpose, we utilize three major tools from today’s mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of “double cateogries”, the theory of “universal dialgebra”, and the “Chu construction”. With the aid of these tools, we define and study a double category that subsumes a significant portion of the formalisms usual within the body of mathematics and theoretical computer science. We show that this double category possesses the properties of “horizontal self-duality” and “vertical self-duality”. Also, we perform a primary investigation about existence of binary horizontal products and coproducts in this category. Finally, we give some suggestions for future work. **
Contents
Preface
Convergence of the various scientific and technological fields, towards solving challenging multi-dimensional problems, is a need that is felt in the twenty-first century far more than anytime in the past. Today, we are the heirs of an enormous amount of scientific and technological achievements, and those continue to accumulate at accelerating rates. Within this roaring ocean of information, the degrees of specialization of the study areas have reached such levels that, frequently, effective transference of findings from one professional to another becomes a serious challenge itself.
In addition, we are the heirs of huge amounts of human and environmental problems. Today, few people in the scientific community ever doubt the role of man in global warming. Non-degradable plastic and rubber waste, various toxic chemicals, petrochemicals, and heavy metals that humans have been producing and releasing into nature since the beginning of the twentieth century have polluted lands and waters; those substances interfere with ecological cycles, they cause death of organisms and cause undesirable changes in food chains, and the result of all these returns to us humans in the form of environmental disasters and health threats. On the other hand, the emergence of drug-resistant pathogens due to overconsumption of antibiotics has made the medical sciences face new challenges in fighting infectious diseases. Yet another set of alarming issues is the crises of water and food shortages and hard-to-treat epidemics and pandemics throughout the world, especially in the impoverished areas. Along with all these problems, one should add the potential dangers of the new technologies. Today, nanotechnology, biotechnology, and information technology are already forming new industrial revolutions throughout the world while many of their side-effects are unknown to us.
For solving difficult multi-dimensional problems in such an extremely complex era, effective cooperation of professionals from different disciplines is a clear necessity. But any effective cooperation requires using a “potent common language” by all involved; therefore, mathematics manifests its value as the common language of sciences and technologies once again. Although various mathematical theories developed up to now have offered brilliant services to natural sciences and engineering fields, currently we need a new mathematics which is even more capable of unifying the infrastructures as well as the bodies of different branches of science and technology.
The crucial point to be considered is that it is impossible for mathematics to succeed in such unification when it is internally fragmented (as we witness today); rather, the process of convergence and unification has to start within mathematics itself. By “unification of mathematics” we do not mean a theory principally for the foundations of mathematics (such as axiomatic set theory), but one which is able to encompass the essence of different theories within the body of mathematics and which provides the working mathematician with the necessary toolbox for effective cross-disciplinary communication of ideas.
The present thesis is done in the same direction. For this purpose, we utilize three major tools from today’s mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of “double cateogries”, the theory of “universal dialgebra”, and the “Chu construction”.
Eilenberg and Mac Lane officially founded the theory of categories in their historic paper in 1945 [6]. There were various generalizations of the theory later, of which we point to Ehresmann’s theory of double categories (see [21] and the references within). The notion of double category can be seen as a “two-dimensional generalization” of the notion of category. The formalism developed in the current thesis makes use of the language of double categories.
From a categorical viewpoint, algebraic theories can have their corresponding “dual theories”. These duals are referred to as coalgebras. Whereas the theory of universal algebra [24, 13] recognizes and studies the common patterns among specific algebraic theories such as the theories of groups, rings, linear algebra, etc., the theory of universal coalgebra does the same with specific coalgebraic theories such as automata, transition systems, Petri nets, and event systems [53, 28].
Again, categorically one can think of dialgebras [44] as common generalizations of algebras and coalgebras. Also, the theory of universal dialgebra [56] has been developed as a common generalization of universal algebra and universal coalgebra. Universal dialgebra recognizes and studies the common patterns among specific dialgebraic theories.
From a different perspective, tracing the property of “self-duality” in categories (see Definition 1.2.27) leads us to a family of categories called the Chu construction [9]. Existence of the self-duality property is essential for the purposes of the present work (see the discussion given in Section 1.1). It is well-known that Set, the category of sets and functions, lacks this property; therefore, in order to achieve a unified formalism for solving interdisciplinary problems, one has to develop the theory of universal dialgebra based on some other category which, along with other desirable properties, possesses self-duality. Consequently, the Chu construction enters the scene as an appropriate substitute for Set.
In this thesis, after introducing the above tools, we define and study a formalism which subsumes a significant portion of the formalisms usual within the body of mathematics and theoretical computer science. The general structure of the thesis is as follows. In Chapter 1 the preliminaries are given. Next, the Chu construction is introduced in Chapter 2. The contents of that chapter are mainly from [9, 18, 45, 49]. Next, universal dialgebra is given in Chapter 3, with the materials mainly inspired by [44, 56].
Then, the main formalism of the thesis is given in Chapter 4. In that chapter, after introducing double categories, we introduce the construction (see Section 4.2). We show that this double category possesses the property of “Klein-invariance” (see Definition 4.1.27), which is the conjunction of the two properties of horizontal and vertical self-duality. Also, we do a primary investigation concerning existence of binary horizontal products and coproducts in . Finally, a few suggestions for future work will be given in Chapter 5.
Chapter 1 Introduction
This chapter discusses the general ideas and motivations behind the present work and provides the preliminaries for the next chapters.
Thesis organization. In Section 1.1 we speak of the fundamental motivations; in Section 1.2 we quickly review the essentials of basic category theory; and in Section 1.3, internal categories are introduced.
Chapter 2 introduces the Chu construction and discusses a number of its properties. Chapter 3 studies universal dialgebra on a given base category in general and on the Chu construction in particular. Chapter 4 begins with introducing the formalism of double categories and proceeds towards the main formalism of the present work. Finally, Chapter 5 gives the conclusions and directions for future work.
1.1 The fundamental motivations
Today, in the twenty-first century, we live at a time of ever-accelerating changes, of which scientific and technological advancements constitute a significant portion. Virtually every aspect of human life is constantly flooded with scientific discoveries and technological innovations. This situation was forecast with relatively high accuracy in [51] in 2002:
“We stand at the threshold of a New Renaissance in science and technology, based on a comprehensive understanding of the structure and behavior of matter from the nanoscale up to the most complex system yet discovered, the human brain. A coherent science and engineering approach based on the unity of nature and its holistic investigation will lead to technological convergence and a more efficient societal structure…”
The article then explains this “technological convergence” as follows [ibid]:
“The phrase ‘convergent technologies’ refers to the synergistic combination of four major ‘NBIC’ (Nano-Bio-Info-Cogno) provinces of science and technology, each of which is currently progressing at a rapid rate: (a) nanoscience and nanotechnology; (b) biotechnology and biomedicine, including genetic engineering; (c) information technology, including advanced computing and communications; (d) cognitive science, including cognitive neuroscience.
Accelerated scientific and social progress can be achieved by combining research methods and results across these provinces in duos, trios, and the full quartet.”
On the other hand, there is a crucial fact concerning the nature of scientific research itself [ibid]:
“The sciences have reached a watershed at which they must combine if they are to continue to advance. The New Renaissance must be based on a holistic view of science and technology that envisions new technical possibilities and focuses on people.”
Finally, the article lays emphasis on the key roles of mathematics, computer science, and system approach in the New Renaissance [ibid]:
“Developments in system approach, mathematics, and computation in conjunction with NBIC allow us for the first time to understand the natural world, and social events and humanity as closely coupled complex, hierarchical systems. Applied both to particular research problems and to the over-all organization of the research enterprise, this complex system approach provides holistic awareness of opportunities for integration, in order to obtain maximum synergism along main directions of progress.”
From the above, it follows that development of mathematics in the twenty-first century shall be heavily influenced by the requirements of intensely-converging sciences and technologies. This shall result in more unified mathematical theories, capable of solving more diverse, more complex, more hierarchical, and more challenging problems arising in the NBIC hybrid. Needless to say, this historical process also requires the pure and applied parts of mathematics to unify and function as a whole.
Now, the present work has been inspired by ideas and motivations inclusive of what described above. The author has been trying to develop a new and unified theoretical framework in which those aspects of pure mathematics that are of (potential or actual) practical importance may be embodied. The result is a theory that interweaves three threads of existing mathematical theories, each of which having a unifying nature itself: category theory, universal dialgebra, and the Chu construction.
Category theory. The twentieth century witnessed a number of triumphs in solidification of mathematical thinking, one of which was the formulation of various axiomatic set theories as candidate foundations of mathematics. Moreover, Eilenberg and Mac Lane officially formulated category theory in their historic paper (“General theory of natural equivalences”) in 1945 [6]. Contrary to set theory which places emphasis on sets and membership, category theory prioritizes arrows, which are relationships between different mathematical objects. This way, category theory sheds light on even the farthest corners of mathematical realm and unifies structures so distant from each other that would seem totally unrelated otherwise. It is also worth mentioning that in addition to the set-theoretic foundations, there are suggestions for category-theoretic foundations of mathematics (e.g. see [59] and the references therein). Therefore, as foundational systems for mathematics, category theory possesses much more unifying power than set theory.
Now, ordinary categories themselves can be seen as kinds of “one-dimensional structures”, in which objects play the role of “points” and arrows that of “one-dimensional entities between points”. These can be generalized to higher dimensions in various ways. The present work utilizes a definite kind of generalization known as “double categories” [21, 22]. These will be introduced in Chapter 4.
Universal dialgebra. From the viewpoint of mathematical logic, groups, rings, fields, lattices, and other algebraic structures can be viewed as models of particular theories. Whereas abstract algebra studies those models, universal algebra deals with algebraic or equational theories in general [24, 69]. Grätzer gives the following notes on the latter subject in his book [24]:
“In A. N. Whitehead’s book on Universal Algebra, published in 1898, the term universal algebra had very much the same meaning that it has today….
Thus universal algebra is the study of finitary operations on a set, and the purpose of research is to find and develop the properties which such diverse algebras as rings, fields, Boolean algebras, lattices, and groups may have in common.”
Now, with the aid of category theory, the above picture can be expanded in a number of ways. First of all, the collection of finitary operations on a given set may be replaced with the notion of “-algebra”, where is an endofunctor (see 1.2.50) on the category of sets . The advantage of this approach is that instead of an indexed set of fundamental operations, we have only one mapping [16]. Next, -algebras can be categorically “dualized” (see 1.2.12) to yield -coalgebras. -coalgebras provide the (categorical) basis for the theory of universal coalgebra. Quoting Rutten [53]:
“These observations, then, have led to the development in the present paper of a general theory of coalgebras called ‘universal coalgebra’, along the lines of universal algebra. Universal algebra … deals with the features common to the many well-known examples of algebras such as groups, rings, etc. The central concepts are -algebra, homomorphism of -algebras, and congruence relation. The corresponding notions … on the coalgebra side are: coalgebra, homomorphism of coalgebras, and bisimulation equivalence. These notions constitute the basic ingredients of our theory of universal coalgebra. (More generally, the notion of substitutive relation corresponds to that of bisimulation relation; hence congruences, which are substitutive equivalence relations, correspond to bisimulation equivalences.) Adding to this the above-mentioned observation that various dynamical systems (automata, transition systems, and many others as we shall see) can be represented as coalgebras, makes us speak of universal coalgebra as ‘a theory of systems’. We shall go even as far as, at least for the context of the present paper, to consider coalgebra and system as synonyms.”
Also, Jacobs [28] writes:
“Mathematics is about the formal structures underlying counting, measuring, transforming etc…. In more recent decades also ‘dynamical’ features have become a subject of research. The emergence of computers has contributed to this development. Typically, dynamics involves a ‘state of affairs’, which can possibly be observed and modified….
Both mathematicians and computer scientists have introduced various formal structures to capture the essence of state-based dynamics, such as automata (in various forms), transition systems, Petri nets and event systems. The area of coalgebra has emerged within theoretical computer science with a unifying claim. It aims to be the mathematics of computational dynamics. It combines notions and ideas from the mathematical theory of dynamical systems and from the theory of state-based computation. The area of coalgebra is still in its infancy but promises a perspective on uniting, say, the theory of differential equations with automata and process theory and with biological and quantum computing, by providing an appropriate semantical basis with associated logic. The theory of coalgebras may be seen as one of the original contributions stemming from the area of theoretical computer science.”
Thirdly, the assumption that universal algebra and universal coalgebra merely deal with set-based operations and dynamics may be dropped. In other words, one can study algebras and coalgebras induced by arbitrary endofunctors , where may be any category, not necessarily the category of sets.
Finally, universal algebra and universal coalgebra themselves can be unified. So far, the situation is roughly as follows: universal algebra unifies specific algebraic structures, universal coalgebra does the same with specific state-based dynamical systems, and these two are categorical duals to each other. Now, unification of the two theories results in the more recent theory of universal dialgebra. The notion of dialgebra was investigated in [44] as a common generalization of algebras and coalgebras. Dialgebras subsume both features of algebraic structuring and coalgebraic dynamics; also, there are many interesting examples of dialgebras that are neither algebra nor coalgebra.
However, it was not until 2010 that the first paper on “universal dialgebra” as a new theory was published. In that year, Voutsadakis [56] gave a systematic treatment of the subject for the first time, and showed how the fundamental results in both universal algebra and universal coalgebra can be viewed as special cases of those in universal dialgebra. There, the notion of -dialgebra is introduced as the categorical formalism of dialgebras, where are arbitrary endofunctors on the category of sets. Although Voutsadakis’s work deals exclusively with set-based dialgebras, as he himself states: “… many of the results (in fact most of them, if adequately translated) will be easily seen to hold in arbitrary categories”. This is what we will do to some extent in Chapter 3.
An interesting fact is that “being a dialgebra” is a self-dual statement (see 1.2.15); that is, the dual of a dialgebra is again a dialgebra. This can be contrasted with the above-mentioned fact that algebras and coalgebras are duals to each other. In other words, whereas the process of dualization interchanges algebraic and coalgebraic concepts, the same process does not affect dialgebras conceptually.
However, this does NOT mean that dialgebras are perfectly immune to dualization. Indeed, there is a subtle fact concerning the dualization process. For example, when (the category of sets and functions), quoting Gumm [26]:
“Universal coalgebra is dual to universal algebra over the dual of the category of sets. As the category Set is not self-dual, universal algebra cannot simply be translated to deliver a corresponding theory of coalgebras. It can, however, serve as a formidable source of inspiration.”
The same issue affects dialgebras, too. Again, this will be discussed in Chapter 3.
A remedy for the above problem is to replace Set with a self-dual category (see 1.2.27). Consequently, in search for a self-dual substitute for Set, the author has found the third essential ingredient of the current thesis.
The Chu construction. Thu Chu construction is exactly what the author has found appropriate for the purposes of the present work. Quoting Barr [9]:
“In 1975, I began a sabbatical leave at the ETH in Zürich, with the idea of studying duality in categories in some depth. By this, I meant not such things as the duality between Boolean algebras and Stone spaces, nor between compact and discrete abelian groups, but rather self-dual categories such as complete semi-lattices, finite abelian groups, and locally compact abelian groups. Moreover, I was interested in the possibilities of having a category that was not only self-dual but one that had an internal hom and for which the duality was implemented as the internal hom into a ‘dualizing object’….
The desired properties were what I subsequently called -autonomy….
By the end of the year, I had in fact produced a moderate number of examples of -autonomous categories. One of them was a full subcategory of topological abelian groups that included all the locally compact abelian (LCA) groups in such a way that the duality restricted to them was the well-known duality of LCA groups….
Another example was a full subcategory of the category of locally convex topological vector spaces….
Thus I ended up with a category whose objects were pairs of vector spaces equipped with a pairing [with being the set of complex numbers]. A map from to is a pair of linear maps in which and (note the direction reversal) such that whenever and . There is no topology assumed and no continuity on the linear maps….”
He then continues to describe how he had formulated a new collection of -autonomous categories; and finally [ibid]:
“It seemed clear that this gave a -autonomous category, but there were a number of unpleasant details to be verified. Since my student, Po-Hsiang Chu needed a master’s project, so I asked him to verify them, which he did…. I now had expanded from six to infinity the repertory of known -autonomous categories.”
Eventually, the new collection of -autonomous categories gets named after P. Chu’s work in his thesis in 1979. The details of the construction will be given in Chapter 2 (see Section 2.2). The Chu construction, especially the set-based Chu construction, has many interesting features (see Chapter 2), among which is self-duality. Those features altogether make the (set-based) Chu construction an excellent replacement for , the category of sets and functions, for serving as a base category for a theory of universal dialgebra.
The present work. Although developing a theory of universal dialgebra on a self-dual basis has been one of the initial motivations for the author, the present work goes beyond it. Indeed, the formalism that we will be developing in Chapter 4 subsumes and interrelates all possible theories of universal dialgebra on the set-based Chu construction. More precisely, assuming a set-based Chu category Chu, we will develop a double categorical structure in which every horizontal “cross-section” corresponds to a “counter-current pairing” of two theories of universal dialgebra on Chu, while every vertical “cross-section” corresponds to interrelations between different dialgebraic theories for a fixed pair of objects of Chu. Moreover, we will show that the new double category is Klein-invariant (see Definition 4.1.27). This way, a two-dimensional unified framework emerges that subsumes a significant portion of what pure and applied mathematicians and computer scientists deal with in everyday work. The author hopes that the results of this work will prove to be beneficial for future scientific and technological advancements.
1.2 A quick review of basic category theory
In this section, we take a brief look at the basic definitions and constructions of category theory. We assume the reader’s familiarity with some kind of axiomatic set theory (e.g., refer to [36]). For the purpose of the present work, we need the concepts of “class” and “conglomerate” besides that of “set” and “function”. The material given in this section is mainly borrowed from [3, 11, 32, 34].
Classes
Intuitively speaking, classes consist of “large collections of sets”. In particular, the following are required.
- (1)
The members of each class are sets. 2. (2)
For every “property” , one can form the class of all sets with prroperty .
Hence there is the largest class of all sets, called the universe. Classes are precisely the subcollections of . Thus, given classes and , one can form such classes as and . Because of this, there is no problem in defining functions between classes, equivalnce relations, etc. 3. (3)
If are classes, then so is the -tuple . 4. (4)
Every set is a class. 5. (5)
There is no surjection from a set to a proper class.
This means that sets have “fewer” elements than proper classs.
Conglomerates
The concept of “conglomerate” has been created to deal with “collections of classes”. The following are required.
- (1)
Every class is a conglomerate. 2. (2)
For every property , one can form the conglomerate of all classes with property . 3. (3)
Conglomerates are closed under analogues of the usual set-theoretic constructions (pairing, union, intersection, product, etc.)
Thus, we can form the conglomerate of all classes, as well as functions between conglomerates.
Remark 1.2.1**.**
Classes that are not sets are called proper classes. Similarly, conglomerates that are not classes are called proper conglomerates. For example, is a proper class, while is a proper conglomerate.
Categories
There are various ways to define a category. We state two of them since each will be useful in some parts of the current work.
Definition 1.2.2**.**
(The first definition of categories.) A category is a quadruple consisting of:
- •
a class , whose elements are called objects of the category or -objects; this class is also denoted by ; we prefer this latter notation, and we will be using it in the sequel;
- •
for every pair of objects, a set , whose elements are called
morphisms or arrows or -morphisms or -arrows from to ; this set is also denoted by or by ; we prefer the last notation, and we will be using it in the sequel;
- •
for each triple of objects, a function
[TABLE]
called the composition, which assigns, to each pair of morphisms , the
composite morphism or just ; each of these two notations has its own advantages and therefore, we will be using both in the sequel;
- •
for each object , an element or of , called the identity morphism or identity arrow on ; we prefer the notation “”, and we will use it most of the time.
These data are subject to the following axioms.
- (1)
Associativity Axiom. Given morphisms
, the following equality holds:
[TABLE]
Hence we can safely discard parentheses and write . 2. (2)
Identity Axiom. Given a morphism , the following equalities hold:
[TABLE] 3. (3)
Disjointness Axiom. The sets are pairwise disjoint.
The union of all sets is denoted by and is called the class of morphisms or the class of arrows of , or equivalently, the class of -morphisms or the class of -arrows.
Remark 1.2.3**.**
- (1)
A morphism is represented by the notation
. The object is called the domain or the source of , and the object is called the codomain or the target of . We may write
[TABLE]
Two arrows with are called composable. 2. (2)
We will often write instead of , and instead of . 3. (3)
Also, in the situation of a diagram like that of 1.1, we say that the diagram is commutative (or the diagram commutes) if, taking any two vertices, the composite of the arrows along any path from the first vertex to the second is equal to the composite along any other path from the first to the second; e.g., when in this diagram.
An analogous terminology holds for diagrams of arbitrary shape. 4. (4)
is the only arrow from to that plays the role of an identity for the composition. Indeed, if is another such morphism, then
[TABLE] 5. (5)
Axiom (3) guarantees that each -morphism has a unique domain and a unique codomain.
Now we state the second definition:
Definition 1.2.4**.**
(The second definition of categories.) Alternatively, a category is a sextuple , where:
- •
are the classes of objects and morphisms of , respectively;
- •
s,t:\mathcal{C}_{\mathrm{mor}}\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}\mathcal{C}_{\mathrm{obj}} are two functions assigning, to every morphism , its source and target, respectively;
- •
is a partial function called the composition, which assigns, to any pair of morphisms with , their composite morphism ;
- •
is a function which assigns to each object a morphism or .
These data are subject to the following axioms:
- (1)
Source and target are respected by composition:
[TABLE] 2. (2)
Source and target are respected by identities:
[TABLE] 3. (3)
Composition is associative; that is, whenever and we have
[TABLE] 4. (4)
Composition satisfies the left and right unit laws; if and , then
[TABLE]
Remark 1.2.5**.**
Each of Definitions 1.2.2 and 1.2.4 has its own advantages when working in different theories. For example:
- •
Definition 1.2.2 works best when introducing the notion of “monoidal category”, a topic we will be introducing in Section 1.4. Monoidal categories provide the foundations for Chapter 2. It is also interesting to note that the (ordinary) study of enriched categories utilizes the language of monoidal categories. There, too, Defintion 1.2.2 generalizes quite nicely to the notion of “enriched category” (e.g., see Chapter 6 of [12]).
- •
In contrast, Definition 1.2.4 generalizes elegantly and straightforwardly to the notion of internal category, to be introduced in Section 1.3. Internal categories are one of the mainstream approaches to the development of the theory of double categories. Double categories will be introduced in Chapter 4 and they provide us with the necessary language to be used in the main formalism of this thesis.
Notation 1.2.6**.**
We will be using capital letters for objects and small letters for morphisms in a category. We will be using calligraphic letters to denote categories in general, and boldface upright letters for named categories (such as Set, Grph, etc.). More specific notations for different situations will come in the sequel.
Next, let us take a look at “size issues”:
Definition 1.2.7**.**
A category is also called a large category. On the other hand, is called a small category whenever is a set.
Remark 1.2.8**.**
- (1)
When is a set, then must be a set, so that the small category must also be a set. 2. (2)
Obviously, every small category is at the same time a large category, but not the converse. Large categories that are not small are called properly large categories.
Definition 1.2.9**.**
A very large category is defined in the same way as (the first definition of) a category except that instead of requiring to be a class and to be a set for all , we require them all to be conglomerates.
Remark 1.2.10**.**
- (1)
Since conglomerates are closed under union, we find out that must also be a conglomerate for the very large category . 2. (2)
Again, clear from the definition is the fact that every (large or small) category is at the same time a very large category, but the converse statement is false in general. Very large categories that are not large are called properly very large categories.
Proposition 1.2.11**.**
*Sets and functions between them constitute a (properly large)
category, which is denoted by Set.*
Other examples of categories are:
- •
the empty category with no objects and no arrows;
- •
the category with one object and one (identity) arrow;
- •
the category with two objects, two identity arrows, and one non-identity arrow:
[TABLE]
(the identities are not shown);
- •
every set might be seen as a discrete category, i.e., a category in which all morphisms are identities;
- •
monoids are categories with only one object, and the arrows are all from that single object to itself;
- •
topological spaces and continuous mappings constitute a category denoted by Top;
- •
groups and group homomorphisms make a category Grp;
- •
, the category of vector spaces and linear transformations over a field ;
- •
Aut, the category of all deterministic Moore automata and simulations between them;
- •
Grph, the category of graphs and graph homomorphisms;
- •
Mon, the category of monoids and homomorphisms between them;
- •
Pos, the category of posets and monotone mappings; and
- •
Rel, the category of sets and binary relations between them.
The duality principle
Quoting Mac Lane [32], “categorical duality is the process ‘Reverse all arrows’ ”. Below, we explain this more.
Definition 1.2.12**.**
Let be a statement about (large/very large) categories. The dual of is formed by making the following replacements throughout in :
- •
“domain” by “codomain” and vice versa;
- •
“” by “” for any arrows ;
- •
arrows and composites are reversed; and
- •
logic (and, or, not, then,…) is unchanged.
The result is Table 1.1.
Remark 1.2.13**.**
Note that the dual of the dual is the original statement: . If a statement involves a diagram, the dual statement involves that diagram with all arrows reversed.
The dual of each of the axioms for a category is also an axiom. Hence in any proof of a theorem about an arbitrary category from the axioms, replacing each statement by its dual gives a valid proof (of the dual conclusion). This is the duality principle:
Proposition 1.2.14**.**
The duality principle.* If a statement about a (large/very large) category is a consequence of the axioms, so is the dual statement .*
The duality principle provides a very useful tool in complicated situations. Having proved a theorem, we immediately gain a dual theorem by applying the duality principle. No proof of the dual theorem is needed to be given.
Definition 1.2.15**.**
A statement (or property) is called self-dual if .
For example, “being an identity morphism” is a self-dual property.
Definition 1.2.16**.**
For any (large/very large) category , the dual (or opposite) (large/very large) category of is the (large/very large) category with the same objects as of but with the arrows of reversed; that is,
[TABLE]
for every , and
[TABLE]
for every .
It is easy to see that is indeed a (large/very large) category.
Proposition 1.2.17**.**
For every (large/very large) category , .
Because of the way dual categories are defined, every statement concerning an object in the category can be translated into a logically equivalent statement concerning the object in the cateogry . Obviously, in general, is not equivalent to .
Functors
Up to now, all of our arguments have been about objects and arrows within a single category. Now we define a “morphism” from one category to another.
Definition 1.2.18**.**
A (covariant) functor from a category to a category , denoted by
, consists of the following:
- •
a function
[TABLE]
often, by some abuse of notation, the image of is written or just ;
- •
for every pair of objects of , a function
[TABLE]
again by abuse of notation, the image of is often written or just .
These data are subject to the following axioms:
- (1)
Preservation of composition. For every pair ,
[TABLE]
where the left hand side composition is in whereas the right hand side composition is in . 2. (2)
Preservation of identities. For every ,
[TABLE]
Definition 1.2.19**.**
Given two functors and
, their composition is defined as
[TABLE]
This composition is obviously associative. The identity functor
[TABLE]
is clearly an identity for the above composition law. Therefore:
Proposition 1.2.20**.**
Small categories and functors between them form a (properly large) category, which is denoted by Cat.
Proposition 1.2.21**.**
Large categories and functors between them form a (properly very large) category, which is denoted by CAT.
Notation 1.2.22**.**
We sometimes use the simplified notations and rather than and . Also, we sometimes denote the action on both objects and morphisms by
[TABLE]
Besides identity functors introduced above, there are some other important examples of functors, including:
- •
the constant functor: for any categories and any -object , there is a functor with value , defined by
[TABLE]
- •
the forgetful functor or the underlying set functor: let be a construct over Set, that is, a category of structured sets (such as groups, rings, etc.) and structure-preserving maps (group homomorphisms, ring homomorphisms, etc.); then there is a functor , where in each case is the underlying set of , and is the underlying function of .
Let us now investigate some properties of functors.
Proposition 1.2.23**.**
All functors preserve isomorphisms; i.e., whenever is a -isomorphism, is a -isomorphism.
Definition 1.2.24**.**
- (1)
A functor is called an isomorphism (functor) provided that is an isomorphism arrow in either Cat or CAT. This means that there exists another functor satisfying
[TABLE]
We may denote the situation by . 2. (2)
The categories are said to be isomorphic provided that they are isomorphic objects in Cat or in CAT. In other words, if there exists an isomorphism functor .
Definition 1.2.25**.**
Let be a functor.
- (1)
is called faithful provided that all the restrictions
[TABLE]
are injective functions. 2. (2)
is called full provided that all the above restrictions are surjective functions. 3. (3)
is called injective on objects provided that is an injective function. 4. (4)
is called a embedding provided that is injective; i.e., is injective on morphisms. 5. (5)
is called a full embedding provided that is full and an embedding.
Proposition 1.2.26**.**
A functor is:
- (1)
an embedding if and only if it is faithful and injective on objects; 2. (2)
a full embedding if and only if it is full, faithful, and injective on objects; 3. (3)
an isomorphism if and only if it is full, faithful, and bijective on objects.
Now, we introduce the notion of “self-duality” for categories.
Definition 1.2.27**.**
A category is called self-dual whenever is isomorphic to .
For example, Rel is self-dual but Set and Pos are not.
Remark 1.2.28**.**
Note that this concept may be defined slightly differently elsewhere (using equivalence of categories instead of isomorphism), but we have chosen Definition 1.2.27 so that it fits the purposes of the present work.
Next, we turn to “contravariant” functors.
Definition 1.2.29**.**
A contravariant functor is defined in the same way as a covariant functor except that the axiom of preservation of composition changes here to:
[TABLE]
In the present work we will be dealing with both covariant and contravariant functors. By default, functors will be assumed to be covariant unless stated otherwise.
It turns out that every contravariant functor may be translated into (two) covariant analogues. The process is described below.
Definition 1.2.30**.**
For every category , the reverser functor is defined as
[TABLE]
It is clear that for every category , is a (contravariant) isomorphism functor:
[TABLE]
Now we can easily change contravariant functors into their covariant analogues, using the reversers:
Proposition 1.2.31**.**
Every contravariant functor can be regarded as either of the following covariant functors:
[TABLE]
or
[TABLE]
In the light of Proposition 1.2.31, we frequently substitute contravariant functors with either or . However, there are some exceptions to this rule. For an important example, see Definition 4.3.2.
Notation 1.2.32**.**
Let be a (covariant) functor. We denote the composite functor
[TABLE]
by . Notice that is a covariant functor. In the literature, it is called the dual (or opposite) functor to .
Remark 1.2.33**.**
Obviously, . To form the dual of a categorical statement that involves functors, we make the same statement, but with each category and each functor replaced by its dual. Then, we translate this back into a statement about the original categories and functors.
Proposition 1.2.34**.**
- (1)
Each of the following properties of functors is self-dual: “isomorphism”, “embedding”, “faithful”, “full”, “isomorphism-dense”, and “equivalence”. 2. (2)
The notion of “self-dual category” introduced in Definition 1.2.27 is self-dual in the sense of Definition 1.2.12.
Subcategories
Definition 1.2.35**.**
- (1)
A category is said to be a subcategory of a (large/very large) category provided that the following conditions are satisfied:
- (a)
;
- (b)
for each , we have ;
- (c)
for each -object , the -identity on is the -identity on ;
- (d)
the composition law in is the restriction of the composition law in to the morphisms of . 2. (2)
is called a full subcategory of if, in addition to the above, for each
, we have .
As an important example, Cat is a full subcategory of CAT. More examples will come in the sequel.
Remark 1.2.36**.**
- (1)
From the above definition it follows that a full subcategory of a category can be specified by merely specifying its object class within . 2. (2)
The conditions (a), (b), and (c) of part (1) of the above definition do not imply (c). 3. (3)
If is a full functor or is injective on objects, then the image of under (i.e. the category formed by and ) is a subcategory of . However, for arbitrary functors , the image of under need not be a subcategory of .
For every subcategory of a (large/very large) category there is an associated inclusion functor . Each such inclusion is (a) an embedding, and (b) a full functor if and only if is a full subcategory of . As the next proposition shows, inclusions of subcateogries are (up to isomorphism) precisely the embedding functors.
Proposition 1.2.37**.**
A functor is a (full) embedding if and only if there exists a (full) subcategory of with inclusion functor and an isomorphism with .
Reflective and coreflective subcategories
Definition 1.2.38**.**
Let be a subcategory of , and let be a object.
- (1)
An -reflection (or -reflection arrow) for is a -morphism from to a -object with the following universal property:
for any -morphism into some -object , there exists a unique -morphism such that
[TABLE] 2. (2)
is called a reflective subcategory provided that each -object has a -reflection.
Proposition 1.2.39**.**
Reflections are essentially unique, i.e.,
- (1)
if and are -reflections for , then there exists a -isomorphism such that
[TABLE] 2. (2)
if is a -reflection for and is a -isomorphism, then is a -reflection for .
Reflections yield the following important proposition:
Proposition 1.2.40**.**
Let be a reflective subcategory of , and for each -object let be a -reflection arrow. Then there exists an unique functor such that the following conditions are met:
- (1)
; 2. (2)
for each -morphism , the diagram
R(D)$$D$$D^{\prime}$$R(D^{\prime})$$\scriptstyle r_{D}$$\scriptstyle f$$\scriptstyle r_{D^{\prime}}$$\scriptstyle R(f)
commutes.
Definition 1.2.41**.**
A functor constructed according to the above proposition is called a reflector for .
The dual of the concept reflective subcateogry is coreflective subcategory. That is:
Definition 1.2.42**.**
is a coreflective subcategory of whenever is a reflective subcategory of .
Thus, dualizing the descriptions given in 1.2.38, 1.2.39, 1.2.40, and 1.2.41 gives a taste of coreflections, coreflective subcategories, and coreflector functors.
Natural transformations
Definition 1.2.43**.**
Consider two functors F,G:\mathcal{C\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}D}. A natural transformation from to is a class of -morphisms , indexed by the -objects, and such that for every morphism Diagram 1.2 commutes.
Proposition 1.2.44**.**
Let be a small category and a category. The functors from to and the natural transformarions between them constitute a category. That category is small if is small.
The above-defined category is called the functor category from to and is denoted by .
Definition 1.2.45**.**
Let be functors.
- (1)
A natural transformation whose components are isomorphisms is called a natural isomorphism. 2. (2)
and are said to be naturally isomorphic (denoted by ) provided that there exists a natural isomorphism from to .
As a trivial example, an identity natural transformation from a functor to itself is automatically a natural isomorphism.
Proposition 1.2.46**.**
- (1)
If is a reflective subcategory of , then any two reflectors for are naturally isomorphic. 2. (2)
A dual statement holds for coreflective subcategories.
Proposition 1.2.47**.**
A functor is an equivalence if and only if there exists a functor such that and .
From the above result it is clear that every isomorphism of two categories is automatically an equivalence between them.
Bifunctors and endofunctors
Definition 1.2.48**.**
A bifunctor or functor of two variables is a functor whose domain is the product of two categories . In such case, then, is called a bifunctor from and to , and the situation is also denoted by
[TABLE]
where the first placeholder “” accepts objects and morphisms from , while the second placeholder does the same with .
Remark 1.2.49**.**
Given a bifunctor as above, fixation of one of its variables yields another (ordinary) functor. That is, assuming a fixed -object , we can derive another functor
[TABLE]
[TABLE]
Similarly, fixation of any -object yields another functor
[TABLE]
Famous examples of bifunctors include the following:
- •
The product bifunctor
[TABLE]
taking any to , and any to .
- •
The coproduct bifunctor
[TABLE]
taking any to , and any to .
- •
The hom functor
[TABLE]
on any small category ; this bifunctor takes any pair of objects to their “hom-set” , and its action on morphisms is defined by formulas
[TABLE]
and
[TABLE]
The restriction is called the covariant hom functor for every fixed , while the restriction is called the contravariant hom functor for every fixed . Specifically, when , is the exponential , i.e., the set of maps from to .
Furthermore, we will introduce two other famous bifunctors in Chapter 2: the tensor product and the internal hom. These two are fundamental to the theory of monoidal categories, and, in particular, -autonomous categories.
Definition 1.2.50**.**
Let be a category. An endofunctor on is a functor
[TABLE]
from to itself.
Endofunctors constitute the basis for the topic of universal dialgebra which we will introduce in Chapter 3.
Cartesian closed categories
Definition 1.2.51**.**
A category is called cartesian closed if it has finite products, and for each -object the functor is left adjoint (to some other functor).
Notation 1.2.52**.**
The right adjoint for the above functor is denoted by
, and is called the exponential. We call the objects power objects. For every , the member of the counit of the adjunction is denoted by and is called the evaluation (at ).
There is a natural isomorphism between the morphisms from a binary product
and the morphisms to an exponential object . There is a famous terminolgy for this bijective correspondence in the literature:
Notation 1.2.53**.**
Let be any two -objects. The bijection
[TABLE]
is called currying, while its inverse is called decurrying (or uncurrying). Beware, however, that the terms “currying” and “decurrying” are used in the even broader context of monoidal categories. We will be dealing with this issue in Chapter 2.
Binary products and pullbacks in CAT
Because of later usage in the study of (large) double cateogries, products and pullbacks in CAT deserve special attention. In this last part of the first section of the current chapter, we take a look at the precise formulations of products and pullbacks in CAT, the properly very large category of all large categories and functors between them.
Remark 1.2.54**.**
Since Cat is a full subcategory of CAT, the formulations to be given here apply to Cat as well.
CAT has binary products as well as pullbacks. The precise formulation of these two constructions goes as follows.
Binary products. For large categories , their product is a triple , where
- •
is the large category consisting of:
- –
objects: all pairs with and ,
- –
morphisms: all pairs , with in , and in ,
- –
composition: performed componentwise:
[TABLE]
and
- –
identities: pairs of an -identity together with a -identity ;
- •
and are the first and second projection functors, respectively.
The above product possesses a universal property, as described below.
The universality of binary product. For every diagram
[TABLE]
in CAT, there exists a unique functor making Diagram 1.3 commute.
The functor takes every -object to the pair ; also, it sends every -arrow to
[TABLE]
Pullbacks. Given any diagram
[TABLE]
in CAT, its pullback is the triple
[TABLE]
where
- •
is the large category consisting of:
- –
objects: all pairs with and such that
,
- –
morphisms: all pairs , with in , and in , such that ,
- –
composition: performed componentwise; for consecutive pairs of
-morphisms and we have
[TABLE]
hence we have
[TABLE]
as a valid composition for ;
- –
identities: pairs of an -identity together with a -identity ; again, we have ;
- •
and are the first and second projection functors, respectively.
The above pullback possesses a universal property, as described below.
The universality of pullback. For every commutative square
\mathcal{B}$$\mathcal{Q}$$\mathcal{A}$$\mathcal{C}$$\scriptstyle G$$\scriptstyle F$$\scriptstyle H$$\scriptstyle K
in CAT, there exists a unique functor making Diagram 1.4 commute. The functor takes every -object to the pair ; also, it sends every -arrow to
[TABLE]
1.3 Internal categories
In this section, we intend to generalize the very notion of “category” to that of internal category. Recall from Remark 1.2.5 that, of the two equivalent definitions of categories we introduced, the second definition (i.e., Definition 1.2.4) is preferred when studying internal categories. According to that definition, a category has a class of objects and a class of morphisms, together with two mappings
[TABLE]
which map an arrow, respectively, to its source and target.
Now suppose that we are given a category . By “defining an internal category in ” we mean a process of “emulating” the formalism of Definition 1.2.4 by using objects and morphisms taken from the category . The result of this process is, then, a structure that behaves much like an ordinary category. In order to achieve this goal, the category must possess certain objects and morphisms; in particular, besides other things, it must have an “object of objects”, an “object of morphisms”, two parallel “source” and “target” morphisms from the former object to the latter, and finally, pullbacks to be built on the source and target morphisms.
Since we will be frequently working with pullbacks, especially with arrows between pullbacks, it is necessary to be able to view the notion of pullback as a bifunctor. But this requires that we introduce the notion of slice category [34] firstly.
Definition 1.3.1**.**
Let be any (large/very large) category, and let be a -object. The (large/very large) slice category is defined as the category with the following data:
- •
Objects. The objects of are -morphisms with codomain .
- •
Morphisms. Given -objects and , a -morphism is a commutative triangle of :
A$$C$$B$$\scriptstyle g$$\scriptstyle h$$\scriptstyle f
We write .
- •
Composition. Composition is defined by pasting the triangles together, so the composition from is also the composite in .
- •
Identities. For any , the identity arrow in is also the identity arrow in .
Now we turn to pullbacks.
Proposition 1.3.2**.**
Let be a (large/very large) category, and let be an -object. Then, for any diagram
[TABLE]
in , the triple is a pullback in if and only if is the (binary) product of in the slice category .
Proposition 1.3.2 tells us that a pullback diagram in a category is essentially the same thing as the binary product of the corresponding arrows in the corresponding slice category. Therefore, we obtain the following useful result.
Proposition 1.3.3**.**
Suppose a (large/very large) category with pullbacks. Given any -object , there exists a bifunctor
[TABLE]
*taking any pair of -objects to the -object , where is the diagonal of the pullback diagram (see Diagram 1.5).
Moreover, the above functor sends any pair of -morphisms to the morphism , that is, the unique arrow making Diagram 1.6 commute.
Now that we are equipped with the above results, we can give the main definition of this section. The material below is mainly from Chapter 8 of [11].
Definition 1.3.4**.**
Let be a (large/very large) category with pullbacks. By an internal category in we mean a sextuple consisting of:
- (1)
an object , called the object of objects, 2. (2)
an object , called the object of arrows, 3. (3)
two morphisms s,t:B\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}A in , called, respectively, source and target, 4. (4)
an arrow in , called identity, 5. (5)
an arrow in , called composition, where the pullback is that of (Diagram 1.7).
These data must satisfy the following axioms:
- A1
(existence of “identity arrows”);
- A2
and (match-up of the target and source of composable pairs);
- A3
(identity property for identity arrows, see Remark 1.3.5 below), where the notation denotes the unique arrow to the pullback;
- A4
(associativity, see Remark 1.3.6 below).
Remark 1.3.5**.**
For Axiom A3, the equations
[TABLE]
imply existence of the arrows and , respectively.
Remark 1.3.6**.**
For Axiom A4, we have two isomorphic objects of “composable pairs”, namely and . The former is seen as the pullback of , while the latter is seen as the pullback of . Viewing the pullback as a bifunctor (Proposition 1.3.3), we find the following arrows in :
[TABLE]
[TABLE]
1.4 Monoidal Categories
In Section 1.2 we gave two equivalent definitions for categories. Then, we noted in Remark 1.2.5 that each of those definitions is used in some parts of the current work. Here we want to use the first one (Definition 1.2.2) as a ‘pattern’ and enter the topic of monoidal categories based on that. The material of this section is mainly from [12].
Definition 1.4.1**.**
A monoidal category consists of:
- (1)
a category ; 2. (2)
a bifunctor , called the tensor product. We write for the image under of the pair ; 3. (3)
an object , called the unit; 4. (4)
for every triple of objects an assoicator isomorphism
[TABLE]
natural in ; 5. (5)
for every object , a left unitor isomorphism
[TABLE]
natural in ; 6. (6)
for every object , a right unitor isomorphism
[TABLE]
natural in .
These data must satisfy the following requirements:
- (1)
Diagram 1.8 is commutative for every quadruple of objects (associativity coherence);
- (2)
Diagram 1.9 is commutative for every pair (unit coherence).
Remark 1.4.2**.**
Usually, the tensor product is denoted by “” in the literature. However, as we will be dealing with two kinds of tensors in the sequel (one for a base monoidal category and one for the Chu construction over ), for the sake of clarity of expressions, we prefer to preserve “” exclusively for the tensor product of the Chu construction and use “” for monoidal categories in general.
Definition 1.4.3**.**
With the notation as above, a monoidal category is symmetric when, moreover, an isomorphism
[TABLE]
is given for every pair of objects, natural in . These isomorphisms must be such that:
- (1)
Diagram 1.10 is commutative for every triple of objects (associativity coherence with symmetry);
- (2)
Diagram 1.11 is commutative for every object (unit coherence with symmetry);
- (3)
Diagram 1.12 is commutative for every pair (the symmetry axiom).
Definition 1.4.4**.**
With the notation as above, a monoidal category is called biclosed when for each object , both functors
[TABLE]
have right adjoints.
Definition 1.4.5**.**
A biclosed symmetric monoidal category is called a closed symmetric monoidal category (CSMC).
Since in a symmetric monoidal category both functors and are naturally isomorphic, thus one obviously has:
Proposition 1.4.6**.**
The following are equivalent for a symmetric monoidal category :
- (a)
* is a CSMC;*
- (b)
for each object , the functor has a right adjoint;
- (c)
for each object , the functor has a right adjoint.
The following is an important example of a CSMC.
Definition 1.4.7**.**
A category is cartesian closed when it admits all finite products and, for every object , the functor has a right adjoint, generally written .
Proposition 1.4.8**.**
Every cartesian closed category is a CSMC, with the cartesian product as the tensor product.
Proof.
Existence of the required natural isomorphisms and the various coherence conditions follows immediately from the universal property of the product. The tensor unit is just the terminal object.
Notation 1.4.9**.**
When is a CSMC, we write
[TABLE]
for the right adjoint to the functor . In particular, the isomorphisms
[TABLE]
yield a “unit” morphism , corresponding with the identity on . In an analogous way the isomorphisms
[TABLE]
yield a morphism
[TABLE]
corresponding with the identity on . It is also useful to consider the (counit) “evaluation morphisms”
[TABLE]
corresponding by adjunction with the identity on , and the “composition morphisms”
[TABLE]
corresponding by adjunction with the composite of Diagram 1.13:
Proposition 1.4.10**.**
On a CSMC we get a bifunctor
[TABLE]
*called the internal hom bifunctor on , whose composite with the hom functor
is just*
[TABLE]
Proof. Given in , the arrow corresponds by adjunction with the composite
[TABLE]
It is routine to check the bi-functoriality of .
On the other hand, the isomorphisms
[TABLE]
prove the second assertion.
Proposition 1.4.11**.**
In a closed symmetric monoidal category :
- (1)
the morphisms are natural in ; 2. (2)
the morphisms are isomorphisms; 3. (3)
the morphisms are natural in ; 4. (4)
for all , Diagrams 1.14 and 1.15 commute.
Proof. The inverse of the morphism is the composite
[TABLE]
The rest of the proof is routine computations.
There are also two other important concepts when dealing with monoidal categories: namely “monoidal functor” and “monoidal transformation” [29, 65].
Definition 1.4.12**.**
Let and be monoidal categories. A lax monoidal functor (or weak monoidal functor) between them is:
- (1)
a functor
[TABLE] 2. (2)
a morphism
[TABLE] 3. (3)
a natural transformation
[TABLE]
for all , satisfying the following conditions:
- (a)
(Associativity) For all objects Diagram 1.16 commutes.
In this diagram, and denote the associators of the respective monoidal categories.
- (b)
(Unitality) For all , Diagrams 1.17 and 1.18 commute, where denote the left and right unitors of the two monoidal categories, respectively.
Definition 1.4.13**.**
If and all in Definition 1.4.12 are isomorphisms, then is called a monoidal functor.
Definition 1.4.14**.**
A monoidal transformation between monoidal functors is a natural transformation that respects the extra structure in an obvious way.
This way, we arrive at the end of Chapter 1. In the next chapter we will introduce the Chu construction.
Chapter 2 The Chu Construction
In Section 1.1 we pointed to the historical roots of the Chu construction. Now, we introduce the precise formalism of the Chu construction in this chapter.
We start with -autonomous categories; next, we will introduce the general form of the Chu construction. We will show that for every CSMC such as , categories are the coreflective and reflective subcategories of , respectively (see Proposition 2.2.3). Additionally, we will prove that if is bicomplete then so is for any (Proposition 2.2.4).
Next, we will focus on the Chu construction on sets (Section 2.3) and will study some of its important properties. Particularly, we will point to extensional, separable, and biextensional Chu spaces (Subsection 2.3.1); we will show that is balanced (Proposition 2.3.12); we will introduce the multiplicative as well as additive connectives of linear logic by the Chu construction (Subsection 2.3.2); we will have a look at “realizations” in Chu (Subsection 2.3.3); and finally, we will study endofunctors on Chu (Subsection 2.3.4) and will show that from every endofunctor , one can obtain an endofunctor (at least in two ways).
2.1 -Autonomous categories
Now we are at the position to introduce the notion of “-autonomous category” [7, 66]. There are two equivalent definitions for it; we choose one and prove the other as an equivalent property for such categories.
Definition 2.1.1**.**
Let be a CSMC. is said to be -autonomous (read “star-autonomous”) if it has a dualizing object: an object such that the canonical morphism
[TABLE]
which is the transpose of the evaluation map
[TABLE]
is an isomorphism for all .
Proposition 2.1.2**.**
A closed symmetric monoidal category is -autonomous if and only if it is equipped with a full and faithful functor
[TABLE]
such that there is a natural isomorphism
[TABLE]
The functor is called the dualization functor, and is said to be the dual of for any object .
Proof. () Define the dualization functor as the internal hom to the dualizing object:
[TABLE]
Then the morphism is natural in , so that there is a natural isomorphism
[TABLE]
We also have
[TABLE]
This yields the desired result.
() Conversely, define the object as the dual of the tensor unit:
[TABLE]
From Proposition 2.1.2 it follows that:
Corollary 2.1.3**.**
Every -autonomous category is self-dual.
Proposition 2.1.4**.**
The following hold for every pair of objects in a -autonomous category :
[TABLE]
Proof. We know that there is an adjunction
[TABLE]
for every . Thus, to prove the left hand side isomorphism, it suffices to show that the functor
[TABLE]
is right adjoint to . By Proposition 2.1.2 we find the natural isomorphisms
[TABLE]
for all . Therefore, , and by uniqueness,
[TABLE]
The other isomorphism is dual to the first one.
Remark 2.1.5**.**
For a -autonomous category , whenever there is a natural isomorphism
[TABLE]
the category is called a compact closed category. Putting in the above isomorphisms we find out that in compact closed categories we always have , i.e., the tensor unit is the same thing as the dualizing object. A standard example is , the category of finite-dimensional vector spaces over some field together with the usual tensor product, in which the field itself plays the roles of the tensor unit and the dualizing object simultaneously. This type of categories will be of little interest in the present work.
Definition 2.1.6**.**
Conversely, if a -autonomous category is not compact closed, then the tensor product induces another bifunctor
[TABLE]
called the par operation, making into a linearly distributive category. From the definition of par it is clear that is a symmetric operation: . For more information on linearly distributive categories, the reader is referred to [64] and the references therein. In the present thesis, it is this type of -autonomous categories that we mainly work with; more precisely, we will be working with the Chu construction (see Sections 2.2 and 2.3).
Note that the par operation is often (but not always) denoted by some special symbol in the literature, namely an upside-down ampersand “
&
”, which is borrowed from linear logic. However, this symbol is difficult to work with–both in handwriting and in typesetting–and so we do not use it here.
Remark 2.1.7**.**
It is noteworthy that in a -autonomous category, seen as a linearly distributive category, we have two different monoidal structures and .
Another important aspect of -autonomous categories is their internal logic. The internal logic of -autonomous categories is the multiplicative fragment of classical linear logic; conversely, -autonomous categories are the categorical semantics of classical linear logic (Proposition 1.5 in [55]). In the sequel, we will have brief looks at the basic operations of classical linear logic based on an important family of -autonomous categories: the categories of the form (see 2.3.2). For more information on topics of internal logic and categorical semantics, see [35].
2.2 The Chu construction
The Chu construction is a general method for constructing a -autonomous category from a given CSMC [8, 9, 68]. It is named after Po-Hsiang Chu, a student of Michael Barr, who introduced the construction in his master’s thesis at McGill University. The formalism has been extensively studied by Pratt and others ([17, 45, 46, 47, 48, 49, 61]) for its potential applications in theoretical computer science.
Definition 2.2.1**.**
Let be a CSMC with pullbacks, and let be an object of . We define a category , called the Chu construction (or the Chu category) over with the following data:
- •
Objects: triples , called Chu objects or Chu spaces, where are -objects, and is a morphism of .
- •
Morphisms: pairs , called Chu morphisms or Chu transforms, where and are -morphisms making Diagram 2.1 commute. This is called the adjointness condition for .
- •
For objects and morphisms , the composition of and is defined as
[TABLE]
which satisfies the adjointness condition and, hence, is a Chu transform. To see this, observe that in Diagram 2.2, all the triangles and inner quadrilaterals commute and consequently, the outer quadrilateral commutes.
- •
Identity morphisms for every are defined the obvious way:
[TABLE]
- •
Finally, one can readily verify that the composition so defined is associative (up to natural isomorphism).
Now we show the -autonomous structure of the Chu construction:
Proposition 2.2.2**.**
Let be a CSMC with pullbacks, and let be an object of .Then the Chu construction is -autonomous. In particular, it is self-dual.
Proof.
There is an evident self-duality
[TABLE]
which takes an object to
[TABLE]
where is the “transpose” of . On morphisms, it takes a pair to . Now it immediately follows that
\textup{{Chu}}(\mathcal{V},\Gamma)^{\textup{op}}$$\textup{{Chu}}(\mathcal{V},\Gamma)$$\scriptstyle(-)^{*}$$\scriptstyle((-)^{*})^{\textup{op}}
is an isomorphism of categories.
Next, we define a tensor and an internal hom on and show that these make the Chu construction into a CSMC. Then, using the self-duality functor defined above, we deduce the -autonomous structure of .
Define the Chu object
[TABLE]
where is an instance of the left unitor isomorphism. Also, denote the dual of by
[TABLE]
where is the transpose of .
For Chu objects , define the -object as the following pullback:
B^{A}$$H$$X^{Y}$$\Gamma^{A\boxtimes Y}$$\scriptstyle\dot{r}$$\scriptstyle\dot{s}
where the exponentials are used to denote the internal homs in , is the result of currying to and then exponentiating by , and similarly for . There is a map
[TABLE]
obtained by decurrying either leg of the above pullback; so, define
[TABLE]
Now define the internal hom .
To form the tensor product , we use the formula
[TABLE]
as was stated and proved in Proposition 2.1.4. Therefore we define
[TABLE]
where the third component is a pullback, and the pairing is obvious. There are three things to be checked:
- (1)
the presence of a canonical isomorphism
[TABLE]
for every ; 2. (2)
verifying that is indeed the tensor unit:
[TABLE] 3. (3)
verifying that is indeed the dualizing object:
[TABLE]
Proposition 2.2.3**.**
The category is a coreflective subcategory of , while is a reflective subcategory of .
Proof. There is a strong monoidal functor
[TABLE]
taking every -object to , where . (Note that this does NOT take to the dualizing object in , unless of course the canonical morphism is an isomorphism.) This embedding admits a right adjoint
[TABLE]
given by the obvious projection, which is also strong monoidal. The unit of the adjunction is an isomorphism, hence is a coreflective (full) subcategory of .
On the other hand, is self-dual, hence also embeds as a full subcategory of , this time reflectively.
Another fundamental property of the Chu construction is expressed the next proposition:
Proposition 2.2.4**.**
If is bicomplete, then so is . The formula for the colimits is the obvious one:
[TABLE]
where is the decurrying of
[TABLE]
and the formula for limits is obtained by dualizing the formula for colimits in .
Proof. Given bicomplete , it suffices to show that the above formula indeed gives the colimits in . By self-duality of , then, a dual formula for limits follows automatically.
Let be an arbitrary diagram in , where is a small category, and let be a family of arrows in for indices . We have two families of -morphisms and . Take the colimit of the former and the limit of the latter. Since is the colimit of , is the limit of . For every , the -arrow has a transpose . Thus, is a cone over and hence, there exists a unique arrow such that the following square commutes:
\Gamma^{C}$$L$$X_{j}$$\Gamma^{A_{j}}$$\scriptstyle s$$\scriptstyle l_{j}$$\scriptstyle\tilde{r}_{j}$$\scriptstyle\Gamma^{c_{j}}
Define the -morphism as the adjoint transpose of , and form the Chu object . Transpose the above square to obtain the following commutative square:
C\boxtimes L$$A_{j}\boxtimes L$$A_{j}\boxtimes X_{j}$$\Gamma$$\scriptstyle c_{j}\boxtimes 1$$\scriptstyle 1\boxtimes l_{j}$$\scriptstyle r_{j}$$\scriptstyle r
which proves the adjointness condition for the pair . Whence, we have a Chu morphism for all . On the other hand, for every the following hold:
[TABLE]
Therefore,
[TABLE]
and is a cocone under in . It is straightforward to check the universality of this cocone. We have thus found the desired colimit diagram for .
2.3 The Chu construction on the category of sets
The category Set of sets and functions is well-known in mathematics. Regarding its properties, one may deduce that Set is a very good candidate for serving as the base category in the Chu construction. Thus, we introduce:
Notation 2.3.1**.**
Putting in Definition 2.2.1 and considering a nonempty set , we arrive at a category
[TABLE]
which we denote by . Whenever is clear from the context, we will omit it and denote our category by Chu.
Therefore, Chu is a -autonomous category with the following data:
- •
objects: Chu spaces with sets, and a map;
- •
morphisms: Chu transforms with maps satisfying the adjointness condition.
It is useful to mention that for Chu spaces and a Chu transform , the (diagrammatic) adjointness condition
A\times X$$A\times Y$$B\times Y$$\Gamma$$\scriptstyle 1_{A}\times f^{-}$$\scriptstyle f^{+}\times 1_{Y}$$\scriptstyle s$$\scriptstyle r
can be restated in terms of memberships as:
[TABLE]
which is sometimes more convenient to use.
From Propositions 2.2.3 and 2.2.4 we deduce:
Corollary 2.3.2**.**
For every nonempty set , the category Set is a coreflective (full) subcategory of , while is a reflective subcategory of .
Corollary 2.3.3**.**
For every nonempty set , the category is bicomplete. The formula for colimits in is
[TABLE]
where denote the coproduct and product in Set, respectively, and is the decurrying of
[TABLE]
A dual formula exists for the case of limits, also.
Proof. Set is bicomplete, and becomes bicomplete by Proposition 2.2.4.
There are interesting applications of Chu spaces in the literature. For example, Abramsky [1] views the Hilbert space of quantum mechanics as a Chu space. Also, Papadopoulos and Syropoulos [42] study fuzzy sets and fuzzy relational structures as Chu spaces.
2.3.1 Extensional, separable, and biextensional Chu spaces
Fix some nonempty set . In this subsection we discuss some additional properties of .
Definition 2.3.4**.**
For a Chu space , the set is called the carrier of while the set is called the cocarrier of . Also, the map is called the matrix of . For arbitrary we have the functions
[TABLE]
and
[TABLE]
with obvious formulas, which are called a row and a column (of ), respectively.
In other words, is a matrix whose rows are indexed by elements of , whose columns are indexed by elements of , and whose entries are -elements. It is interesting to note that this way, the dual Chu space of is , where the matrix is just the matrix transpose of defined by the formula . Especially, note that , that is, the dualization functor on Chu is an involution. Hence the name “transpose” is justified.
Definition 2.3.5**.**
A Chu space is called extensional if for every ,
[TABLE]
(i.e., no repeated columns in ). Dually, is called separable if for every ,
[TABLE]
(i.e., no repeated rows). Also, is called biextensional if it is both extensional and separable.
Notation 2.3.6**.**
We write for the full subcategories of determined by the extensional, separable, and biextensional Chu spaces, respectively.
Definition 2.3.7**.**
For a given Chu space , we define the equivalence relations on and on as follows:
[TABLE]
These are evidently equivalence relations. is exactly when is the identity. Likewise, is separable exactly when is the identity. Finally, is biextensional exactly when both relations are the identities. There are Chu transforms
[TABLE]
and
[TABLE]
and
[TABLE]
where are the quotient maps for , respectively. The Chu space
[TABLE]
is called the biextensional collapse of . We denote this Chu space by the lowercase letter .
Proposition 2.3.8**.**
Every Chu transform between Chu spaces induces a Chu transform
[TABLE]
in a canonical manner.
Proof. What we have to show is that there is a pair of functions and that satisfy the adjointness condition. This pair of functions can be found via the following.
For , define ; also, for define . We claim that these two definitions are well-defined. We prove our claim for the first one, and the proof for the second one will be similar.
Assume for some ; then we have
[TABLE]
Now let be arbitrary. Thus, and
[TABLE]
but from the adjointness condition for the Chu morphism ,
[TABLE]
and since was arbitrary, we have
[TABLE]
or
[TABLE]
and we are done.
It remains to show the adjointness of :
[TABLE]
and the proof is complete.
Corollary 2.3.9**.**
Biextensional collapses and biextensional morphisms form a category.
This category is denoted by chu (the “small Chu”), and the functor indeuced by Proposition 2.3.8 is denoted by (the biextensional collapse functor).
Next, we have [18]:
Proposition 2.3.10**.**
Suppose are Chu transforms. Then
- (1)
if is extensional, then implies ; 2. (2)
if is separable, then implies ; 3. (3)
if are biextensional, then if and only if .
Thus, the forward and backward components in a morphism determine each other uniquely in the category bChu. [Bif]
Proof. Let us write and . First we show (1). Suppose is extensional and . Then, for all and all we have
[TABLE]
Hence by extensionality of . Now (2) follows by dualization, and (1) and (2) together imply (3).
In the next step we take a look at monics and epics [18]:
Proposition 2.3.11**.**
We have:
- (1)
A morphism in Chu is monic if and only if is injective and is surjective. 2. (2)
A morphism in eChu is monic if and only if is injective. 3. (3)
A morphism in bChu is monic if and only if is injective. 4. (4)
Suppose is a morphism in Chu and is extensional. If is surjective, then is injective. 5. (5)
A morphism in Chu is epic if and only if is surjective and is injective. 6. (6)
A morphism in sChu is epic if and only if is surjective. 7. (7)
A morphism in bChu is epic if and only if is surjective. 8. (8)
Suppose is a morphism in Chu and is separable. If is injective, then is surjective.
Proof. (1) The “If” part is obvious. We check the “Only If” part. Suppose is such that for any pair of morphisms , if , then . We show that is injective and is surjective. Assume .
Firstly, we show that is surjective. Suppose otherwise. Choose two sets of the same cardinality as the cardinality of , in a way that be pairwise disjoint. Put . For , choose a bijection and let be the joint extension of the identity and of . For , let
[TABLE]
Let . Then are Chu morphisms from to . Indeed,
[TABLE]
if , and
[TABLE]
also, if . Moreover, yield the same composition with because behave the same on the image set . Now being monic implies that , a contradiction since . Hence . Note that for this construction to work, cannot be required to be extensional.
The proof for the injectivity of is the same as the “Only If” part for item (2), given next.
(2) and (3) “If”. Let be a Chu transform and be injective. Consider two arrows , which yield the same compositions with . Then since is injective. By Proposition 2.3.10 we have . Whence, is monic.
“Only If”. Let be monic and write . Assume are such that . Construct a Chu space as follows. Let be a singleton, and . Also, let for every . Clearly, is biextensional.
Now define as follows. Let . For , put
. Then, g_{1},g_{2}:\mathsf{C\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}A} are Chu transforms. Clearly, . We claim that , also. Indeed, if and , then
[TABLE]
Hence, g_{1},g_{2}:\mathsf{C\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}A} yield the same compositions with . Since is monic, it follows that . Thus, , and is injective.
Let with , say. Choose any and then with . Then, . Then, by extensionality.
Parts (5)–(8) are duals to parts (1)–(4), respectively.
We also have the following remarkable property:
Proposition 2.3.12**.**
The category Chu is balanced.
Proof. Let , and let be a monic epic Chu transform. By Proposition 2.3.11 parts (1), (5) we find that must be an injective surjective map, i.e., a bijective map. Similarly, must be bijective.
Consider the pair of functions . We claim that is a Chu transform. If either of or is empty then our claim holds trivially. Thus, assume that . Let . Since both and are bijective, there exist unique elements with
[TABLE]
From the adjointness condition for we have
[TABLE]
or
[TABLE]
Since were arbitrary, we find
[TABLE]
Therefore, is a Chu transform satisfying
[TABLE]
2.3.2 Linear logic in Chu
Barr proposed the Chu construction as a source of constructive models of linear logic [7, 45]. The case is particularly important for its combination of simplicity and generality. The latter case was first treated by Lafont and Streicher [45]. Here, we list a number of endofunctors that yield the main operations used in linear logic. We have already defined most of them in the previous sections. Below, are Chu spaces and are Chu transforms.
a. Multiplicative connectives:
These include the duality, tensor, linear implication, and par operations, together with their special objects, namely the tensor unit and perp.
a1. Duality. The duality functor
[TABLE]
which is sometimes referred to as the perp functor and denoted by , gives the dualization operation which is “involutive”: .
a2. Tensor. From Proposition 2.2.2, the tensor product on Chu is found to be
[TABLE]
[TABLE]
where the cocarrier is the pullback depicted in Diagram 2.3,
and the matrix is defined the obvious way:
[TABLE]
On the other hand, its effect on morphisms can be described as:
[TABLE]
with
[TABLE]
and
[TABLE]
a3. Tensor unit. The tensor unit is
[TABLE]
with the singleton, and for every .
a4. Linear implication. This is exactly the internal hom bifunctor
[TABLE]
Using the equation (equation since the dualization on Chu is actually an involution), we find
[TABLE]
with
[TABLE]
On the other hand, for we have:
[TABLE]
with
[TABLE]
and
[TABLE]
[TABLE]
a5. Dualizing object. The dualizing object is
[TABLE]
with for all .
a6. Par. The par bifunctor is the De Morgan dual to :
[TABLE]
On objects,
[TABLE]
where
[TABLE]
On morphisms ,
[TABLE]
with
[TABLE]
and
[TABLE]
[TABLE]
b. Additive connectives
These include the plus and with connectives, together with their respective units.
b1. Plus. Plus is the binary coproduct bifunctor
[TABLE]
[TABLE]
On objects:
[TABLE]
where is the coproduct (disjoint union) of the sets ; also
[TABLE]
[TABLE]
On morphisms ,
[TABLE]
[TABLE]
b2. Plus unit. Defined as:
[TABLE]
where is the unique empty matrix. [math] has the property that
[TABLE]
b3. With. This is the binary product bifunctor
[TABLE]
[TABLE]
which is the De Morgan dual to plus:
[TABLE]
On objects we have
[TABLE]
so that
[TABLE]
[TABLE]
On morphisms ,
[TABLE]
[TABLE]
b4. With unit. Defined as
[TABLE]
where is again the unique empty matrix. We have
[TABLE]
c. Other connectives
Although Chu is not cartesian closed, one can still define some sort of “exponential” on cartesian closed retractions of this category. The exponential serves syntactically to “loosen up” formulas so that they can be “duplicated” or “deleted”. For more information on this subject, see [45].
2.3.3 Realizations
The notion of realization we intend here is the strong version defined by Pultr and Trnková [45].
Definition 2.3.13**.**
A Chu space is called normal whenever and for every . For normal Chu spaces, the matrix is clearly understood from the context and therefore, the normal Chu space is abbreviated as . A normal Chu transform is a Chu transform between two normal Chu spaces. Normal spaces and normal transforms form a full subcategory of .
Definition 2.3.14**.**
A functor is a representation of objects by objects when is a full embedding (see Definition 1.2.25 and Proposition 1.2.26).
Definition 2.3.15**.**
A representation is a realization when in addition,
[TABLE]
where and are the corresponding underlying-set functors.
The above realization in called a Chu realization when , and is called a normal Chu realization if (where nChu abbreviates ).
Remark 2.3.16**.**
It is clear that every realization is a concrete functor (see Chapter 1).
Pratt [45, 47] discusses many normal Chu realizations including the realizations of sets, pointed sets, preorders, topological spaces, semilattices, distributive lattices, Boolean algebras, etc. Because of their importance in illuminating the power of the Chu construction, we sketch two examples here, namely the cases of sets and topological spaces.
Using the conventions we have:
Theorem 2.3.17**.**
Set* is normally realized in .*
This realization is in fact trivial: any set is realized as the (normal) Chu space , and any function is realized as the (normal) Chu transform , where “” is the unique map , doing the double duty of the empty matrix (in ) as well as the empty map (in ). Note that the composition yields the (strong monoidal) functor introduced in Proposition 2.2.3.
Theorem 2.3.18**.**
A topological space can be viewed as an extensional normal Chu space in , whose columns are closed under arbitrary union and finite intersection. The normal Chu transforms between topological spaces are exactly the continuous functions between the corresponding topological spaces.
Theorem 2.3.18 tells us that normal Chu spaces and transforms (in ) can in fact be regarded as some generalization of topological spaces and continuous functions, a generalization in which the conditions of open sets being closed under arbitrary unions and finite intersections are removed.
Also:
Theorem 2.3.19**.**
Assuming the Generalized Continuum Hypothesis, is realizable in if and only if .
Another notable realization in Pratt’s work is the normal Chu realization of relational structures:
Theorem 2.3.20**.**
Any full subcategory of the category of n-ary relational structures and their homomorphisms is realized in .
Consequently, for example, we have the next corollary:
Corollary 2.3.21**.**
- (1)
The category Grp of groups and group homomorphisms is realized in . 2. (2)
The category TopGrp of topological groups and continuous group homomorphisms is realized in .
Also we have:
Theorem 2.3.22**.**
The following functor realizes the category of vector spaces over a field in the category , where denotes the underlying set of :
[TABLE]
in which is the dual map to in , and the map (the evaluation) is defined as for .
Finally, we mention a remarkable result Pratt has given in […]:
Theorem 2.3.23**.**
Every small concrete category embeds fully in , where is the number of arrows of .
2.3.4 Chu endofunctors
Because of their fundamental roles in universal dialgebra (Chapter 3) and later in the construction (Chapter 4), Chu endofunctors deserve special attention. This subsection is meant to provide for a minimum necessary treatment of the issue.
First of all, following Proposition 2.2.3, we introduce a notation that will play a key role in the current thesis:
Notation 2.3.24**.**
Let be a CSMC, and let be an endofunctor on . Also, let and be the projection functors deduced in the proof of Proposition 2.2.3. We use the following notations in the sequel:
[TABLE]
In particular, when , we have the functors and
for any given Chu endofunctor .
Secondly, we introduce an important notion in the next definition:
Definition 2.3.25**.**
Let be an endofunctor on Set. Let be a nonempty set. An uplifting of is a Chu endofunctor that makes Diagram 2.4 commute. In the diagram, the functor is the same as in Notation 2.3.24.
In other words, for an uplifting we have . The following theorem demonstrates the usefulness of the notion of uplifting.
Theorem 2.3.26**.**
Assume a nonempty set . Then, every endofunctor can be uplifted to a Chu endofunctor
[TABLE]
Moreover, this uplifting can be done at least in two different ways.
Proof. Fix a nonempty . Consider the endofunctor
. We construct two distinct upliftings of .
The first construction. Define
[TABLE]
is a well-defined functor because:
[TABLE]
also, for all consecutive arrows in Chu,
[TABLE]
Now, for any Chu space ,
[TABLE]
and for any Chu transform ,
[TABLE]
Therefore, is an uplifting of .
The second construction. Since is nonempty, there is some element . Let denote the singleton. Define
[TABLE]
Again, is a well-defined functor: firstly, for every Chu transform , the pair
obviously satisfies the adjointness condition, and so, is a valid Chu morphism; also,
[TABLE]
on the other hand, for all consecutive arrows in Chu,
[TABLE]
Now, for any Chu space ,
[TABLE]
and for any Chu transform ,
[TABLE]
Therefore, is another uplifting of .
Finally, it is clear that , and we are done.
Remark 2.3.27**.**
In general, a set endofunctor may have many upliftings, quite different in structure and behavior. As a remarkable example, consider the endofunctor for some fixed set with at least two distinct elements. This functor has at least the following upliftings:
- •
either of the constructions given in the proof of Theorem 2.3.26;
- •
the functor for some nontrivial ; and
- •
the functor , again, for some nontrivial .
In addition to the notion of uplifting, it is good to point to the following notion:
Definition 2.3.28**.**
Let and be endofunctors on Set. Let be a nonempty set. A bi-uplifting of is a Chu endofunctor that makes both squares in Diagram 2.5 commute. In the diagram, the functors are the same as in Notation 2.3.24.
Every bi-uplifting of set functors is clearly an uplifting of , also. On the other hand, as an example of a non-trivial bi-uplifting when and with a given set functor, see Definition 13 of [41] (termed “-lifting” therein). In general, characterization of bi-upliftings for arbitrary and arbitrary pairs of set functors may be an interesting subject of study by itself.
In the next chapter, we will introduce the basics of universal dialgebra, with special attention to the theory of universal dialgebra on the Chu construction.
Chapter 3 Universal Dialgebra
In Section 1.1 of Chapter 1 we discussed the historical origins of universal dialgebra. Now we proceed towards its formalism. Our approach here slightly generalizes that of [56]; that is, we study universal dialgbera not on Set but on a given (bicomplete) category . We will study isomorphisms and bisimulations in (Section 3.2); and we will take a look at limits and colimits in the latter category (Section 3.3). After that, we will pay attention to the problem of dualization (Section 3.4) which we mentioned in Chapter 1. Finally, we will specifically focus on universal dialgebra on Chu (Section 3.5).
3.1 Basic notions
Many of the familiar structures in mathematics can be expressed in terms of “-algebras” and/or “-coalgebras”, in which are set functors. As a few examples:
- •
a semigroup may be viewed as an -algebra of the form in which ;
- •
a partial function may be viewed as a -coalgebra of the form where .
On the other hand, the above examples can also be viewed as “-dialgebras” such that are again set functors (assuming for the first example and for the second). As a non-trivial example of -dialgebras, one may take a field
[TABLE]
This is an -dialgebra for some non-identity set functors .
In addition to the above, one may think of generalized -dialgebras for endofunctors
[TABLE]
where is an arbitrary category. In the following, we study such formalisms.
Definition 3.1.1**.**
Let be a category. Let F,G:\mathcal{C}\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}\mathcal{C} be two endofunctors on . An -dialgebra is a pair consisting of a -object , together with a -morphism . Whenever the functors are clear from the context, we may simply refer to as a “dialgebra”.
Definition 3.1.2**.**
Let be two -dialgebras. An
-dialgebra homomorphism is a -arrow making Diagram 3.1 commute.
Remark 3.1.3**.**
The arrow is called the stem of the arrow , or equivalently, one may say that the homomorphism stems from (via ). Yet another equivalent statement is that yields a homomorphism (via ). We use boldface characters to represent the corresponding homomorphisms of the stems.
Identity homomorphisms are -dialgebra homomorphisms and, given two dialgebra homomorphisms and , the composition yields a dialgebra homomorphism (Diagram 3.2). This composition is clearly associative, also. Therefore:
Proposition 3.1.4**.**
Given endofunctors F,G:\mathcal{C\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}C} on some category , -dialgebras together with -dialgebra homomorphisms form a category.
Notation 3.1.5**.**
This category is denoted by . We may refer to as the base category for . To simplify notation for special cases, let and .
Remark 3.1.6**.**
is essentially the same thing as the category of -algebras over while is just the category of -coalgebras over . This way, universal algebra and universal coalgebra may be viewed as two special cases of universal dialgebra.
The reader may refer to [10, 33, 40, 44, 56] for various examples of categories of dialgebras. For algebras and coalgebras, references [13, 16, 24, 27, 28, 53] are suggested. Also, Abramsky [2] gives an interesting example of connections between coalgebras and the Chu construction. Chang and Keisler [14] point to the connection between universal algebra and model theory. Pavlović and Pratt [43] introduce the continuum of real numbers as a final coalgebra (i.e. as a terminal object in the category of coalgebras). Gumm [25] studies functors for coalgebras. Moss [37] studies coalgebraic logic. Palmigiano [40] introduces abstract logics as dialgebras. Martins et al [33] suggest dialgebras as appropriate models for computational processes which are combinations of “algebraic construction” and “coalgebraic observation”. Finally, Rodrigues [52] develops a dialgebraic theory over the category Rel (the category of sets and binary relations).
3.2 Isomorphisms and bisimulations
In this section, is a fixed category and are two fixed -endofunctors.
Definition 3.2.1**.**
A dialgebra homomorphism is called a dialgebra isomorphism if it is an isomorphism arrow in the category .
The following proposition shows that the existence of an inverse homomorphism is equivalent to the existence of an inverse for the stem.
Proposition 3.2.2**.**
- (1)
If is an isomorphism in , then its stem is an isomorphism in . 2. (2)
Conversely, if has an inverse , then yields a dialgebra homomorphism such that . That is, is a dialgebra isomorphism.
Therefore, a dialgebra homomorphism is a dialgebra isomorphism if and only if its stem is an isomorphism arrow in the corresponding base category.
Proof. (1) is obvious. We only prove (2):
Consider
GA$$FA$$FB$$GB$$A$$B$$\scriptstyle\alpha$$\scriptstyle\beta$$\scriptstyle h$$\scriptstyle k$$\scriptstyle Fh$$\scriptstyle Fk$$\scriptstyle Gh$$\scriptstyle Gk
We have ; thus
[TABLE]
Therefore, is a homomorphism, and clearly, .
Definition 3.2.3**.**
A homomorphism is called a (dialgebra) monomorphism if it is a monic arrow in , i.e., if for every dialgebra and all homomorphisms \mathbf{f,g:C\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}A},
[TABLE]
Dually, is said to be an(a) (dialgebra) epimorphism whenever is an epic arrow in .
Proposition 3.2.4**.**
- (1)
Every dialgebra homomorphism stemming from a monic arrow is monic. 2. (2)
Dually, every dialgebra homomorphism stemming from an epic arrow is epic.
Proof. (1) For a homomorphism with monic stem , the equality for some homomorphisms implies , hence , and consequently .
Remark 3.2.5**.**
Contrary to the case of Proposition 3.2.2, the converse statements for Proposition 3.2.4 are false: there are counterexamples monomorphisms (epimorphisms) for which the stem is not a monic (epic) arrow in the base category . For instance, take the category of rings, where is the correponding endofunctor. Here we have an epimorphism ; however, its stem is the inclusion map which is obviously not surjective (hence not epic) in Set.
Definition 3.2.6**.**
A homomorphism is called a (dialgebra) section provided that it is a section arrow in , i.e., if there exists a homomorphism with .
Dually, is a (dialgebra) retraction if it is a retraction arrow in , that is, if there exists with .
Proposition 3.2.7**.**
- (1)
If is a section (retraction) in , then its stem is also a section (retraction) in . 2. (2)
If is a -arrow that makes a section (retraction), and if a homomorphism stems from , then the homomorphism is a section (retraction) as well.
Definition 3.2.8**.**
A dialgebra is called a subdialgebra of a dialgebra if there exists a homomorphism that stems from a monic . By Proposition 3.2.4 (1) we know that such must be a dialgebra monomorphism.
Dually, is called a quotient dialgebra of provided that there exists a homomorphism such that its stem is epic. Again, from Proposition 3.2.4 (2) we know that such is necessarily a dialgebra epimorphism.
Now we turn to the fundamental concept of “bisimulation” for dialgebras. In [56], the concept was defined and investigated for the case . Here, we generalize the concept for categories with finite products, possibly non-cartesian-closed cases. Before proceeding we need a categorical definition of the concept of “reltion”. The following material is a generalization of what can be found in [12].
Definition 3.2.9**.**
Let be a category. By a relation between objects we mean an object together with a pair of arrows
[TABLE]
which form a monomorphic pair of arrows, that is, given an object and parallel arrows f,g:X\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}R,
[TABLE]
For every object we write
[TABLE]
which is a relation in the usual sense (i.e. set-theoretic), and call it the corresponding relation between and . Also, by a relation on we mean a relation between and itself.
Recall that an ordinary (set-thoretic) relation between sets was defined as a subset of the (cartesian) product of and . In category-theoretic terms, this might be expressed as an injective arrow in the category Set. The following proposition generalizes this idea to categories with finite products:
Proposition 3.2.10**.**
Let be a category with finite products, and let . Then, every relation between can be viewed as a monic arrow
[TABLE]
and vice versa.
Proof. () Let be the product of and . Then by universality of the product, there exists a unique arrow such that
[TABLE]
To see being monic, assume parallel arrows f,g:X\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}R with . Then
[TABLE]
or
[TABLE]
for . But since are a monomorphic pair of arrows, we have .
() Conversely, assume that the product and a mono are given. Define for each . For any parallel pair f,g:X\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}R, the equalities imply
[TABLE]
Since is itself a relation between , (because form a monomorphic family), we must have
[TABLE]
By hypothesis, is monic; thus .
Given a relation on an object of some category , it is now possible to require the classical properties on the various relations on the sets .
Definition 3.2.11**.**
By an equivalence relation on an object of a category we mean a relation on such that for every object , the corresponding relation on the set is an equivalence relation. More generally, the relation is reflexive (resp. symmetric, transitive, antisymmetric, etc.) when each corresponding realtion is so.
In Set, given an equivalence relation , one can take the quotient of by , arriving at a diagram
[TABLE]
The coequalizer of is the quotient of by the equivalence relation generated by the pairs , which is . On the other hand, iff , which indicates that is the kernel pair of .
Definition 3.2.12**.**
An equivalence relation on an object of a category is effective when the coequalizer of exists, and, is the kernel pair of .
For more on categorical equivalence relations, see [12].
Now we return to dialgebras and bisimulations:
Definition 3.2.13**.**
Let be two dialgebras in . An -bisimulation between and is a dialgebra , where is a relation between , such that both and are dialgebra homomorphisms. In other words, Diagram 3.3 commutes.
We omit the functors and use the term bisimulation whenever and are clear from the context. Also, an -bisimulation on is an -bisimulation between and itself. Finally, an -bisimulation equivalnce on is a bisimulation on that is also an equivalence relation on .
Next, another important concept is introduced. Following McLarty [34]:
Definition 3.2.14**.**
Suppose that has finite products, and take any arrow . The graph arrow of , denoted by , is the arrow that makes Diagram 3.4 commute.
Proposition 3.2.15**.**
* as defined above is an equalizer for and .*
Proof. We have
[TABLE]
Also, for any other with , consider the composition
[TABLE]
We have
[TABLE]
and then by universality of the product ,
[TABLE]
Finally, suppose that there is some other arrow with . Then
[TABLE]
so is the unique arrow with the above property. This completes the proof.
Corollary 3.2.16**.**
The graph arrow defined above is always monic.
Consequently, by Proposition 3.2.10:
Corollary 3.2.17**.**
For any , the graph arrow is a relation between .
In addition, we have:
Proposition 3.2.18**.**
For any with a product with itself, the diagonal equals the graph arrow of :
[TABLE]
Now, equipped with all the above, we state and prove the following theorem, which generalizes Theorem 9 in [56].
Theorem 3.2.19**.**
Assume that has finite products, and let be two -dialgebras in . Then an arrow yields a dialgebra homomorphism if and only if its graph arrow induces an -bisimulation.
Proof. By Corollary 3.2.17 we know that for any arrow , the graph arrow is equivalent to a relation between . Since is always a dialgebra homomorphism, it obviously follows that yields a homomorphism if and only if yields a bisimulation between .
Corollary 3.2.20**.**
Let be a dialgebra. The diagonal of yields a bisimulation equivalence on .
Proof. Use Proposition 3.2.18 together with Theorem 3.2.19.
3.3 Limits and colimits
Now let be a bicomplete category. In this section, a study of limits and colimits in the category is undertaken. The ultimate goal is to prove that has all limits that are preserved by G, and all colimits that are preserved by .
Recall that in the category theory literature, especially in the study of limits and colimits, a functor is sometimes called a diagram, with the category being called the scheme of [3]. Now we sate another closely-related definition [56].
Definition 3.3.1**.**
By the type of a limit or colimit, we mean the isomorphism class, in the category Grph of graphs and graph homomorphisms, of the base graph of the limit or colimit, respectively. A functor is said to preserve a type of limit (colimit), if for every diagram with limit (colimit) ,
[TABLE]
is the limit (colimit) of the diagram .
Let be the forgetful functor from the category of -dialgebras to . For every dialgebra , and, for every dialgebra homomorphism , . For this functor we consider the following definition.
Definition 3.3.2**.**
The functor is said to create a type limit (colimit) if for every diagram , its limit (colimit) is constructed by first taking the limit (colimit) of in , and then supplying it in a unique way with an -dialgebra structure.
Theorem 3.3.3**.**
Assume that is bicomplete. Then:
- (1)
The forgetful functor creates and preserves all types of limits that the functor preserves. 2. (2)
The forgetful functor creates and preserves all types of colimits that the functor preserves.
Proof. We only prove part (1). Part (2) is automatically proved by dualization.
Let be a graph and a diagram in . Suppose that preserves limits of type . Consider the diagram . Since is complete, has a limit in , such that for all in , the following diagram commutes:
L$$Ud(v_{1})$$Ud(v_{2})$$\scriptstyle l_{v_{1}}$$\scriptstyle l_{v_{2}}$$\scriptstyle Ud(e)
and such that, for all other cones with analogous commutativity conditions as above, there exists a unique morphism such that the following triangle commutes for all :
Ud(v)$$M$$L$$\scriptstyle f_{v}$$\scriptstyle l_{v}$$\scriptstyle f
Now consider the diagram
FL$$FUd(v_{1})$$FUd(v_{2})$$GL$$GUd(v_{1})$$GUd(v_{2})$$\scriptstyle F(l_{v_{1}})$$\scriptstyle F(l_{v_{2}})$$\scriptstyle F(Ud(e))$$\scriptstyle F(l_{v_{1}})$$\scriptstyle F(l_{v_{2}})$$\scriptstyle F(Ud(e))$$\scriptstyle\delta_{d(v_{1})}$$\scriptstyle\delta_{d(v_{2})}
Since preserves limits of type , the cone is a limiting cone in . Therefore, since
[TABLE]
there exists a unique map , such that the following diagram commutes in :
FL$$FUd(v_{1})$$FUd(v_{2})$$GL$$GUd(v_{1})$$GUd(v_{2})$$\scriptstyle F(l_{v_{1}})$$\scriptstyle F(l_{v_{2}})$$\scriptstyle F(l_{v_{1}})$$\scriptstyle F(l_{v_{2}})$$\scriptstyle\delta_{d(v_{1})}$$\scriptstyle\delta_{d(v_{2})}$$\scriptstyle\lambda$$\scriptstyle F(Ud(e))$$\scriptstyle F(Ud(e))
Clearly, is a dialgebra and, for all , is a dialgebra homomorphism.
To show that is a limiting cone in , consider any other cone in . Since is a limiting cone in , there exists a unique arrow in such that for all
[TABLE]
It suffices to show that yields a dialgebra homomorphism . For all we have:
FL$$FUM$$GUM$$GL$$GUd(v)$$\scriptstyle Ff$$\scriptstyle Gf$$\scriptstyle\mu$$\scriptstyle Gl_{v}$$\scriptstyle\lambda
[TABLE]
whence, by the universal arrow property of , it now follows that .
Following the lines of the proof of Theorem 3.3.3, the next theorem may also be proved.
Theorem 3.3.4**.**
Assume that is bicomplete. Let be a graph, and be a diagram in .
- (1)
If the functor preserves weak limits of type , then the limit of in may be endowed with a dialgebra structure , such that Diagram 3.5 commutes in , for all in .
- (2)
If the functor preserves weak colimits of type , then the colimit of in may be endowed with a dialgebra structure , such that Diagram 3.6 commutes in , for all in .
The following theorem exhibits some of the fruitful interaction of the notion of bisimulation with the weak preservation of limits by the functor .
Theorem 3.3.5**.**
Assume that is bicomplete. Let be -dialgebras, and be dialgebra homomorphisms in . If preserves weak pullbacks, then the pullback of in yields a bisimulation from to in .
Proof. Let and be homomorphisms. Consider the pullback diagram in :
B$$A\times_{C}B$$A$$C$$\scriptstyle\pi_{2}$$\scriptstyle f$$\scriptstyle\pi_{1}$$\scriptstyle g
Then, since preserves weak pullbacks, by Theorem 3.3.4 (1), there exists an arrow such that both and are homomorphisms.
3.4 The problem of dualization
As we discussed earlier (see 1.1), there is a problem concerning the dualization of dialgebras. We explain this more here. Firstly, we give a statement of the problem:
Statement of the problem. *Let be endofunctors on . Can the results in be translated into corresponding ones in ?
To answer the above question, we pay attention to the fact that there is a formal relationship between the category of -coalgebras and the category of -algebras [27]:
Proposition 3.4.1**.**
Let be any category. Then the category of -coalgebras arises formally as the category .
This fact can be generalized to arbitrary dialgebras:
Proposition 3.4.2**.**
Let be any category. Then the category of -dialgebras arises formally as the category .
Therefore, whenever is non-self-dual (e.g. when ), our problem seems to have no simple answer (also, see [26]). However, self-dual bases provide us with an advantage:
Proposition 3.4.3**.**
Let be self-dual (see Definition 1.2.27), and let be endofunctors on . Then
[TABLE]
In other words, we have a (contravariant) isomorphism of categories of dialgebras whenever the base category is isomorphic to its dual.
3.5 Universal dialgebra on the Chu construction
Eventually, we fix for some fixed nonempty set , and study some specific properties of the category for some fixed endofunctors . One pleasant thing about Chu is that it is bicomplete (and also, balanced). Therefore, all the statements proven in the previous sections apply to it. Below we give more detailed statements regarding the above.
First of all, let us take a look at the detailed structure of a relation between two Chu spaces. For Chu spaces , the categorical product has the form , as was discussed before. Now, the following corollary to Proposition 3.2.10 characterizes the relations between Chu spaces.
Corollary 3.5.1**.**
Let be Chu spaces. Then every relation between can be viewed as a monic arrow and vice versa. For and monic , the function is injective while is surjective.
Proof. Use Propositions 3.2.10 and 2.3.11.
Next, the graph arrow of Chu transforms:
Proposition 3.5.2**.**
Let be Chu spaces. For every Chu transform we have
[TABLE]
where and denote the graph arrows of and in the categories Chu and Set, respectively, and denotes the unique arrow that makes the following diagram commute. In this diagram, the top arrows are the obvious inclusions:
X\sqcup Y$$X$$X$$Y$$\scriptstyle\left[1_{X},f^{-}\right]$$\scriptstyle 1_{X}$$\scriptstyle f^{-}
Proof. This easily follows from the properties of the graph arrow in Diagram 3.4.
Now we turn to limits and colimits. Following Theorem 3.3.3:
Corollary 3.5.3**.**
- (1)
The forgetful functor creates and preserves all types of limits that the functor preserves. 2. (2)
The forgetful functor creates and preserves all types of colimits that the functor preserves.
In the same manner, one can deduce corollaries from Theorems 3.3.4 and 3.3.5 when .
Finally, we state the analog of Proposition 3.4.3:
Proposition 3.5.4**.**
We have
[TABLE]
Chapter 4 The Double Category of Paired Dialgebras on Chu
As we mentioned in Chapter 1, the theory of universal dialgebra was first developed over the category Set [56]. There are a number of possible stages of expanding the theory in various ways. In the first stage of expansion, the base category Set might well be generalized to some other bicomplete category. What we did in the previous chapter was taking a few steps just in that direction. More precisely, we observed how the category Chu can serve as a substitute for Set.
In the second stage, one may try to generalize the concept of “universal dialgebra” itself to an even broader framework. Here, equipped with all the eesential tools having been developed in the previous chapters, we are to enter that second stage, which constitues the main part of the current thesis.
In this chapter we introduce double categories firstly (Section 4.1). Then, we will introduce the main formalism of the present thesis, i.e., the construction (Section 4.2), and we will show that the construction is well-defined. Lastly, we will investigate some of the basic properties of the formalism (Section 4.3).
4.1 Double categories
Our “second-stage” generalization of universal dialgebra utilizes the language of double categories. Double categories were introduced by C. Ehresmann and have been further developed by several people since then (see [21] and the references therein). The notion of double category might be seen as a “two-dimensional” generalization of the very notion of category. That is to say, whereas in ordinary cateogries we used to deal with objects (“zero-dimensional points”, diagrammatically) and morphisms (“one-dimensional arrows”), in double categories we have objects (the so-called “0-cells”), horizontal morphisms (“horizontal 1-cells”), vertical morphisms (“vertical 1-cells”), and 2-cells. This way, then, ordianry categories can be seen as special cases of double categories when some of the double-categorical structure is trivialized. It is worth noting that there also exist other two-dimensional generalizations of ordinary categories, namely 2-categories and bicategories. We intend to mention the fact that double categories–together with their “weak” versions–include 2-categories and bicategories as special cases (see Remark 4.1.6).
It is important to know that development of a theory of double categories can be done in various ways. The usual method is to introduce them as internal categories either in CAT or in Cat. This is exactly the approach we take in the present work. However, there is another approach in the literature that develops the theory based on the theory of indexed categories (see [22]); last but not least, some authors believe that double categories are worth an independent treatment, directly founded on basic category theory [22].
In Section 1.3 we introduced internal categories. Now, we proceed as the following. The material in this section is borrowed from [4, 19, 20, 21, 22, 38, 39, 54, 60, 67].
Definition 4.1.1**.**
- (1)
A (large) double category is an internal category in CAT. 2. (2)
Likewise, a small double category is an internal category in Cat. 3. (3)
A double category is said to be properly large if it is not small.
Remark 4.1.2**.**
The following explanations may help the reader obtain a better understanding of the notion of double category. A double category
[TABLE]
consists of an “object of objects” , an “object of arrows” , a “source” , a “target” , an “identity” , and a “composition” . Then, as is internal to CAT, it follows that and are themselves categories, and are themselves functors.
Therefore, itself has a class of objects and a class of morphisms , together with source and target maps
[TABLE]
and similarly for :
[TABLE]
Also, each of the functors and consists of a map on objects and a map on morphisms. Diagram 4.1 depicts all of these maps together.
In this diagram, the following commutativity conditions hold:
[TABLE]
On the other hand, each of is itself composed of a function on objects as well as a function on arrows. That is, we have functions
[TABLE]
[TABLE]
and also
[TABLE]
[TABLE]
Let the compositions in be denoted by , respectively. Then, by functoriality of we have for any ,
[TABLE]
[TABLE]
From the functoriality of we find
[TABLE]
Also, the functoriality of amounts to
[TABLE]
for , and
[TABLE]
for , whenever all the above compositions are defined.
Now we analyze the subject from a different viewpoint. What the above formalism actually gives us is four classes of “things”. We interpret these “things” in the following manner:
- ✓
we regard as the class of 0-cells;
- ✓
we regard as the class of horizontal 1-cells;
- ✓
we regard as the class of vertical 1-cells; and
- ✓
we regard as the class of 2-cells.
Let us look at what a 2-cell in looks like. It has a source and target in , so it has a “source horizontal 1-cell” and a “target horizontal 1-cell”; but it also has a source and target in , thus it has a “source vertical 1-cell” and a “target vertical 1-cell”. The commutativity conditions () and () of Diagram 4.1 tell us that the corners of the adjacent 1-cells match up. The result looks like the cell structure sketched in Diagram 4.2. Notice that the horizontal and vertical arrows in that diagram are depicted by different shapes of arrowheads, in order to distinguish between the horizontal and vertical 1-cells.
Now let us see what kinds of compositions we have here. There are two things that are going on here. First of all, the fact that and are themselves categories means that each of them is equipped with a composition, namely and . The composition composes the adjacent 2-cells along the vertical 1-cells, while the composition composes the adjacent horizontal 1-cells along the 0-cells. The commutativity conditions () and () of Diagram 4.1 ensure that these two compositions are compatible with each other. The result is the horizontal composition sketched in Diagram 4.3.
On the other hand, we have the internal composition bifunctor . This internal composition provides a way for vertical composition of stacked cell structures, as sketched in Diagram 4.4.
Remark 4.1.3**.**
Notice that we have adopted different notational conventions for horizontal and vertical compositions; namely, we have used the “pasting order” for (so that abbreviates ), while we have used the usual “algebraic order” for .
Now, these horizontal and vertical compositions must satisfy the previously-mentioned equations (Remark 4.1.2). For example, for 2-cells in Diagram 4.5 we have
[TABLE]
Next, we pay attention to further structures that “emerge” from our formalism of double categories.
Proposition 4.1.4**.**
The -objects (i.e. the 0-cells) together with the -objects (i.e. the vertical 1-cells) form a category.
Proof. For every -object , seen as an arrow between two -objects, the domain and codomain are given by and , respectively. Also, consecutive -objects compose as . Identity morphisms are given by Finally, the composition is associative.
By similar reasoning one can prove:
Proposition 4.1.5**.**
The class of -morphisms (i.e. the horizontal 1-cells) together with the class of -morphisms (i.e. the 2-cells) form a category, for which the composition is given by .
Remark 4.1.6**.**
It is worth noting here that if all the vertical 1-cells happen to be identities (i.e., if is a discrete category), then the double cateogry reduces to what is called a 2-category in the literature. Also, if all the horizontal 1-cells are identities, then the result will be another 2-category. Thus, every double category yields two different 2-categories as special cases. For more on 2-cateogries and their relationships to double categories and other closely-related concepts (such as their respective “weak” versions), the reader is referred to [15, 31, 57, 58, 62].
Next, we give another important definition.
Definition 4.1.7**.**
The transpose of a double category is the double category
[TABLE]
where is the category introduced in Proposition 4.1.4, and is the category introduced in Proposition 4.1.5; the source functor is given as the pair while is defined as ; the functor is made of the identity functions of , and finally, the composition bifunctor comes from the compositions of the categories .
In other words, is the double category which consists of the same 0-cells, 1-cells, and 2-cells as of , but in which the roles of horizontal and vertical categories are interchanged.
Remark 4.1.8**.**
It follows immediately that by transposing the transposed category we return to the original cateogry :
[TABLE]
Definition 4.1.9**.**
Let be a double category, and let Diagram 4.6 be a cell structure in .
The boundary of the 2-cell is defined as the 4-tuple
[TABLE]
and the situation is denoted by
[TABLE]
Definition 4.1.10**.**
A double category is said to be flat if its 2-cells are completely determined by their boundaries. In such case, then, for a cell structure like Diagram 4.6 we write:
[TABLE]
Definition 4.1.11**.**
Let be a double category. The horizontal dual of , denoted by , is defined as
[TABLE]
for which we have
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
Definition 4.1.12**.**
Let be a double category. The vertical dual of , denoted by , is defined as
[TABLE]
Remark 4.1.13**.**
Therefore, the vertical dual will have the following data:
[TABLE]
where is the category consisting of a class of objects and a class of morphisms such that
[TABLE]
where was given in Definition 4.1.7, and
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
Also,
[TABLE]
where was given in Definition 4.1.7, and
[TABLE]
[TABLE]
[TABLE]
[TABLE]
further, for every composable arrows in there is a horizontal composition as
[TABLE]
finally, for every there is a vertical composition given by
[TABLE]
Definition 4.1.14**.**
Let be a double category. The central dual of , denoted by , is defined as
[TABLE]
Remark 4.1.15**.**
Let denote the dihedral group of order 8, corresponding to the symmetry group of a square [5, 50]; that is
[TABLE]
where are two generators and is the identity element of the group. As stated in [22], for any double category , the group acts on . In particular, we have
[TABLE]
that is, horizontal dualization commutes with vertical dualization. Other useful relations are
[TABLE]
[TABLE]
Remark 4.1.16**.**
It is sometimes better to view the notion of double category together with its transpose, its horizontal, vertical, and central duals in the following schematic way. This viewpoint has the advantage that it respects, and clearly manifests, the two-dimensional nature of the cell structures in double categories.
Let be a double category, and be its transpose. We know that
[TABLE]
that is, every 2-cell is at the same time a 2-cell in and vice versa. Therefore, we can depict as an inclined double-arrow in the cell structure of Diagram 4.7.
In this diagram, the inclined double-arrow represents the 2-cell both as a member of within (i.e., as an arrow from the leftmost vertical arrow to the rightmost vertical arrow) and as a member of within (i.e., as an arrow from the uppermost horizontal arrow to the lowermost horizontal arrow). This way, the 2-cell is truly regarded as a “two-dimensional arrow” capable of doing two different duties in two different dimensions.
Consequently, the cell structures in together with those in its horizontal, vertical, and central duals can easily be depicted as the following (Diagram 4.8).
(There are also four other cell structures, with the vertical and horizontal 1-cells interchanged, corresponding to the transposes of each of the above cell structures.)
Next, we take a look at horizontal isomorphisms.
Definition 4.1.17**.**
Let the following be a cell structure in a double category
:
Y$$X$$X^{\prime}$$Y^{\prime}$$f$$g$$v$$u$$\mathbbm{c}
Then, the 2-cell is called a horizontal isomorphism from to if
[TABLE]
is an isomorphism in , with inverse . Note that it follows from this definition and from the functoriality of that:
- (1)
both of the horizontal 1-cells must be isomorphisms in , with inverses , respectively; and 2. (2)
the boundary of shall be .
In such case, then, the 2-cell is called the horizontal inverse to the 2-cell .
Remark 4.1.18**.**
For flat double categories, the above situation simplifies to:
[TABLE]
Definition 4.1.19**.**
- (1)
For the double category as above, the 2-cell is called a vertical isomorphism from to if is a horizontal isomorphism in . 2. (2)
For the double category as above, the 2-cell is called a a central isomorphism from to if is both a horizontal isomorphism from to and a vertical isomorphism from to .
Remark 4.1.20**.**
There are also other kinds of isomorphisms and equivalences definable in double categories. See for example [22].
Now we introduce another fundamental concept:
Definition 4.1.21**.**
Let and be two double categories. A double functor consists of the following data:
[TABLE]
where and are functors that make Diagram 4.9 commute.
In this diagram, is the pullback of , while is the pullback of ; also,
[TABLE]
is the unique arrow according to the universality of .
Remark 4.1.22**.**
A double functor is sometimes called a double diagram in , especially when working with limits and colimits. The double diagram is said to be small whenever is a small double category.
Definition 4.1.23**.**
- (1)
Let be a double category. The double functor
[TABLE]
is called the identity double functor on . 2. (2)
We define a composition for double functors; that is, for consecutive :
[TABLE]
It is immediate that satisfies the commutativity conditions of Diagram 4.9, and, hence, is well-defined. 3. (3)
A double functor is called an isomorphism double functor if there exists another double functor such that
[TABLE]
In such case, we may denote the isomorphism situation by . 4. (4)
A constant double functor is a double functor in which both are constant functors.
Proposition 4.1.24**.**
A double functor is an isomorphism if and only if are isomorphisms as ordinary functors.
Proof. The “Only if” side is obvious. We prove the “If” side. Assume that are double categories and is a double functor from to such that both are (ordinary) isomorphism functors. Thus, have corresponding inverses, namely . It suffices to show that the pair
[TABLE]
actually forms a double functor from to . Referring to Diagram 4.9, we do the following observation: by replacing all with , the unique arrow finds an inverse
[TABLE]
Consequently, the whole diagram again commutes, and therefore, is a well-defined double functor.
Definition 4.1.25**.**
Let be a double functor between double categories and . The transpose of is the double functor defined canonically. That is,
[TABLE]
with functors and defined as the following:
[TABLE]
It is easy to check the commutativity conditions of 4.9 for . For example, the equation follows from the definition of and from the functoriality of , and so on.
Now we introduce a concept from group theory [5, 50].
Definition 4.1.26**.**
The Klein four-group is the group defined as
[TABLE]
where are two generators, and is the commutator of . The underlying set of has four elements (hence the name “four-group”):
[TABLE]
is abelian, a subgroup of the dihedral group , and the smallest non-cyclic group. Also, geometrically, is the symmetry group of a rhombus and of a rectangle which are not squares, the four elements of the symmetry group being identity, vertical reflection, horizontal reflection, and 180° rotation (Diagram 4.10).
We need the group for the next definition:
Definition 4.1.27**.**
A double category is said to be Klein-invariant or -invariant if there exist the following isomorphism double functors:
[TABLE]
and are called the horizontal self-duality and the vertical self-duality of , respectively.
Remark 4.1.28**.**
It follows immediately that for every Klein-invariant double category we have
[TABLE]
where the composite isomorphism
[TABLE]
is called the central self-duality of .
There is another useful definition (which is not used in the present work but may be useful for future development):
Definition 4.1.29**.**
- (1)
A double category is said to be self-transpose if
[TABLE] 2. (2)
is said to be strictly self-transpose if
[TABLE]
Next, we turn to transformations between double functors [22].
Definition 4.1.30**.**
Let \mathcal{F,G}:\mathbb{D\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}E} be double functors from to . A horizontal (natural) transformation assigns
- (1)
a family of -morphisms (horizontal 1-cells) for each -object (0-cell) , 2. (2)
a family of -morphisms (2-cells) for each -object (vertical 1-cell) ,
so that the following preservation and naturality conditions hold:
- (HT1)
for every ;
- (HT2)
for all ;
- (HT3)
for every in (Diagram 4.11).
Remark 4.1.31**.**
It follows that the arrows give a natural transformation .
Remark 4.1.32**.**
If is flat, then (HT1) and (HT2) are trivially satisfied while (HT3) reduces to ordinary naturality. A horizontal transformation reduces thus to a natural transformation such that, for every vertical 1-cell in , the boundary
[TABLE]
determines a unique 2-cell.
Horizontal transformations compose canonically:
Definition 4.1.33**.**
Given and , their (horizontal) composition is defined as
[TABLE]
Likewise, one can define identity horizontal (natural) transformations, horizontal natural isomorphisms, etc.
Next, we take a look at (horizontal) limits and colimits.
Definition 4.1.34**.**
Let be a double diagram in (see Remark 4.1.22). Also, let be a constant double functor.
- (1)
A horizontal natural source for is a horizontal transformation . 2. (2)
A horizontal natural sink for is a horizontal transformation . 3. (3)
A horizontal limit for is a horizontal natural source which is universal in the sense that for any other horizontal natural source , there exists a unique horizontal transformation such that
[TABLE] 4. (4)
A horizontal colimit for is a horizontal natural sink which is universal in the sense that for any other horizontal natural sink , there exists a unique horizontal transformation such that
[TABLE]
This way, we can have (binary) horizontal products and coproducts, horizontal pullbacks and pushouts, etc.
4.2 The main formalism
First of all, we introduce an auxiliary category, which will be used in the sequel.
Definition 4.2.1**.**
Consider the category for some fixed nonempty . By the fluid category on Chu, denoted by , we mean the category which consists of the following data:
- •
Objects: all dialgebras of the form , where is a Chu space, and are Chu endofunctors, and is a Chu transform. More precisely, we take
[TABLE]
where the right hand side is the disjoint union of classes.
- •
Morphisms: if are two objects with and
for endofunctors , then
- –
for , there are no morphisms between ;
- –
but for , the morphisms are pairs of the form
, where
[TABLE]
are Chu transforms that make Diagram 4.12 commute.
The pair is called a local transformation from to .
- •
Composition: the pairs and compose componentwise:
[TABLE]
- •
Identities: pairs for each object .
The category is intended to serve as one of the resources for our main formalism:
Definition 4.2.2**.**
Consider the category for some fixed nonempty set . Also, let be a fixed set (possibly empty). The (properly large) double category is defined by the following data:
[TABLE]
such that categories and functors are defined as below:
a. The category . The category (the “object of objects”) is defined as the following:
a.1. Objects of . The -objects (the 0-cells) are pairs
[TABLE]
such that
a.1.1. is a pair called a dialgebra column, where is an
-dialgebra in for endofunctors , while is a -dialgebra in for endofunctors ;
a.1.2. is a pair of functions
[TABLE]
is called a super-matrix. Furthermore, the functorial profile of is defined as
[TABLE]
a.2. Morphisms of . For 0-cells and , if , then there are no -morphisms between them; but if with
[TABLE]
the -morphisms (the horizontal 1-cells) are pairs of the form
[TABLE]
where is a pair such that is an -dialgebra homomorphism in while is a -dialgebra homomorphism in , and Diagram 4.13 commutes, in which the left and right diamonds are called the Positive and Negative Horizontal Super-adjointness conditions, or briefly PHS and NHS, respectively (in this diagram, also, are the stems of , respectively).
a.3. Composition in . For horizontal 1-cells with , their composition is given by
[TABLE]
with composition in each row being done in the corresponding category. The above composition satisfies the positive and negative super-adjointness conditions and, hence, is well-defined (see Step 1 of the proof of Proposition 4.2.3 below).
a.4. Identities in . For a 0-cell ,
[TABLE]
where are the identity dialgebra homomorphisms on , respectively.
b. The category . The category (the “object of arrows”) is defined as the following. Before proceeding we introduce an auxiliary category:
b.1. The auxiliary category . Consider the category consisting of the following data:
- •
-objects: the same as objects of :
[TABLE]
- •
-morphisms: for 0-cells and with
, the morphisms are pairs of the form
[TABLE]
where and are arrows in , such that Diagram 4.14 commutes (the left and right triangles are called the Positive and Negative Vertical Super-adjointness conditions, or briefly PVS and NVS, respectively).
- •
-composition: -morphisms compose componentwise: for and ,
[TABLE]
- •
-identities: The identities are defined componentwise; for an object ,
[TABLE]
that is, is defined as a pair of identity -arrows (the notation is used in order to avoid confusion with the identity defined in part (a.4) in the above).
Also, the above composition is associative because of associativity of -arrows. Therefore, is indeed a category.
b.2. Objects of . The -objects (the vertical 1-cells) are exactly the -morphisms defined above:
[TABLE]
b.3. Morphisms of . For -objects
[TABLE]
[TABLE]
for -morphisms
[TABLE]
and for -objects
[TABLE]
the -morphisms (the 2-cells), also called the cubicles, are of the form
[TABLE]
provided that the following four parallelograms commute (Diagram 4.15):
Notice the fact that the above conditions imply the commutativity of both of the cubes in the following diagram (Diagram 4.16).
Also, notice that the above definition means that we are defining a flat double category since every 2-cell is completely determined by its boundary (see Definitions 4.1.9 and 4.1.10).
b.4. Composition in . For cubicles
[TABLE]
the composition is defined as
[TABLE]
b.5. Identities in . For every vertical 1-cell , the identity 2-cell is defiend as
[TABLE]
c. The internal source and target functors. The functors \mathcal{s,t:B\raisebox{-1.0pt}{\begin{array}[]{c}\longrightarrow\ \longrightarrow\end{array}}A} are defined as the following:
c.1. Internal source and target on -objects. For a -object ,
[TABLE]
c.1. Internal source and target on -morphisms. For a -morphism
with and ,
[TABLE]
d. The internal identity functor. The functor is defined as the following:
d.1. Internal identity on -objects. For ,
[TABLE]
where was defined in part (b.1).
d.2. Internal identity on -morphisms. For ,
[TABLE]
e. The internal composition bifunctor. For the pullback of Diagram 4.17,
the composition bifunctor
[TABLE]
is defined as the following:
e.1. Internal composition on objects. Considering a pair
[TABLE]
and abbreviating as , we define
[TABLE]
where is composition in the category (see parts (b.1), (b.2)).
e.1. Internal composition on morphisms. Considering a pair
[TABLE]
with
[TABLE]
[TABLE]
we define
[TABLE]
Whenever are clear from the context, we denote the double category by . The initialism “DLC” stands for “the properly large flat Double category of paired Dialgebras and dialgebra homomorphisms, paired Local transformations, and Cubicles on Chu”.
We need to show that Definition 4.2.2 is well-defined.
Proposition 4.2.3**.**
* as defined in Definition 4.2.2 is well-defined.*
Proof. We prove this through the following steps:
Step 1. Composition in *is well-defined.
The composition of and was given by
[TABLE]
Well-definedness of the above composition is proved by the commutativity of the following diagrams (Diagrams 4.18, 4.19). The former diagram guarantees the PHS condition to hold for , while the latter verifies NHS.
Step 2. The identity and associativity propoerties hold for -morphisms. Given , it is clear that are actually the identity morphisms on since
[TABLE]
for every .
With a similar line of reasoning, as are dialgebra homomorphisms for every
, the associativity of -morphisms is verified.
Step 3. Composition in *is well-defined.
The composition of and was given by
[TABLE]
Well-definedness of this composition is proved by the commutativity of Diagram 4.20. In the diagram, the left half guarantees the PVS condition to hold for while right half verifies NVS.
Step 4. -morphisms *are well-defined.
To show that the cubicles are well-defined, we observe that for the cubicle
defined in part (b.2) of Definition 4.2.2, the horizontal and vertical super-adjointness conditions, PHS, NHS, PVS, and NVS are compatible with each other. In other words, Diagram 4.21 commutes.
In this diagram, the upper-left, upper-right, lower-left, and lower-right diamonds are and , respectively (the superscripts refer to the corresponding horizontal 1-cells). Also, the front and rear parallelograms with common segment are , and , respectively (the subscripts referring to the corresponding vertical 1-cells). Finally, the commutativity of the front and rear lateral parallelograms follows immediately from the commutativity of Diagram 4.15. Whence, the whole shape commutes, and consequently, cubicle is a well-defined arrow from to .
Step 5. Axiom A1 of Definition 1.3.4 holds for as an internal category in CAT*.
Consider the functors and . For every -object
[TABLE]
we have
[TABLE]
[TABLE]
Also, for every -morphism ,
[TABLE]
[TABLE]
Therefore,
[TABLE]
Step 6. Axiom A2 of Definition 1.3.4 holds for as an internal category in CAT*.
For any pair with and we have
[TABLE]
[TABLE]
On the other hand, for a pair with and ,
[TABLE]
[TABLE]
So,
[TABLE]
as desired.
Step 7. Axiom A3 of Definition 1.3.4 holds for as an internal category in CAT*.
Let be a -object with
[TABLE]
Then, and , thus
[TABLE]
[TABLE]
Whence,
[TABLE]
[TABLE]
These imply that we have the following agreement of functors on every -object :
[TABLE]
On the other hand, assume a -morphism between -objects
[TABLE]
together with -morphisms
[TABLE]
such that
[TABLE]
We have
[TABLE]
[TABLE]
Therefore,
[TABLE]
[TABLE]
These imply that we have the following agreement of functors on every -morphism :
[TABLE]
Now, results imply
[TABLE]
Step 8. Axiom A4 of Definition 1.3.4 holds for as an internal category in CAT*.
Finally, we verify the internal associativity. Consider the bifunctors
[TABLE]
[TABLE]
where the pullback is that of , while the pullback is that of (see Propositions 1.3.2 and 1.3.3). Assume that
[TABLE]
are -objects such that
[TABLE]
This means
[TABLE]
and
[TABLE]
But these two conditions together are equivalent to stating that
[TABLE]
therefore,
[TABLE]
Similarly, for -morphisms it can shown that
[TABLE]
Now let
[TABLE]
so that is a morphism in . Then
[TABLE]
From the above results on objects and morphisms we conclude:
[TABLE]
and the proof is complete.
Remark 4.2.4**.**
At this point, it is interesting to take a look at the transpose double category . It consists of the following data:
[TABLE]
where is exactly the auxiliary category defined in part (b.1) of Definition 4.2.2; objects of are -morphisms , morphisms of are the -morphisms (i.e. the cubicles)–this time viewed as arrows between -morphisms–and the functors are determined according to Definition 4.1.7.
4.3 Some of the basic properties
Now we state and prove some basic properties of . First and foremost, we have the fundamental property of Klein-invariance. We prove this as a corollary of Theorems 4.3.1 and 4.3.8; in these theorems, respectively, we explicitly construct the isomorphism double functors and . The Klein-invariance of follows immediately afterwards. Next, we will take a look at (binary) horizontal products and coproducts in .
4.3.1 Klein-invariance
Theorem 4.3.1**.**
For every set and every nonempty set , the double category is horizontally self-dual.
Proof. Assume an arbitrary set and an arbitrary nonempty set . Consider the double category . Observe that for , the double category consists of the following data:
[TABLE]
Now we define
[TABLE]
where are functors we define below. Firstly,
[TABLE]
has the following data:
- •
on -objects: for any with we define
[TABLE]
in which we have identified the isomorphic coproducts
[TABLE]
and also
[TABLE]
so that the super-matrix remains the same;
- •
on -morphisms: for any , where is an -morphism, we define
[TABLE]
Note that satisfies the PHS and NHS conditions (in fact, the corresponding commutative diagram for is a “vertical flip” of Diagram 4.13), hence it is a well-defined -morphism.
On the other hand, is such that:
- •
on -objects: for any we define
[TABLE]
which satisfies the PVS and NVS conditions (with commutativity diagrams the same as Diagram 4.14), and is thus a well-defined -object;
- •
on -morphisms: for any where
[TABLE]
is a -morphism, we define
[TABLE]
which clearly satisfies the commutativity conditions of Diagram 4.15 and is, therefore, well-defined.
Now, from the definition of , the following holds for every -object
:
[TABLE]
Also, for every -morphism ,
[TABLE]
Equations (1) and (2) together imply
[TABLE]
Likewise, one can deduce
[TABLE]
Next, from the definition of , for every -object we have
[TABLE]
Also, for every -morphism where ,
[TABLE]
Equations (5) and (6) together imply
[TABLE]
Now consider Diagram 4.22.
In this diagram, are the projections for
, making the left hand side diamond commute. Now, in addition, from (3), (4), and (7) we know that, respectively, the lower-right parallelogram, the lower-left parallelogram, and the bottom rectangle all commute. Therefore, we have the following equations:
[TABLE]
So, by universality of the pullback , there exists a unique arrow
[TABLE]
making the upper-left and upper-right parallelograms commute. Now, in order to prove the double functoriality of , it remains to prove the commutativity of the top rectangle.
On objects we have
[TABLE]
on morphisms,
[TABLE]
These complete the proof of commutativity of Diagram 4.22. Thus, is actually a double functor.
The final step of the proof is to show that is an isomorphism. For this, according to Proposition 4.1.24, it suffices to show that both and are isomorphisms (as ordinary functors). More precisely, we show that the opposite functors
[TABLE]
are inverses to and , respectively.
For any -object with ,
[TABLE]
thus, on -objects, . Similarly, on -objects, .
On the other hand, for any -morphism , where is an -morphism,
[TABLE]
that is, on -morphisms, . Similarly, on -morphisms,
. We conclude from all the above that is an isomorphism.
For the case of the reasoning goes as the following: for any -object ,
[TABLE]
On the other hand, for any -morphism where is a -morphism,
[TABLE]
so, . By a similar argument, . Consequently, , too, is an isomorphism. This completes the proof of the horizontal self-duality of .
For the vertical self-duality a different line of reasoning is to be taken. First of all, recall that the -autonomous structure of Chu includes a (covariantly written) self-duality functor
[TABLE]
that sends every Chu space to the Chu space , and sends every to the Chu transform . To be able to work with -dialgebras, we need a contravariant version of the above self-duality. Therefore, we define:
Definition 4.3.2**.**
The contravariant self-duality functor is defined as
[TABLE]
for which the reverser was introduced in Definition 1.2.30.
Further, we expand the above definition to dialgebras:
Definition 4.3.3**.**
Let be two Chu endofunctors, and let be an -dialgebra. Then we define
[TABLE]
where abbreviates , and so on.
Proposition 4.3.4**.**
Let . A Chu transform yields an -dialgebra homomorphism if and only if yields an -dialgebra homomorphism . Moreover, .
Proof. In Diagram 4.23, the commutativity of the left square is equivalent to the commutativity of the right one.
It is obvious that for every and for every . So, the map sending every to , together with the map which sends every -dialgebra homomorphism to the -dialgebra homomorphism , constitute an isomorphism functor .
Even more—by some abuse of notation—we expand the definition of to the case of the category :
Definition 4.3.5**.**
For every -object with we define
[TABLE]
where . Also, for every -morphism , we define
[TABLE]
It is evident that satisfies the PHS and NHS conditions (the corresponding commutative diagram for is a “180° rotation” of Diagram 4.13), thus it is a well-defined -morphism. This way, can be seen as an endofunctor.
Proposition 4.3.6**.**
The endofunctor is a (contravariant self-duality) isomorphism.
Proof. By definition, for every , ; also, for every we have .
Proposition 4.3.7**.**
The endofunctor induces a (contravariant self-duality) isomorphism on .
Proof. Let an endofunctor be defined as the following: for every dialgebra ,
[TABLE]
on the other hand, for every -morphism we define
[TABLE]
(Notice the reversal of the order of the letters .) Now it is evident that for every ,
[TABLE]
as desired.
Now, equipped with all the above, we are ready to state and prove our next theorem:
Theorem 4.3.8**.**
For every set and every nonempty set , the double category is vertically self-dual.
Proof. Assume that an arbitrary set and an arbitrary nonempty set are given. Consider the double category . Observe that the double category consists of the following data:
[TABLE]
Now we define:
[TABLE]
where
[TABLE]
and the functor is defined as the following:
- •
for any -object where is a -object (equivalently, an -morphism),
[TABLE]
which satisfies the PVS and NVS conditions (with commutativity diagram being a “180° rotation” of Diagram 4.14), and is thus a well-defined -object;
- •
for any -morphism where is a -morphism,
[TABLE]
which satisfies the commutativity conditions of Diagram 15 and is therefore, well-defined.
Now, from the definition of , the following holds for every -object where :
[TABLE]
also, for every -morphism where ,
[TABLE]
Equations (1) and (2) together imply
[TABLE]
Likewise, one can deduce
[TABLE]
Next, from the definition of , for every -object we have
[TABLE]
also, for every -morphism ,
[TABLE]
Equations (5) and (6) together imply
[TABLE]
Now we consider Diagram 4.24.
In this diagram, are the projections for , making the left hand side diamond commute. Now, in addition, from (3), (4), and (7) we know that, respectively, the lower-right parallelogram, the lower-left parallelogram, and the bottom rectangle all commute. Therefore, we have the following equations:
[TABLE]
So, by universality of the pullback , there exists a unique arrow
[TABLE]
making the upper-left and the upper-right parallelograms commute. Now, in order to prove the double functoriality of , it remains to show the commutativity of the top rectangle.
On objects we have
[TABLE]
for morphisms,
[TABLE]
These complete the proof of commutativity of Diagram 4.24, and is actually a double functor (from to ).
The final step of the proof is to show that is an isomorphism. For this, according to Proposition 4.1.24, it suffices to show that both and are isomorphisms as ordinary functors. By Proposition 4.3.6 we already know that the functor is inverse to itself. On the other hand, we show that the functor
[TABLE]
which is defined below, is inverse to .
We define as the functor which sends every -object
to the -object
[TABLE]
and which sends every -morphism to the -morphism
[TABLE]
Now, for any -object ,
[TABLE]
also, using (8), we have for any -object ,
[TABLE]
On the other hand, for any -morphism ,
[TABLE]
also, using (10), we have for any -morphism ,
[TABLE]
Now, Equations (8), (10) together imply
[TABLE]
Likewise, Equations (9), (11) together imply
[TABLE]
Consequently, , too, is an isomorphism. This completes the proof of the vertical self-duality of .
Theorems 4.3.1 and 4.3.8 together yield one of the fundamental features of :
Corollary 4.3.9**.**
For every set and every nonempty set , the double category is Klein-invariant.
Corollary 4.3.9 is so important that it deserves special attention. What it tells is that we have the following four isomorphic double categories:
[TABLE]
This means that whenever one proves a result in any of the above four double categories, that result automatically yields three other analogous results in the same double category by horizontal, vertical, and central self-dualizations, respectively. This situation is comparable to (and is a generalization of) the self-duality of Chu.
4.3.2 Binary horizontal products and coproducts
In this subsection we have both negative and positive results. We start with negative results.
Proposition 4.3.10**.**
Assume a nonempty set and a (possibly empty) set . Then:
- (1)
there exist 0-cells in such that for any two vertical 1-cells
* and there exist no horizontal binary product and no horizontal binary coproduct;* 2. (2)
there exist 0-cells in such that for any two vertical 1-cells
* and there exist no horizontal binary product and no horizontal binary coproduct.*
Proof. (1) Consider any two 0-cells with different functorial profiles
[TABLE]
and consider vertical 1-cells for some . Also, assume that
[TABLE]
is the horizontal product of . This implies that the 0-cell must be the (ordinary) product of . On the other hand, we know that at least one of the following holds:
[TABLE]
Assume, for example, . But this means that there can be no horizontal 1-cells from to ; thus, we have no projection from to , and consequently, no projection 2-cell from to . Therefore, cannot be a product of , and cannot be a horizontal product of . Contradiction.
A similar argument works for the coproduct of , as well.
(2) For this part, just apply the vertical self-duality of on part (1).
In addition, when , the situation is even worse:
Proposition 4.3.11**.**
Assume nonempty sets . Then, in the double category :
- (1)
there exist 0-cells with , such that for any pair of 0-cells with and vertical 1-cells no horizontal binary product exists; 2. (2)
there exist 0-cells with , such that for any pair of 0-cells with and vertical 1-cells no horizontal binary coproduct exists; 3. (3)
there exist 0-cells with , such that for any pair of 0-cells with and vertical 1-cells no horizontal binary product exists; 4. (4)
there exist 0-cells with , such that for any pair of 0-cells with and vertical 1-cells no horizontal binary coproduct exists.
Proof. We only prove part (1); parts (2), (3), and (4) are automatically proved by horizontal, vertical, and central self-dualities, respectively.
Assume nonempty sets , and consider the double category
[TABLE]
Consider -objects with nonempty carriers . Also, consider four -endofunctors such that for every Chu space with a nonempty carrier ,
[TABLE]
(for example, take ). Assume that
[TABLE]
are dialgebras.
Fix . Define 0-cell as
[TABLE]
such that
[TABLE]
Also, define 0-cell as
[TABLE]
such that
[TABLE]
Now, consider any pair of 0-cells with , together with vertical 1-cells
[TABLE]
We claim that there are no horizontal products of .
We prove the claim by contradiction. Assume there exists some vertical 1-cell
together with, say, cubicles
[TABLE]
[TABLE]
that possess the universal property of horizontal product. Then,
[TABLE]
must be a (product) diagram in . Let . Then, the above diagram implies that for the horizontal 1-cells and we must have the following positive horizontal super-adjointness conditions and , respectively:
\Sigma$$F^{+}\mathsf{C}\sqcup K^{+}\mathsf{D}$$F^{+}\mathsf{A}_{1}\sqcup K^{+}\mathsf{D}$$F^{+}\mathsf{A}_{1}\sqcup K^{+}\mathsf{B}_{1}$$F^{+}\mathsf{A}_{2}\sqcup K^{+}\mathsf{D}$$F^{+}\mathsf{A}_{2}\sqcup K^{+}\mathsf{B}_{2}$$\textup{PHS}_{1}$$\textup{PHS}_{2}$$\scriptstyle T^{+}$$\scriptstyle F^{+}f_{1}\sqcup 1$$\scriptstyle S^{+}_{1}$$\scriptstyle 1\sqcup K^{+}g_{1}$$\scriptstyle F^{+}f_{2}\sqcup 1$$\scriptstyle S^{+}_{2}$$\scriptstyle 1\sqcup K^{+}g_{2}
Since , we obtain from that
[TABLE]
or
[TABLE]
Now if , it follows that which contradicts (1) because the coproduct is the disjoint union of the sets and . Therefore, we must have
[TABLE]
On the other hand, considering , we find from that
[TABLE]
or
[TABLE]
But Equation (2) says that , thus
[TABLE]
which clearly contradicts (3). Consequently, there can be no such product diagram as , and we are done.
Finally, we have a positive result for the case .
Proposition 4.3.12**.**
Assume a nonempty set , and let . Assume that are 0-cells in the double category such that
[TABLE]
Then, for every pair of vertical 1-cells we have the following:
- (1)
If the endofunctors preserve binary products and the endofunctors preserve binary coproducts, then there exists a horizontal product for ; that is, there exists a vertical 1-cell for some , together with cubicles
[TABLE]
with the following universal property: for any other vertical 1-cell and any diagram
[TABLE]
there exists a unique cubicle such that
[TABLE] 2. (2)
If the endofunctors preserve binary coproducts and the endofunctors preserve binary products, then there exists a horizontal coproduct for ; that is, there exists a vertical 1-cell for some , together with cubicles
[TABLE]
with the following universal property: for any other vertical 1-cell and any diagram
[TABLE]
there exists a unique cubicle such that
[TABLE]
Proof. We only prove part (1); part (2) is automatically proved by horizontal self-duality.
Note that since , the positive and negative horizontal super-adjointness conditions are trivially satisfied for all horizontal 1-cells, and the positive and negative vertical super-adjointness conditions are trivially satisfied for all vertical 1-cells. Thus, whenever we define either a horizontal 1-cell or a vertical 1-cell, there will be no need to worry about any of the conditions PHS, NHS, PVS, or NVS.
Assume that and for
, where each of is a pair of empty functions. Since preserve binary products, using Corollary 3.5.3, we find that there exist product dialgebras
[TABLE]
and
[TABLE]
These products are equipped with projection dialgebra homomorphisms
[TABLE]
On the other hand, since preserve binary coproducts, again using Corollary 3.5.3, we obtain coproduct dialgebras
[TABLE]
and
[TABLE]
These too, are equipped with some injection dialgebra homomorphisms
[TABLE]
Let and where
[TABLE]
are all empty functions. Define
[TABLE]
Now, for any pair of vertical 1-cells with
[TABLE]
define
[TABLE]
Also, define the cubicles
[TABLE]
We claim that the triple is a horizontal product for .
To see this, let
[TABLE]
be a double diagram in , such that is a vertical 1-cell between 0-cells
[TABLE]
for some dialgebras , and pairs of empty functions , and such that
[TABLE]
with
[TABLE]
Then, by universalities of dialgebras , there exist unique dialgebra homomorphisms
[TABLE]
satisfying the following equations for :
[TABLE]
Therefore, we have a unique cubicle
[TABLE]
which satisfies
[TABLE]
In the next chapter, we will outline some of the themes for future development of the formalism presented in the current chapter.
Chapter 5 Conclusion and Suggestions for Future Work
In the final chapter of this work, we sum up what has been presented so far, and give some guidelines for future theoretical developments as well as for future practical implementations of the new formalism.
5.1 Conclusion
In the previous chapters, we took the initial steps of developing what may be called “ theory” or “cubicle theory”. First of all, we introduced the preliminary concepts and definitions, including the essentials of basic category theory and internal categories in Chapter 1. Then, in Chapter 2, we did the same for monoidal categories and -autonomous categories. We then proceeded towards the Chu construction, we focused on , and we gave a number of its important properties. We observed the bicompleteness of the Chu construction in general and of Chu in particular; we dealt with extensional, separable, and biextensional Chu spaces, and we proved that Chu is balanced.
Next, we paid attention to linear logic in Chu. We gave exact formulations for multiplicative as well as additive connectives of linear logic in Chu. Multiplicative connectives consist of dualization, tensor, linear implication, and par operations, together with the tensor unit and the dualizing object. On the other hand, additive connectives consist of plus and with operations (which are exactly the categorical binary coproduct and binary product, respectively), together with the plus unit and the with unit.
The issue of realization was our next subject of discussion. There, we quoted some remarkable results indicating the vast potentials of the Chu construction to realize concrete mathematics: Set and Top are realized in , Grp is realized in , TopGrp is realized in , -ary relational structures in general are realized in , is realized in , and so on.
In the final subsection of Chapter 2, we focused on Chu endofunctors, establishing a general method for uplifting arbitrary set functors to Chu functors. Also, we mentioned bi-uplifting as a generalization of the notion of uplifting.
In Chapter 3, we turned to universal dialgebra. We gave the basic notions of the theory for a general (bicomplete) base category , and we stated and proved some of the fundamental properties of the categories of the form .
In Chapter 4, we firstly introduced double categories as categories internal to CAT. Next, we introduced the main formalism of the present work, namely the construction; we proved its well-definedness, and we studied a number of its basic properties. The most important property was Klein-invariance, which we likened to a two-dimensional generalization of the self-duality of the Chu construction. Also, we observed that although horizontal products and coproducts do not exist in in many situations, they do exist at least when certain conditions are met (concerning the functorial profiles and the supermatrices).
With all the above, we finished the present work. Now it is time to point to some opportunities for future work.
5.2 Future development
For this, the following suggestions are given.
Horizontal and vertical limits/colimits in general
A very special kind of limits/colimits was studied in this work, namely binary horizontal products and coproducts. The study may well be continued to cover arbitrary horizontal as well as vertical limits/colimits in .
Other kinds of double-categorical constructions
Other double-categorical concepts are to be developed in , also. These include:
- •
various subcategories of ;
- •
“exponentials” (see [22]);
- •
“comma double categories ([ibid]);
- •
“double isomorphisms” and “sesqui-isomorphisms” ([ibid]);
- •
“double limits/colimits” ([ibid]);
- •
various “forgetful” and “free functors”;
- •
“double adjunctions” and “free monads” ([19]);
- •
“Kan extensions” ([32, 23, 30]) and “Kan lifts” ([63]) in ;
- •
etc.
Certainly, there are other theoretical as well as practical aspects that may be suggested for future development of cubicle theory; however, the author prefers to postpone mentioning them to other occasions.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] S. Abramsky. Big toy models: representing physical systems as Chu spaces. Synthese , 186(3):697–718, 2012. DOI: 10.1007/s 11229-011-9912-x . Also available at: https://arxiv.org/abs/0910.2393 . · doi ↗
- 2[2] S. Abramsky. Coalgebras, Chu spaces, and representations of physical systems. J. Philos. Logic , 42(3):551–574, 2013. DOI: 10.1007/s 10992-013-9276-4 . Also Available at: https://arxiv.org/abs/0910.3959 . · doi ↗
- 3[3] Herrlich, H., Adámek, J. and G. E. Strecker. Abstract and Concrete Categories, The Joy of Cats . John Wiley and Sons, 2004. ISBN: 0-471-60922-6, Online edition available at: http://katmat.math.uni-bremen.de/acc/ .
- 4[4] N. Andruskiewitsch and S. Natale. Double categories and quantum groupoids. Publ. Mat. Urug. , 10:11–51, 2005. Available at: https://arxiv.org/abs/math/0308228 v 2 .
- 5[5] M. A. Armstrong. Groups and Symmetry . Springer-Verlag, 1988. ISBN: 0-387-96675-7.
- 6[6] S. Awodey. Category Theory . Oxford University Press, 2nd edition, 2010. ISBN (Hbk.) 978-0-19-958736-0, Electronic version available at: https://people.mpi-sws.org/~dreyer/courses/catlogic/awodey.pdf .
- 7[7] M. Barr. *-Autonomous categories and linear logic. Math. Struct. Comp. Sci. , 1:159–178, 1991. Reprint available at: http://www.math.mcgill.ca/barr/papers/scatll.pdf .
- 8[8] M. Barr. The Chu construction. Theory Appl. Categ. , 2:No. 2, 17–35, 1996. Available at: www.tac.mta.ca/tac/volumes/1996/n 2/n 2.pdf .
