(The following three paragraphs are given for context. Readers already aware of the terminology can skip to “the problem” below.)
In a spatial topos $\mathop{\textbf{Sh}}(X)$ the MacNeille sections (or MacNeille reals, MacNeille cuts, Dedekind-MacNeille reals, bounded extended reals, or a wealth of other confusingly similar terms) is the sheaf whose sections on $U\subseteq X$ open are pairs $(f_\flat,f_\sharp)$ of real-valued functions on $U$ such that $f_\flat(x) = \mathop{\textrm{lim.inf}}\limits_x f_\sharp$ and $f_\sharp(x) = \mathop{\textrm{lim.sup}}\limits_x f_\flat$ for each $x\in U$ (here $\mathop{\textrm{lim.inf}}\limits_x g$ stands for $\mathop{\textrm{sup}}\limits_{V\in\mathscr{V}(x)} \mathop{\textrm{inf}}\limits_{y\in V} g(y)$ with $\mathscr{V}(x)$ the neighborhood filter of $x$, and analogously for $\mathop{\textrm{lim.sup}}\limits_x g$; note that $f_\flat$ and $f_\sharp$ are then automatically lower and uppper semicontinuous respectively).
(Reference: P. Johnstone, Sketches of an Elephant (2002), section D.4.7, where the MacNeille reals are defined internally using cuts, and the definition of the previous paragraph appears as corollary D.4.7.5(ii). Note that in A. S. Troelstra & D. van Dalen, Constructivism in Mathematics (1988), chapter 5, section 5, the same object, defined internally, is given the name “bounded extended reals”. Further note that functions such as $(f_\flat,f_\sharp)$ are also known as (in our case, locally bounded) normal uppper/lower semicontinuous, see R. P. Dilworth, “The Normal Completion of the Lattice of Continuous Functions”, Trans. Amer. Math. Soc. 68 (1950), 427–438. Finally, note that from results in Kenneth Hardy's 1968 thesis “Rings of normal functions”, 1.20–1.24, summarized in K. Hardy, “On normal functions”, General Topology and Appl. 2 (1972), 157–163, prop. 2.2, if $X$ is a Baire space, a normal function pair $(f_\flat,f_\sharp)$ can also be represented as an element of the inductive limit over all dense $G_\delta$ sets $W \subseteq U$ of the set of continuous real-valued functions on $W$ with the obvious restriction maps; we need to add “locally bounded” everywhere to agree with the object defined above, but I believe this is no problem, and clearly irrelevant to my question.)
The strict order on the MacNeille sections is (I think!) given by $(f_\flat,f_\sharp) < (g_\flat,g_\sharp)$ (on $U\subseteq X$ open) iff $f_\sharp(x) < g_\flat(x)$ for each $x \in U$. Addition and multiplication are not given by pointwise operations on $f_\flat,f_\sharp$, but when $X$ is a Baire space they can be defined by restricting to a dense $G_\delta$ on which the function is continuous (see reference to Hardy in previous paragraph) and then performing pointwise operations on this restriction.
The problem: P. Johnstone, Sketches of an Elephant, proposition D.4.7.10(i), claims that if $f$ is a MacNeille section which is invertible, then $f>0$ or $f<0$ holds in $\mathop{\textbf{Sh}}(X)$ (which means externally that $X$ is covered by an open set on which the restriction of $f$ is $>0$ and an open set on which the restriction of $f$ is $<0$). I believe this is incorrect, and a counterexample is provided by $X=\mathbb{R}$ and $f$ the “step” function taking the value $-1$ on the negative reals and $+1$ on the positive reals (at $0$ we have $f_\flat(0)=-1$ and $f_\sharp(0)=+1$, at all other points they coincide): this MacNeille section satisfies $f^2=1$ identically (so it is certainly invertible), but the open set where $f>0$ consists of the positive reals, the open set where $f<0$ consists of the negative reals, and they do not cover $X=\mathbb{R}$.
Questions: Is my counterexample correct¹ and is the statement in the Elephant indeed flawed? If so, is there a correct statement that is analogous, or should we simply disregard this? (I believe a correct statement is that $f$ is invertible iff $|f|>0$, where $|f| = \mathop{\textrm{sup}}\limits ( f,-f ) $.)
- The main reason I have doubts is that I'm not sure I correctly translated the definition of the strict order on the MacNeille sections, defined internally, into the relation on the pair of normal semicontinuous functions above, or that I have the right multiplication, but on this example I fail to see what else it could be.
Meta: I hesitate on how to tag this question. I'm giving it the “topos-theory” and “constructive-mathematics” because it's about a statement in the Elephant and the validity of a statement that can be formulated in constructive math, but you can also make the case that it's a question about rings of continuous and semicontinuous functions on a topological space. Feel free to add another tag if you feel strongly about this.
