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.
Should the predicate ⋄ on a formal topology be regarded as making it into an overt space?
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.
Can you say anything about why every formal space impredicatively has a positivity predicate, and how it differs from overtness?
Sure. As indicated in the third remark following the definition at formal topology, ⋄a holds iff every cover of a is inhabited. So impredicatively, we can define
a:S⊢⋄a≔∀U:𝒫S,a⊲U⇒∃x:S,x∈U.But as this definition involves a quantification over subsets of S, it’s impredicative. (Predicatively but nonconstructively, we can also define ⋄a≔¬(a⊲∅). 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:S⊢a∈U⇒a⊲{x:S|x∈U∧⋄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 S is a semilattice, except that I don’t understand what Unit is supposed to even mean.)
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! of the pullback r*:Op(1)→Op(X), which always exists impredicatively – but overtness says rather that r:X→1 is an open map, which means that not only does 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.
What does “locally (−1)-connected” mean in this context? At locally n-connected (n,1)-topos, I only see a definition of that case, where the ns match. Here we have a (0,1)-topos (and hence an (n,1)-topos for n≥0), but you want it to be locally (−1)-connected. (I could truncate it to a (−1,1)-topos, but that no longer detects overtness.)
Otherwise, that all seems right to me.
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.
I don’t understand why “locally (−1)-connected” should mean “open”, in either the context of 1-toposes or (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 1 is the same as an essential geometric morphism, which has only that property, whereas an open geometric morphism to 1 is stronger. So if a morphism to 1 is locally 1-connected iff it has a left adjoint, I don’t see how such a morphism is (−1)-connected only iff it also satisfies Frobenius reciprocity!
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* unless the locale is overt.
I added some explanation of this to overt space.
OK, but I still don’t understand the numbering. Do you mean to say that overtness is local 0-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=0, we get a locally 0-connected (0,1)-topos. (And if n=−1, we get a locally (−1)-connected (−1,1)-topos, but that’s definitely not what we want.)
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 is trivial”). So an (n,1)-topos whose morphism to 1 is essential should be called (n-1)-connected.
Ah right, this is the old “n-connected” should really be interpreted as short for “n-simply connected” business. (H’m, that page should be connected better with Urs’s stuff.)
Right, annoying ±1s. Have to rush now. But Toby has fixed it, right?
Probably. But I’d like your comments here.
1 to 15 of 15