# What concretely does it mean to "do mathematics in a topos X"?

I don't know if this is the right kind of question, but I've heard people say this phrase "do mathematics in a topos", and the idea that Set is the topos people usually work in, but only one of many.

Before I delve deep into category theory let me ask what I will find:

What concretely does it mean to do mathematics in a different topos than Set?

• Does it mean that if I want to prove a proposition $$\forall x, \exists y, Q(x,y)$$, I will have to prove them in very different ways?
• Does it mean that the proposition just means a different thing?
• Does it just mean that I am focusing on different propositions than I am used to?
• Does it mean that I cannot use the same logical rules I am used to?

PS. For the purpose of this question, think of me as a second year math undergrad.

If one is being precise, working a topos $$\mathcal{E}$$ means that we are going to prove some a statement in some formal system and then interpret that statement/proof into $$\mathcal{E}$$ to conclude some fact about morphisms and objects there (which then hopefully tells us something useful).

As a result, what mathematical principles you're allowed to use when carrying out this proof depends on what formal system you're using and the only real limit is that there must be a way to model this system within $$\mathcal{E}$$ (and, subjectively, this model should actually let you state and prove interesting things!)

However, when people talk about working internally to $$\mathcal{E}$$, they are often making several implicit assumptions about the formal system and its model in $$\mathcal{E}$$.

1. Usually the formal system is (intuitionistic) higher-order logic (iHOL) or extensional type theory (ETT)
2. The model is the "standard" model available in any topos which interprets various logical connectives by corresponding categorical operations.

Let's focus on iHOL. In this case, you will prove some formal statement in higher-order logic in almost exactly the way you would "ordinarily" except you must avoid the law of excluded middle ($$\forall p.\,p \lor \neg p$$) and the axiom of choice. This is the "intuitionistic" part and it is important: these principles are not valid in every topos. Once you prove something, you must work out what this statement means in $$\mathcal{E}$$. Depending on the size of the statement, this might be slightly complex but there is a translation procedure which converts formula into a statement in $$\mathcal{E}$$ in a compositional way (i.e., to convert $$p \land q$$ you translate $$p$$, then $$q$$ then do something with the results to translate the $$\land$$). For certain topoi, this process is referred to as the "Kripke-Joyal semantics/unfolding". It's worth noting that if you carry out this process for $$\mathcal{E} = \mathbf{Set}$$, you will get exactly the standard interpretation of higher-order logic. In general, however, the translation can turn a fairly simple proposition into a rather complex statement; this is the purpose of this method in some sense, since we can focus on the simpler proposition rather than the unfolded interpretation.

Finally, we must address what statement you ought to prove. This is where it gets a little tricky: often when working in $$\mathcal{E}$$ we don't want to just study some formula built of only the standard connectives of HOL. We usually also want to include special propositions, sorts, functions, and even connectives which allow us to describe some particular aspect of $$\mathcal{E}$$. In a certain sense then, we extend iHOL with new constants and correspondingly extend our interpretation of iHOL into $$\mathcal{E}$$ to interpret these new symbols as the intended objects. For instance, in the Zariski topos we might extend our logic with a new symbol to denote the 'generic ring object' which exists in this topos.

In a 'well-engineered' internal proof, usually one fixes these things up front and has a relatively minimal set of extra constants. After all, the point of working in iHOL and using the interpretation into $$\mathcal{E}$$ is to do as much as possible in IHOL to simplify one's argument.

• wow what a great answer, thank you. Is there a place I can look to learn how to use this for a simple non-Set topos? I don't know if its possible, but ideally: practice oriented with minimal categorical bsckground knowledge. (I know about iHOL though). Commented Jul 18 at 14:25
• For a specification of a certain system which is commonly used, you might look up terms such as: the Bénabou language, and Kripke-Joyal semantics. (I'm not too familiar with these references myself, but either Sheaves in Geometry and Logic or Views of an Elephant should cover those topics.) Commented Jul 18 at 14:52
• @user56834 That's a good question, but I don't know if I have a reference to hand. If you have some knowledge of algebraic geometry then the work of Ingo Blechschmidt (youtube.com/watch?v=7S8--bIKaWQ) might be nice to listen to for inspiration. The problem is that since people don't usually start category theory with topos theory, actual books/papers/etc on topos theory tend to assume familiarity with category theory. Commented Jul 18 at 14:55
• I do think Blechschmidt is the best first option for most people, though you'll probably need to know at least a bit about algebraic geometry. Commented Jul 18 at 17:32
• @user56834 maybe this series of blog posts by John Baez would be helpful (the other posts are listed at the bottom). He works through examples in simple toposes like the topos of graphs and the topos of "time-dependent sets", which are comparatively easy to understand while being different from Set in interesting ways. Commented Jul 19 at 5:17

For a quick example, let me present a simple application. The starting point will be that in intuitionistic logic, you have a tautology: $$\lnot \lnot \lnot p \leftrightarrow \lnot p$$. Now, to see how that translates in the case of a topos, we have that propositions in intuitionistic logic are translated into generalized elements of an object $$\Omega$$ of the topos, called the subobject classifier; and we have (among other things) a morphism $$\lnot \in \operatorname{Hom}(\Omega, \Omega)$$. The interpretation of the tautology given above says that for this morphism, we have $$(\lnot)^3 = \lnot$$.

In the particular case where the topos is the category of sheaves of sets on a topological space $$X$$, the object $$\Omega$$ is the sheaf where for $$U \subseteq X$$ open, $$\Omega(U) = \{ V \subseteq U \mid V \mathrm{~open} \}$$, and the restriction maps $$\Omega(U) \to \Omega(V)$$ map open $$W \subseteq U$$ to $$W \cap V \subseteq V$$. Also, the morphism $$\lnot : \Omega \to \Omega$$ turns out to be exactly the morphism defined such that $$\lnot(U) : \Omega(U) \to \Omega(U)$$ maps open $$V \subseteq U$$ to $$\operatorname{int}(U \setminus V) \subseteq U$$. If we trace through the definitions, from $$(\lnot)^3(X) = \lnot(X)$$ we can arrive at the following:

Corollary: If $$X$$ is a topological space and $$U \subseteq X$$ is open, then $$\operatorname{cl}(\operatorname{int}(\operatorname{cl}(U))) = \operatorname{cl}(U)$$.

Corollary: If $$X$$ is a topological space and $$S \subseteq X$$ is any set, then $$\operatorname{cl}(\operatorname{int}(\operatorname{cl}(\operatorname{int}(S)))) = \operatorname{cl}(\operatorname{int}(S))$$ and $$\operatorname{int}(\operatorname{cl}(\operatorname{int}(\operatorname{cl}(S)))) = \operatorname{int}(\operatorname{cl}(S))$$. In other words, both $$\operatorname{cl}\circ \operatorname{int} : \mathcal{P}(X) \to \mathcal{P}(X)$$ and $$\operatorname{int}\circ \operatorname{cl} : \mathcal{P}(X) \to \mathcal{P}(X)$$ are idempotent operations.

Now, in algebraic geometry, or in differential geometry or synthetic differential geometry, etc., we already have commonly used sheaves used in studying those topics -- for example, the structure sheaf $$\mathscr{O}_X$$ on a scheme $$X$$, or sheaves of differentials $$\Omega^1_{X/k}$$ if $$X$$ is a smooth scheme over an algebraically complete field $$k$$, or the sheaf of $$k$$-forms $$\Omega^k$$ on a differential manifold $$M$$. In those situations, it can be useful to use the Bénabou language to define other sheaves based on the sheaves under study, and/or to use the Kripke-Joyal semantics on intuitionistic theorems to derive statements of interest regarding sections of those sheaves. Furthermore, on an informal level, it can be a useful framework for thinking about those sections and what relations might exist between certain sections under study.

• $\neg$ is the map that classifies $\bot : 1 \to \Omega$, which in turn classifies $0 \to 1$, right? Is there a more "direct" way to define it? Commented Jul 18 at 16:37
• I tend to think of it as being specified uniquely by the condition that for $p, q : U \to \Omega$, $p \le \lnot q$ if and only if $p \wedge q = \bot_U$; in terms of the corresponding subobjects of $U$, where $\lnot$ corresponds to a "weak complement" operation $T \mapsto T^c$, we have $S \subseteq T^c$ if and only if $S \cap T$ (the fibered product $S \times_U T$ as a subobject of $U$) is the initial subobject of $U$. (This, of course, is a special case of $p \rightarrow q$ in a Heyting algebra being uniquely specified by the condition $r \le (p \rightarrow q)$ iff $r \wedge p \le q$.) Commented Jul 18 at 16:46
• So for example, in a complete distributive lattice, $\lnot p$ ends up being the supremum of all $q$ such that $p \wedge q = \bot$. It's not hard to see how that more or less directly translates into taking the interior of the complement in the case of sheaves on a topological space. Commented Jul 18 at 16:49
• Incidentally, this answer is largely meant as an addendum to the answer by daniel gratzer, where that answer explains the generalities well (my summary would be that the internal language of a topos is set up to look very much like type-theoretic foundations for intuitionistic mathematics, and proofs in that internal language can be done pretty much like you'd do formal proofs in a natural deduction system for intuitionistic logic). Then, this answer is an illustration of how the framework would work in a simple example, and an overview of how it could be used generally in practice. Commented Jul 18 at 17:48

Mathematicians use sets all of the time. A topos is an axiomatisation of the category of sets using the language of category theory. This is one sense of what mathematics done in a topos means.

In another sense, every topos has an internal lanuage which is intuitionistic logic and hence one can formalise an argument in this language.

There is also the notion of internalisation when we define a matgematical object in the context of some ambient category. For example, the usual notion of a category is defined in the category Set. If we change the ambient context to Cat, then a category in the context of Cat is the notion of a strict 2-category.