Re: local maps of toposes are always UIAO

Re: local maps of toposes are always UIAO

[categories]

Date: Tue, 4 Nov 1997 10:31:16 +0000 (GMT)
From: Dr. P.T. Johnstone <P.T.Johnstone@dpmms.cam.ac.uk>

Thomas Streicher asked

> I'd like to know whether the following simple observation is well known.
> If F -| U : E -> S is a local map of toposes i.e. Gamma : Gl(F) -> Gl(Id_S)
> has a fibred right adjoint Nabla then U is full and faithful, i.e. one has
> the situation of a Unity and Identity of Adjoint Opposites in Lawvere's
> sense.

Yes, there is a simple proof of this fact in Proposition 1.4 of "Local
maps of toposes" by Johnstone & Moerdijk (Proc. London Math. Soc. (3)
58 (1989), 281--305).

local maps of toposes are always UIAO

[categories]

Date: Mon, 03 Nov 1997 14:51:58 MEZ
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>

I'd like to know whether the following simple observation is well known.
If F -| U : E -> S is a local map of toposes i.e. Gamma : Gl(F) -> Gl(Id_S)
has a fibred right adjoint Nabla then U is full and faithful, i.e. one has
the situation of a Unity and Identity of Adjoint Opposites in Lawvere's sense.
Of course, UIAO entails that the geom. morph. is local.
For the reverse direction the argument is as follows. If Gamma has a fibred
right adjoint Nabla then Gamma preserves sums, i.e. is a cocartesian functor.
Let

         FI ============ FI
         ||              |
         ||              | Ff    be a cocartesian arrow in  E / F
         ||              V
         FI -----------> FJ
                Ff

then its image under Gamma is the left square in the diagram below

                i            q
          I ----------> P ------>UFI
         ||             |         |
         ||             | p  pbk  | UFf     with q o i = eta_I
         ||             V         V
          I ----------> J ------>UFJ
                f          eta_J

where i is an isomorphism as Gamma is cocartesian. That means 

         eta_I
      I -------> UFI
      |          |
      |          | UFf    is a pullback for all f : I -> J
      V          V
      J -------> UFJ
         eta_J

Choosing J = 1 we get that  eta_I  is an iso, i.e. eta is a natural iso.
Thus, F and the right adjoint of U are both full and faithful.

Of course, this argument doesn't go through when "local" is defined as U 
having an ordinary right adjoint.

Thomas Streicher