* pratt cat
@ 1997-10-31 2:32 categories
0 siblings, 0 replies; 2+ messages in thread
From: categories @ 1997-10-31 2:32 UTC (permalink / raw)
To: 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.
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: pratt cat
@ 1997-10-31 19:39 categories
0 siblings, 0 replies; 2+ messages in thread
From: categories @ 1997-10-31 19:39 UTC (permalink / raw)
To: 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
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~1997-10-31 19:39 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1997-10-31 2:32 pratt cat categories
1997-10-31 19:39 categories
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).