From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2618 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: arithmetical and geometric reals in (models of) SDG Date: Fri, 26 Mar 2004 15:07:42 +0100 (CET) Message-ID: <200403261407.PAA29318@fb04209.mathematik.tu-darmstadt.de> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018781 5013 80.91.229.2 (29 Apr 2009 15:26:21 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:26:21 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Mar 26 12:54:38 2004 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 26 Mar 2004 12:54:38 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1B6uYp-0006NL-00 for categories-list@mta.ca; Fri, 26 Mar 2004 12:51:59 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 41 Original-Lines: 31 Xref: news.gmane.org gmane.science.mathematics.categories:2618 Archived-At: Recently I was asking myself what is the relation between the arithmetical (Dedekind) reals in a topos and a ring R satisfying the usual SDG axioms (i.e. at least the Kock-Lawvere) axiom. >>From the few things I know about models of SDG it seems to me as if in the usual sheaf models (over a site Loc of `loci') the Dedekind reals form a subring of R = y(\Re) (where \Re is the locus corresponding to the reals). As long as one considers just presheaves that's clear as the Dedekind reals are given by \Delta(\Re). Probably taking sheaves that situation isn't changed dramatically? So my impression is that in the usual sheaf models of SDG the real line R carries the structure of an algebra over the Dedekind reals. However, I don't see how to construct such an embedding of Dedekind reals into R based only on the usual axioms of SDG. Of course, when given an order on R and R is assumed as a Q-algebra then one has a good candidate for a function from R to R_D sending x \in R to {q \in Q | q.1 \leq x}. But how to define purely logically an embedding of R_D into R remains mysterious (to me). I am fully aware of the fact that my question is a bit `against the strain' of SDG but we know that both kinds of reals do coexist in topos models. But is this coexistence only peaceful or rather more collaborative? I am certain that people must have thought about this but I couldn't find anything at the usual places where to look. So I would be grateful for comments (on the correctness of my above speculations) or pointers to existing literature or folklore. Best, Thomas Streicher