defining sets from abelian groups
I want to say something along the lines of "You can define abelian groups in the internal logic of Set, but you can't define sets in the internal logic of Ab." Is this intuition supportable? Ideally there would be a precise technical sense in which it is provably the case. Vaughan Pratt
Vaughan says -- correctly I think -- that "you can't define sets in the internal logic of Ab." I suspect that the proof will have to use the dualities that reside in Ab. Let Gr be the category of all groups, abelian or not. Then: The category of co-groups in Gr is equivalent to Set. Cf: The category of co-groups in Ab is equivalent to Ab. "Co-group" means, of course, "group in the opposite category". The second of the two assertions above holds for any additive category: it's easy to show that each object in any additive category has a unique co-group (indeed, a unique co-monoid) structure (the co-multiplication is the diagonal map). I know no citation for the first assertion. To prove it, one shows that the only groups with co-group structures are free groups and that the only co-multiplication on Free(X) is such that X -> Free(X) -> Free(X+X) is the point-wise product of the two functions of the form X -> X+X -> Free(X+X).
- I want to say something along the lines of "You can define abelian - groups in the internal logic of Set, but you can't define sets in the - internal logic of Ab." - - Is this intuition supportable? Ideally there would be a precise - technical sense in which it is provably the case. - - Vaughan Pratt - - I don't know, since I don't understand these issues sufficiently well, but if you can define the free abelian group cotriple, you can then define the coalgebra category for that cotriple and that is the category of sets. In fact, that is a ! operation, in Girard's sense, on the fragment of linear logic that Ab satisfies. (This last was an observation of Jim Otto's.) Michael Barr
In the Spring of 1971 at Chicago, Peter Freyd gave some very interesting lectures in which he showed how to construct a topos from a symmetric monoidal closed category by considering certain structured co-commutative co-algebras. This was done in such a way that for a group G one could recover the topos of G-sets (and hence the group itself) from the category of linear representations. Since the category of abelian groups has a unique closed monoidal structure, this should refute Vaughan Pratt's conjecture. It should have even many more applications than that, which is why I have long urged Peter to write it up. Bill Lawvere
I don't know, since I don't understand these issues sufficiently well, but if you can define the free abelian group cotriple, you can then define the coalgebra category for that cotriple and that is the category of sets. Peter Freyd succinctly shows you can't with The category of co-groups in Ab is equivalent to Ab. Interesting that Peter used duality to prove it, since my reason for strongly believing it was also duality-based. The general principle I used for my reasoning was that the only categories "definable" in the internal logic of a self-dual category are full subcategories of it. FinAb is self-dual, but FinSet does not fully embed in FinAb. If only I knew what "definable" meant this would be a proof. I came to appreciate this principle while investigating Chu(Set,K). All notions of "definable" I understand (e.g. first order definable) are subsumed by this principle. However that's not sufficient reason to call it a theorem, since someone may have a method of definition I don't know about that violates it. For example I have not yet figured out whether the method of sketches violates it, though I can't imagine how it could. In fact, that is a ! operation, in Girard's sense, on the fragment of linear logic that Ab satisfies. (This last was an observation of Jim Otto's.) Is Jim's statement even well-defined? ! is a functor projecting LL onto a cartesian closed full subcategory of itself. For the above to make sense you would need a full embedding of the coalgebra category, namely Set, back into Ab. But unless I'm dreadfully confused (which I often am) there isn't such. What could a set reasonably be other than the free abelian group on it? But when you're inside Ab, Ab(G,H) = H for H a fag, so that's not it. Similar deal with Rel or CSLat. I was dreadfully confused about this in 1991 when I first got involved with duality via CSLat and their sibling Event spaces. I wish someone had pointed out to me that my ! *didn't* produce a cartesian closed category as I was claiming. Instead I had a long period of waiting for my vision problems to clear up. Adding ! to LL stretches LL out a lot, much wider than Ab with respect to the Stone gamut (the Set<->Set\op axis). Enough in fact to make it look rather like Chu(Set,K) for indefinite K, less such amenities as induction and such obscurities as 1 par 1 |- 1 (noticed by Lafont and Streicher---with its contrapositive _|_ |- _|_ @ _|_, the two objects 1 par 1 and _|_ become sort of the "two halves" of a single coalgebra in Chu(Set,K)). You just have to take the bad with the good when you have a nice model like Chu(Set,K). I've incorporated my proof that Set is a bicomplete equational topos (meaning one with all natural isos identities) into my LL'96 paper, "Linear Logic complements Classical Logic," sent off last night. In the light of Peter Johnstone's remarks it seemed prudent to add an explanatory paragraph as a sort of talisman against the nonmonotonic logic of antiChoice fundamentalism extolled on Sundays. This is now available as ftp://boole.stanford.edu/pub/llcocl.ps.gz, with tex and dvi counterparts in the usual subdirectories, /pub/TEX and /pub/DVI. I'll post the abstract here shortly, or look it up yourself in the file ABSTRACTS in the same directory. This is paper 45 in that directory, getting time to compress its scattered ideas down a bit. Vaughan Pratt
Peter Freyd's assertion
Let Gr be the category of all groups, abelian or not. Then:
The category of co-groups in Gr is equivalent to Set.
is slightly incorrect. A better formulation should use the category $Set_*$ of pointed sets instead of $Sets$. As such this is essentially an old result of Peter Hilton and Beno Eckmann. They proved that any cogroup in the category of groups is free. I would like to say that the younger generation is not always aware that Eckmann and Hilton have fundamental contributions to category theory. They have provided basic examples of objects equipped with algebraic structures in categories. Consequently opening the road to further abstractions, like the concept of algebraic theory in the sense of Lawvere. Among other things, Eckmann and Hilton where interested in identifying all cogroups in the homotopy category $hTop_*$ of pointed topological spaces. A basic example of such cogroup is the circle $S^1$. It explains why the functor $\pi_1(-)=[S^1,-]:hTop_*\to Sets$ has a natural group structure. If $G$ is a cogroup in $hTop_*$ then so is the smash product $X\smash G$ for any pointed topological space $X$ This is because $X\smash(-)$ preserves coproduct since it has a right adjoint (here we are supposing that Top is a convenient category of topological space). In particular, the spheres $S^{n+1}=S^n\wedge S^1$ have a cogroup structure. Any wedge (topologists call the coproduct the wedge) of cogroups is obviously a cogroup. In particular, any wedge of spheres of dimension $n\geq 1$ has a co-group structure. All the known examples of cogroups in $hTop_*$ are obtained by taking a smash $X\smash S^1$. It was conjecture by Eckmann and Hilton that all cogroups in $hTop^*$ are of the form $X\smash S^1$. They observe that $\pi_1(G)$ is a cogroup in $Groups$ when $G$ is a cogroup in $hTop_*$. This is because the functor $\pi_1: hTop_*\to Groups$ preserves coproducts by Van Kampen theorem. In support to their conjecture they proved that any cogroup in $Groups$ is free. It follows that all cogroups in $Groups$ are of the form $\pi_1(X\smash S^1)$ where $X$ is a pointed set. Andre Joyal
participants (6)
-
Andre Joyal -
Michael Barr -
MTHFWL＠ubvms.cc.buffalo.edu -
Peter Freyd -
Vaughan Pratt -
Vaughan Pratt