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.
At overt space there was a remark that since the definition quantifies over “spaces”, the overtness of a single space might depend on the general meaning chosen for “space”, but that no example was known to the author. I added an example involving synthetic topology, which may not be quite what the author of that remark was thinking of, but which I think is interesting.
Added to overt space two examples: locales induced by topological spaces and spectra of commutative rings in which nilpotency is decidable. (I’ll add details of the spectrum example later.)
I added a link to topological locale.
Thanks that you are looking into this.
After your request in the other thread I had already included an informal pointer here.
But the proper way to do this is, of course. to add a decent Proposition-environment to compact space of the form
+-- {: .num_defn #EscardoCharacterizationOfCompactness}
###### Proposition
**(Escardo's characterization of compactness)**
A topological space $X$ is compact precisely if...
(...)
=--
+-- {: .proof}
###### Proof
(...)
=--
and then link to that from the entry overt space by typing
Notice that (by [this Prop.](compact+space#EscardoCharacterizationOfCompactness)) a [[topological space]] is _[[compact]]_ if an olny if ...
You wanna try to do that edit? It would be a nice service to the community!
I wouldn’t necessarily call it “Escardo’s characterization of compactness”. Just because it’s in his paper doesn’t mean it originated with him. (I’m not sure who should be credited, but in any case I think it might better be called something like “overt characterization of compactness”.)
It's not the overt characterization but the dual-overt characterization; compact spaces are dual to overt spaces. But I believe that it predates overtness anyway.
I'd call it a quantifier characterization. If you have some proposition with free variables that stand for points in topological spaces, such that the truth set of the proposition is open in the product space, and you universally quantify one of the variables, then is the truth set still open? If the variable that you quantified over stood for a point in a compact space, then Yes. (And only a compact space will guarantee that the answer is Yes no matter what the rest of the details are.)
Escardó attributes this to Nachbin. But once you think of it, the proof is very follow-your-nose, especially if you already know the closed-projection characterization of compactness.
I simply meant that (to me, anyway) the etymology of “overt” might serve to remind one that preservation of opens (under appropriate quantification) is taken to be primary. The rest of what you say is obviously true.
moving redirects for overt locale, overt locales, open locale, open locales to article on locally positive locale
Anonymous
1 to 12 of 12