Subject: defining sets from abelian groups

From: categories <[email-masked]>
Date: Sun, 17 Mar 1996 22:21:20 -0400 (AST)

Date: Sun, 17 Mar 1996 08:54:16 -0800
From: Vaughan Pratt <[email-masked]>

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

---

From: categories <[email-masked]>
Date: Mon, 18 Mar 1996 10:35:22 -0400 (AST)

Date: Mon, 18 Mar 1996 07:47:40 -0500
From: Peter Freyd <[email-masked]>

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).

---

From: categories <[email-masked]>
Date: Mon, 18 Mar 1996 10:50:43 -0400 (AST)

Date: Mon, 18 Mar 1996 09:39:51 -0500
From: Michael Barr <[email-masked]>

- 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

---

From: categories <[email-masked]>
Date: Mon, 18 Mar 1996 16:08:05 -0400 (AST)

Date: Mon, 18 Mar 1996 13:28:17 -0500 (EST)
From: [email-masked]

   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

---

From: categories <[email-masked]>
Date: Mon, 18 Mar 1996 16:30:37 -0400 (AST)

Date: Mon, 18 Mar 1996 10:46:38 -0800
From: Vaughan Pratt <[email-masked]>

	category of sets.

Peter Freyd succinctly shows you can't with

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

---

From: categories <[email-masked]>
Date: Tue, 19 Mar 1996 21:00:30 -0400 (AST)

Date: Tue, 19 Mar 1996 15:12:22 -0500 (EST)
From: Andre Joyal <[email-masked]>

Peter Freyd's assertion
> Let  Gr  be the category of all groups,
> abelian or not. Then:
> 
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