Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorZhen Lin
    • CommentTimeAug 9th 2011

    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 XX is isomorphic to the sheaf of continuous functions on XX.

    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.

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeAug 9th 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 9th 2011

    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.

    • CommentRowNumber4.
    • CommentAuthorZhen Lin
    • CommentTimeAug 9th 2011

    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.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 9th 2011

    Nice start; thank you! I think I might add more, later.

    • CommentRowNumber6.
    • CommentAuthorzskoda
    • CommentTimeAug 9th 2011

    Great work guys!

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeAug 10th 2011

    I have added a link to it from natural numbers object.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeAug 11th 2011

    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:

    • uniqueness of a RNO,
    • existence of a RNO in a topos with NNO,
    • existence in a Π\Pi-pretopos with NNO and WCC,
    • existence in a Π\Pi-pretopos with NNO and subset collection.
    • CommentRowNumber9.
    • CommentAuthorZhen Lin
    • CommentTimeAug 11th 2011

    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?

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 11th 2011

    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.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 11th 2011
    • (edited Aug 11th 2011)

    “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 XX \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.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeAug 12th 2011

    Also, we have some material on this at field.

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2011

    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).

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeAug 12th 2011

    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][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.

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2011
    • (edited Aug 12th 2011)

    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.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeAug 12th 2011

    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.)

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2011

    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?

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeAug 13th 2011

    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,UL,U is located if, whenever a<ba \lt b as rational numbers, aLa \in L or bUb \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.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 13th 2011

    Okay, that makes sense – thanks.

    • CommentRowNumber20.
    • CommentAuthorTobyBartels
    • CommentTimeAug 18th 2011

    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.

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 19th 2011

    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?

    • CommentRowNumber22.
    • CommentAuthorTobyBartels
    • CommentTimeAug 19th 2011
    • (edited Aug 19th 2011)

    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 WCCWCC will the Cauchy construction give an RNO. (Most toposes don’t satisfy WCCWCC, 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.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 19th 2011

    Okay, thanks very much for the clarification.

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeAug 19th 2011

    I also added uniqueness to the properties. (I still need to write in proofs of these properties!)

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeAug 19th 2011
    • (edited Aug 19th 2011)

    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).

    • CommentRowNumber26.
    • CommentAuthorTobyBartels
    • CommentTimeAug 19th 2011

    Regarding parametrised subobjects (which Zhen Lin called “still a mystery”): notice that in the construction of an RNO in a topos, LL (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 LL is in the general definition (except using RR in place of \mathbb{Q}, since I’m giving the condition for RR 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.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeAug 20th 2011
    • (edited Aug 20th 2011)

    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 xRx\in R such that L={bR|b<x}L = \{ b\in R | b\lt x\} and U={bR|x<b}U = \{ b\in R | x\lt b\}” in the stack semantics.

    • CommentRowNumber28.
    • CommentAuthorZhen Lin
    • CommentTimeAug 20th 2011

    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).

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2011

    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?

    • CommentRowNumber30.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2011
    • (edited Aug 25th 2011)

    Here’s the proof as I wrote it:

    Suppose that x,x:ΓRx, x'\colon \Gamma \to R both satisfy the required properties, and consider x#xx \# x', which is a subobject of Γ\Gamma. By the strong connectedness of <\lt, x#xx \# x' is contained in (factors through) x<xx<xx \lt x' \vee x' \lt x, which is the union of x<xx \lt x' and x<xx' \lt x.

    Now consider x<xx \lt x', and let aa be a generalised element of Γ\Gamma. If aa belongs to (factors through) x<xx \lt x', or equivalently (x(a),x(a))(x(a), x'(a)) belongs to <\lt, it follows that (a,x(a))(a,x(a)) belongs to LL. Thus, (x(a),x(a))(x(a), x(a)) also belongs to <\lt, or equivalently aa belongs to x<xx \lt x. By the strong irreflexivity of <\lt, this is contained in x#xx \# x; by the irreflexivity of #\#, this is contained in \bot (as a subobject of Γ\Gamma). Since every aa that belongs to x<xx \lt x' belongs to \bot, x<xx \lt x' is contained in (and so equals as a subobject) \bot.

    Similarly (either by swapping xx with xx' or by using UU instead of LL), x<xx' \lt x is also \bot. Therefore, x#xx \# x' is \bot. By the tightness of #\#, x=xx = x'.

    Here’s the same proof in naïve language:

    Suppose that x,x:Rx, x'\colon R both satisfy the required properties, and suppose that x#xx \# x'. By the strong connectedness of <\lt, x<xx \lt x' or x<xx' \lt x.

    Now suppose that x<xx \lt x'. It follows that xx belongs to LL, so x<xx \lt x. By the strong irreflexivity of <\lt, x#xx \# x; by the irreflexivity of #\#, we have a contradiction.

    Similarly (either by swapping xx with xx' or by using UU instead of LL), x<xx' \lt x is also false. Therefore, x#xx \# x' is false. By the tightness of #\#, x=xx = x'.

    • CommentRowNumber31.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 25th 2011

    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.

    • CommentRowNumber32.
    • CommentAuthorTobyBartels
    • CommentTimeAug 25th 2011
    • (edited Aug 25th 2011)

    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.

    • CommentRowNumber33.
    • CommentAuthorZhen Lin
    • CommentTimeAug 26th 2011

    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.

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeAug 27th 2011
    • (edited Aug 27th 2011)

    Here’s the direct translation of your naive proof into stack semantics.

    Suppose that x,x:Rx, x'\colon R both satisfy the required properties, and suppose that x#xx \# x'.

    Suppose that x,x:ΓRx, x'\colon \Gamma \to R both satisfy the required properties. Suppose additionally that (x,x):ΓR×R(x,x')\colon \Gamma \to R\times R factors through [#][\#].

    By the strong connectedness of <\lt, x<xx \lt x' or x<xx' \lt x.

    By the strong connectedness of <\lt, there exists a (regular) epimorphism [p,q]:U+VΓ[p,q]\colon U+V \to \Gamma such that (x,x)p(x,x')p factors through [<][\lt] and (x,x)q(x',x)q factors through [<][\lt].

    Now suppose that x<xx \lt x'. It follows that xx belongs to LL, so x<xx \lt x.

    Since (xp,xp)(x p, x' p) factors through [<][\lt], by assumption on xx', we have that (p,x)(p,x) factors through LL.

    By the strong irreflexivity of <\lt, x#xx \# x; by the irreflexivity of #\#, we have a contradiction.

    This implies that (xp,xp)(x p, x p) factors through [<][\lt], hence also through [#][\#]. But (xp,xp)(x p, x p) also factors through [=][=] (the diagonal of RR), and irreflexivity of #\# means that [#][=]=0[\#]\cap [=] = 0, the initial object. Therefore, since initial objects are strict, UU is also initial.

    Similarly (either by swapping xx with xx' or by using UU instead of LL), x<xx' \lt x is also false.

    Similarly, we conclude that VV is initial.

    Therefore, x#xx \# x' is false.

    Since Γ\Gamma is regular epimorphic image of 0+0=00+0 = 0 an initial object, it is also initial, under the hypothesis that (x,x):ΓR×R(x,x')\colon \Gamma \to R\times R factors through [#][\#]. By definition, this means that without that hypothesis (i.e., given only x,x:ΓRx, x'\colon \Gamma \to R both satisfying the required properties), we have that (x,x)(x,x') factors through ¬[#]\neg [\#].

    By the tightness of #\#, x=xx = x'.

    By the tightness of #\#, it follows that (x,x)(x,x') factors through [=][=], which is to say x=xx=x'.

    • CommentRowNumber35.
    • CommentAuthorTobyBartels
    • CommentTimeAug 27th 2011

    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<xx \lt x' and x<xx' \lt x, then drew the proper conclusion from this, without going into the details.

    Your version is actually simpler than mine when dealing with LL and UU as parametrised subobjects. I noticed that the generalised element aa 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.