What is Kock's "comprehensive axiom" in synthetic differential geometry?

81 Views Asked by At

Anders Kock mentions many axioms in his book about synthetic differential geometry. It seems that, what nlab calls: "the Kock-Lawvere axiom", is called axiom $1^W_k$ in the book. This axiom states that for a Weil algebra $W$ over $k$ we have that $R \otimes W$ is isomorphic to $R^{\text{Spec}_R(W)}$.

This makes a decent amount of sense to me, however in this book axiom $1^W_k$ is actually a consequence of axiom $2^k$, which he calls: "The comprehensive axiom". This axiom states that for finitely presented $k$-algebras $B$, and any $R$-algebra $C$, the canonical map $$\text{hom}_{R\text{-Alg}}(R^{\text{Spec}_R(B)},C) \to \text{Spec}_C(B)$$ is an isomorphism.

I don't quite understand this axiom and I especially don't get why one would assume this, as it is not necessarily about infinitesimals.

So why is this axiom assumed? Is this axiom maybe just a standard result in algebraic geometry, and if so which?