adding a few sentences on compact topological spaces vs compact convergence spaces in constructive mathematics in section “Compactness via convergence”. In particular, the failure of the equivalence of the definitions in constructive mathematics suggests that this article needs to be split up into “compact topological space” and “compact convergence space”, because that compact topological spaces (in the sense of open covers and finite subcovers) are compact convergence spaces (in the sense of nets and convergent subnets) implies excluded middle.

Anonymous

]]>Yes, the distinction isn’t relevant for compactness.

]]>Right, that would be a more structural (actually, algebraic over posets) notion of direction where the phrase “define a direction” would make sense. It seems that direction (written largely by Toby, I think) was not written with this possibility in mind – and offhand, it strikes me as a superfluous consideration for the compact space article.

]]>I don’t know if this is what tphyahoo has in mind, but in constructive mathematics one might want the “directedness” of a directed poset to be given by a function assigning a particular upper bound to any two elements, since in the absence of choice having such a thing is a stronger assumption than the mere existence of upper bounds. However, in a join-semilattice there is always a function that selects the *least* upper bound, since those are uniquely defined.

By the way, I don’t mean to sound overly harsh in my last comment. In view of the way the article direction is written, it’s not necessarily wrong to speak of “defining a direction” (on a set) – it’s just that in this context, it sounds really weird and overly elaborate to write that way. It would be more appropriate to write that way if one started with a set $S$ and was contemplating, among the infinitely many ways in which $S$ could carry a structure of directed partial order, which one of them one wishes to single out as the topic of discussion. But in the present discussion, there’s really no choice in the matter: the only relevant partial ordering is given by subset inclusion (or the given partial order if one is starting with a frame or subsets of a frame), and it’s only a question of whether the poset under discussion is directed or not.

So much so that if a reader encounters the phrase “define a direction by” in the article compact space, it would be natural to wonder if the author was confused or didn’t quite understand what they were talking about.

]]>It’s really very simple: a poset is directed if it is nonempty and any two elements have a common upper bound. The upper bound doesn’t have to be the union.

I sort of wish you’d get away from this idea of “defining a direction” here. In practice, one defines a partially ordered set, and then that partially ordered set is either directed or it isn’t: there is no extra step of “defining a direction” that needs to be done. (Even “defines a partial order” sounds too elaborate, because in this context the partial order is invariably subset inclusion.) As far as any defining goes: at some point in the proof, one introduces (or defines) an open cover $\mathcal{U}'$ and then *verifies* that it is directed.

I don’t know what is confusing you in this article, but let’s talk about it here. We have the traditional notion of compact space: every open cover has a finite subcover. The proposition in question states that compactness of a space $X$ is equivalent to another condition: that any directed open cover of $X$ has $X$ among its elements. I’ll call that condition D.

Let’s just take a moment to be very explicit what all this means. First, an *open cover* of $X$ is a collection $\mathcal{U}$ of open subsets $U \subseteq X$ whose union is $X$. An open cover $\mathcal{U}$ is *directed* if, whenever one is given finitely many elements $U_1, \ldots, U_n \in \mathcal{U}$, there is an element $U \in \mathcal{U}$ such that $U_1 \subseteq U, \ldots, U_n \subseteq U$, in other words there exists an element $U \in \mathcal{U}$ that is an upper bound of the $U_1, \ldots, U_n$ with respect to subset inclusion. This $U$ doesn’t always have to be the actual union (i.e., the least upper bound), although it can be.

To show that a compact space $X$ satisfies condition D, let $\mathcal{U}$ be any directed open cover. (We are not obliged to assume that $\mathcal{U}$ is closed under finite unions.) By compactness, $\mathcal{U}$ has a finite subcover, meaning there are finitely many elements $U_1, U_2, \ldots, U_n$ of $\mathcal{U}$ whose union (i.e. least upper bound) is $X$. By the assumption that $\mathcal{U}$ is directed, there exists an upper bound $U$ of $U_1, \ldots, U_n$ belonging to $\mathcal{U}$. I claim $U = X$. First, $U \subseteq X$ because by definition of open cover of $X$, an element $U \in \mathcal{U}$ is automatically a subset of $X$. But also $X \subseteq U$, because $U$ is an upper bound of the $U_1, \ldots, U_n$, and the union $X$ which is the *least* upper bound is contained in the upper bound. So $U = X$ belongs to $\mathcal{U}$, and thus we have verified that condition D holds.

Now suppose that condition D holds for $X$. We want to show that $X$ is compact. So, let $\mathcal{U}$ be any open cover of $X$; we want to show that under condition D, there exists finitely many $U_1, \ldots, U_n \in \mathcal{U}$ whose union is $X$. Of course we can’t apply condition D directly to $\mathcal{U}$ because $\mathcal{U}$, regarded as being partially ordered by subset inclusion, might not be directed. But if we introduce a new open cover $\mathcal{U}'$ whose elements are precisely the possible finite unions of elements of $\mathcal{U}$, then $\mathcal{U}'$ *is* directed. (Of course this should be proven. So, suppose given elements $V_1, \ldots, V_n$ of $\mathcal{U}'$. According to how $\mathcal{U}'$ was defined, each $V_i$ is a finite union $U_{i, 1} \cup \ldots \cup U_{i, k_i}$ of elements of $\mathcal{U}$. But then $V = V_1 \cup \ldots \cup V_n = \bigcup_{i=1}^n \bigcup_{j=1}^{k_i} U_{i, j}$, being a union of finitely many elements of $\mathcal{U}$, belongs to $\mathcal{U}'$. This $V$ is an upper bound of $V_1, \ldots, V_n$.) Since $\mathcal{U}'$ is directed and since condition D holds, we have that $X \in \mathcal{U}'$. But then by definition of $\mathcal{U}'$, the set $X$ is a union of finitely many elements $U_1, \ldots, U_n$ of $\mathcal{U}$. This completes the proof.

It seems likely to me to be the case, but I could imagine there might be other ways of defining a direction on the opens. And maybe these don't work for compactness..

So if it is always upper bound of two opens is the union here for the direction, I think it would be clearer to state this explicitly. ]]>

(By the way, I agree that “diffs” are often hard to read. It might sometimes be easier reading different revisions in different tabs.)

]]>I don’t think much of these are really improvements. In some cases you have been replacing other people’s words, which were fine and clear enough, with words that you would have chosen instead, such as “unioning”, a word I find grating and cacophonous outside of very informal speech.

But let’s look at this stuff about directed open covers, where you have the paragraph with the word “Firstly”.

Firstly, note that unions of finite opens give a direction on any open cover. This gives us the notion of a directed open cover, which is useful for locales.

As samples of mathematical writing, both sentences of that paragraph are flawed. What one should be saying – and what I read proofs in former revisions *to be* saying – is that given an open cover, one can form a *new* cover that is directed. Not that the old cover was “given a direction”. (By the way, “give a direction” sounds clunky to my ears. I realize that the link for “directed” goes to a page titled “direction”, but I think that’s partly because of a rule we have about using noun phrases as titles. But anyway, nobody ever “gives a direction” to an open covering or to a preorder: either an open covering is directed or it isn’t. What one does is replace an open covering that may not be directed with another that is, by adding in more open sets.)

The second sentence is flawed because “this”, whatever the antecedent is, is not “giving us a notion of” anything. “Giving a notion”, to my mind, means performing an act of conceptual analysis, as in abstracting a new concept that captures or expresses a variety of observed phenomena. “This gives us a directed open cover” is closer to what one should say, but only after fixing the first sentence.

Really, I think it might be better to roll back to an earlier revision, and then fix whatever tiny typos needed fixing. I’m sorry to say, but I think some of the newer revisions are worsening the article. I’m not sure why you’re doing this.

]]>I only worked on 2.5, the first prop in compactness for locales.

If there are any ideas why these diffs are coming in ugly, I would like to know. Again, I apologize. ]]>

statement of compactness for locales.

]]>If every open cover is a directed open cover, then

"Proposition 2.5. A space is compact iff every directed open cover of it has the entire space as one of its opens."

is simply

"Proposition 2.5. A space is compact iff every open cover of it has the entire space as one of its opens." ]]>

statement of compactness for locales

]]>statement of compactness for locales

]]>break off definition of directed open cover. simplify statement of compactness for locales.

]]>give directed open cover as a definition, simplify definition of compact for locales.

]]>I do think the changes make it more understandable. ]]>

same as last (prop 2.5, locales, if direftion)

]]>Clarify if direction of prop 2.5 (locales)

]]>Typos like that don’t have to be mentioned.

]]>missing prime in compactness for locales

]]>