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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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).
  1. Added to one-sided real number a short discussion of the correspondence of internal lower reals in a sheaf topos Sh(X)\mathrm{Sh}(X) and upper semicontinuous functions X{+}X \to \mathbb{R} \cup \{ +\infty \}.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 11th 2013


    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 30th 2017

    The section at one-sided real number on suprema and infima has this to say:

    In predicative constructive mathematics, we cannot necessarily take the infimum of a set of lower reals, nor the supremum of a set of upper reals. Even in impredicative constructive mathematics (where these infima and suprema exist by the adjoint functor theorem), these may not be what we really want; an obvious example of this is if we take the infimum of a set of lower reals that happen to all be located, in which case what we really want is an upper real. We can, however, always interpret such a supremum or infimum as a MacNeille real number (and then ask whether this MacNeille real happens to be an upper real or a lower real or even both at once, in which case it is an ordinary located real number).

    I don’t think I agree with all of this. First of all, I believe that the infimum of a set of lower reals {L i}\{L_i\} is just the interior of their intersection, iL i={q|r>q,r iL i}\bigwedge_i L_i = \{ q\in \mathbb{Q} | \exists r\gt q, r \in \bigcap_i L_i \}. Is that impredicative? In any case it’s more concrete than an appeal to AFT.

    Second, I think the sentence about MacNeille reals is at best misleading, unless it means something different than I’m used to by “MacNeille real”. A MacNeille real number, as defined in the Elephant, is always both an upper real and a lower real at once (and in particular that doesn’t make it located). In fact, I believe that taking the interior of the complement in both directions gives an adjunction between lower and upper reals (under \le), whose fixed elements are precisely the MacNeille reals. Thus the MacNeille reals are coreflective in the upper reals, hence closed under suprema but not infima, and reflective in the lower reals, hence closed under infima but not suprema. So both suprema and infima of MacNeille reals are constructed as interiors of intersections on one side and the interior of the complement on the other, which means that they aren’t usually what we want in constructive analysis. In particular, I think that located subspace is correct to say that locatedness means that the upper real infimum (not the MacNeille infimum) is a located real number (and I have edited it to emphasize this).

    If no one disagrees, I will go ahead and edit the page to reflect this.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 30th 2017

    The section on arithmetic also claims that the MacNeille reals simultaneously generalize the upper and lower reals, which as above I don’t believe. (You can make both an upper and a lower real into a MacNeille real, but this is a reflection or coreflection, not an embedding.)

    I do believe that there’s a common generalization of the upper and lower reals, but it’s rather more complicated. I call it the “Conway reals”: it’s the set of surreal numbers that have an expression as {LR}\{L\mid R\} where LL is a lower real and RR an upper real. If LL is any lower real, then taking RR to be the interior of its complement defines a Conway real, and dually. I believe this embeds both the lower and upper reals into the Conway reals as sub-posets whose intersection is the MacNeille reals. But constructively, the Conway reals are quite large. They can be both added and subtracted, but we don’t know how to multiply them constructively (unless we restrict to positive ones). I haven’t thought about whether they have suprema and infima.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJan 31st 2017

    Since you can subtract them, presumably you can multiply positive Conway numbers and negative Conway numbers, but you can't multiply them in general because there is no way to decide which they are?

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeJan 31st 2017

    You're quite right about the interior of the intersection/union, and I keep meaning to edit one-sided real number to reflect this, but I've never gotten around to it.

    But I seem to have been operating under a misconception; while knowing that I don't really grasp MacNeille real numbers yet, I could have sworn that I'd read that they were more general than one-sided real numbers, and you are claiming otherwise.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 31st 2017

    Well, I was wrong that upper and lower reals embed in the Conway reals; the upper reals inf{0P}\inf \{ 0\mid P \} and inf{0¬¬P}\inf \{ 0 \mid \neg\neg P\} are identified in the Conway reals, just as they are in the MacNeille reals. The only sort of “real number” I can think of that contains both the upper and lower reals is the set of pairs (L,U)(L,U) such that LU=L\cap U = \emptyset and ¬L¬U=\neg L \cap \neg U = \emptyset, which is still classically equivalent, but constructively I don’t even know how to add them.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJan 31st 2017

    I edited one-sided real number to reflect my current understanding. If it turns out to be wrong, we can fix it, but I wanted to get it done before I get sucked away into other things.

  2. Added reference


    diff, v20, current