Constructive analysis and synthetic differential geometry

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.

• 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? Nov 16 '17 at 0:38
• Not in any straightforward way, since “x^2 = 0 implies x = 0” holds constructively, but not in SDG. Nov 16 '17 at 1:46
• 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. Nov 16 '17 at 2:46
• @MattF What is a "post-constructivist"? Google wasn't helpful with this term.
– ಠ_ಠ
Nov 16 '17 at 22:55
• @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. Nov 17 '17 at 4:25

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.
• 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$?? Nov 16 '17 at 9:54
• 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. Nov 16 '17 at 17:27
• @მამუკაჯიბლაძე 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. Nov 16 '17 at 21:48
• @მამუკაჯიბლაძე 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? Nov 17 '17 at 8:41