3
$\begingroup$

I was watching Tom LaGatta's talk on category theory recently, and one of the audience brought up a statement that caught my attention (around the 56:15 mark):

I was gonna say, there was a book I read, and they claim that some fella discovered there was a functor between differential equations and [...] logic with quantifiers.

I tried searching for some pointers in Google, MO and nLab, but came up with nothing relevant. Does anyone have any idea what result specifically he was talking about?

$\endgroup$
  • $\begingroup$ Also, I wasn't sure whether to post this on math.SE or here, so please, do correct me if it's not appropriate here. $\endgroup$ – Matěj G. Apr 14 '16 at 20:09
  • 2
    $\begingroup$ How do these things even form a category? $\endgroup$ – Thomas Rot Apr 14 '16 at 21:26
  • $\begingroup$ @MatějG. I think this is far above the limit of "research level", and it definitely belongs here. $\endgroup$ – Amir Sagiv Apr 16 '16 at 9:04
6
$\begingroup$

I'm not sure what "book" prompted them to say this, but the ideas sound like the ideas from Synthetic Differential Geometry (SDG) (see also Synthetic Geometry of Manifolds) and Fractional Exponential Functors and Categories of Differential Equations, and the "fella" was probably Anders Kock (probably via Bill Lawvere). Lawvere has a brief, informal set of seminar notes that sketches the idea (unfortunately the PDF is somewhat broken) and led to the fractional exponential functors paper.

Very roughly sketching SDG and considering only first-order (autonomous) ordinary differential equations, we model the "real line" as a rig object $R$ in our (Grothendieck) topos, $\mathcal{E}$, and we characterize a subobject of $R$, $D$, via the following axiom (the simplest form of the Kock-Lawvere axiom): the map $(x,y) \mapsto (d \mapsto x + dy) : R^2 \to R^D$ is an isomorphism. In particular, we can write the inverse map as $f \mapsto (f(0), f'(0))$. We think of the elements $d \in D$ as the elements of $R$ such that $d^2 = 0$. We see that every map in $D \to R$ is affine. (Objects which have this property are generally called "microlinear" which includes any powers of $R$.) The tangent bundle of $X$ is represented by the arrow $\pi_X \equiv f \mapsto f(0) : X^D \to X$. A vector field (i.e. an autonomous first-order ODE) on $X$ can be viewed as an arrow $v : X \to X^D$ which satisfies $v(x)(0) = x$. We can form the category of $(-)^D$-coalgebras (not comonad coalgebras) and the category of vector fields will be a subcategory of that, namely coalgebras that are sections of $\pi$.

As a generality, the category of coalgebras for a right adjoint endofunctor on a Grothendieck topos is itself a Grothendieck topos and has an essential geometric surjection from the base topos to it. Now here's where things get interesting. In (at least some forms of) SDG, $(-)^D$ has a right adjoint written $(-)^{\frac{1}{D}}$. To get the category of 1ODEs to be a Grothendieck topos, we need to show that the subcategory they correspond to is still a Grothendieck topos. In the fractional exponents paper, this is done by proving a general result (Theorem 2) about certain equifiers. Second order ODEs arise from arrows $X^D \to X^{D_2}$ for which we use the transpose $X \to X^{D_2/D}$ and then essentially the same argument. Grothendieck toposes enable geometric logic, so categories of 1ODEs and 2ODEs (as well as the underlying topos $\mathcal{E}$) support finitary conjuction, infinitary disjunction, and existential quantification in a way that will be preserved by the inverse image functor of the geometric surjection. Grothendieck toposes are also elementary toposes and so support additionally universal quantification and implication (and are models of an intuitionistic set theory), but this additional structure won't be preserved by geometric morphisms. (As an aside, elementary toposes also support a dependent product type and (global) sections of bundles are just global elements of dependent products, i.e. a vector field on $X$ is a (global) element of $\prod x\!:\!X.\{ f : X^D\ |\ f(0) = x \}$ using a type theoretic notation.)

$\endgroup$
  • $\begingroup$ Do I understand this correctly (in very layman terms) that the categorical interpretation of 1/2ODEs induces a structure that also happens to support a form of intuitionistic logic via the Grothendieck topos, so that the logic is kind of "embedded" in it? Is this the case rather than, what seems to have been suggested in the video in OP, that there is a mapping from ODEs to logical formulae with quantifiers (as is the case, for instance, in the Curry–Howard correspondence)? $\endgroup$ – Matěj G. Apr 18 '16 at 20:12
  • $\begingroup$ @MatějG. So there are, at least, three things going on. The logical formulae in the internal language of the topos that 1/2ODEs form are, like everything in the topos, ODEs and maps between them, in exactly the CH way. There's also a mapping of 1/2ODEs into $\mathcal{E}$ which has it's own internal language with quantification. Finally, as I alluded to at the end, if we take the right adjoint of pullback along the unique map $X\to 1$ and apply it to the tangent bundle $\pi_X : X^D\to X$, we get a "type" of vector fields on $X$ (including the section constraint!). $\endgroup$ – Derek Elkins left SE Apr 19 '16 at 3:28
  • $\begingroup$ Still, a lot of this is not patently obvious from the resources I mentioned, so I'm somewhat hesitant to imagine these are the "book" the audience member refers to. There is also general categorical semantics for (arbitrary) differential equations (with or without SDG) and, very recently, differential homotopy type theory, which may provide a different perspective and may hold a better answer. $\endgroup$ – Derek Elkins left SE Apr 19 '16 at 3:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.