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
    • CommentTimeJan 11th 2011

    Should the predicate \Diamond on a formal topology be regarded as making it into an overt space?

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJan 13th 2011

    No.

    Impredicatively (and therefore in every topos), every formal space has a positivity predicate, even though not every locale is overt (and of course, every formal space gives rise to a locale which ought to be the same space in different guise).

    I see that some places (at least page 12 of Bas Spitter’s Located and overt locales) say things like

    If a locale carries a positivity predicate it is said to be overt, or open

    However, the definition there of ‘positivity predicate’ is stricter (and is indeed equivalent to giving rise to an overt locale).

    This all reinforces my idea that there is a lot of variation in discussion of formal topology, and I’m no longer sure that following Sambin (as I did in the article) is the right thing to do.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 13th 2011

    Can you say anything about why every formal space impredicatively has a positivity predicate, and how it differs from overtness?

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeJan 13th 2011
    • (edited Jan 13th 2011)

    Sure. As indicated in the third remark following the definition at formal topology, a\Diamond{a} holds iff every cover of aa is inhabited. So impredicatively, we can define

    a:SaU:𝒫S,aUx:S,xU. a\colon S \;\vdash\; \Diamond{a} \;\coloneqq\; \forall U\colon \mathcal{P}S,\; a \lhd U \;\Rightarrow\; \exists x\colon S,\; x \in U .

    But as this definition involves a quantification over subsets of SS, it’s impredicative. (Predicatively but nonconstructively, we can also define a¬(a)\Diamond{a} \;\coloneqq\; \neg(a \lhd \varnothing). Classically, these definitions agree.)

    Now, a locale is overt iff every open has a cover consisting only of positive opens. (This is in impredicative but constructive locale theory; it should be in the Elephant.) I believe that the condition Pos on page 12 of Spitter is the analogue to this. Correcting an obvious typo and putting it in my notation, this reads

    U:𝒫S,a:SaUa{x:S|xUx}. U\colon \mathcal{P}S,\; a\colon S \;\vdash\; a \in U \;\Rightarrow\; a \lhd \{x\colon S \;|\; x \in U \;\wedge\; \Diamond{x}\} .

    This is evidently stronger than my axiom (8), which I got from Sambin (first cited reference, bottom of page 3). (The other axioms in the definition on pages 11&12 all correspond, if you assume that SS is a semilattice, except that I don’t understand what Unit is supposed to even mean.)

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2011

    Ah, I think I get it. The positivity predicate is (as its name implies) the “notion of positiveness” which is definable, impredicatively. Overtness then adds the extra condition of “local positivity.”

    In more topos-looking terms, the positivity predicate is the left adjoint r !r_! of the pullback r *:Op(1)Op(X)r^* : Op(1) \to Op(X), which always exists impredicatively – but overtness says rather that r:X1r: X\to 1 is an open map, which means that not only does r !r_! exist, it satisfies the “Frobenius reciprocity” law.

    Also, a more generalizing name for overtness is “locally (-1)-connected”, and in the case of higher local-connectivity the existence of the left adjoint is not automatic even impredicatively.

    Does that all seem right? If so, I will add some comments to that effect in appropriate places.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeJan 15th 2011

    What does “locally (1)(-1)-connected” mean in this context? At locally n-connected (n,1)-topos, I only see a definition of that case, where the nns match. Here we have a (0,1)(0,1)-topos (and hence an (n,1)(n,1)-topos for n0n \geq 0), but you want it to be locally (1)(-1)-connected. (I could truncate it to a (1,1)(-1,1)-topos, but that no longer detects overtness.)

    Otherwise, that all seems right to me.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 15th 2011

    I was just defining “locally (-1)-connected geometric morphism” to mean “open geometric morphism.” But the definition of open geometric morphism is sort of an “internalization” to not-necessarily-localic topoi of the notion of open map of locales. I expect that by categorifying that, one could define a notion of locally k-connected (n,1)-topos for any n and k.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeJan 15th 2011

    I don’t understand why “locally (1)(-1)-connected” should mean “open”, in either the context of 11-toposes or (0,1)(0,1)-toposes. But I don’t understand local connectedness in that context very well, so that should not surprise you.

    I do see the connection between open geometric morphisms and locally connected geometric morphisms, in that both have a left adjoint to the inverse image functor (among other properties). But a locally connected geometric morphism to 11 is the same as an essential geometric morphism, which has only that property, whereas an open geometric morphism to 11 is stronger. So if a morphism to 11 is locally 11-connected iff it has a left adjoint, I don’t see how such a morphism is (1)(-1)-connected only iff it also satisfies Frobenius reciprocity!

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 15th 2011

    Well, that’s because what I said in #5 is wrong! According to the Elephant (at about C3.1.16), for locale maps to 1 it is also Frobenius reciprocity that is automatic, just like for geometric morphisms to 1. So I guess the point is rather that while one can always define “positivity” impredicatively, it doesn’t give you a left adjoint to r *r^* unless the locale is overt.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2011

    I added some explanation of this to overt space.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 16th 2011

    OK, but I still don’t understand the numbering. Do you mean to say that overtness is local 00-connectedness? You write

    this condition is the “(0,1)-topos theoretic” version of the notion of locally connected topos and locally n-connected (n,1)-topos

    but if n=0n = 0, we get a locally 00-connected (0,1)(0,1)-topos. (And if n=1n = -1, we get a locally (1)(-1)-connected (1,1)(-1,1)-topos, but that’s definitely not what we want.)

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2011

    Hmm, actually I think locally n-connected (n,1)-topos is wrong. Connectedness is one of the things where the numbering is off by one from where it “should” be: plain “connected” is the same as “0-connected” (the reason being that it’s equivalent to “π 0\pi_0 is trivial”). So an (n,1)-topos whose morphism to 1 is essential should be called (n-1)-connected.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJan 16th 2011

    Ah right, this is the old “nn-connected” should really be interpreted as short for “nn-simply connected” business. (H’m, that page should be connected better with Urs’s stuff.)

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJan 16th 2011

    Right, annoying ±1\pm 1s. Have to rush now. But Toby has fixed it, right?

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeJan 16th 2011

    Probably. But I’d like your comments here.