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