MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).
2

Hi !

I'm considering in a general topos $T$ the object $R$ of lower semi-continuous real (one sided lower non-empty Dedekind cuts, as for exemple in http://ncatlab.org/nlab/show/one-sided+real+number ).

I want to know if, even if substraction is not possible, there is (internally) some sort of simplification rules for addition like :

If $x$ is 'bounded' (there exist a rational q such that $x \leqslant q$ ) then $x+a=x+b$ imply $a=b$.

It's seem true to me, but only because of an argument involving a covering of $T$ by a boolean topos, if it's possible I would prefer a completely internal argument, and I can't find it.

[Edited by Andrej Bauer] A lower Dedekind cut is a subset $L \subseteq \mathbb{Q}$ which is

  • rounded: $q \in L \iff \exists r \in L . q < r$
  • inhabited $\exists q \in \mathbb{Q} . q \in L$
  • bounded: $\exists q \in \mathbb{Q} \forall r \in L . r < q$
flag
Have a look at Davorin Lešnik's PhD thesis, available at fmf.uni-lj.si/storage/19160/PhD_Davorin.pdf. He has an extensive treatment of reals, done constructively and without countable choice. I think he speaks about lower reals as well. – Andrej Bauer Sep 25 at 13:00
Please write down the definition of a one-sided cut because it is easy to get that wrong in an intuitionistic setting. – Andrej Bauer Sep 25 at 13:01
Thank you for this reference. I edited my question to include the definition of a cut. – Simon Henry Sep 25 at 14:52
I fixed your definition to make it prettier (but probably equivalent to what you had). – Andrej Bauer Sep 25 at 17:23
I confirm : this is equivalent. – Simon Henry Sep 25 at 22:31

1 Answer

1

Ok I think I finally found an internaly valid proof by my self, so I explain it briefly here in case someone is interested some day :

If $U \in \Omega$ is a subterminal object, you can define the element $1_U \in R$ as :

$q \in 1_U$ when $q < 0 \cup (U \cap q<1)$.

(this correspond to the indicator function of an open set... )

It's easy to show that if $x+1_U \leqslant y + 1_U$ then $x \leqslant y$ :

if $q < x$, then $q < x+1_U$, hence, $\exists u,v$ such that $q=u+v, u < y$ and $v < 0 \cup (v<1 \cap U)$

  • First case : $v<0$ then, $q < u < y$, we have $q < y$.
  • Second case : we have 'U' then $1_U = 1$ so $q+1 < x+1_U$,

    $q+1 < y +1$

    $q < y$

In both case, $q < y$ so $x \leqslant y$.

Now, if $x$ is any bounded positive element, let $N$ be an integer such that $x < N$.

on can define :

$\displaystyle h = \frac{1}{n} \sum_{i=1}^{N.n } 1_{x> (i/n)} $

and one can show that (but it's a little longer) : $h \leqslant x \leqslant h+\frac{1}{n}$.

It's now easy to conclude if $x$ is positive and bounded and $a + x \leqslant x + b$ then if $q < a$, take $q'$ another rational such that $q < q' < a$, let $n$ an integer such that $q'-q < \frac{1}{n}$. and let $h$ be as above :

$ a + h \leqslant a +x \leqslant b+x \leqslant b + h + 1/n $

but by a simple recurence, h can be simplified so :

$ a \leqslant b+1/n $

so $q' < b+1/n$, and finaly $q < q'-1/n < b $

If $x$ is not positive, just take some $q < x$, and $x-q$ will be positive

link|flag
I do not understand the definition of $1_U$. What does it mean to take the union of $q < 1$ and $U \cap q < 1$? What does it mean to take the intersection of $U$ and $q < 1$? Are you thinking of $U$ as a truth value, and then $\cup$ and $\cap$ are disjunction and conjunction? Ah, that must be it. So your $1_U$ is $0$ if $U$ is false and $1$ if $U$ is true (but of course that is not a definition). – Andrej Bauer Sep 27 at 12:33
exactly, I'm thinking of U, q<0 and q<1 as truth value. and $1_U$ is the indicator function. Maybe I should edit to replace $\cup$ by $\vee$ and $\cap$ bu $\wedge$. – Simon Henry Sep 27 at 12:41
I would rewrite your proof a bit. Might do. – Andrej Bauer Sep 27 at 17:16

Your Answer

Get an OpenID
or

Not the answer you're looking for? Browse other questions tagged or ask your own question.