2
$\begingroup$

[Cross-posted from M.SE, where it didn't get an answer]

In constructive logic, it's possible for a set $X$ to satisfy $$\forall x,y \in X.\, x = y$$ while being non-trivial. Such a set is called a subsingleton. Now consider the set of all subsingletons over a set $S$, denoted $S_\perp$. The question is, what are its sections in a sheaf topos? Or rather, how do the sections of $S$ relate to the sections of $S_\perp$?

I have a guess: The sections of an open subset $U$ of $S_\perp$ are pairs $(V, f)$ where $V$ is an open subset of $U$ and $f$ is a section of $V$ in the sheaf $S$.

I guess one could compute what the sections are by applying Kripke-Joyal semantics to the expression $\{X \in \mathcal P(S) \mid \forall x,y \in X.\, x=y\}$. I'm trying to figure out how to do that from Page 22 of this: https://rawgit.com/iblech/internal-methods/master/notes.pdf

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ Look at $S_\bot$ as a subsheaf of $\mathcal P(S)$. Sections of $\mathcal P(S)$ over an $U$ correspond to arbitrary subsheaves $R\subseteq[U]\times S$. Here $[U]$ is the sheaf corresponding to $U$, it has a single section over $V\subseteq U$ and no sections over $V\nsubseteq U$. Sections of $S_\bot$ over $U$ correspond to such $R$ that the composite $R\subseteq[U]\times S\to[U]$ with the projection is an inclusion. This inclusion then identifies $R$ with a subsheaf of $[U]$ which always has form $[V]$ for some $V\subseteq U$, and $R\subseteq[U]\times S\to S$ determines a section of $S$ over $V$ $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Dec 8, 2019 at 11:07
  • 1
    $\begingroup$ Conversely a pair $(V,f)$ as in your guess gives a sheaf map $[V]\to S$ which in turn determines an inclusion $(i,[f]):[V]\rightarrowtail[U]\times S$, where $i:[V]\to[U]$ corresponds to the inclusion of $V$ into $U$ and $[f]:[V]\to S$ corresponds to $f$. $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Dec 8, 2019 at 11:13
  • $\begingroup$ @მამუკაჯიბლაძე Thanks! $\endgroup$
    – wlad
    Commented Dec 8, 2019 at 11:14
  • 1
    $\begingroup$ Alternatively, you can use internal logic to prove the following: Given $V \subset U$ and $V \rightarrow S$, there is a unique map $U \rightarrow S^{\perp}$ which makes the square a pullback. This shows that (externally) maps from an arbitrary object $U$ so $S^\perp$ are the same as pairs $V \subset U$ and $f:V \rightarrow U$. You then get the desired result by applying this to $U$ a representable sheaf. $\endgroup$
    – Simon Henry
    Commented Dec 8, 2019 at 15:47

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .