Research

The internal language of toposes

Very briefly, a topos is a category 𝓔 which is sufficiently rich to support an internal language, a device which allows to pretend that the objects of the topos are plain old sets and that the morphisms of the topos are plain old maps between those sets. We write “𝓔 ⊨ φ” to express that the statement φ holds from the internal perspective of 𝓔. We can picture toposes as universes in which we can do mathematics in, since the internal language supports logical reasoning: Any (intuitionistically) provable statement holds in the internal language of any topos.

The prototypical topos is Set, the category of sets. Its internal language is the usual mathematical language, in that 𝓔 ⊨ φ holds if and only if φ holds in the usual sense.

A further example is Eff, the effective topos. A statement holds in Eff if and only if it can be witnessed by a Turing machine. For instance, the statement “for any number, there exists a prime larger than it” holds in Eff, since there is a Turing machine which given a number computes a larger prime number. In contrast, the statement “any Turing machine halts or doesn’t halt” is false in Eff, since its external meaning is that there exists a Turing machine which determines whether a given Turing machine halts or doesn’t halt. But such a halting oracle doesn’t exist. This example demonstrates that generally, toposes only support intuitionistic reasoning.

You can learn more about the effective topos here.

Applications in commutative algebra

Let A be a commutative ring with unit. The topos Sh(Spec(A)) of set-valued sheaves over the spectrum of A contains a mirror image of A, the structure sheaf 𝓞_Spec(A). From the point of view of Sh(Spec(A)), this sheaf of rings is an ordinary ring. To a first approximation, this ring can be thought of as a reification of all stalks of A. For instance, 𝓞_Spec(A) is an integral domain from the point of view of Sh(Spec(A)) if and only if all stalks of A are integral domains.

However, the sheaf 𝓞_Spec(A) also has unique properties not shared by A or its stalks, and this is where the internal point of view derives most of its uses and its interest from. One of the most important such properties is that 𝓞_Spec(A) is almost a field, in the sense that, from the point of view of Sh(Spec(A)), any element of 𝓞_Spec(A) which is not invertible is nilpotent. If A is assumed to be a reduced ring, then 𝓞_Spec(A) is reduced as well, in which case 𝓞_Spec(A) really is a field.

This observation can be exploited, for instance, to give a constructive one-paragraph proof of Grothendieck’s generic freeness lemma, basically because Grothendieck’s generic freeness lemma is trivial for fields. The previously known proofs are somewhat convoluted and proceed in a series of reduction steps, while the new proof is direct and even constructive.

Applications in algebraic geometry

Towards synthetic algebraic geometry

Details

Details can be found in my PhD thesis. Large portions require only familiarity with scheme theory, not with topos theory.

I’m always happy to answer questions and discuss topos-related matters by mail.

I’m keeping a research diary. It’s public, but probably of limited usefulness to others.