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.
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 \}$.
Thanks!
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.
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.
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?
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.
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.
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.
1 to 8 of 8