Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeJul 22nd 2015

    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 XX is a locale, write X EX_E for the object of points of XX in a topos EE, so for instance if RR is the locale of real numbers then R ER_E is the Dedekind real numbers object in EE. Then if XX is a spatial T UT_U locale and YY is a subspace, then Y EX EY_E\to X_E is relatively codiscrete. In particular, taking X=RX=R and Y=R >0Y=R_{\gt 0}, we find that strict inequality of real numbers is relatively codiscrete, hence (over a classical base with 0=0\sharp0=0) ¬¬\neg\neg-closed, which is AMP.

    • If UU is an object of the site of EE, then the slice topos E/UE/U admits a local geometric morphism to a spatial localic topos Sh(L U)Sh(L_U). Since local geometric morphisms are left orthogonal to grouplike ones, including T UT_U locales, it follows that sections X E(U)X_E(U), i.e. maps UX EU\to X_E, i.e. geometric morphisms E/UXE/U \to X, are equivalently continuous maps L UXL_U\to X. Moreover, since XX and L UL_U are spatial, such a map is just a map of sets (L U) 0X 0(L_U)_0 \to X_0 with the property of being continuous. And since YY is a subspace of XX, continuous maps L UYL_U\to Y are just continuous maps L UXL_U\to X that happen to factor through YY 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?

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 22nd 2015

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

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeJul 23rd 2015

    T UT_U is a separation axiom: a locale XX is T UT_U if, for any locale TT, the poset of locale morphisms TXT \to X is discrete.

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 23rd 2015

    Ah, thanks.