Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 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

1. • CommentRowNumber1.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeFeb 8th 2013
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexAdded to _[[one-sided real number]]_ a short discussion of the correspondence of internal lower reals in a sheaf topos $\mathrm{Sh}(X)$ and upper semicontinuous functions $X \to \mathbb{R} \cup \{ +\infty \}$.

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

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 11th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThanks!

   Thanks!

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJan 30th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe 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\}$ is just the interior of their intersection, $\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.

   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\}$ is just the interior of their intersection, $\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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 30th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe 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 $\{L\mid R\}$ where $L$ is a lower real and $R$ an upper real. If $L$ is any lower real, then taking $R$ 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.

   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 $\{L\mid R\}$ where $L$ is a lower real and $R$ an upper real. If $L$ is any lower real, then taking $R$ 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.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeJan 31st 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSince 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?

   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?

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeJan 31st 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYou\'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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 31st 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, I was wrong that upper and lower reals embed in the Conway reals; the upper reals $\inf \{ 0\mid P \}$ and $\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)$ such that $L\cap U = \emptyset$ and $\neg L \cap \neg U = \emptyset$, which is still classically equivalent, but constructively I don't even know how to add them.

   Well, I was wrong that upper and lower reals embed in the Conway reals; the upper reals $\inf \{ 0\mid P \}$ and $\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)$ such that $L\cap U = \emptyset$ and $\neg L \cap \neg U = \emptyset$, which is still classically equivalent, but constructively I don’t even know how to add them.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeJan 31st 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthornLab edit announcer
   • CommentTimeFeb 2nd 2024
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexAdded reference * [[Guillaume Raynaud]], *Fibred Contextual Quantum Physics* ([etheses:1685](https://etheses.bham.ac.uk/id/eprint/1685/), [pdf](https://etheses.bham.ac.uk//id/eprint/1685/1/Raynaud14PhD.pdf) Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/one-sided+real+number/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/one-sided+real+number/20">v20</a>, <a href="https://ncatlab.org/nlab/show/one-sided+real+number">current</a>

   Added reference

   • Guillaume Raynaud, Fibred Contextual Quantum Physics (etheses:1685, pdf

   Anonymouse

   diff, v20, current