Re: pratt cat

Re: pratt cat

[categories]

Date: Fri, 31 Oct 1997 01:03:22 -0800
From: Vaughan R. Pratt <pratt@cs.Stanford.EDU>


Peter's response to my question about categories having all the common
properties of toposes and abelian categories was a very pleasant
surprise.

First I was not at all expecting such a definite answer.

Second I did not expect a representation theorem, especially not such a
nice one as "every such category is a product of an abelian category
and a topos".  This is the converse of the automatic (by Horn) fact
that such a product is such a category, where (for this converse at
least) the language can be taken to be as large as the full Horn theory
common to abelian categories and toposes.

Third I did not expect at all that the class would be finitely
axiomatizable (but on the other hand neither did I have any reason to
suppose not).

Fourth and very nice, unless I'm overlooking something, Peter's
representation theorem implies that my original question (does the
common *elementary* theory allow anything other than abelian categories
and toposes?) can now be answered in the negative.  The elementary
sentence "either all the objects are A-type or all the objects are
T-type" is obviously true in both abelian categories and (pre)toposes,
and rules out hybrids like Set x Ab.  I'd been wondering what
elementary sentence might fail for that example, and Peter's A-type and
T-type constructs lead straight to it.

Minor remarks:

The trick of multiplying by 0 to tease out both the A- and T-components
at once is beautiful, not just intrinsically but also because it
reveals a certain duality between A and T that is not at all apparent
(to me anyway) from their separate definitions.  The actual
multiplication projects out the T part without disturbing the A part,
and then the pushout 

                    AX		(where AX = 0xX)
                   /  \
                  0    X
                   \  /
                    TX

neatly quotients out that surviving A part by forcing the left side
through the zero object while on the right AX->X communicates only the
A part which is therefore the only part that the pushout quotients out
from 0 + X (if that's not too clumsy a way of putting it).

The upshot is then that the AX's form (as an abelian category) a
coreflective subcategory of the whole while the TX's form (as a
pretopos) a reflective subcategory.  That's really beautiful!

The following is presumably the key to proving completeness of Peter's
axiomatization...

>VAE) For every  X  there's a map  TX -> X  such that 
>
>                    AX     TX
>                      \   /
>                        X

...by permitting any model to be constructed directly as a
product of an abelian category and a topos (not even "subcategory"
seems to be needed here, so this is an even stronger representation
theorem than the representation of a Boolean algebra as a subalgebra of
a power set).

>And note that the type-A objects can not be 
>reflective: if  1  has a map to any type-A object the entire category
>collapses.

Whoops, a bug here if I'm understanding things.  Only the T part
collapses, if the category were abelian to begin with then there'd be
no collapse.

>Define  TX -> X  as the image of rX.

This was lovely (getting rid of the E in VAE above).


Some questions.

1.  Can this representation theorem be extended to the full Horn
theory, i.e. any number of alternations of quantifiers?  (Note that my
disjunction---every object is A-type or every object is T-type---is not
a Horn sentence.)  (Now that I look again, I guess the answer must be
yes, since products preserve *all* Horn sentences.)

2.  In a text that treated both toposes and abelian categories, would
your axiomatization be a good starting point prior to doing either?
You could then quickly define an abelian category to be a category of
this general type with the additional property of being strongly
connected.  I don't see right off how to define a pretopos as slickly.

3.  What about bringing in the closed structure?  Might that permit
some simplification of your axiomatization?  For example it looks as
though you could define a T-type object to be one having a unique map
to the tensor unit.  Then you could answer the last sentence of the
previous paragraph simply with "the tensor unit is terminal."

Vaughan Pratt

pratt cat

[categories]

Date: Thu, 30 Oct 1997 16:39:48 -0500 (EST)
From: Peter Freyd <pjf@saul.cis.upenn.edu>

Vaughan wrote:

  To the extent that both toposes and abelian categories share much
  pleasant structure, the models of the intersection of their
  theories, for a suitable choice of language, would seem to be a nice
  class in its own right.

There are several variations on the topic. I'll look first at the
theory obtained by starting with 

  finite completeness,
  coterminator,
  pushouts for pairs of maps one of which is monic,
  pushouts for kernel pairs

then adjoining all universal Horn sentences in these predicates that
hold for both the category of abelian groups and the category of sets
(or, if prefered, hold for all abelian categories and all pre-topoi).
We will see that this theory can be finitely axiomatized and that the
representations of its models into the categories of abelian groups
and sets are collectively faithful. This will be the "first task.
The representation will be done by finding a single faithful
representation into the product of an abelian category and a topos and
using known theorems thereon. By a representation I here mean a
functor that preserves finite limits, coterminators, pushouts of pairs
of maps one of which is monic and pushouts of kernel pairs. (It
follows that a representation preserves epimorphisms, finite
coproducts and images.)

If we expand the theory to include all positive AE sentences it
remains finitely axiomatizable, and the only models are those
categories that are a product of an abelian category and a pre-topos.
This will be the "second task".

After that, I'll add some more essentially algebraic structure so that
we can talk about power-objects using universal Horn sentences and
obtain again the finite axiomatizability and the fact that the the
only models are those categories that are a product of an abelian
category and a pre-topos. This will be the "third task".

Note that each of axioms below is true for both abelian categories and
topoi. Until we reach axiom VAE, all can be turned into universal
Horn sentences if the completeness conditions listed above are turned
into an essentially algebraic theory.

V1) Effective regular category. (Yes this can be stated as universal
Horn conditions on pullbacks and the special pushouts mentioned
above.)

V2)  0 -> 1  is monic.

Note that it follows that all maps from  0  are monic.

In the diagrams below all non-horizontal lines should have arrows
added in downwards direction.

V3) If  A -> C  is monic and 
                              A
                            /   \
                           B     C
                            \   /
                              D

is a pushout then it's a pullback, 

V4)  and so is
                             0xA
                            /   \
                         0xB     0xC
                            \   /
                             0xD.


Note that binary coproducts therefore exist and are disjoint.

V5) If  B -> 0xC  is epic and
                               A
                             /   \
                            0     B
                             \   /
                              0xC

is a pullback then it's a pushout.

Two definitions: let
                        0 x X
                       /     \
                      0       X
 
be a product diagram. If the map to  0  is an iso, I'll say 
that  X  is type-T; if the map to X is an iso, I'll say that
it's type-A. 

Note that (using V2) an object is type-A iff it has a map to  0. The
type-A objects are closed under binary products and coproducts,
subobjects and quotient objects. The full subcategory of A objects is
coreflective, with  AX = 0xX  as coreflector. Most important, it is an 
abelian category.

V5) If the rhombi in
                     A     B
                     |\   /|
                     D  C  E
                      \ | /
                        F
are pullbacks and if 
                     D     E
                      \   /
                        F

is a coproduct diagram, and if all the objects are type-T
then 

                     A     B
                      \   /
                        C

is also a coproduct diagram.

Note that an object is type-T iff every type-A object has a unique map
thereto. Type-T objects are closed under binary products and
coproducts, subobjects and quotient objects. (For coproducts use V3.)
The full subcategory of type-T objects forms a reflective subcategory:
the reflector, T, is defined via the pushout diagram:

                    0xX
                   /   \
                  0     X
                   \   /
                     TX

One now has what's needed to show that the full subcategory of type-T
objects is a pre-topos.

Note that the functor  A  preserves pullbacks and pushouts
of pairs of maps one of which is monic (V4). Add 

V6) T preserves pullbacks.

(It clearly preserves pushouts.)

Only one more axiom is needed for the first task:

V7)  If  f  is a map such that  Af  and  Tf  are both isos then
f  is an iso.

For the second task add:

VAE) For every  X  there's a map  TX -> X  such that 

                    AX     TX
                      \   /
                        X

is a coproduct diagram.

Note that  TX -> X  is a coreflector (making V6 redundant). One can
force the map to be unique by further requiring that  TX -> X -> TX
is the identity map. And note that the type-A objects can not be 
reflective: if  1  has a map to any type-A object the entire category
collapses.

For the third task, I'll add the following structure: functions
on objects P,E,l, r such that  lX:EX -> PX  and  rX:EX -> X  and 

V8)  <lX,rX>:EX -> PXxX  is monic and  PX, EX  are type-T.

I need one more operation, denoted with an upcase lambda, here 
written as  /\.  Given a pair of maps  f:R -> Y, g:R -> X
where  R  is of type-T, then  /\(f,g): Y -> PX  is defined and 

V9> The composition of relations

       /\(f,g)        (lX)'         rX
   Y  ----------> PX -------> EX ---------> X

is equal to 
         f'         g
   Y  -------> R --------> X

(where  '  is being used to denote the reciprocation operator on
relations).

V10) If
             R
         f /   \ g
          Y     EX
         h \   /lX
            TX

is a pullback and R of type-T, then  /\(f,(rX)g)  = h.

Note that in the full category of type-T objects, P  yields
power-objects with  E, l, r  naming the universal relations. (V10 
provides the uniqueness condition.)

In any abelian category the only type-T object is the zero
object, which forces  P=E=0  for abelian categories.

It's routine that both  A  and  T  preserve the new structure. We can
now remove the existential from VAE. Define  TX -> X  as the image of
rX. The third task is finished with:

V11) For every  X  

                    AX     TX
                      \   /
                        X

is a coproduct diagram.



These axioms will, no doubt, be much simplified.