Yes, that's right. If F --> Set[O] is localic, then the object (X, say) of F which it clasifies is what I call a pre-bound for F, which means that the subobjects of its finite powers generate F. So fullness on subobjects of finite powers of X implies fullness on subobjects of all objects. The problem really is that, if you form the "full geometric theory" of R, you end up with a theory whose only model is R, because the language is rich enough to contain names for all the elements of R and the axiom which says that every element has exactly one of these names. So if you want to get something nontrivial, you have to be somehow selective about *which* relations you allow the theory to talk about. Peter ---------------------- On Sat, 16 Apr 2011, Richard Garner wrote:
In fact, I think the condition of being an E-map in this new sense says: f : E --> F over Set[O] is such a map just when, on taking the hyperconnected-localic factorisations E --> E' --> Set[O] and F --> F' --> Set[O], the induced geometric morphism f' : E' --> F' is hyperconnected. In particular, if F --> Set[O] is localic, then f is an E-map if and only if it is hyperconnected. So this gets us no further than before. Oh well!
Richard
On 16 April 2011 10:31, Richard Garner <richard.garner@mq.edu.au> wrote:
Thanks Peter. It did occur to me last night that this probably was the hyperconnected-localic factorisation and it is nice to have this feeling confirmed! The problem is that the factorisation system I described allows one to adjoin n-ary relations to _arbitrary_ objects of Set[O], rather than merely to the generic object. In particular, as you point out, of the first group of maps I listed it is only necessary to consider the case n=1, and in fact on looking at at your proof, orthogonality to this immediately implies orthogonality to the last of the maps I listed.
Here's an attempt to overcome this; I suspect it will end up suffering the same fate as the previous one but you never know! Rather than describing a factorisation system on GTop, I am going to describe one on GTop / Set[O]. The generating right maps will simply be the maps from the classifying topos of an object equipped with an n-ary relation into Set[O], though now these maps are viewed as maps over Set[O]. If this generates a factorisation system (E, M), then its M-maps with codomain E --> Set[O] will correspond to those things constructible by repeatedly adjoining n-ary relations or equations between n-ary relations to the specified object of E. Every such map will be localic, but I think that the E-maps are no longer the hyperconnected morphisms; the inverse image part of such a map need only be full on subobjects of the specified object of its domain.
Now on factorising the unique map from R: Set --> Set[O] into the terminal object of GTop / Set[O], it is possible that we obtain something non-trivial which captures the structures (in geometric logic) supported by the reals. I am however a bit hesitant about this as my feeling is that if p: E --> F is an E-map of toposes over Set[O], and F --> Set[O] is localic, then p probably is actually hyperconnected (i.e., fullness on subobjects of the (image of) the generic object implies fullness on all subobjects) so that we are back in the situation we were in before...
Richard
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]