Date: Tue, 17 Jun 1997 08:32:58 -0300 (ADT)
Subject: pushouts in toposes 

Date: Mon, 16 Jun 1997 14:22:42 +0000
From: Cesc Rossello <dmifrl0@ps.uib.es>

Dear categorists

A PhD student of mine, Merce Llabres, and I we have got involved in
proving some properties of pushouts on toposes, similar (but somehow
dual) 
to those known for pullbacks. 
We are worried by the fact that perhaps somebody else has already proved
many of the 
results we are interested in.
So, before struggling to prove some probably well-known things, we
would really appreciate  some pointers to literature on the topic.

For instance:

Assume you have a family of pushouts in a topos
Ai ---> Bi
|            |
v  f       v
A------> B
 (all squares have the same bottom arrow    f)
with vertical arrows monic, and assume the pullbacks of (Ai -->A)_i
and (Bi---> B)_i exist, say A0 and B0, and consider the obvious square

A0 ---> B0
|              |
v  f         v
A------> B

It is a pushout square when the family of squares is finite, and 
for arbitrary families in all complete toposes we have tried 
(sets, hypergraphs, total unary algebras,
unary partial algebras with closed homomorphisms,...). 
Moreover, a proof (for complete toposes) can probably be derived from
the techniques in the paper by Kawahara in TCS vol 77 (1990). But, has 
somebody already proved (or disproved) such a result? 

Thanks in advance      Cesc Rossello


Date: Tue, 17 Jun 1997 23:52:15 -0300 (ADT)
Subject: Re: pushouts in toposes 

Date: Tue, 17 Jun 1997 10:32:21 -0400 (EDT)
From: Peter Freyd <pjf@saul.cis.upenn.edu>

Cesc Rossello asks about pushouts in topoi. In particular, assume that
for each i, 

   Ai ---> Bi      

   |       |

   A  ---> B
       f

is a pushout (same  f  each  i) and that the vertical maps are monic
(henceforth to be treated notationally as inclusion maps). Let  A0  be
the intersection of the  Ai's  and  B0  the intersection of the  Bi's.
Then is it the case that

   A0 ---> B0

   |       |

   A  ---> B   is also a pushout?

Yes for finite families, no for arbitrary families.

The case for finite families is an straightforward consequence of the
representation theorem for pre-topoi and the fact that such
representations preserve pushouts of monics. (See 1.636 and 1.65 in
Categories, Allegories.)

For the failure in the infinite-family case specialize to the case
that  f:A --> B  is also an inclusion map. The result, if true, would
translate to:

    A v /\Bi  =  /\(A v Bi).

Take sheaves on any non-discrete  T1-space,  X,  for a counterexample. 
Let  B  be the terminal sheaf (i.e.  X  itself), A  the complement of 
some non-isolated point and  {Bi}  the family of all other complements 
of one-element sets.


Date: Tue, 17 Jun 1997 23:53:24 -0300 (ADT)
Subject: Re: pushouts in toposes 

Date: Tue, 17 Jun 1997 11:54:07 -0400 (EDT)
From: Peter Freyd <pjf@saul.cis.upenn.edu>


The distributivity condition is not only necessary and but a
sufficient condition for the pushout result. A square

   A'--> B'

   |     |

   A --> B
      f

in which the vertical arrows are monic is a pushout iff the
following three conditions hold:

  1)  the square is a pullback;
  2)  B  is the union of  Image(f)  and  B';
  3)  the congruence, E, induced by  f  is the union of the
      identity relation and  E ^ (A' x A').

Hence, the desired result reduces to:

   B  =  Image(f) v /\Bi;
   E  =  I v /\(E ^ (Ai x Ai))  =  I v (E ^ /\(Ai x Ai)).


Date: Sun, 29 Jun 1997 11:37:02 -0300 (ADT)
Subject: Re: pushouts in toposes 
 
Date: Sun, 22 Jun 1997 11:54:47 -0300
From: RJ Wood <rjwood@cs.dal.ca>
 
A belated, somewhat tangential comment, on the distributivity
condition 
A v /\Bi  =  /\(A v Bi)
that Peter mentioned in his posts. The subobject classifier,
Omega, satisfies this condition (internally) if and only if the
topos is boolean. See the proof of Theorem 10 in Constructive
Complete Distributivity II, Math Proc Cam Phil Soc, (1991) 110,
245-249, by Rosebrugh and Wood, which shows that if Omega^op
is Heyting then Omega is Boolean. This result was discovered
independently by Richard Squire in his thesis.
 
It has always struck me as somewhat surprising but in the Rosebrugh/
Wood proof it is an immediate consequence of the corollary of the
following result which I believe is due to Benabou and which seems
to be not well known:
 
LEMMA If f <= id:Omega--->Omega then f(u) = u/\f(true).
 
COROLLARY If f <= id:Omega--->Omega and f(true) = true then f = id.
 
(If Omega^op is Heyting, apply the corollary to --, where - is the
negation for Omega^op.)
RJ