Constant derivative in SDG

Question

In the context of Synthetic Differential geometry as in the first few sections of Kock's book, so that $R$ is ring satisfying Axiom 1. Let ${f : R \rightarrow R}$ be such that ${f' = 0}$. How do you prove that $f$ is constant?

Answer 1

In most developments of classical analysis, one proves this theorem early on.

However, in synthetic differential geometry, the proof requires the use of the more complicated order and integration axioms, so is usually left for later.

Hadamard's lemma (Proposition 13.1 on page 50 in my edition of Kock's book) gives the following:

For any $a \leq b \in $ and function $f: [a,b] \rightarrow R$, and any $x,y \in [a,b]$, we have that $$ f(y) - f(x) = (y - x) \int_{0}^{1} f'(x + t(y-x)) \:dt$$

Therefore, if $f:R \rightarrow R$ satisfies $f'(z) = 0$ for all $z \in [a,b]$, we immediately get that $$f(y) - f(x) = (y-x) \int_{0}^{1} 0 \:dt = 0$$ and so $f(y) = f(x)$. Since $a,b,x,y$ were arbitrary, it follows that $f$ is constant everywhere.