Uday Reddy poses the following (with a few changes in notation]:
Consider a monoid <M,*,e> in a CCC. The operations of interest are natural transformations E:[-,M] -> M that satisfy the following equations (in the internal language of the CCC):
E_A(\x.e) = e E_A(\x. a * gx) = a * E_A(g) E_A(\x. gx * a) = E_A(g) * a E_A(\x. E_B(\y.hxy)) = E_B(\y. E_A(\x.hxy))
I wonder if naturality is really desired: it would seem to force M to be trivial. By the familiar Yoneda-lemma argument, E must be constant as far as the "points" of [A,M] are concerned. (Actually one doesn't need the argument, just the lemma itself; consider the transformation that E induces between set-valued functors (-,M) -> (1,M); Yoneda says it must be constant.) The condition E_A(\x.e) = e forces just which constant it is. That is, for any f:A -> M it will be the case that E_A will send f to e. But then either condition E_A(\x. a * gx) = a * E_A(g) or E_A(\x. gx * a) = E_A(g) * a will force M to be trivial. (It's clear in the \-calculus notation. But that argument would be implicitly using the fact that E_A is constant and we officially know only that it's constant on points. So take, say, the second condition. It says in diagrammatic language: 1 x K P [A,*] [A,M] x M -----> [A,M] x [A,M] ---> [A,MxM] -----> [A,M] | | | E_A x 1_M | E_A | | * M x M ----------------------------------------> M where K is the standard "constant-map" operator that's adjoint to the projection AxM -> M and P is the standard operator that defines MxM (given products in Set). Specialize to A = M and precompose with <f,1>: M -> [M,M] x M where f doesn't matter. If the commutative rectangle above is chased clockwise one obtains the map constantly valued e. Chased counterclockwise one obtains the identity map. And, of course, it didn't matter what f is.)
Response by Peter Freyd to a question of mine:
Consider a monoid <M,*,e> in a CCC. The operations of interest are natural transformations E:[-,M] -> M that satisfy the following equations (in the internal language of the CCC):
E_A(\x.e) = e E_A(\x. a * gx) = a * E_A(g) E_A(\x. gx * a) = E_A(g) * a E_A(\x. E_B(\y.hxy)) = E_B(\y. E_A(\x.hxy))
I wonder if naturality is really desired: it would seem to force M to be trivial.
Indeed! (Peter Johnstone and Dusko Pavlovic also pointed out that I went wrong in asking for naturality.) Something got lost in abstracting from my application domain. My examples had additional parameters which made naturality possible. But, discarding those parameters in the interest of abstration seems to have produced a statement that is quite impossible to satisfy. My apologies. Dusko Pavlovic pointed out some of what we could do once we discard the naturality condition. The second and third equations can be regarded as naturality properties by thinking of M and [A,M] as categories and E_A as a functor. (That is good, because it singles out the first equation as a "pretender." So, I shouldn't be worried when it breaks.) On the other hand, I don't know what to make of the fourth equation. It says that for E_A to be an abstraction operator (tentatively using Pavlovic's terminoloty), it has to commute with every other abstraction operator E_B. For one, that prevents me from giving a local definition of what an abstraction operator is. One needs to define the whole collection of abstraction operators at one go. (Now that naturality is gone out the window, there is no reason to require even that the family of operators be indexed by objects. There could be any number of maps for an object A.) Secondly, looking at it from the application point of view, there is something "intrinsic" about these operators that makes them commute with each other. It is not really a property of the whole collection of operators. The presence or absence of another operator in the collection shouldn't matter. I really have no idea how to capture this kind of "uniformity" in the commutativity property. Some hyperdoctrine-like idea, perhaps? Despite the fact the first equation doesn't hold in all toposes, I think the example of the existential quantifier is an illuminating one. Evaluation at a particular point is a "degenerate" example in that it also satisfies E_A(\x. fx * gx) = E_A(f) * E_A(g) The existential quantifier gives a better intuition for the idea of these operators. Hope this explains the question better. Uday Reddy
participants (2)
-
Peter Freyd -
Uday S. Reddy