Date: Fri, 19 Aug 1994 14:16:00 +0500 (GMT+4:00)
Subject: Gordon Plotkin
Date: Thu, 18 Aug 94 09:51:00 BST
From: John Power
Those category theorists involved with computer science may like to hear
the happy news that Gordon Plotkin was married to his long time friend
Hephzi last weekend in California. They now live in Edinburgh, with summer
visits to California.
John Power.
Date: Tue, 23 Aug 1994 09:43:16 +0500 (GMT+4:00)
Subject: duality in 2-categories
Date: Mon, 22 Aug 94 17:07:58 PDT
From: john baez
Does anyone know a good treatment of duality in 2-categories?
I'm interested in situations where the objects have duals
but also the objects in the Hom-categories have duals. I
guess Fischer discusses this in his paper on 2-categories and
2-knots, but I'm looking for a more detailed and extended
treatment.
Regards,
John
Date: Sun, 28 Aug 1994 13:01:48 +0500 (GMT+4:00)
Subject: distributivity
Date: Sat, 27 Aug 94 14:47:55 EDT
From: Michael Barr
I pass on to you a curious fact that was mentioned to me by Richard
Squire and he credited it to Jim Loveys. Let P and Q be quantifiers.
(What is a quantifier? Well as a first approximation it is a map from
X--o L to L which is in some obscure (to me) sense polymorphic. Limits
(both in categories and posets), integrals and, evidently, univeral and
existential quantifiers in logic, where L is the object of truth values.
Looking at all the examples, you realize immediately that polymorphism
is certainly not functoriality and if some of them give inequalities or
morphisms, they do so in different directions (say SUP vs INF or A vs
E).)
Well, anyway, P and Q are quantifiers. Say that P distributes over
Q if there is an equation
P(x:X).Q(y:Y).f(x,y) = Q(s:X--o Y).P(x:X).f(x,s(x))
One aspect of polymorphism is that this makes sense. Here f: X x Y
--> L and if treat this as a map Y --> (X--o L), then the LHS makes
sense. As for the RHS, we are doing the same thing with X x (X--o Y)
--> X x Y --> L, where the first map is and the second is f.
Here are 2 1/2 examples: If P is universal quantification, Q is
existential and L is the object of truth values in a topos, then this is
the axiom of choice. If P is sup in a lattice and Q is inf and if X and
Y are restricted to finite sets, then this is the statement of
distributivity. If P is SUP in a complete lattice and Q is INF, then
this is the complete distributivity identity. Now here is the startling
fact. In all three cases, the distributivity of P over Q implies that
of Q over P! For the lattices, these facts are well-known. For the AC,
it is easy to see (at least in a boolean topos) since you can negate and
replace f by its complementary relation. (Yes a topos that satisfies AC
is boolean, but it does not immediately follow that these two
complementary conditions are equivalent, since perhaps only one of them
implies AC in the non-boolean case.) This doesn't always hold. For
example, in a topos, finite products distribute over (finite) sums, but
the converse is certainly false.
Date: Mon, 29 Aug 1994 15:35:16 +0500 (GMT+4:00)
Subject: Top\op is a quasi-variety
Date: Sat, 27 Aug 94 14:47:11 EDT
From: Michael Barr
by Michael Barr and M. Cristina Pedicchio
We show that there is a certain variety (= category tripleable over
sets) and a simple Horn sentence in it of the form phi(u) = phi(v) ==>
psi(u) = psi(v) whose category of models is equivalent to the opposite
of topological spaces. The theory consists of that of frames together
with a unary operation we denote ' (it is a kind of pseudocomplement)
satisfying a small set of equations plus an equation scheme that forces
all intervals of the form [u /\ u',u \/ u'] to be complete atomic
boolean algebras with the Sup and ' as operations. The underlying set
functor on Top\op takes a space to the set of all pairs (U,A) where U is
open and A is an arbitrary subset of U. The frame operations are the
usual, while (U,A)' = (U,U - A). The Horn clause is u \/ u' \/ 1' = v
\/ v' \/ 1' ==> u \/ u' = v \/ v'.
[note from moderator: Michael says the paper will be available by ftp from
triples.math.mcgill.ca soon.]
Date: Mon, 29 Aug 1994 15:36:20 +0500 (GMT+4:00)
Subject: Partial Topos
Date: Mon, 29 Aug 94 18:37:23 +0200
From: Thomas Streicher
Dear All,
I'd like to know whether the following is aloready well known ?
Around 1980 in a lecture course at Louvain-la-Neuve Jean Benabou
introduced the notion of partial topos. He defined it as a category
IB with pullbacks such that each slice is an elementary topos and the
reindexing functors f* are logical and have right adjoints Pi_f .
One immediately can see that it is enough to claim that each slice is
an elementary topos :
slices having products means that one has pullbacks
and for any f : J -> I the reindexing functor f* is logical and
has a right adjoint as it is isomorphic to the functor
(f : f -> id_I)* : (IB/I) -> (IB/I)/f
which is the inverse image part of a local homeomorphism.
Nevertheless this definition of partial topos as a category all whose
slices are toposes has a certain defect - pointed out by Benabou
himself - namely that ANY groupoid is a partial topos as it has
pullbacks and any slice is the trivial topos.
Now what is a natural condition ruling out this defect.
I propose the following condition
(Weakening) for any I the forgetful functor Sigma_I : IB/I -> IB
has a right adjoint I* : IB -> IB/I
I call this weakening as any category with pullbacks is a model of
extensional type theory not allowing empty contexts (which would be
interpreted as the (non-existing) terminal object). Nevertheless we
would like to have weakening by a type which corresponds to the rule
Gamma |- B A a type
---------------------------
A , Gamma |- B
the categorical semantics of "weakening by A" is applying the right
adjoint to Sigma_A : IB/A -> IB.
LEMMA 1 An ARBITRARY category IB has weakening iff IB has binary
products.
Proof : If Sigma_I -| I* then I*X : I*X -> I is the first
projection and the counit eps_X : I*X -> X is the second
projection.
end_of_proof
Now the condition of weakening rules out nontrivial groupoids.
LEMMA 2 If IB is a groupoid satisfying weakening then for any I
in IB the functor Sigma_I : IB/I -> IB has a right adjoint and
therefore preserves colimits. Now id_I considered as an object of
IB/I is initial and therefore I = Sigma_I(id_I) is initial.
Thus all objects of the groupoid are initial and the groupoid is
trivial.
end_of_proof
This suggests the following new
DEFINITION A category IB is a PARTIAL TOPOS iff
(i) any slice of IB is a topos
(ii) IB has weakening, i.e. all binary products.
Immediate consequences of the definition :
LEMMA 3 Let IB be a partial topos. The the following hold
(i) IB has equalizers
(ii) any finite diagram in IB has a colimit iff
it has at least one cocone
(iii) IB / O is trivial
(iv) if f : A -> B and the exponential object B^A exists
then IB has a terminal object .
In more elementary terms partial toposes can be characterized as
follows.
LEMMA 4
IB is a partial topos iff
(i) IB has pullbacks and binary products
(ii) any f* has a right adjoint Pi_f
(iii) for any I the category IB/I has a subobject classifier
(i.e. there exists an epi Omega_I : Omega_I -> I
split by T_I : I -> Omega_I such that
for any f : A -> I and subobject m : A' >--> A
there exists a unique morphism chi : A -> Omega_I
with chi ; Omega_I = f and m = chi*T_I )
Proof : (ii) is equivalent to any slice being cartesian closed.
EXAMPLES of Partial Toposes
(i) (Benabou 1980)
Let IE be an elementary topos and F a nonempty downward closed
subset of Sub_IE(1). Let IE_F be the full subcategory of IE
consisting of those subobjects X s.t. support(X) is in F .
Then IE_F is a partial topos.
Taking IE = Set^I and for F the subsets of I containing at
most one element (the downward closure of the atoms in Sub_IE(1))
then IE/F is not closed under finite sums.
(ii) the category of finite trees is a partial topos
(Benabou, private communication)
(iii) the category of spaces and local homemorphisms
is a partial topos
(cf. mail of Freyd in April '94 on CATEGORIES)
(iv) the category of small (finite) categories and
discrete fibrations is a partial topos
(the slice over C is equivalent
to the topos of (finite) presheaves over C)
binary products can be constructed by showing that for any C
Sigma_C has a right adjoint; the construction of the right
adjoint is suggested by the Yoneda lemma
Are there other useful examples ??
Is this the "correct" definition of "partial topos" ?
Thomas Streicher
Date: Tue, 30 Aug 1994 20:07:16 +0500 (GMT+4:00)
Subject: re: distributivity
Date: Tue, 30 Aug 1994 12:56:51 -0400 (EDT)
From: Andreas Blass
This is a comment tangential to Michael Barr's message about
quantifiers. His 2 1/2 examples can be improved to 3, because the
condition he calls complementary to AC also implies classical logic.
Recall that this condition reads:
(exists x:X) (forall y:Y) f(x,y) iff
(forall s: X --> Y) (exists x:X) f(x,s(x)). (*)
The left-to-right implication here is trivial, but I claim the
right-to-left implication implies (not not u) ==> u and thus Boolean
logic.
The easiest proof proceeds as follows in the internal logic. Given an
arbitrary truth value u , let X={.|u}, i.e., X has at most one
element and it's inhabited iff u, and let Y be empty. Then
(not not u) implies the right side of (*) [vacuously: the existence of
such an s implies not u ], while the left side of (*) implies u .
For people who would like to banish the empty set at the cost of some
simplicity (universal algebraists?), there is an alternate argument
using only inhabited sets. Again, let a truth value u be given, let
Y=2, i.e., a set with exactly two, definitely distinct elements, and
let X be the quotient of Y in which the two elements have been
identified iff u . Let f(x,y) mean that the canonical projection
from Y to X sends y to x. Again, one can check that (not not u)
implies the right side of (*) and that the left side of (*) implies u.
It is curious that the same X, Y, and f as in this second proof are
also used for the (internal) proof of Diaconescu's theorem that AC
implies classical logic.
Andreas Blass
ablass@umich.edu
Date: Wed, 31 Aug 1994 09:08:00 +0500 (GMT+4:00)
Subject: Re: distributivity
Date: Tue, 30 Aug 1994 22:55:07 -0300
From: Richard Wood
Here is another comment somewhat tangential to Mike's post about
distributivity. If a lattice is completely distributive, CD, then
the fact that the opposite distributivity holds might be written
AC==>(CD<==>CD^op), for at least some aspect of choice seems to
be necessary. Write CCD, "constructive complete distributivity",
for the apparent weakening of CD that requires distributivity, in
the sense Mike posted, of infs over sups of down-closed subsets.
Then AC<==>(CD<==>CCD). On the other hand, writing BOO for the
axiom which states that the object of truth values is Boolean, one
has BOO<==>(CCD<==>CCD^op). Combining these results gives an
indirect proof of AC==>BOO.
The fact that BOO is necessary for CCD<==>CCD^op is, at first,
surprising. The equivalence of CCD and CCD^op rests entirely on
whether or not the object of truth values, which is always CCD,
is CCD^op. In set^2, the object of truth values being 3--->2,
one expects a counterexample to the claim. The pitfall here is
that distributivity of binary sup over binary inf does not extend
to distributivity of sups over infs of up-closed subobjects. To
sketch a proof of the necessity of BOO, show that CCD==>HEY.
Unlike the situation for general Heyting algebras, it follows
from a lemma attributed to both Benabou and Reyes that if the
opposite of the object of truth values is Heyting then it is
Boolean.
These observations are simplified by the fact that CCD(L) is
equivalent to the statement that sup:DL--->L has a left adjoint,
where DL is the lattice of down-closed subobjects of L, and DL
is equivalent to ord(L^op, Omega), where Omega is the object of
truth values.
RJ