Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I just came across a very interesting result in Sheaves in Geometry and Logic, and it seemed like the sort of thing which ought to be recorded in nLab somewhere, yet isn’t.
Theorem. The object of Dedekind reals in the topos of sheaves on a topological space $X$ is isomorphic to the sheaf of continuous functions on $X$.
Proof. See Mac Lane and Moerdijk [1994, Ch. VI, §8].
At the moment, there’s an article about real numbers and an article about Dedekind cuts, but very little is said about them in the context of the internal logic of a topos. I was thinking about starting an article on the topic, but I’m not very sure what should be discussed.
I think it would be good to open a section at Dedekind cuts titled “Topos theoretic generalizations” and explain the theorem there. If the entry becomes to big somebody will split it off at some point.
Zhen Lin: the result is in the nLab; it’s just hard to find. :-) Look under vector bundle.
Anyway, you’re right that this sort of statement should be placed more prominently (and also the characterization of Cauchy reals in a topos). I think real number object in a topos would be a fine place to write about both. Go for it! For example, you can just write down the thing you read in Mac Lane-Moerdijk and leave it at that if you want; someone else may come by and add more.
I went ahead and created an article for real numbers object.
I don’t know anything about intuitionistic Cauchy real numbers (or, for that matter, anything much about topos theory at all—I’m still learning the basics!) so I’ve not said much about it at the moment.
Nice start; thank you! I think I might add more, later.
Great work guys!
I have added a link to it from natural numbers object.
Nice! I’ve had in the back of my head to write this, but I didn’t know (or I forgot) the result that inspired you.
I don’t have time now, but I want to rewrite the definition to be an abstract definition of a real-numbers object (in, say, a Heyting pretopos with NNO) by slightly externalising from (generalised) elements of a power object to (parametrised) subobjects. Then your construction becomes a proof that a RNO exists in every topos with NNO.
Actually, the full list of theorems would be:
Thanks, but I'm really only summarising what's in Mac Lane and Moerdijk, so it's definitely not ‘my’ construction! (But whose is it? The book doesn't say much in the way of history.)
I agree it would be nice to weaken the definition a bit to make it work without internal higher-order logic, but I'm afraid I don't know enough to help there. Parametrised subobjects are still a mystery to me. It would be even nicer if we could find a universal property characterising RNOs, but I fear any such will be enormously more unwieldy than what's already in the article. (Does the notion ‘unique complete totally-ordered field’ still work?)
As for uniqueness: in the current definition, isn't this essentially automatic? Any two NNOs are uniquely isomorphic, so the given constructions of the integers and the rational numbers objects are automatically unique up to unique isomorphism (as coequalisers of certain maps). As defined, the RNO is a specific subobject named in the Mitchell–Bénabou language, which I'm quite confident makes it unique up to unique isomorphism (where isomorphism here includes compatibility with some monstrous diagrams arising from the interpretation of the various conditions). But perhaps you had something more interesting in mind?
Yes, it is basically a universal property of RNOs that I want to put in, a complicated one, which essentially says “complete ordered field” in the M-B language. It is this that we can prove is unique; and we can prove that the construction from ML-M satisfies it.
“Field” is a notoriously tricky word in this context. One can formulate the notion of field in coherent logic, but the Dedekind reals are not generally a field under this notion. E.g., for the topos of sheaves over a space, taking stalks at a point preserves coherent logic, but the stalk of the Dedekind RNO (= sheaf of real-valued continuous functions $X \to \mathbb{R}$) at a point is typically not a field, but a local ring.
There are other notions of field one can work with. The Elephant has some material on this in section D.4.7.
Edit: Also, regarding the completeness of the RNO, the Elephant has an interesting result in Theorem D.4.7.11.
Also, we have some material on this at field.
Okay, good! So you feel pretty confident about this claim?
Yes, it is basically a universal property of RNOs that I want to put in, a complicated one, which essentially says “complete ordered field” in the M-B language. It is this that we can prove is unique; and we can prove that the construction from ML-M satisfies it.
Because that would be very interesting, and something I’ve not heard claimed elsewhere. Comment 11 was to sound warnings to the unwary (not meaning you).
Yes, except for the fairness of the phrase “universal property”, which is probably not really appropriate. (There are approaches to constructing $\mathbb{R}$ or $[0,1]$ as an ordered set that lay better claim to this term, but that’s not what I’m talking about, and I don’t think that they give the same result as the located Dedekind RNO in an arbitrary topos.) I just need a block of time in front of a decent keyboard to write it out.
Okay, I’ll be interested to see how you treat completeness (I take it you are working in the context of an arbitrary topos). In particular, why the restrictions on the topos implied by Elephant’s theorem D.4.7.11 do not impinge on your treatment.
I can’t get at my copy of the Elephant right now, so I don’t know what’s in D.4.7.11. But for “completeness” I intend to use completeness under located Dedekind cuts, which is sufficient for uniqueness of the RNO and for existence in each of the three cases listed in #6. As for whether this RNO additionally satisfies stronger notions of “completeness” (which is what I’m guessing D.4.7.11 is about), that would only happen in certain categories. (And my intended general context is a Heyting pretopos, since that’s the most general situation that I care about, and I actually don’t know how to make it work in a more general context.)
Thanks, Toby. But I’m sorry, I don’t know what ’located’ means here.
I’m also confused by the fact that you are working in the context of a Heyting pretopos. This gives a context for internalizing intuitionistic first-order logic in a category (right?), but I always think of the construction of the reals as being a second-order construction. At the risk of asking a stupid question: how will you construct an object of cuts in your context? Are you assuming some higher-order constructions?
See #8 again; in the general context, I’d only define it and prove uniqueness. To prove existence (to construct the RNO), I need a stronger context (not necessarily a topos, but with at least some second-order constructions).
A two-sided Dedekind cut $L,U$ is located if, whenever $a \lt b$ as rational numbers, $a \in L$ or $b \in U$ (property (7) at Dedekind cut). This is actually only the beginning of a massive generalisation (perhaps one day at located subspace), all of which is classically trivial. If you replace (7) with something weaker, then you get a stronger notion of completeness.
Okay, that makes sense – thanks.
I have put in the definition of RNO in an arbitrary Heyting pretopos, but I want to add details. I’ve also put in an outline of the rest of what I want to write.
I would love to see details!
I have to say: this look awfully tricky to me. You appear to be using the Cauchy definition in the context of a $\Pi$-pretopos, and asserting that this specializes to the Dedekind reals in the case of a topos?
No, that’s not what I’m doing.
The Cauchy construction goes through in any $\Pi$-pretopos with an NNO (and every topos is a $\Pi$-pretopos). However, only if the $\Pi$-pretopos satsifies $WCC$ will the Cauchy construction give an RNO. (Most toposes don’t satisfy $WCC$, although Boolean toposes do, and so does the effective topos.) This is the second construction.
On the other hand, if the $\Pi$-pretopos satisfies subset collection (which every topos does), then it is also possible to modify the Cauchy construction in such a way that the modified construction does give an RNO. This is the third construction.
Okay, thanks very much for the clarification.
I also added uniqueness to the properties. (I still need to write in proofs of these properties!)
I now have the complete definition of an RNO in an arbitrary Heyting category. Also, the properties are stated as precise theorems (but still requiring proofs).
Regarding parametrised subobjects (which Zhen Lin called “still a mystery”): notice that in the construction of an RNO in a topos, $L$ (half of Dedekind cut) was given as a generalised element of $\mathcal{P}\mathbb{Q}$, that is a morphism from some object $\Gamma$ to $\mathcal{P}\mathbb{Q}$. But morphisms from $\Gamma$ to $\mathcal{P}\mathbb{Q}$ are in natural bijection with subobjects of $\Gamma \times \mathbb{Q}$. And that is a parametrised subobject of $\mathbb{Q}$, which is what $L$ is in the general definition (except using $R$ in place of $\mathbb{Q}$, since I’m giving the condition for $R$ to be Dedekind-complete rather than constructing the Dedekind completion of $\mathbb{Q}$).
So, if you can do generalised elements, then you can do parametrised subobjects.
And if you prefer not to have to think about generalized elements and parametrized subobjects all the time, then the stack semantics is a way to package them up “once and for all”, so that you can just say things like
An ordered field object R is Dedekind-complete if it satisfies the sentence “for all Dedekind cuts (L,U) in R, there exists an element $x\in R$ such that $L = \{ b\in R | b\lt x\}$ and $U = \{ b\in R | x\lt b\}$” in the stack semantics.
Toby: Ah, that's what I thought a parametrised subobject would be. Thanks for clarifying.
Mike: That looks quite nice! I haven't had time to digest the whole of the paper yet, but it seems like definition 7.2 would make a good starting point for an article on stack semantics (or, for that matter, Kripke–Joyal semantics, appropriately modified).
The other day, I put in a proof of the uniqueness of the point determined by a Dedekind cut. Is it legible? Would it be better to simply write a proof in naïve language and instruct the reader to interpret it in the stack semantics?
Here’s the proof as I wrote it:
Suppose that $x, x'\colon \Gamma \to R$ both satisfy the required properties, and consider $x \# x'$, which is a subobject of $\Gamma$. By the strong connectedness of $\lt$, $x \# x'$ is contained in (factors through) $x \lt x' \vee x' \lt x$, which is the union of $x \lt x'$ and $x' \lt x$.
Now consider $x \lt x'$, and let $a$ be a generalised element of $\Gamma$. If $a$ belongs to (factors through) $x \lt x'$, or equivalently $(x(a), x'(a))$ belongs to $\lt$, it follows that $(a,x(a))$ belongs to $L$. Thus, $(x(a), x(a))$ also belongs to $\lt$, or equivalently $a$ belongs to $x \lt x$. By the strong irreflexivity of $\lt$, this is contained in $x \# x$; by the irreflexivity of $\#$, this is contained in $\bot$ (as a subobject of $\Gamma$). Since every $a$ that belongs to $x \lt x'$ belongs to $\bot$, $x \lt x'$ is contained in (and so equals as a subobject) $\bot$.
Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also $\bot$. Therefore, $x \# x'$ is $\bot$. By the tightness of $\#$, $x = x'$.
Here’s the same proof in naïve language:
Suppose that $x, x'\colon R$ both satisfy the required properties, and suppose that $x \# x'$. By the strong connectedness of $\lt$, $x \lt x'$ or $x' \lt x$.
Now suppose that $x \lt x'$. It follows that $x$ belongs to $L$, so $x \lt x$. By the strong irreflexivity of $\lt$, $x \# x$; by the irreflexivity of $\#$, we have a contradiction.
Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also false. Therefore, $x \# x'$ is false. By the tightness of $\#$, $x = x'$.
Toby, I think it’s legible. But I also think you could put in both the ’naive’ version and the version as you have it, in separate sections if need be.
The point is that there will be some readers who prefer the naive version (together with the highly anti-naive instruction to interpret it in the stack semantics), but others will probably find that too cavalier. Those other readers may prefer the more formal version, but the first set of readers may find it harder to read.
There is plenty of room in the nLab to write in such a way to catch as many readers as possible. I personally tend to feel more comforted by having lots of detail written out.
Thanks, I’m glad that it makes sense. (And I encourage Zhen Lin and Mike, as well as anybody else, to also reply.)
You’ll notice the difference in length. This is a short proof, compared to some of the others, and my worry is that spelling everything out will be very long.
I wonder if I might put this proof in both ways, then write all of the others in the internal language. (Of course, this wouldn’t preclude other people from writing external versions if they wish.)
By the way, I’m just sort of assuming, before I finish his paper, that Mike’s stack semantics interpret the second proof as the first one. If they don’t, then I’m missing the point.
The internal proof is certainly much easier to understand, and I think it illuminates the essence of the proof by hiding irrelevant details. (Do we really need to know about the parametrisation domain $\Gamma$? etc.) On the other hand the given external proof is probably neater than a direct translation of the internal proof into Kripke–Joyal/stack/standard semantics.
Here’s the direct translation of your naive proof into stack semantics.
Suppose that $x, x'\colon R$ both satisfy the required properties, and suppose that $x \# x'$.
Suppose that $x, x'\colon \Gamma \to R$ both satisfy the required properties. Suppose additionally that $(x,x')\colon \Gamma \to R\times R$ factors through $[\#]$.
By the strong connectedness of $\lt$, $x \lt x'$ or $x' \lt x$.
By the strong connectedness of $\lt$, there exists a (regular) epimorphism $[p,q]\colon U+V \to \Gamma$ such that $(x,x')p$ factors through $[\lt]$ and $(x',x)q$ factors through $[\lt]$.
Now suppose that $x \lt x'$. It follows that $x$ belongs to $L$, so $x \lt x$.
Since $(x p, x' p)$ factors through $[\lt]$, by assumption on $x'$, we have that $(p,x)$ factors through $L$.
By the strong irreflexivity of $\lt$, $x \# x$; by the irreflexivity of $\#$, we have a contradiction.
This implies that $(x p, x p)$ factors through $[\lt]$, hence also through $[\#]$. But $(x p, x p)$ also factors through $[=]$ (the diagonal of $R$), and irreflexivity of $\#$ means that $[\#]\cap [=] = 0$, the initial object. Therefore, since initial objects are strict, $U$ is also initial.
Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also false.
Similarly, we conclude that $V$ is initial.
Therefore, $x \# x'$ is false.
Since $\Gamma$ is regular epimorphic image of $0+0 = 0$ an initial object, it is also initial, under the hypothesis that $(x,x')\colon \Gamma \to R\times R$ factors through $[\#]$. By definition, this means that without that hypothesis (i.e., given only $x, x'\colon \Gamma \to R$ both satisfying the required properties), we have that $(x,x')$ factors through $\neg [\#]$.
By the tightness of $\#$, $x = x'$.
By the tightness of $\#$, it follows that $(x,x')$ factors through $[=]$, which is to say $x=x'$.
Neat! I was a little worried that my external proof might be bad, since I didn’t say anything about regular epimorphisms, but I think that it’s all right; I proved what I needed to about $x \lt x'$ and $x' \lt x$, then drew the proper conclusion from this, without going into the details.
Your version is actually simpler than mine when dealing with $L$ and $U$ as parametrised subobjects. I noticed that the generalised element $a$ of $\Gamma$ in my proof could just be the identity morphism, but it seemed more natural to take an arbitrary element as the definition suggested. If that part had been written in the stack semantics all along, then I might have done it differently.
1 to 35 of 35