9
$\begingroup$

I am curious if (any of) the various inequivalent constructions of the real line in constructive mathematics can be used to build a model of Kock and Lawvere's synthetic differential geometry? In other words, do any of the constructions of the real line (in say HoTT) satisfy the Kock-Lawvere axiom for a class of functions which deserve to be called smooth? If not, how can we "augment" the real line with nilpotent infinitesimals for this to be true?

I am a complete novice when it comes to constructive mathematics, but I'm reasonably comfortable with Anders Kock's synthetic differential geometry texts. Unfortunately, I haven't had a chance to read the Models of SDG text yet, so I apologize if this is covered there.

Improve this question
$\endgroup$
12
  • $\begingroup$ Do you mean, can one build a sheaf model of SDG inside constructive mathematics by starting from these real numbers, analogously to how one builds a sheaf model of SDG inside classical mathematics by starting from the classical real numbers? Or do you mean, can one prove inside a particular model of constructive mathematics that these real numbers satisfy the Kock-Lawvere axioms for a line object? $\endgroup$
    – Mike Shulman
    Commented Nov 16, 2017 at 0:38
  • 5
    $\begingroup$ Not in any straightforward way, since “x^2 = 0 implies x = 0” holds constructively, but not in SDG. $\endgroup$
    – user44143
    Commented Nov 16, 2017 at 1:46
  • 3
    $\begingroup$ Yes. After all, the proof is easy: For each n, |x|>0 or |x|<1/n, but the first option is incompatible with x^2=0. So for each n, |x|<1/n. So x=0. For anything worth calling "a construction of the real line in constructive mathematics", that argument should work. $\endgroup$
    – user44143
    Commented Nov 16, 2017 at 2:46
  • 1
    $\begingroup$ @MattF What is a "post-constructivist"? Google wasn't helpful with this term. $\endgroup$
    – ಠ_ಠ
    Commented Nov 16, 2017 at 22:55
  • 1
    $\begingroup$ @MattF. I would not call your (c) a "criterion of equality", not like (a) and (b): its conclusion is indeed an equality, but its hypothesis also involves equalities, so it's rather a property that the entire ring satisfies. I think Michael is asking a good question, which I would phrase precisely like this: is there any constructive construction of a ring which (1) produces the Kock-Lawvere line object when interpreted in a standard model of SDG, and (2) produces the classical real numbers when interpreted in classical mathematics? I suspect not, but I don't think I have a proof. $\endgroup$
    – Mike Shulman
    Commented Nov 17, 2017 at 4:25

1 Answer 1

Reset to default
6
$\begingroup$

In the smooth-topos models of SDG, the situation is generally something like this. The internally-definable Cauchy real numbers $\mathbf{R}_c$ are the sheaf of locally constant $\mathbb{R}$-valued functions, while the internally-definable Dedekind real numbers $\mathbf{R}_d$ are the sheaf of continuous $\mathbb{R}$-valued functions. In between these there is the sheaf $\mathbf{R}_s$ of smooth $\mathbb{R}$-valued functions, $\mathbf{R}_c \to \mathbf{R}_s \to \mathbf{R}_d$, which in turn is a quotient of the "line object" $\mathbf{R}_l$ that contains infinitesimals. Despite much trying, I don't know of any internal construction that produces $\mathbf{R}_s$ or $\mathbf{R}_l$ in these toposes; it seems that they have to be considered extra structure with which the topos is equipped. However, they are related to other structure it has, such as differential cohesion. You may also be interested in smooth structures on a topos.

Improve this answer
$\endgroup$
8
  • $\begingroup$ If I understand Lawvere's intent correctly, when objects of your topos are certain functors on $\mathbb R$-algebras, then the forgetful functor should correspond to $\mathbb R_l$, with the tiny object $D$ represented by $\mathbb R[\varepsilon]/(\varepsilon^2=0)$ sitting inside. What I cannot figure out right away is what is the subobject $R$ of $D^D$ consisting of zero preserving endomorphisms that Lawvere would consider. Is this $R$ isomorphic to any of the $\mathbb R_c$, $\mathbb R_l$, $\mathbb R_s$ or $\mathbb R_d$?? $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Nov 16, 2017 at 9:54
  • 2
    $\begingroup$ Yes, that's $\mathbf{R}_l$. I don't know the answer to the other question, but you could check Moerdijk-Reyes to see if they consider it, or write out the definition and unravel it as a sheaf. $\endgroup$
    – Mike Shulman
    Commented Nov 16, 2017 at 17:27
  • 2
    $\begingroup$ @მამუკაჯიბლაძე Imposing some abstract conditions on $D$ to recover $R$ seems to be one of the suggestions of Lawvere. See for example his article Euler’s Continuum Functorially Vindicated or this talk by Peter Johnstone. $\endgroup$
    – Michael Bächtold
    Commented Nov 16, 2017 at 21:48
  • 2
    $\begingroup$ @მამუკაჯიბლაძე the n-lab and other sources call $D$ the smallest (non-trivial) tiny object. Might a property like "$D$ has no sub objects besides the point and itself" help to characterise it? $\endgroup$
    – Michael Bächtold
    Commented Nov 17, 2017 at 8:41
  • 2
    $\begingroup$ @ಠ_ಠ you can certainly build something like them. The abstract theory of sheaf toposes on sites works fine constructively, and there are constructive notions of smooth function and so on. I don't know how many of the same properties the resulting toposes have though. $\endgroup$
    – Mike Shulman
    Commented Nov 19, 2017 at 11:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .