Re: The boringness of the dual of exponential
On Mon, Nov 7, 2011 at 07:59, Ross Street <ross.street@mq.edu.au> wrote:
The conjecture is false. Take any category E where exponentiable is interesting. Then the dual of exponentiable is not boring in E^op.
Indeed! And this is clearly true of the example given by Thomas, namely Set^op. However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory? Also, in logic, "and" goes in pair with "or", "for all" goes in pair with "there exists". But implication is always left alone. Why is it so? Is it not the case in "dialectical logic" mentioned by Thomas? By the way, I'd love to have some reference on models of dialectical logic. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
When David originally posted his question, I thought it was rather a silly one and that it was quite rightly dismissed by various people. On the other hand, he now says
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
In other words, these things are "idioms" or "naturally occurring things" in mathematics, but there is a gap in the obvious symmetries. Looking for gaps in symmetries is a good thing to do. For example Dirac (whose biography by Graham Farmelo I have just started reading) predicted the positron this way. Actually, if we're looking at the categorical structure of the category of sets, it isn't very symmetrical at all. The second edition of Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's famous textbook, but illustrates how categorists had way overemphasised duality. For example the terminal object yields the classical notion of element or point, whereas the initial object is strict and boring. Products and coproducts of sets are very different. I explored this kind of thing in my book. For example, the section on coproducts shows how different they are in sets/spaces and algebras. So David's question becomes a good one that deserves an answer if we read it as one about the phenomenology of mathematics rather than its technicalities. Paul Taylor PS There is a boring technical answer that I don't think anyone has mentioned, namely copowers, especially of modules. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hello! David Leduc is not satisfied:
Take any category E where exponentiable is interesting. Then the dual of exponentiable is not boring in E^op.
Indeed! And this is clearly true of the example given by Thomas, namely Set^op.
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
I wonder whether it makes sense to introduce notions, which only in the duals of familiar categories. Of course, Set^op is equivalent to the category of complete atomic Boolean algebras, but I do not see that the dual of exponentiation plays an important role in the theory if these Boolean algebras.
Also, in logic, "and" goes in pair with "or", "for all" goes in pair with "there exists". But implication is always left alone. Why is it
In classical logic, one can form this "co-implication" but it does not look very interesting to me. In intuitionistic logic I do not see how to add it more ore less meaningfully (e.g. in such a way that it is left adjoint to "or" in the first argument). Greetings Reinhard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Your observation about lack of symmetry in \set is underscored by the fact that the yoneda functor for \set has a left adjoint which has a left adjoint which has a left adjoint which has a left adjoint but but the co-yoneda functor for \set has a right adjoint that fails to preserve even finite sums. R_j
When David originally posted his question, I thought it was rather a silly one and that it was quite rightly dismissed by various people. On the other hand, he now says
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
In other words, these things are "idioms" or "naturally occurring things" in mathematics, but there is a gap in the obvious symmetries.
Looking for gaps in symmetries is a good thing to do. For example Dirac (whose biography by Graham Farmelo I have just started reading) predicted the positron this way.
Actually, if we're looking at the categorical structure of the category of sets, it isn't very symmetrical at all. The second edition of Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's famous textbook, but illustrates how categorists had way overemphasised duality.
For example the terminal object yields the classical notion of element or point, whereas the initial object is strict and boring.
Products and coproducts of sets are very different.
I explored this kind of thing in my book. For example, the section on coproducts shows how different they are in sets/spaces and algebras.
So David's question becomes a good one that deserves an answer if we read it as one about the phenomenology of mathematics rather than its technicalities.
Paul Taylor
PS There is a boring technical answer that I don't think anyone has mentioned, namely copowers, especially of modules.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Your observation about lack of symmetry in \set is underscored by the fact that the yoneda functor for \set has a left adjoint which has a left adjoint which has a left adjoint which has a left adjoint but the co-yoneda functor for \set has a right adjoint that fails to preserve even finite sums. R_j
When David originally posted his question, I thought it was rather a silly one and that it was quite rightly dismissed by various people. On the other hand, he now says
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
In other words, these things are "idioms" or "naturally occurring things" in mathematics, but there is a gap in the obvious symmetries.
Looking for gaps in symmetries is a good thing to do. For example Dirac (whose biography by Graham Farmelo I have just started reading) predicted the positron this way.
Actually, if we're looking at the categorical structure of the category of sets, it isn't very symmetrical at all. The second edition of Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's famous textbook, but illustrates how categorists had way overemphasised duality.
For example the terminal object yields the classical notion of element or point, whereas the initial object is strict and boring.
Products and coproducts of sets are very different.
I explored this kind of thing in my book. For example, the section on coproducts shows how different they are in sets/spaces and algebras.
So David's question becomes a good one that deserves an answer if we read it as one about the phenomenology of mathematics rather than its technicalities.
Paul Taylor
PS There is a boring technical answer that I don't think anyone has mentioned, namely copowers, especially of modules.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Some short remarks from a dilettante in universal algebra, category theory and philosophy: I came along the unsatisfactory asymmetry in the category SET when looking at coalgebras and asking about coequations some years ago. Having in mind that kernels play a central role in universal algebra I was expecting that co-kernels should play a similar role in universal coalgebra. One can easily dualize the kernel reasoning. Such a dualization, however, looks kind of artificial since a co-kernel just provides a "strange coding" of the image of a map, i.e., a subset, so to speak. One can identify the asymmetry by looking at exponentiation, but isn't the asymmetry already related to the fact that SET is a distributive category, i.e., that addition is trivial and boring compared to multiplication? My interest in coalgebras was also a kind of philosophically triggered. The "classical western scientific cultur" relies and focusses on the existence of "objects/things" and the category SET is somehow the abstract essence of this perception of the world as a bunch of objects/things which are assumed to be identifiable and existing until the end of the time. Buddhistic and/or dialectical reasoning, in contrast, perceives the world as a net of mutual dependent and interweaved "processes". So, my question was if there is anything in mathematics reflecting on a formal level this buddhistic and dialectical reasoning based on "processes". I don't consider coalgebras in SET as such formalization. Those coalgebras are based on "object/thing reasoning" thus they can only give an approximation of the philosophical concept of a "process", namely in terms of distinctions and observations. Uwe Wolter Quoting Paul Taylor <pt11@PaulTaylor.EU>:
When David originally posted his question, I thought it was rather a silly one and that it was quite rightly dismissed by various people. On the other hand, he now says
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
In other words, these things are "idioms" or "naturally occurring things" in mathematics, but there is a gap in the obvious symmetries.
Looking for gaps in symmetries is a good thing to do. For example Dirac (whose biography by Graham Farmelo I have just started reading) predicted the positron this way.
Actually, if we're looking at the categorical structure of the category of sets, it isn't very symmetrical at all. The second edition of Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's famous textbook, but illustrates how categorists had way overemphasised duality.
For example the terminal object yields the classical notion of element or point, whereas the initial object is strict and boring.
Products and coproducts of sets are very different.
I explored this kind of thing in my book. For example, the section on coproducts shows how different they are in sets/spaces and algebras.
So David's question becomes a good one that deserves an answer if we read it as one about the phenomenology of mathematics rather than its technicalities.
Paul Taylor
PS There is a boring technical answer that I don't think anyone has mentioned, namely copowers, especially of modules.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
One point that no-one has mentioned yet is that you can't have exponentiation and its dual in the same category, unless it is a preorder. If exponentiation exists, then the initial object 0 is strict, and so 0 x 0 = 0 (read all equality signs as isomorphisms). But if A + (-) has a left adjoint then it distributes over product, so A = A + 0 = A + (0 x 0) = (A + 0) x (A + 0) = A x A which implies that any two maps into A (with the same domain) are equal. Of course, bi-Heyting algebras (posets P such that both P and P^op are cartesian closed) are of some interest, as has already been mentioned; but if you want to work in non-preordered categories then you have to choose one or the other. Peter Johnstone On Tue, 8 Nov 2011, Paul Taylor wrote:
When David originally posted his question, I thought it was rather a silly one and that it was quite rightly dismissed by various people. On the other hand, he now says
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
In other words, these things are "idioms" or "naturally occurring things" in mathematics, but there is a gap in the obvious symmetries.
Looking for gaps in symmetries is a good thing to do. For example Dirac (whose biography by Graham Farmelo I have just started reading) predicted the positron this way.
Actually, if we're looking at the categorical structure of the category of sets, it isn't very symmetrical at all. The second edition of Paul Cohn's "Universal Algebra" was evidently influenced by Mac Lane's famous textbook, but illustrates how categorists had way overemphasised duality.
For example the terminal object yields the classical notion of element or point, whereas the initial object is strict and boring.
Products and coproducts of sets are very different.
I explored this kind of thing in my book. For example, the section on coproducts shows how different they are in sets/spaces and algebras.
So David's question becomes a good one that deserves an answer if we read it as one about the phenomenology of mathematics rather than its technicalities.
Paul Taylor
PS There is a boring technical answer that I don't think anyone has mentioned, namely copowers, especially of modules.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 11/9/2011 7:58 AM, RJ Wood wrote:
Your observation about lack of symmetry in \set is underscored by the fact that the yoneda functor for \set has a left adjoint which has a left adjoint which has a left adjoint which has a left adjoint but but the co-yoneda functor for \set has a right adjoint that fails to preserve even finite sums. R_j
Richard modestly omitted that he and our esteemed moderator showed (necessarily by classical reasoning) that what Richard just said characterized \set up to equivalence. On 11/10/2011 1:29 AM, Prof. Peter Johnstone wrote:
One point that no-one has mentioned yet is that you can't have exponentiation and its dual in the same category, unless it is a preorder.
Peter modestly omitted that he is the go-to category theorist when it comes to toposes. He also omitted that he was confining himself to cartesian closed categories when he mentioned his point, understandable given that every topos is cartesian closed. To expand a little on my (1965) classmate Ross Street's counterexample of Set^op, Set x Set^op is yet another counterexample. Here I've one-upped Ross (I must be getting competitive in my dotage) by contradicting Peter and giving a counterexample in which both exponentiation *and* dual exponentiation are present simultaneously. How did I know that? Well, Set x Set^op is equivalent (in fact isomorphic) to Chu(Set, 1). For *any* set K, both exponentiation and dual exponentiation are admissible in Chu(Set,K), product being of the tensor kind in this case. How did I know *that*? Well, every Chu category is a *-autonomous category in the sense of Barr 1979. If you don't know why every *-autonomous category contains both exponentiation and dual exponentiation, then like Ebert and Siskel I'm not going to give away the plot and you'll just have to fork out to see the movie, or steal it if you're a nerd, or watch this space (someone is bound to be a spoiler). Open question. At this year's CT, conveniently held 3 km from my sister's house so I could bike in, I talked about TAC's, or topoalgebraic categories. These are defined by picking two sets of objects from an arbitrary category (TAC's for dummies), some details of which may be found at http://boole.stanford.edu/pub/sortprop.pdf . (At question time PTJ insightfully observed that TACs would cause immense confusion if I submitted my write-up to TAC.) A Chu category is precisely a dense complete TAC for which J and L are singleton monoids. That is, one sort and one property, both rigid. The open question: Characterize those dense complete TAC's admitting both exponentiation and dual exponentiation. Chu categories do so, but what about others? Many thanks to Ross, Richard, and Jeff Eggers for their respective roles in the representation of TAC objects (A,r,X) over a profunctor K as a profunctor morphism r: AX --> K. (Ross and I would call them bimodules, much as Mike Barr calls monads triples.) But toposes are fun too. *-autonomous categories are to Democrats as toposes are to Republicans. Vaughan (donkey) Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Thu, 10 Nov 2011, Vaughan Pratt wrote:
... Well, Set x Set^op is equivalent (in fact isomorphic) to Chu(Set, 1). For *any* set K, both exponentiation and dual exponentiation are admissible in Chu(Set,K), product being of the tensor kind in this case.
How did I know *that*? Well, every Chu category is a *-autonomous category in the sense of Barr 1979. If you don't know why every *-autonomous category contains both exponentiation and dual exponentiation, then like Ebert and Siskel I'm not going to give away the plot and you'll just have to fork out to see the movie, or steal it if you're a nerd, or watch this space (someone is bound to be a spoiler).
I hadn't intended to say this, but since Vaughan brought up *-autonomous cats, here goes. In Cockett-Seely "Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories" (TAC 1997) we showed that bilinear logic, formulated with both exponentials (ie suitable left adjoints to tensoring with an object) and dual exponentials (ie suitable right adjoints to co-tensoring ("par'ing") with an object), are just *-autonomous categories. So not only do *-autonomous cats have these two types of "internal homs" (4 operators in all, in the non-symmetric case), but if (eg) a linearly distributive category has them all, then it must be *-autonomous. (In the paper the result is a bit "finer", since we consider two variants of bilinear logic, the Lambek-style one as above, and what we call "Grishin categories", BILL and GILL in the paper. Both amount to different presentations of *-autonomous cats.) So, in the non-Cartesian context, suitable duals to exponentials are anything but boring ... -= rags =- -- <rags@math.mcgill.ca> <www.math.mcgill.ca/rags> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Also, in logic, "and" goes in pair with "or", "for all" goes in pair with "there exists". But implication is always left alone. Why is it so?
I am afraid logic is polyamorous: 1. "and" goes with "implies" because they are adjoint. 2. "and" goes with "or" because they are dual. By the way: 1. "forall" goes with "weakening" because it is adjoint to it on the right. 2. "exists" goes with "weakening" because it is adjoint to it on the left. But why is "forall" dual to "exists"? With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Wed, 9 Nov 2011, Andrej Bauer wrote:
Also, in logic, "and" goes in pair with "or", "for all" goes in pair with "there exists". But implication is always left alone. Why is it so?
I am afraid logic is polyamorous: ... By the way:
1. "forall" goes with "weakening" because it is adjoint to it on the right. 2. "exists" goes with "weakening" because it is adjoint to it on the left.
What's the definition of "weakening"? I've not seen this word used formally.
... Andrej
Thanks Jocelyn [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
1. "forall" goes with "weakening" because it is adjoint to it on the right. 2. "exists" goes with "weakening" because it is adjoint to it on the left.
What's the definition of "weakening"? I've not seen this word used formally.
-> A to the subobject M x B >-> A x B, i.e., it is pullback along the
Weakening is the map Sub(A) -> Sub(A x B) which takes a subobject M projection pi1 : A x B -> A. The existential quantifier over B is the left adjoint to weakening, where Sub(A) and Sub(A x B) are viewed as posetal categories. The universal quantifier is the right adjoint. Working out the details in Set is instructive. As far as I know the terminology comes from logic. The rule of weakening says that a logical derivation may be "wakened" with an additional (but unneeded) hypothesis: Gamma |- A ---------------------- Gamma, H |- A With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 11/9/2011 4:45 PM, Jocelyn Ireson-Paine wrote:
What's the definition of "weakening"? I've not seen this word used formally.
I had the same question about "boring", which came earlier. I believe "sleeping" comes later, then "dreaming," "awakening," and so on. Eventually the lecture ends and we either resume elsewhere with "boring" or move on to "eating." Vaughan [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Vaughan, An excellent remark, once again from your side. The general audience of this remark may, however, not identify the subtlety of these states with respect to modelling of parallel programs and what apparently now happens on clouds and grids with services and brokers, and not even to mention customers using these services. So perhaps I may suggest to recall e.g. the dining philosophers paradigm, which was widely used during the early days of CSP (Communicating Sequential Processes) decades ago. The philosophers go through only three states, namely, thinking, getting hungry (and thereby stop thinking), and eating. After eating then go back to thinking, and so on. They use chopsticks, one by one (in a very non-Asian fashion), and communicate about using these resources with fellow philosophers around the table. Simple objectives are e.g. to avoid starvation. The relationship between states you mention is much more elaborate, they overlap, and it is not entirely clear when one state is over, and another one begins. I would even say that some of these states, in the sense of being members of a "set of states", call for more structure in underlying categories. Perhaps you already thought about transforming this into a new paradigm. I seriously think it would be a challence to the CSP programmers (some of them fascinated e.g. by Goguen's institutions!) to encode some behaviour involving those states in conventional CSP, and making the observation that we may need additional language constructions, and more underlying structures. The parallel paradigm is still all too non-categorical. Cheers, Patrik On Sat, 12 Nov 2011, Vaughan Pratt wrote:
On 11/9/2011 4:45 PM, Jocelyn Ireson-Paine wrote:
What's the definition of "weakening"? I've not seen this word used formally.
I had the same question about "boring", which came earlier. I believe "sleeping" comes later, then "dreaming," "awakening," and so on. Eventually the lecture ends and we either resume elsewhere with "boring" or move on to "eating."
Vaughan
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 14/11/2011 9:36 AM, Patrik Eklund wrote:
Dear Vaughan,
An excellent remark, once again from your side.
The general audience of this remark may, however, not identify the subtlety of these states with respect to modelling of parallel programs and what apparently now happens on clouds and grids with services and brokers, and not even to mention customers using these services.
So perhaps I may suggest to recall e.g. the dining philosophers paradigm, which was widely used during the early days of CSP (Communicating Sequential Processes) decades ago. The philosophers go through only three states, namely, thinking, getting hungry (and thereby stop thinking), and eating. After eating then go back to thinking, and so on. They use chopsticks, one by one (in a very non-Asian fashion), and communicate about using these resources with fellow philosophers around the table. Simple objectives are e.g. to avoid starvation.
My recollection was that there were two versions - "dining philosophers" who had shared access to two forks, either one of which sufficed; and "dining Chinese philosophers" who had shared access to two chopsticks of which both were needed. But perhaps I have got it wrong? Robert [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
David Leduc wrote:
On Mon, Nov 7, 2011 at 07:59, Ross Street <ross.street@mq.edu.au> wrote:
The conjecture is false. Take any category E where exponentiable is interesting. Then the dual of exponentiable is not boring in E^op.
Indeed! And this is clearly true of the example given by Thomas, namely Set^op.
However, I am not yet satisfied. Let me precise my thoughts. In the textbooks and lecture notes on category category that I have read, there are always product and coproduct, pullback and pushout, equalizer and coequalizer, monomorphism and epimorphism, and so on. However exponential is always left alone. That is why I assumed it is boring. If it is not boring, why is it never mentioned in textbooks and lecture notes on category theory?
For what it's worth, I have seen such co-exponentials natually occur in programming language semantics. They seem to occur in certain extensions of lambda calculus. More specifically, in call-by-value functional programming languages with call/cc style control operators. When I say they occur "naturally", I mean that they exist in such languages, not that they are typically used in any meaningful way by programmers. Very roughly speaking, in such languages, if A is a type, then (not A) is the type of environments that can consume an element of type A and then proceed with some task (called a "continuation" for A in programming language lingo). A continuation for a function f : A -> B is a pair of type A * (not B). In other words, an environment hoping to interact with some function has to supply (1) an input to the function, which is of type A, and (2) some task to complete after receiving the output, i.e., something of type (not B). It so happens that in a call-by-value language with sufficient support for continuations, there will be a one-to-one correspondence between programs of type (A * not B) -> C and programs of type A -> B + C. This is spelled out in long and very technical detail in my paper "Control categories and duality" [1], sections 4.2 (definition of co-control categories) and 7.3 (the call-by-value lambda-mu-calculus is an internal language for co-control categories). The idea itself is 10 years older and is due to Andrzej Filinski [2], where co-exponentials appear explicitly on p.33, second paragraph. [1] http://www.mathstat.dal.ca/~selinger/papers.html#control [2] http://www.diku.dk/hjemmesider/ansatte/andrzej/papers/DCaCD.ps.gz -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (14)
-
Andrej Bauer -
David Leduc -
Jocelyn Ireson-Paine -
Patrik Eklund -
Paul Taylor -
Prof. Peter Johnstone -
Reinhard Boerger -
RJ Wood -
rjwood＠mathstat.dal.ca
-
Robert Dawson -
Robert Seely -
selinger＠mathstat.dal.ca -
Uwe.Wolter＠ii.uib.no -
Vaughan Pratt