Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m trying to prove the analytic Markov’s principle “synthetically” in classical real-cohesion. The proof I know that it holds in a topological model goes by way of the following two statements:
If $X$ is a locale, write $X_E$ for the object of points of $X$ in a topos $E$, so for instance if $R$ is the locale of real numbers then $R_E$ is the Dedekind real numbers object in $E$. Then if $X$ is a spatial $T_U$ locale and $Y$ is a subspace, then $Y_E\to X_E$ is relatively codiscrete. In particular, taking $X=R$ and $Y=R_{\gt 0}$, we find that strict inequality of real numbers is relatively codiscrete, hence (over a classical base with $\sharp0=0$) $\neg\neg$-closed, which is AMP.
If $U$ is an object of the site of $E$, then the slice topos $E/U$ admits a local geometric morphism to a spatial localic topos $Sh(L_U)$. Since local geometric morphisms are left orthogonal to grouplike ones, including $T_U$ locales, it follows that sections $X_E(U)$, i.e. maps $U\to X_E$, i.e. geometric morphisms $E/U \to X$, are equivalently continuous maps $L_U\to X$. Moreover, since $X$ and $L_U$ are spatial, such a map is just a map of sets $(L_U)_0 \to X_0$ with the property of being continuous. And since $Y$ is a subspace of $X$, continuous maps $L_U\to Y$ are just continuous maps $L_U\to X$ that happen to factor through $Y$ as a map of sets. This gives the relative codiscreteness in the previous claim.
Now I’m trying to extract from one or the other of these statements something that can be proven from categorical adjoint-functor properties like the others that we see in cohesion (plus, perhaps, classicality properties of the base topos). The second one is a standard sort of “big topos” property, but it seems sort of orthogonal to the other kind of “big topos” properties that a cohesive topos has (locality, stable/punctual local connectedness, etc.). Anyone have thoughts?
Forgive me for being dense, but what’s a $T_U$ locale?
$T_U$ is a separation axiom: a locale $X$ is $T_U$ if, for any locale $T$, the poset of locale morphisms $T \to X$ is discrete.
Ah, thanks.
1 to 4 of 4