Re: Abelian-topos (AT) categories

[categories <cat-dist@mta.ca>]

Date: Mon, 03 Nov 1997 21:57:20 -0800
From: Vaughan R. Pratt <pratt@cs.Stanford.EDU>


I appreciate that there are people on the list with more years of
experience with abelian categories than I have days.  AC's don't seem
to have penetrated much into computer science, and I have no idea
whether they need to.

But the finite axiomatizability of the quasivariety generated by Set
and Ab definitely has my attention.  And the fact that toposes and
abelian categories, so far apart intuitively (sets vs. abelian
groups?), are brought to within so short an axiom of each other by the
definition of AT cats, has the potential to make abelian categories
much more relevant to fans of toposes.

Peter (and privately Fred Linton and Mike Barr) have answered my
question about what I was naively calling "abelian closed".  "Abelian"
and "cartesian" are not interchangeable adjectives inasmuch as the
latter describes the tensor product in the context of "cartesian
closed" while the former names a quasivariety.  While I was aware of
the distinction, I was hoping that abelian categories as the models of
the universal Horn theory of Ab, combined with Ab having closed
structure, would somehow make the juxtaposition "abelian closed"
meaningful, but the examples show this to be wishful thinking.  And
Peter's

	define  TX  as the image of  rX

removes any motivation to define TX as 1@X.  (Meanwhile I've reconciled
myself to TX as the pushout of the projections of 0xX.)

>After saying that it's a regular category with a coterminator contained
                          ^^^^^^^  [Is "effective" not needed? -v]
>in its terminator, I'd start with the  P-E-l-r-/\  structure as in my
>last post, and prove it to be the correflection of X into the full
>subcategory of type-T objects.  0xX -> X  is easily seen to be the
>correflection of  X  into the full subcategory of type-A objects. Then
>the axiom that these two correflections yield a coproduct decomposition
>for each object allows one to prove quickly that the category is the
>cartesian product of the two correfletive subcategories. The type-T
>objects clearly form a topos. All that's needed now is a couple of
>axioms to make the type-A objects abelian.

Not just finitely axiomatizable but beautifully so.

Vaughan