internal functional relations versus arrows

internal functional relations versus arrows

[Eduardo J. Dubuc]

I am not an expert on elementary topos (meaning by this to work with the
internal language in a Grothendiek topos) and I rather be told than
struggle with the following:

Consider an elementary topos EE, a locale G in EE, the unique locale
morphism i^*: Omega --> G, and any arrow b: X x Y --> G:

Consider the following formulae on "b":

ed): Supremun_y  b(x, y) = 1

uv): b(x, y) inf b(x, y') <_=  i^*[[y = y']].

Let u: X x Y --> Map(X, Y) be the universal locale furnished with such
an arrow
(that is, forall b exists! t^* : Map(X, Y) --> G   t^* u = b.

Gavin Wraith (in "Localic Groups", Cahiers de
Top. et Geom. Diff. Vol XXII-1 1981) defines an object

Points(G) = LocalMorphisms(G, Omega) C Omega^G  and says that it is
clear that:

a) Points(Map(X, Y)) = Y^X.

  From this taking global sections it follows that:

b) There is a bijection between
              arrows X x Y --> Omega  and arrows  X --> Y
(where the arrow on the right satisfy ed) and uv))

QUESTION 1] I ask for a convincing proof of a), or better, of the weaker
? b).

Concerning b), consider the following conditions
                                       on a relation  R C X x Y:

exed) pi_1: R --> X is an epimorphism.

exuv) The family y = pi_2 (x, y): Z --> R --> Y is a compatible family
with respect to the family x = \pi_1 (x, y): Z --> R --> X (indexed by
all (x, y): Z --> R)

Then, using that epis are strict it follows using standard category theory:

R satisfy exed) and exuv)  iff
        exists!  f: X --> Y such that R = Gamma_f (the Graph of f)

Thus, b) will follow if we can prove :

R satisfy exed) and exuv)  iff  cf_R satisfy ed) and uv)
(cf_R = characteristic function).

This is more related with the formula

uv'): b(x, y)  inf  b(x', y') inf i^*[[x = x']]  <_=  i^*[[y = y']].

Also, by standard category theory it follows that "exed) + exuv)" are
equivalent to "pi_1 is mono and epi".  This may help ?

NOTE: All the above is very clear in the topos of Sets, but my problem
is that I am very uncomfortable when the experts write "we do as if the
base topos is the topos of Sets". Does this slogan apply to the above ?.

SUBQUESTION] Are uv) and uv') equivalent ?

Now a more substantial question:

QUESTION 2]

Consider now a geometric morphism  g: FF  --> EE. We have a bijection
between arrows

X x Y --> g_* Omega_FF   and arrows   g^*X x g^*Y  --> Omega__EE.

I want to know if the arrows satisfying ed) and uv) correspond under
this bijection.

e.d.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]