7
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – მამუკა ჯიბლაძე Oct 25 '16 at 3:41
  • 2
    $\begingroup$ I can't think of anything else you could hope to get in the case of G-sets... $\endgroup$ – Mike Shulman Oct 27 '16 at 3:05
  • $\begingroup$ @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 [1], nothing good left). I'm asking this question just to confirm that puncture a topos is not a trivial thing. $\endgroup$ – h__ Oct 27 '16 at 4:30
  • $\begingroup$ @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. $\endgroup$ – h__ Oct 27 '16 at 6:27
  • 2
    $\begingroup$ @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. $\endgroup$ – Andrej Bauer Oct 27 '16 at 6:37
2
$\begingroup$

A more general question is how do you form the image of a geometric morphism f : E -> F, as a subtopos of F, and how do you form its complement? Recall that if U is a subobject of 1 in F then it defines an open subtopos (given by the operator U => ? on subobjects of 1) and its closed complement F-U is given by the operator of union with U on subobjects of 1. The closure of the image of f has to be the complement of the suprema of all the subobjects U of 1 in F for which f*(U) is 0. I have memories of a nice paper by Anders Kock about glueing which may yield more.

$\endgroup$
  • 1
    $\begingroup$ You probably mean Glueing Analysis for Complemented Subtoposes by Kock and Plewe? It contains characterization of some complemented subtoposes, but I wonder whether all complemented subtoposes have been described anywhere. Maybe for points it is easier... $\endgroup$ – მამუკა ჯიბლაძე May 20 '17 at 20:57
  • $\begingroup$ I believe Harry Simmonds wrote a paper on complementation, but I cannot remember the title. $\endgroup$ – Gavin Wraith May 22 '17 at 8:33
  • $\begingroup$ Hard to say - Simmons has almost all of his work, including the full publication list, displayed on his homepage but I could not find it there. Actually there also is a paper "Sublocale lattices" by Till Plewe which presents some further progress after his paper with Kock. However in any case all of the above could only help with localic toposes, whereas the question is about general ones. $\endgroup$ – მამუკა ჯიბლაძე May 22 '17 at 9:30

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.