Ellis Cooper asked,
What are the general rules for calculating the sub-object classifier of a topos? Or, for what class of toposes is there an algorithm for calculating the sub-object classifier of its members?
Thanks to Bill and Fred for describing the constructions. I would suggest, however, that it is rather stretching the meaning of the word "algorithm" to describe them as such. What kind of machine might be able to perform these operations? A propos of this question, it is well known both to new students of category theory and to those who like to use the subject to discuss Life, The Universe And Everything, that: (1) a topos is a cartesian closed category with (2) an internal Heyting algebra Omega, so ehat is the least that we have to add to these correct but incomplete statements to give a characterisation of a topos? Obviously I do not mean just reciting the definition of a subobject classifier. We should begin by strengthening these two statements: The term "cartesian closed" is ambigious in its usage. In computer science, it has come to require just products (and exponentials), whereas it seems to be implicit in older mathematical literature that all finite limits are needed, including EQUALISERS in particular. I therefore replace (1) by (1') a category with all finite limits and exponentials. Secondly, the Heyting algebra Omega is COMPLETE: there are morphisms some_X: PX = Omega^X --> Omega and PX = all_X: Omega^X --> X whose properties are easy to state. So (2) becomes (2') an object Omega with some_X and all_X for every object X. Let's try to prove some things from this: In order to avoid towers of exponentials, which are difficult enough in LaTeX but quite illegible in ASCII, I will write PX for Omega^X, but use the lambda calculus for exponentials. Since Omega is a Heyting algebra it also has an internal equality: equals_Omega : Omega x Omega --> Omega Using completeness, we can define an equality for all objects: equals_X : X x X --> Omega where equals_X (x, y) is all_PX (lambda phi:PX. equals_Omega(phi x, phi y) so that a morphism i:X-->Y is mono iff equals_Y (i x, i x') = equals_X (x, x'). Given such a mono we can also define I : PX --> PY by I phi == lambda y. some_X (lambda x. phi x /\ equals_Y (i x, y)) and I would like to show that I phi (i x) = i x. However, to do this we need another assumption, the Frobenius law for some_X, specifically some x'X. (phi x /\ x=x') == phi x /\ some x'.x=x' where I have replaced the earlier notation with a friendlier one. Instead of asserting the Frobenius law, I prefer a more general property of Omega itself that I call the EUCLIDEAN PRINCIPLE: (3) omega /\ F (omega) == omega /\ F (T) for all omega:Omega and F:Omega^Omega, which is to be interpreted in either the lambda calculus or using generalised elements, ie omega : X --> Omega and F : X x Omega --> Omega. We're not quite there. None of the operations that we have introduced so far yields elements of a general type X. So the final hypothesis is (4) every object X is SOBER by which I mean that the diagram X ->> PPX ==> PPPP X involving units of the monad (PP, eta, mu = P eta P) is an equaliser, or (4') every object X admits definition by description. Under these hypotheses, any mono i:X-->Y is uniquely classified by some psi:Y-->Omega and the category is a topos. More detail of these ideas is to be found in my papers geohol: Geometric and Higher Order Logic (TAC 2000) foufct: Foundations for Computable Topology (shortly to appear in a collection of papers about foundations of mathematics edited by Giovanni Sommaruga) equitop: Equideductive Topology (see my previous posting) all of which are available from my website www.PaulTaylor.EU/ASD/ followed by the acronym above. Paul [For admin and other information see: http://www.mta.ca/~cat-dist/ ]