Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeJul 22nd 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'm trying to prove the [analytic Markov's principle](http://ncatlab.org/nlab/show/Markov%27s+principle#analytic_markovs_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?

   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 is a locale, write for the object of points of in a topos , so for instance if is the locale of real numbers then is the Dedekind real numbers object in . Then if is a spatial locale and is a subspace, then is relatively codiscrete. In particular, taking and , we find that strict inequality of real numbers is relatively codiscrete, hence (over a classical base with ) -closed, which is AMP.

   • If is an object of the site of , then the slice topos admits a local geometric morphism to a spatial localic topos . Since local geometric morphisms are left orthogonal to grouplike ones, including locales, it follows that sections , i.e. maps , i.e. geometric morphisms , are equivalently continuous maps . Moreover, since and are spatial, such a map is just a map of sets with the property of being continuous. And since is a subspace of , continuous maps are just continuous maps that happen to factor through 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?

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeJul 23rd 2015
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexForgive me for being dense, but what's a $T_U$ locale?

   Forgive me for being dense, but what’s a locale?

3. • CommentRowNumber3.
   • CommentAuthorZhen Lin
   • CommentTimeJul 23rd 2015
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItex$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.

   is a separation axiom: a locale is if, for any locale , the poset of locale morphisms is discrete.

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeJul 23rd 2015
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAh, thanks.

   Ah, thanks.