# Is there a way to “puncture” a topos?

Let $E$ be a (Grothendieck) topos, e.g. $E = \text{Sh}(X)$ for a topological space $X$. And let $p = (p^*, p_*):\text{Set}\to E$ be a point of $E$, is there a way to "puncture" $E$ in some sense? By "puncture" I mean a way to remove the point $p$ and still get a topos.

e.g. one may expect to get $\text{Sh}(X\backslash\{p\})$ if $E = \text{Sh}(X)$ for a topological space $X$ and $p \in X$ is a usual point. But it's not obvious to see how to do this at the level of topos.

I'm asking this question because I want to know if topoi are "unpuncturable" in some sense.

• The image of $p$ is a subtopos, and since subtoposes form a coHeyting algebra, you always can get the copseudocomplement of this subtopos. Note however that with toposes like $G$-sets (for some group $G$) you will get the trivial topos this way, which is probably not what you want. – მამუკა ჯიბლაძე Oct 25 '16 at 3:41
• I can't think of anything else you could hope to get in the case of G-sets... – Mike Shulman Oct 27 '16 at 3:05
• @MikeShulman I can't think of anything else either. Another example is the presheaf topos $\text{Fun}(C^{\text{op}}, \text{Set})$, any object of $C$ defines a point, and there is no easy way to remove it from that category without destroying most of the structure (similar to the fact that puncture the complex plane destroys simply connectedness. E.g. if one "puncture" the category of simplicial sets at the point defined by , nothing good left). I'm asking this question just to confirm that puncture a topos is not a trivial thing. – h__ Oct 27 '16 at 4:30
• @MikeShulman And I feels like it's not trivial to puncture a type in type theory, since there shall be something non-constructive going on here. E.g. if one tries to "puncture" $\mathbb{R}$ (defined as Cauchy sequence of rationals) at the point $0$, since there is no universal algorithm that can prove a sequence is non-zero constructively, there shall be some trouble. – h__ Oct 27 '16 at 6:27
• @h__: You can puncture $\mathbb{R}$ in type theory: $\Sigma_{x : \mathbb{R}} \mathrm{Id}_\mathbb{R}(x, 0) \to \mathrm{Empty}$. Even better is $\Sigma_{x : \mathbb{R}} (x < 0) + (0 < x)$. Your comment about algorithms is not correct since type theory (and constructive mathematics in greneral) can perfectly well speak about non-decidable predicates. There is no trouble, just the usual constructive difficulties. – Andrej Bauer Oct 27 '16 at 6:37