pullbacks of local operators

pullbacks of local operators

[Dr. P.T. Johnstone]

Dear Colleagues,

I've recently come across a result in elementary topos theory which
looks as if it ought to be well known, but which I've never seen
before. So I'm writing to ask whether anyone else knows about it.

The context for the result is as follows: given a geometric morphism
f: E' --> E and a local operator (or Lawvere--Tierney topology, if
you prefer) j on E, it's well known that one can construct a local
operator j' on E' such that

       sh_j'(E') -----> sh_j(E)
           |               |
           |               |
           v       f       v
           E' -----------> E

is a pullback. To do this, let J >--> \Omega be the subobject
classified by j, and form the smallest local operator j' for which
the corresponding J' contains the image of

       f^*J >--> f^*\Omega ---> \Omega'

(the second factor being the canonical comparison map, which
classifies f^*(true)). See "Topos Theory", Example 3.59(iii).

The result in question is that, for any f and J, the object J' is
simply the upward closure in \Omega' of the image of the above
composite; equivalently, that the classifying map of the upward
closure of the image is always a local operator (in particular, that
it's idempotent).

When I first came across evidence that this might be true, a couple
of months ago, I was inclined to disbelieve it, on the grounds that
if it were true we'd surely have known it for twenty years or so.
However ... I now have (separate, and completely different) proofs
that it holds in several particular cases, including the case in
which f is an open map, and that in which f is a closed inclusion.
But it's also clear that the class of f's for which it holds is
closed under composition, and using Artin glueing one can factor any
f as a closed inclusion followed by an open map; so it's true for all f.

Has anyone seen this result before? In particular, does anyone have a
"uniform" proof of it that works for all f? If so, please let me know.

Peter Johnstone