Start a new discussion

Not signed in

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

Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeNov 19th 2016

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.

• CommentRowNumber2.
• CommentAuthorIngoBlechschmidt
• CommentTimeApr 1st 2017
• (edited Apr 1st 2017)

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.)

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeApr 2nd 2017

• CommentRowNumber4.
• CommentAuthorTobyBartels
• CommentTimeFeb 20th 2019

Replace ‘subset’ with ‘subspace’ for generality’s sake (except in one case where the specificity was proper).

• CommentRowNumber5.
• CommentAuthortphyahoo
• CommentTimeFeb 18th 2020
"2. Motivation
Recall that a topological space X is compact if and only if, for every other space Y and any open subspace U of X×Y, the subspace

∀XU={b:Y|∀a:X,(a,b)∈U}
is open in Y."

This was not obvious to me. I asked about it on compact spaces page and Todd said this is proven in escardo 09, lemma 4.3. Can we add a pointer here, or otherwise make it easier to understand this fact?

escardo 09: https://www.cs.bham.ac.uk/~mhe/papers/compactness-submitted.pdf
• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeFeb 18th 2020
• (edited Feb 18th 2020)

Thanks that you are looking into this.

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!

• CommentRowNumber7.
• CommentAuthortphyahoo
• CommentTimeFeb 18th 2020
For sure, I'll give it a shot.
• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 18th 2020

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”.)

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeFeb 29th 2020

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.

• CommentRowNumber10.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 29th 2020

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.