Thoughts on Noncommutative Synthetic Differential Geometry

What is SDG?

Synthetic Differential Geometry is the study of constructive logic augmented with, at minimum, the following axioms.

• \(R\) is a ring.

• Let \(D = \{x \in R \mid x^2=0\}\). Then the linear map \(R^2 \to (D \to R)\) given by \((a,b) \mapsto (x \mapsto a+bx)\) is invertible.

These axioms make it trivial to build up many of the common concepts from calculus. For instance, the inverse of \((a,b) \mapsto (x \mapsto a+bx)\) acts as the function \(f \mapsto (f(0), f'(0))\). And suddenly we have derivatives.

Other concepts are just as easy. The tangent bundle to a manifold \(M\) is simply the type \(D \to M\). Literally an infinitesimal curve in the manifold!

These ideas are explored in far more depth in these books by Anders Kock.

Topos Models

A Noncommutative Version?

To me, this raises an obvious question. What if we instead look at the classifying topos of noncommutative local rings?

Let's try it.

The first thing to note is that this classifying topos is a monoidal topos. In addition to the cartesian product and coproduct, it has another, equally important monoidal structure.

We could try to simply axiomatize this monoidal product, but that's awkward. Better to build it into our ambient logic, such as is done in this thesis by Ulrich Schöpp.

But that paper is geared toward a very different topos. The Schanuel topos, which classifies infinite decidable objects. Does the type theory even apply here?

Yes. Their type theory is far more general than their paper admits. It turns out that there's a simple three-step process to model it in the classifying topos of an arbitrary theory.

• (Geometrically) define a binary relation \(\sim\) between each pair of sorts of your theory.

  • For the Schanuel topos, that's the apartness relation.
  • For the classifying topos of local rings, that's the "commutes" relation, \(x \sim y \iff xy = yx\).

• Check that \(x \sim y \iff y \sim x\).

• Fix any \(x\) in any sort of your theory. Check that, if you restrict each sort \(A\) to the subset \(\{a \in A \mid a \sim x\}\), you get a (sub)model of the same theory.

  • For the Schanuel topos, this says that removing one element of an infinite decidable object yields another infinite decidable object.
  • For the classifying topos of local rings, this says that for any \(x\) in a local ring \(R\), the centralizer \(C_R(\{x\})\) is still a local ring.

If you can do that, you can interpret Schöpp's type theory in your topos.