Constructing a Cartesian Closed Topos for Real Closed Fields

[Hurkyl]

Suppose I have some arbitrary category C.

I would like to construct a cartesian category C' with C embedded in it. If at all possible, the embedding would be full, and C' would be universal amongst all such constructions.

What would be a good way to go about doing that? Can I even do that in general?

Once I've found C', I would like to construct a cartesian closed category C'', again with there being a full embedding of C into C'', and universal amongst all such constructions.


Once I have that, I what I really want is some topos E in which C is embedded, preferably fully. It would be nice, too, if E was universal amongst all such topoi, or at least being minimal amongst extensions.


Actually, the first category I want to do this with is already cartesian, and has a subobject classifier. (It would be cool if it was still the subobject classifier when extended to a topos) But I'm still curious about the more general case too!

 

[mathwonk]

yukkk. ok what is a cartesian category?

and next what is a topos?

third: why do, you want this &&**^^!

 

[Hurkyl]

A cartesian category is one with all finite products. (So it has a terminator -- the empty product)

It's cartesian closed if it's cartesian and has exponentials -- that is, for any A, B, we have a natural isomorphism Hom(_xA, B) --> Hom(_, B^A)

To be a topos, it has to be cartesian closed, have equalizers, and a subobject classifier Ω. That means there's a natural isomorphism
Sub(Bx_) --> Hom(_, Ω^B)

(There are lots of equivalent ways to define a topos -- I'm not really sure which would be the simplest for this purpose)


A topos is the categorical substitute for set theory. In fact, Set is a topos. (It's subobject classifier is 2 = {true, false}) What I want to do is, given a theory, to build a topos that naturally serves to model that theory, rather than start with my favorite topos and try to build a model of the theory within that topos.

At the moment, I'm interested in doing this to the theory of real closed fields. (ordered fields R such that R is algebraically closed)

I always thought the theory was pretty because it's logically complete. Any statement true for one real closed field is true for all. In particular, every real closed field satisfies the completeness axiom!... as long as the only "sets" you can build are solutions to a system of equalities and inequalities. (or, equivalently, semialgebraic subsets of R^n)

So, we see that the prettiness is destroyed when we start analyzing the theory with set theory. (e.g. most real closed fields do not satisfy the completeness axiom!)