Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorTodd_Trimble
   • CommentTimeOct 16th 2010
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexAs an outcome of recent discussion at Math Overflow <a href="http://mathoverflow.net/questions/42186/does-compact-iff-projections-are-closed-require-some-form-of-choice">here</a>, Mike Shulman suggested some nLab pages where comparisons of different definitions of compactness are rigorously established. I have created one such page: [[compactness and stable closure]]. (The importance and significance of the stable closure condition should be brought out better.)

   As an outcome of recent discussion at Math Overflow here, Mike Shulman suggested some nLab pages where comparisons of different definitions of compactness are rigorously established. I have created one such page: compactness and stable closure. (The importance and significance of the stable closure condition should be brought out better.)

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJul 18th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added to the Properties-section at _[[compact space]]_ that in Hausdorff space every compact subset is closed.

   I have added to the Properties-section at compact space that in Hausdorff space every compact subset is closed.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMar 31st 2016
   • (edited Mar 31st 2016)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have tried to edit _[[compact space]]_ just a little for readability. For one, I tried to highlight nets over proper filters just a tad more (moving the statements for nets out of parenthesis, adding reminder to the equivalence via their eventuality filters), just so that the entry gets at least a little closer to giving the reader the expected statement about convergence of sequences. Also I pre-fixed the text of all of the many equivalent definitions by "$X$ is compact if..." to make it read more like a text meant for public consumption, and less like a personal note.

   I have tried to edit compact space just a little for readability.

   For one, I tried to highlight nets over proper filters just a tad more (moving the statements for nets out of parenthesis, adding reminder to the equivalence via their eventuality filters), just so that the entry gets at least a little closer to giving the reader the expected statement about convergence of sequences.

   Also I pre-fixed the text of all of the many equivalent definitions by “$X$ is compact if…” to make it read more like a text meant for public consumption, and less like a personal note.

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeMar 31st 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexLooks good!

   Looks good!

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeNov 19th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI am confused about the constructive notion of "compact locale". In the Elephant just before C3.2.8, Johnstone says > If $X$ is a locale in a Boolean topos, then the unique locale map $\gamma:X\to 1$ is [[proper map|proper]] iff $\gamma_*$ preserves directed joins... Constructively, the Frobenius reciprocity condition [$f_*(U\cup f^*(V)) = f_*(U)\cup V$]... is a nontrivial restriction even on locale maps with codomain 1; so we include it in the definition of compactness --- that is, we *define* $X$ to be compact if $X\to 1$ is proper. However, as far as I can tell this additional Frobenius condition is *not* included in the general definition of [[proper geometric morphism]], which just says (in the [[stack semantics]] of $E$) that $f:F\to E$ preserves directed unions of subterminals. It makes sense that some extra condition is necessary when speaking externally about a general locale map $f:X\to Y$, since "$f_*$ preserves directed unions" is not internalized to the stack semantics of $Sh(Y)$. However, when talking about a map $X\to 1$, we should already be in the stack semantics of $Sh(1) = Set$. So I don't understand why we need the Frobenius condition separately in the constructive definition of "compact locale". Johnstone doesn't give an example, and I don't have Moerdijk or Vermuelen's papers. On the other hand, I don't see how to prove the Frobenius condition either. I have looked through section C3.2 of the Elephant as carefully as I can, and I haven't been able to extract an actual proof that a proper geometric morphism between localic toposes satisfies the Frobenius condition to be a proper map of locales. Prior to defining proper geometric morphisms, he says > ...we may reasonably *define* a geometric morphism $f:F\to E$ to be proper if... $f_*(\Omega_F)$ is a compact internal frame in $E$. What does it mean to say that an internal frame... is compact in a general topos $E$? For the case $E=Set$, we saw how to answer this in topos-theoretic terms in 1.5.5: it means that the direct image functor $Sh(X) \to Set$... preserves directed colimits of subterminal objects. and then proceeds to define $f:F\to E$ to be proper if "$f_*$ preserves directed colimits of subterminal objects" is true in the stack semantics of $E$. But C1.5.5 used "$f_*$ preserves directed unions" as a definition of "compact locale", which the first quote above claims is *not* sufficient constructively, i.e. over a general base $E$. So I am confused; can anyone help?

   I am confused about the constructive notion of “compact locale”. In the Elephant just before C3.2.8, Johnstone says

   If $X$ is a locale in a Boolean topos, then the unique locale map $\gamma:X\to 1$ is proper iff $\gamma_*$ preserves directed joins… Constructively, the Frobenius reciprocity condition [$f_*(U\cup f^*(V)) = f_*(U)\cup V$]… is a nontrivial restriction even on locale maps with codomain 1; so we include it in the definition of compactness — that is, we define $X$ to be compact if $X\to 1$ is proper.

   However, as far as I can tell this additional Frobenius condition is not included in the general definition of proper geometric morphism, which just says (in the stack semantics of $E$) that $f:F\to E$ preserves directed unions of subterminals. It makes sense that some extra condition is necessary when speaking externally about a general locale map $f:X\to Y$, since “$f_*$ preserves directed unions” is not internalized to the stack semantics of $Sh(Y)$. However, when talking about a map $X\to 1$, we should already be in the stack semantics of $Sh(1) = Set$. So I don’t understand why we need the Frobenius condition separately in the constructive definition of “compact locale”. Johnstone doesn’t give an example, and I don’t have Moerdijk or Vermuelen’s papers.

   On the other hand, I don’t see how to prove the Frobenius condition either. I have looked through section C3.2 of the Elephant as carefully as I can, and I haven’t been able to extract an actual proof that a proper geometric morphism between localic toposes satisfies the Frobenius condition to be a proper map of locales. Prior to defining proper geometric morphisms, he says

   …we may reasonably define a geometric morphism $f:F\to E$ to be proper if… $f_*(\Omega_F)$ is a compact internal frame in $E$. What does it mean to say that an internal frame… is compact in a general topos $E$? For the case $E=Set$, we saw how to answer this in topos-theoretic terms in 1.5.5: it means that the direct image functor $Sh(X) \to Set$… preserves directed colimits of subterminal objects.

   and then proceeds to define $f:F\to E$ to be proper if “$f_*$ preserves directed colimits of subterminal objects” is true in the stack semantics of $E$. But C1.5.5 used “$f_*$ preserves directed unions” as a definition of “compact locale”, which the first quote above claims is not sufficient constructively, i.e. over a general base $E$. So I am confused; can anyone help?

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeNov 30th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOk, I found Vermeulen's paper, and I believe he has a constructive proof that if $r:X\to 1$ preserves directed joins then it satisfies the Frobenius condition. Suppose $U\in O(X)$ and $V\in O(1) = \Omega$; we must show that if $r_\ast(U \cup r_\ast(V))$ is true, then so is $r_\ast(U) \cup V$. Note that $r_\ast(W)$ is the truth value of the statement "$W=X$", while $r^*(P) = \bigcup \{ X \mid P \} $. Suppose $r_\ast(U \cup r_\ast(V))$, i.e. that $U\cup \bigcup \{ X \mid V \} = X$. Now consider the set $\{ W\in O(X) \mid V \vee (W\le U) \}$; this is evidently directed, and our supposition in the last sentence says exactly that its union is $X$. Therefore, if $X$ is compact in the sense that its top element is inaccessible by directed joins, there exists a $W$ such that $V \vee (W\le U)$ and $X\le W$. In other words, either $V$ or $X\le U$, i.e. either $V$ or $r_\ast(U)$, which is what we wanted. So my current conclusion is that the first Elephant quote above is wrong about the Frobenius condition being an additional restriction constructively. This did seem like the most likely resolution, since otherwise the definition of proper geometric morphism would probably be wrong, which seems unlikely.

   Ok, I found Vermeulen’s paper, and I believe he has a constructive proof that if $r:X\to 1$ preserves directed joins then it satisfies the Frobenius condition. Suppose $U\in O(X)$ and $V\in O(1) = \Omega$; we must show that if $r_\ast(U \cup r_\ast(V))$ is true, then so is $r_\ast(U) \cup V$. Note that $r_\ast(W)$ is the truth value of the statement “$W=X$”, while $r^*(P) = \bigcup \{ X \mid P \}$. Suppose $r_\ast(U \cup r_\ast(V))$, i.e. that $U\cup \bigcup \{ X \mid V \} = X$. Now consider the set $\{ W\in O(X) \mid V \vee (W\le U) \}$; this is evidently directed, and our supposition in the last sentence says exactly that its union is $X$. Therefore, if $X$ is compact in the sense that its top element is inaccessible by directed joins, there exists a $W$ such that $V \vee (W\le U)$ and $X\le W$. In other words, either $V$ or $X\le U$, i.e. either $V$ or $r_\ast(U)$, which is what we wanted.

   So my current conclusion is that the first Elephant quote above is wrong about the Frobenius condition being an additional restriction constructively. This did seem like the most likely resolution, since otherwise the definition of proper geometric morphism would probably be wrong, which seems unlikely.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 1st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI have added this proof to [[covert space]], with pointers to it from [[compact space]] and [[proper map]].

   I have added this proof to covert space, with pointers to it from compact space and proper map.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeApr 23rd 2017
   • (edited Apr 23rd 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThere seems to be something wrong right at the beginning of _[[compact space]]_: After def. 2.1, the usual definition about existence of finite open subcovers, there is def. 2.2 which is the _immediate_ reformulation in terms of closed subsets: a collection of closed subsets whose intersection is empty has a finite subcollection whose intersection is still empty. But this def. 2.2 is introduced with the remark that it needs excluded middle to be equivalent to 2.1, which is not true. Probably what that remark about excluded middle was meant to refer to is instead the further formulation in terms of closed subsets, the one which says that a collection of closed subsets with the finite intersection property has non-empty intersection. [edit: I have added what seems to be missing at _[[compact space]]_ to _[[finite intersection property]]_]

   There seems to be something wrong right at the beginning of compact space:

   After def. 2.1, the usual definition about existence of finite open subcovers, there is def. 2.2 which is the immediate reformulation in terms of closed subsets: a collection of closed subsets whose intersection is empty has a finite subcollection whose intersection is still empty.

   But this def. 2.2 is introduced with the remark that it needs excluded middle to be equivalent to 2.1, which is not true.

   Probably what that remark about excluded middle was meant to refer to is instead the further formulation in terms of closed subsets, the one which says that a collection of closed subsets with the finite intersection property has non-empty intersection.

   [edit: I have added what seems to be missing at compact space to finite intersection property]

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeApr 23rd 2017
   • (edited Apr 23rd 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexHow are closed sets being defined here? If we are defining closed sets to be precisely the complements of open sets (in symbols, $\neg U$), then I can see that the usual open set formulation implies the closed set formulation you just mentioned: if $\bigcup_{i \in I} U_i = X$, then surely $\bigcap_{i \in I} \neg U_i = \neg \left(\bigcup_{i \in } U_i \right) = \neg X = \emptyset$ since $\neg$ takes unions to intersections. But then how would we turn this implication around (to assert equivalence of the two formulations)? Without excluded middle, I don't see how every open set $U$ would be the complement of a closed set.

   How are closed sets being defined here?

   If we are defining closed sets to be precisely the complements of open sets (in symbols, $\neg U$), then I can see that the usual open set formulation implies the closed set formulation you just mentioned: if $\bigcup_{i \in I} U_i = X$, then surely $\bigcap_{i \in I} \neg U_i = \neg \left(\bigcup_{i \in } U_i \right) = \neg X = \emptyset$ since $\neg$ takes unions to intersections.

   But then how would we turn this implication around (to assert equivalence of the two formulations)? Without excluded middle, I don’t see how every open set $U$ would be the complement of a closed set.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexOh, okay. I'll make all that explicit in the entry now.

    Oh, okay. I’ll make all that explicit in the entry now.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, I have edited statement and proof at [compact+space#fip](https://ncatlab.org/nlab/show/compact+space#fip). I made explicit the use of excluded middle for identifying opens with complements of closed subsets, and a second use of excluded middle for getting what is usually labeled "fip", which is the contrapositive of what was formerly stated here.

    Okay, I have edited statement and proof at compact+space#fip. I made explicit the use of excluded middle for identifying opens with complements of closed subsets, and a second use of excluded middle for getting what is usually labeled “fip”, which is the contrapositive of what was formerly stated here.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeApr 23rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexFWIW, constructively there are at least two distinct definitions of [closed set](https://ncatlab.org/nlab/show/closed+subspace#constructive_mathematics).

    FWIW, constructively there are at least two distinct definitions of closed set.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have added some elementary details at _[compact space -- Examples -- General](https://ncatlab.org/nlab/show/compact+space#ExamplesGeneral)_, such as the proof that closed intervals are compact.

    I have added some elementary details at compact space – Examples – General, such as the proof that closed intervals are compact.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 15th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have added the statement about unions and intersections of compact subspaces, [here](https://ncatlab.org/nlab/show/compact+space#UnionsAndIntersectionOfCompactSubspaces)

    I have added the statement about unions and intersections of compact subspaces, here

15. • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 3rd 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexIn accordance with a recent discussion, I moved the detailed elementary proof of the example of closed intervals to its own page. Also, I added the example of cofinite topology to [[compact space]].

    In accordance with a recent discussion, I moved the detailed elementary proof of the example of closed intervals to its own page. Also, I added the example of cofinite topology to compact space.

16. • CommentRowNumber16.
    • CommentAuthortphyahoo
    • CommentTimeJul 2nd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextProposition 3.2. (complements of compact with open subspaces is compact) seems wrong. Take [0,3] as compact space and (1,3) as subspace of R1. The complement is two half open spaces: [0,1) and (2,3] and by nonexample 4.6 "half open intervals are not compact" Either proposition 3.2 is wrong or I am missing some intuition. A proof or a reference to a proof would help clear this up if I am wrong here.

    Proposition 3.2. (complements of compact with open subspaces is compact)
    
    seems wrong.
    
    Take [0,3] as compact space and (1,3) as subspace of R1.
    
    The complement is two half open spaces: [0,1) and (2,3] and by nonexample 4.6 "half open intervals are not compact"
    
    Either proposition 3.2 is wrong or I am missing some intuition. A proof or a reference to a proof would help clear this up if I am wrong here.
17. • CommentRowNumber17.
    • CommentAuthortphyahoo
    • CommentTimeJul 2nd 2017
    • (edited Jul 2nd 2017)
    • PermaLink
    Author: tphyahoo
    Format: TextDefinition 2.4, point 4 is "For every topological space (Y,τY) (Y,\tau_Y) the projection map out of the product topological space πY:(X×Y,τX×Y)→(Y,τY) \pi_Y \;\colon\; (X \times Y, \tau_{X \times Y}) \to (Y, \tau_Y) is a closed map. and proof of this is stated as "The proof of the equivalence of statement 4 is discussed at closed-projection characterization of compactness." further down Definition 2.10. (closed-projection characterization of compactness) is "X X is compact iff for any space Y Y, the projection map X×Y→Y X \times Y \to Y out of their Cartesian product is closed (see e.g. Milne, section 17)." Aren't these two ways of saying the same thing? Proposed fix: 2.4, point 4 and its proof should be deleted from 2.4 and merged to 2.10. Possible issue, assuming validity of above fix: Does 2.10 then require excluded middle? It is claimed that point 2.4 point 4 requires excluded middle, but it is not clear why this is. In fact linked "closed-projection characterization of compactness" claims a means of circumventing both excluded middle. My guess is excluded middle is not required but I don't know.

    Definition 2.4, point 4 is
    "For every topological space (Y,τY) (Y,\tau_Y) the projection map out of the product topological space πY:(X×Y,τX×Y)→(Y,τY) \pi_Y \;\colon\; (X \times Y, \tau_{X \times Y}) \to (Y, \tau_Y) is a closed map.
    
    and proof of this is stated as
    "The proof of the equivalence of statement 4 is discussed at closed-projection characterization of compactness."
    
    further down
    
    Definition 2.10. (closed-projection characterization of compactness) is
    "X X is compact iff for any space Y Y, the projection map X×Y→Y X \times Y \to Y out of their Cartesian product is closed (see e.g. Milne, section 17)."
    
    Aren't these two ways of saying the same thing?
    
    Proposed fix: 2.4, point 4 and its proof should be deleted from 2.4 and merged to 2.10.
    
    Possible issue, assuming validity of above fix:
    
    Does 2.10 then require excluded middle?
    It is claimed that point 2.4 point 4 requires excluded middle, but it is not clear why this is.
    In fact linked "closed-projection characterization of compactness" claims a means of circumventing both excluded middle. My guess is excluded middle is not required but I don't know.
18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJul 2nd 2017
    • (edited Jul 2nd 2017)
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe: #16, $[0,3] \setminus (1,3)$ is $[0,1] \cup \{3\}$, which is compact.

    Re: #16, $[0,3] \setminus (1,3)$ is $[0,1] \cup \{3\}$, which is compact.

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJul 2nd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe: #17, I think you're right that 2.4(4) and 2.10 are redundant. I don't have an opinion on which of them should be kept.

    Re: #17, I think you’re right that 2.4(4) and 2.10 are redundant. I don’t have an opinion on which of them should be kept.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have now spelled out a detailed proof of prop. 3.2 [here](https://ncatlab.org/nlab/show/compact+space#ProofIntersectionCompactWithOpen).

    I have now spelled out a detailed proof of prop. 3.2 here.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding the duplication of the statement of the _[[closed-projection characterization of compactness]]_: I have removed item 4 from prop. 2.4, but I also moved the former "Definition" 2.10 up to what is now prop. 2.5, so that it is still the next statement after item 3 of prop. 2.4. (Todd should please have a look.) My main request about this entry is: Somebody should turn the long list of "Definitions" 2.7 to 2.13 of compactness into a list of propositions that state that certain statements are equivalent.

    Regarding the duplication of the statement of the closed-projection characterization of compactness:

    I have removed item 4 from prop. 2.4, but I also moved the former “Definition” 2.10 up to what is now prop. 2.5, so that it is still the next statement after item 3 of prop. 2.4.

    (Todd should please have a look.)

    My main request about this entry is: Somebody should turn the long list of “Definitions” 2.7 to 2.13 of compactness into a list of propositions that state that certain statements are equivalent.

22. • CommentRowNumber22.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThanks, Urs. It looks good to me. Does the mention of excluded middle now make sense to tphyahoo? To circumvent excluded middle (as in [[closed-projection characterization of compactness]]), one has to change the statement to say the dual image operator $\forall_\pi: P(X \times Y) \to P(Y)$ takes open sets to open sets; the statement as it is, that the direct image along projection takes closed sets to closed sets, is equivalent to the other statement by De Morgan duality, but that's where excluded middle comes in.

    Thanks, Urs. It looks good to me. Does the mention of excluded middle now make sense to tphyahoo? To circumvent excluded middle (as in closed-projection characterization of compactness), one has to change the statement to say the dual image operator $\forall_\pi: P(X \times Y) \to P(Y)$ takes open sets to open sets; the statement as it is, that the direct image along projection takes closed sets to closed sets, is equivalent to the other statement by De Morgan duality, but that’s where excluded middle comes in.

23. • CommentRowNumber23.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextThank you yes, much clearer now.

    Thank you yes, much clearer now.
24. • CommentRowNumber24.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextAfter a bit of grammar cleanup, Definition 2.12 now seems more obviously incoherent. First, we need a definition of stably closed. The colon suggests a definition, but I believe it may be an error. If it is not an error, this could be clarified by defining it on its own concept page (currently nonexistent). If it is an error as I suspect and "stably closed" is unrelated to the closed projection characterization, then: 1) "stably closed" should be its own definition and perhaps its concept page should be created as well. 2) Then definition 2.12 and 2.13 should be merged or moved up to be closer to Proposition 2.5 so that all the stuff about closed projection is in one place.

    After a bit of grammar cleanup, Definition 2.12 now seems more obviously incoherent.
    
    First, we need a definition of stably closed. The colon suggests a definition, but I believe it may be an error. If it is not an error, this could be clarified by defining it on its own concept page (currently nonexistent).
    
    If it is an error as I suspect and "stably closed" is unrelated to the closed projection characterization, then:
    
    1) "stably closed" should be its own definition and perhaps its concept page should be created as well.
    
    2) Then definition 2.12 and 2.13 should be merged or moved up to be closer to Proposition 2.5 so that all the stuff about closed projection is in one place.
25. • CommentRowNumber25.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextI think the link to the "logic" page in "a logical characterisation of compactness is used in Abstract Stone Duality:" should be removed.

    I think the link to the "logic" page in
    
    "a logical characterisation of compactness is used in Abstract Stone Duality:"
    
    should be removed.
26. • CommentRowNumber26.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextIt is not clear if the assumption of the ultrafilter theorem applies just to 2.7, or to 2.8 and 2.9 as well or even 2.10 and 2.11. I believe that Section 2.10 and 2.11 is unrelated to filters/nets but this should be made more obvious with better section numbering and breaks. I also believe section 2.12 is unrelated to the earlier section, but I noted this before.

    It is not clear if the assumption of the ultrafilter theorem applies just to 2.7, or to 2.8 and 2.9 as well or even 2.10 and 2.11.
    
    I believe that Section 2.10 and 2.11 is unrelated to filters/nets but this should be made more obvious with better section numbering and breaks.
    
    I also believe section 2.12 is unrelated to the earlier section, but I noted this before.
27. • CommentRowNumber27.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextI think section 2.7 through 2.9 should be grouped under Proposition N.N. (compactness in terms of filters) If these are all equivalent (and ultrafilter theorem requirement applies to all) then the proposition should be along the lines of "the following three statements are equivalent." Similarly, section 2.10 and 2.11 should be grouped under Propsition N.N (compactness in terms of open sets) Possibly Definition 2.12 and 2.13 then get merged under proposition 2.5. Possibly there is also a new proposition about proper maps, that is broken out of 2.12.

    I think section 2.7 through 2.9 should be grouped under
    
    Proposition N.N. (compactness in terms of filters)
    
    If these are all equivalent (and ultrafilter theorem requirement applies to all) then the proposition should be along the lines of "the following three statements are equivalent."
    
    Similarly, section 2.10 and 2.11 should be grouped under
    
    Propsition N.N (compactness in terms of open sets)
    
    Possibly Definition 2.12 and 2.13 then get merged under proposition 2.5.
    
    Possibly there is also a new proposition about proper maps, that is broken out of 2.12.
28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexI agree, with #24, that's what I was referring to at the end of #21. This needs to go to the attention of Toby and Todd, I think. The request would be: Turn these terse remarks into something a little more self-contained and inviting.

    I agree, with #24, that’s what I was referring to at the end of #21.

    This needs to go to the attention of Toby and Todd, I think. The request would be: Turn these terse remarks into something a little more self-contained and inviting.

29. • CommentRowNumber29.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextI am having trouble making the above changes because of struggles with wiki markup, however, to be more explicit I think we should have something like Proposition 2.6. (compactness in terms of filter or net convergence) Let X be a topological space. Assuming the ultrafilter theorem (a weak form of the axiom of choice), then the following are equivalent: 1 X is compact in the sense of def. 2.2. 2-.... reformulation of definitions 2.6-2.9

    I am having trouble making the above changes because of struggles with wiki markup, however, to be more explicit I think we should have something like
    
    Proposition 2.6. (compactness in terms of filter or net convergence)
    
    Let X be a topological space. Assuming the ultrafilter theorem (a weak form of the axiom of choice), then the following are equivalent:
    
    1 X is compact in the sense of def. 2.2.
    2-.... reformulation of definitions 2.6-2.9
30. • CommentRowNumber30.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: Textthen Proposition 2.7 (compactness in terms of frames of opens) Let X be a topological space. Then the following are equivalent: 1 X is compact in the sense of def. 2.2. 2-.... reformulation of definitions 2.10 and 2.11

    then
    
    Proposition 2.7 (compactness in terms of frames of opens)
    
    Let X be a topological space. Then the following are equivalent:
    1 X is compact in the sense of def. 2.2.
    2-.... reformulation of definitions 2.10 and 2.11
31. • CommentRowNumber31.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextProposition 2.8 same thing for stably closed, if this is a stand alone concept unrelated to closed projection characterization of compactness.

    Proposition 2.8 same thing for stably closed, if this is a stand alone concept unrelated to closed projection characterization of compactness.
32. • CommentRowNumber32.
    • CommentAuthortphyahoo
    • CommentTimeJul 3rd 2017
    • PermaLink
    Author: tphyahoo
    Format: TextProposition 2.5 can then perhaps be reforumulated as Let X be a topological space. Then the following are equivalent: 1 X is compact in the sense of def. 2.2 2 current contents of proposition 2.5 3-... reformulation of definitions 2.12 and 2.13

    Proposition 2.5 can then perhaps be reforumulated as
    
    Let X be a topological space. Then the following are equivalent:
    
    1 X is compact in the sense of def. 2.2
    2 current contents of proposition 2.5
    3-... reformulation of definitions 2.12 and 2.13
33. • CommentRowNumber33.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexOkay, I'll begin having a look. Much of this was written (I think) by Toby quite a while ago, and his presence here has lately become more sporadic. Please be patient though. I am finding some of the tone harsh (e.g., "now seems more obviously incoherent" -- that I find excessive), and it's a bit of a barrage of comments now to process.

    Okay, I’ll begin having a look. Much of this was written (I think) by Toby quite a while ago, and his presence here has lately become more sporadic.

    Please be patient though. I am finding some of the tone harsh (e.g., “now seems more obviously incoherent” – that I find excessive), and it’s a bit of a barrage of comments now to process.

34. • CommentRowNumber34.
    • CommentAuthortphyahoo
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextI'm very sorry about my tone. I am extremely enthusiastic about constructive math (an amateur obviously, I admit). And I admire what the nlab has accomplished collectively, as well as the individual contributors here and on the cluster of pages where I lurk. Todd / Urs / Toby: thanks for everything you've done. The reason I sent so many comments is I wanted to lay a breadcrumb trail for future edits to the wiki, since I was unable to edit the wiki myself to my satisfaction. It keeps cutting off the page halfway due to some formatting glitch I can't track down. And there doesn't seem to be a preview functionality. If there is any advice or links about editing / maintaining the wiki I will review and try to do better in the future. BTW, I am https://www.linkedin.com/in/thomashartman1/ just to put a face to the edits. I have been interested in constructive math for some years as a software developer doing haskell / coq for personal interest and some for work. Lurker on nlab for years I guess. I am primarily interested in constructive characterization of the reals, probably following the abstract stone duality path.

    I'm very sorry about my tone.
    
    I am extremely enthusiastic about constructive math (an amateur obviously, I admit). And I admire what the nlab has accomplished collectively, as well as the individual contributors here and on the cluster of pages where I lurk. Todd / Urs / Toby: thanks for everything you've done.
    
    The reason I sent so many comments is I wanted to lay a breadcrumb trail for future edits to the wiki, since I was unable to edit the wiki myself to my satisfaction. It keeps cutting off the page halfway due to some formatting glitch I can't track down. And there doesn't seem to be a preview functionality.
    
    If there is any advice or links about editing / maintaining the wiki I will review and try to do better in the future.
    
    BTW, I am https://www.linkedin.com/in/thomashartman1/ just to put a face to the edits. I have been interested in constructive math for some years as a software developer doing haskell / coq for personal interest and some for work. Lurker on nlab for years I guess. I am primarily interested in constructive characterization of the reals, probably following the abstract stone duality path.
35. • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexOkay, I've gone through and reorganized section 2 of [[compact space]] according to comments/suggestions above and my own personal knowledge. Roughly I classified the various "definitions" (now called propositions) under three headings: elementary reformulations, via convergence, and via stability properties. There is still plenty left to do: plenty of proofs which can be filled in or farmed out to other parts of the nLab, as appropriate, and still links left to be made, among other things. It is good that you (tphyahoo) brought your concerns to our attention, so thanks for that. I do think the article has a better shape now. The "obviously incoherent" former 2.12 is, I hope you will now see, coherent after all. I also changed the link from [[logic]] to [[quantification]] which is more precise I think.

    Okay, I’ve gone through and reorganized section 2 of compact space according to comments/suggestions above and my own personal knowledge. Roughly I classified the various “definitions” (now called propositions) under three headings: elementary reformulations, via convergence, and via stability properties. There is still plenty left to do: plenty of proofs which can be filled in or farmed out to other parts of the nLab, as appropriate, and still links left to be made, among other things.

    It is good that you (tphyahoo) brought your concerns to our attention, so thanks for that. I do think the article has a better shape now. The “obviously incoherent” former 2.12 is, I hope you will now see, coherent after all. I also changed the link from logic to quantification which is more precise I think.

36. • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Todd!! That's great.

    Thanks, Todd!! That’s great.

37. • CommentRowNumber37.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexSomething seems wrong with Proposition 3.3, that the category of compact spaces has limits. (Of course compact *Hausdorff* spaces have limits.) The problem is that the equalizer of two maps need not be a closed subspace; that kind of thing is true if we are working with Hausdorff spaces, but not for more general spaces. An explicit example is where we take two maps $[0, 1] \to \{0, 1\}$ where the codomain is given the indiscrete topology, where one of the maps $f$ has $f^{-1}(1) = [0, 1/2)$, and the other is the constant map at $1$. If an equalizer in $Comp$ existed, then $\hom(1, -): Comp \to Set$ would have to preserve it, so set-theoretically it would have to be $[0, 1/2)$. The topology on $[0, 1/2)$ would have to be the same as or finer than the subspace topology in order for the equalizer map to be continuous. But if the subspace topology isn't compact, then no finer topology would make it compact either. (Here I'm taking the contrapositive of the proposition that if $(X, \tau)$ is compact and $\tau' \subseteq \tau$ is a coarser topology, then $(X, \tau')$ is also compact.) I guess I could go in and change it to a true statement, but I'd want to know first about the situation for compact locales. Again, for compact *regular* locales, there's no problem.

    Something seems wrong with Proposition 3.3, that the category of compact spaces has limits. (Of course compact Hausdorff spaces have limits.) The problem is that the equalizer of two maps need not be a closed subspace; that kind of thing is true if we are working with Hausdorff spaces, but not for more general spaces.

    An explicit example is where we take two maps $[0, 1] \to \{0, 1\}$ where the codomain is given the indiscrete topology, where one of the maps $f$ has $f^{-1}(1) = [0, 1/2)$, and the other is the constant map at $1$. If an equalizer in $Comp$ existed, then $\hom(1, -): Comp \to Set$ would have to preserve it, so set-theoretically it would have to be $[0, 1/2)$. The topology on $[0, 1/2)$ would have to be the same as or finer than the subspace topology in order for the equalizer map to be continuous. But if the subspace topology isn’t compact, then no finer topology would make it compact either. (Here I’m taking the contrapositive of the proposition that if $(X, \tau)$ is compact and $\tau' \subseteq \tau$ is a coarser topology, then $(X, \tau')$ is also compact.)

    I guess I could go in and change it to a true statement, but I’d want to know first about the situation for compact locales. Again, for compact regular locales, there’s no problem.

38. • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI feel like if compact locales had limits we would know about it. Could you do something similar to your counterexample with the Sierpinski space instead of the indiscrete 2-point space?

    I feel like if compact locales had limits we would know about it. Could you do something similar to your counterexample with the Sierpinski space instead of the indiscrete 2-point space?

39. • CommentRowNumber39.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 4th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYes, it seems the same counterexample works with Sierpinski space, since $1$ is usually taken to be the open point. (Maybe this is discussed somewhere in Stone Spaces? I don't have my copy within easy view.) So yeah, if I think about it a little longer, maybe it will become obvious that compact frames lack coequalizers, or maybe you already see that's true.

    Yes, it seems the same counterexample works with Sierpinski space, since $1$ is usually taken to be the open point. (Maybe this is discussed somewhere in Stone Spaces? I don’t have my copy within easy view.) So yeah, if I think about it a little longer, maybe it will become obvious that compact frames lack coequalizers, or maybe you already see that’s true.

40. • CommentRowNumber40.
    • CommentAuthortphyahoo
    • CommentTimeJul 8th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextFrom the introduction a compact space "is a kind of ultimate topological expression of the general idea of a space being “closed and bounded”" but is it true that all compact spaces are closed with regard to some topology, or only metric spaces, or only euclidean spaces? Proposition 3.1 (2) has the precondition that "if the compact spaces are also closed" then the claim about inersections. Well, if all compact spaces are closed then this precondition can be dropped as the claim applies to all compact spaces. But if not all compact spaces are closed, perhaps this should be dropped from the idea section, or qualified "In metric spaces..."

    From the introduction a compact space
    
    "is a kind of ultimate topological expression of the general idea of a space being “closed and bounded”"
    
    but is it true that all compact spaces are closed with regard to some topology, or only metric spaces, or only euclidean spaces?
    
    Proposition 3.1 (2) has the precondition that "if the compact spaces are also closed" then the claim about inersections.
    
    Well, if all compact spaces are closed then this precondition can be dropped as the claim applies to all compact spaces.
    
    But if not all compact spaces are closed, perhaps this should be dropped from the idea section, or qualified "In metric spaces..."
41. • CommentRowNumber41.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 8th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThat "Idea" section should be read at a very intuitive level; the language is somewhat fuzzy (I suppose by design). The author of those words should be granted some poetic license. Any space, compact or not, is closed in itself, so under strict interpretations some of the language of the Idea section won't make a lot of sense. The real sense of that passage is concentrated in the words "every net has an accumulation point" (*that* certainly has a precise meaning), and that should be the main takeaway from what the author is trying to convey. The rest of it seems to be a simple appeal to the archetypal image we all carry around in our heads of compact sets: sets in $\mathbb{R}^n$ which are closed and bounded, and the author is trying to draw a connection between that intuitive conception of "closed and bounded", based on that (finite-dimensional) picture, and the more precise mathematical conception "every net must have an accumulation point". In infinite-dimensional Hilbert space (for example), "closed and bounded" do not imply compact. So that intuition comes with a (largish) grain of salt! In fact the word "bounded" isn't quite a topological concept; it makes sense for metric spaces but it doesn't have a meaning for general topological spaces. Turning to Proposition 3.1: now we're doing mathematics, not waving intuitive wands. As it happens, compact subspaces of *Hausdorff* spaces are closed (and Hausdorff spaces make up the majority of spaces one encounters when first learning topology), but in general compact subsets need not be closed in the ambient space. Thus the closure hypothesis has to be inserted by hand for the proposition to work in the generality given there. Anyway, you may be right that the Idea section is (for some readers anyway) more confusing than enlightening. It's hard to say, but perhaps the opening should be reconsidered.

    That “Idea” section should be read at a very intuitive level; the language is somewhat fuzzy (I suppose by design). The author of those words should be granted some poetic license.

    Any space, compact or not, is closed in itself, so under strict interpretations some of the language of the Idea section won’t make a lot of sense. The real sense of that passage is concentrated in the words “every net has an accumulation point” (that certainly has a precise meaning), and that should be the main takeaway from what the author is trying to convey. The rest of it seems to be a simple appeal to the archetypal image we all carry around in our heads of compact sets: sets in $\mathbb{R}^n$ which are closed and bounded, and the author is trying to draw a connection between that intuitive conception of “closed and bounded”, based on that (finite-dimensional) picture, and the more precise mathematical conception “every net must have an accumulation point”.

    In infinite-dimensional Hilbert space (for example), “closed and bounded” do not imply compact. So that intuition comes with a (largish) grain of salt! In fact the word “bounded” isn’t quite a topological concept; it makes sense for metric spaces but it doesn’t have a meaning for general topological spaces.

    Turning to Proposition 3.1: now we’re doing mathematics, not waving intuitive wands. As it happens, compact subspaces of Hausdorff spaces are closed (and Hausdorff spaces make up the majority of spaces one encounters when first learning topology), but in general compact subsets need not be closed in the ambient space. Thus the closure hypothesis has to be inserted by hand for the proposition to work in the generality given there.

    Anyway, you may be right that the Idea section is (for some readers anyway) more confusing than enlightening. It’s hard to say, but perhaps the opening should be reconsidered.

42. • CommentRowNumber42.
    • CommentAuthortphyahoo
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: tphyahoo
    Format: Text"by boundedness it cannot escape, and by closure the point is in the space." can "it" here be replaced by "accumulation point"? I think that would be clearer.

    "by boundedness it cannot escape, and by closure the point is in the space."
    
    can "it" here be replaced by "accumulation point"? I think that would be clearer.
43. • CommentRowNumber43.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexNo, the "it" here is the net (nets are generalized sequences).

    No, the “it” here is the net (nets are generalized sequences).

44. • CommentRowNumber44.
    • CommentAuthortphyahoo
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextHow about "In typical spatial domais (such as R^n) compactness is a kind of ultimate topological expression of the general idea of a space being “closed and bounded”: .........

    How about
    
    "In typical spatial domais (such as R^n) compactness is a kind of ultimate topological expression of the general idea of a space being “closed and bounded”: .........
45. • CommentRowNumber45.
    • CommentAuthortphyahoo
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextWhat do you think of singly linking "closed and bounded" to the heine borel theorem section (4.5) rather than linking "closed" and "bounded" separately to the two concept pages as is currently the case. Doesn't this give a better intuition?

    What do you think of singly linking "closed and bounded" to the heine borel theorem section (4.5) rather than linking "closed" and "bounded" separately to the two concept pages as is currently the case.
    
    Doesn't this give a better intuition?
46. • CommentRowNumber46.
    • CommentAuthortphyahoo
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextAlso it seems like many of the "Examples" (such as heine borel) fix in better in the Definitions / Characterizations section.

    Also it seems like many of the "Examples" (such as heine borel) fix in better in the Definitions / Characterizations section.
47. • CommentRowNumber47.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • (edited Jul 9th 2017)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #46: no, the definitions/characterizations section is general. Heine-Borel is for a specialized set of circumstances and belongs to Examples.

    Re #46: no, the definitions/characterizations section is general. Heine-Borel is for a specialized set of circumstances and belongs to Examples.

48. • CommentRowNumber48.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexOkay, I tweaked the opening paragraph just a little. I don't agree with joining "closed" to "bounded" as in #45, but I did mention Heine-Borel. Hopefully it's now clear that it's more about nets and convergence than it is about being closed and bounded.

    Okay, I tweaked the opening paragraph just a little. I don’t agree with joining “closed” to “bounded” as in #45, but I did mention Heine-Borel. Hopefully it’s now clear that it’s more about nets and convergence than it is about being closed and bounded.

49. • CommentRowNumber49.
    • CommentAuthortphyahoo
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: tphyahoo
    Format: TextMuch clearer. The verb "captures" is used twice, which makes it a little hard to concentrate on exactly what is being captured. I reworded to avoid this.

    Much clearer.
    
    The verb "captures" is used twice, which makes it a little hard to concentrate on exactly what is being captured. I reworded to avoid this.
50. • CommentRowNumber50.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexBut there was no mention of compactness in the 2nd paragraph of your edit; attention was momentarily deflected away to talk about "closed and bounded". So I had to reword again. Please do not remove the parentheses. They signal that a side remark is being made, which the reader can pursue if she likes, but the main focus needs to be kept on what the property is about. Thank you for your input, but now that some clarity has been reached, I suggest that we not spend a lot of time on what Feynman called "wordsmithing". I'll add that I made a change suggested by comment #37.

    But there was no mention of compactness in the 2nd paragraph of your edit; attention was momentarily deflected away to talk about “closed and bounded”. So I had to reword again.

    Please do not remove the parentheses. They signal that a side remark is being made, which the reader can pursue if she likes, but the main focus needs to be kept on what the property is about.

    Thank you for your input, but now that some clarity has been reached, I suggest that we not spend a lot of time on what Feynman called “wordsmithing”. I’ll add that I made a change suggested by comment #37.

51. • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexI took a look and ended up making some last changes myself to the [Idea](https://ncatlab.org/nlab/show/compact+space#Idea) section: * made explicit that "everything" in the first sentence referred to sequences and nets * linked the line about not needing and ambient space for the definition with the line saying that nevertheless one does often consider compact subspaces; * after the claim that one likes to consider compact Hausdorff spaces, I added one reason * grouped the two lines about compact locales together, now at the end of the Idea-section.

    I took a look and ended up making some last changes myself to the Idea section:

    • made explicit that “everything” in the first sentence referred to sequences and nets

    • linked the line about not needing and ambient space for the definition with the line saying that nevertheless one does often consider compact subspaces;

    • after the claim that one likes to consider compact Hausdorff spaces, I added one reason

    • grouped the two lines about compact locales together, now at the end of the Idea-section.

52. • CommentRowNumber52.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThose are useful improvements, Urs -- thanks.

    Those are useful improvements, Urs – thanks.

53. • CommentRowNumber53.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexUrs, in the idea section, did you really mean to say "paracompact" and not "locally compact"?

    Urs, in the idea section, did you really mean to say “paracompact” and not “locally compact”?

54. • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeJul 9th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexArgh. :-) Thanks. I have fixed it, and also added pointer to the proof.

    Argh. :-)

    Thanks. I have fixed it, and also added pointer to the proof.

55. • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexMention Bishop-compactness (complete and totally bounded) <a href="https://ncatlab.org/nlab/revision/diff/compact+space/85">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/85">v85</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    Mention Bishop-compactness (complete and totally bounded)

    diff, v85, current

56. • CommentRowNumber56.
    • CommentAuthortphyahoo
    • CommentTimeFeb 17th 2020
    • PermaLink
    Author: tphyahoo
    Format: Textthe overt space page states 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. I think this should be stated somewhere on the compact space page, but I don't see it. Neither in any of the other related pages. IE, closed characterization compactness and stable closure There is a lot of material and maybe I overlooked something. If so, could someone point me the right place? If not, can it be proven? It seems related to closed projection characterization. On that page we have Theorem 1.1. A topological space X is compact if and only if for every space Y, the projection map π:Y×X→Y out of the product topological space is a closed map. Seems close? Anyway, can someone prove the claim above about the open product subspace U?

    the overt space page states
    
    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.
    
    I think this should be stated somewhere on the compact space page, but I don't see it. Neither in any of the other related pages. IE,
    
    closed characterization
    compactness and stable closure
    
    There is a lot of material and maybe I overlooked something. If so, could someone point me the right place? If not, can it be proven?
    
    It seems related to closed projection characterization. On that page we have
    
    Theorem 1.1. A topological space X is compact if and only if for every space Y, the projection map π:Y×X→Y out of the product topological space is a closed map.
    
    Seems close? Anyway, can someone prove the claim above about the open product subspace U?
57. • CommentRowNumber57.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 18th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexIt is so stated. See [closed projection characterization](https://ncatlab.org/nlab/show/closed-projection+characterization+of+compactness), point 5. under Variant Proofs. It's mentioned that this approach is in Escardo's 2009 paper. See lemma 4.3 there.

    It is so stated. See closed projection characterization, point 5. under Variant Proofs. It’s mentioned that this approach is in Escardo’s 2009 paper. See lemma 4.3 there.

58. • CommentRowNumber58.
    • CommentAuthortphyahoo
    • CommentTimeFeb 21st 2020
    • (edited Feb 21st 2020)
    • PermaLink
    Author: tphyahoo
    Format: Textin Compactness via completeness "A uniform space X is compact if and only if it is complete and totally bounded." can this be "In classical mathematics, a uniform space X is compact (def 2.2) if and only if it is complete and totally bounded." ?

    in Compactness via completeness
    
    "A uniform space X is compact if and only if it is complete and totally bounded."
    
    can this be
    
    "In classical mathematics, a uniform space X is compact (def 2.2) if and only if it is complete and totally bounded."
    
    ?
59. • CommentRowNumber59.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2020
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, that's what's meant. But this page is written in classical mathematics as the default, so I don't think there's a need to say so explicitly here, especially since the subsequent paragraph clarifies the situation in constructive mathematics.

    Yes, that’s what’s meant. But this page is written in classical mathematics as the default, so I don’t think there’s a need to say so explicitly here, especially since the subsequent paragraph clarifies the situation in constructive mathematics.

60. • CommentRowNumber60.
    • CommentAuthorDaniel Luckhardt
    • CommentTimeMar 15th 2020
    • (edited Mar 15th 2020)
    • PermaLink
    Author: Daniel Luckhardt
    Format: MarkdownItexsorry, wrong thread

    sorry, wrong thread

61. • CommentRowNumber61.
    • CommentAuthorGuest
    • CommentTimeMar 22nd 2020
    • PermaLink
    Author: Guest
    Format: TextIn definition 2.1 "Let (X,τ) be a topological space. Then an open cover is a set {Ui⊂X}i∈I of open subsets (i.e. (Ui⊂X)∈τ⊂P(X)) such that their union is all of X" This doesn't cover standard open covers of the unit interval, because it only talks about the whole space, not subspaces. Wikipedia https://en.wikipedia.org/wiki/Cover_(topology) has "..... Also, if Y is a subset of X, then a cover of Y is a collection of subsets of X whose union contains Y" I think this should be added to definition 2.1

    In definition 2.1
    
    "Let (X,τ) be a topological space. Then an open cover is a set {Ui⊂X}i∈I of open subsets (i.e. (Ui⊂X)∈τ⊂P(X)) such that their union is all of X"
    
    This doesn't cover standard open covers of the unit interval, because it only talks about the whole space, not subspaces. Wikipedia
    
    https://en.wikipedia.org/wiki/Cover_(topology)
    
    has "..... Also, if Y is a subset of X, then a cover of Y is a collection of subsets of X whose union contains Y"
    
    I think this should be added to definition 2.1
62. • CommentRowNumber62.
    • CommentAuthortphyahoo
    • CommentTimeMar 22nd 2020
    • PermaLink
    Author: tphyahoo
    Format: TextSorry, #61 was me, tphyahoo. Forgot to sign in.

    Sorry, #61 was me, tphyahoo. Forgot to sign in.
63. • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeMar 22nd 2020
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAn open cover of a subset is just an open cover of that set regarded as a space with the induced topology. But we could add that as a remark afterwards.

    An open cover of a subset is just an open cover of that set regarded as a space with the induced topology. But we could add that as a remark afterwards.

64. • CommentRowNumber64.
    • CommentAuthortphyahoo
    • CommentTimeMay 11th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexmissing prime in compactness for locales <a href="https://ncatlab.org/nlab/revision/diff/compact+space/87">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/87">v87</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    missing prime in compactness for locales

    diff, v87, current

65. • CommentRowNumber65.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 12th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexTypos like that don't have to be mentioned.

    Typos like that don’t have to be mentioned.

66. • CommentRowNumber66.
    • CommentAuthortphyahoo
    • CommentTimeMay 12th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexClarify if direction of prop 2.5 (locales) <a href="https://ncatlab.org/nlab/revision/diff/compact+space/88">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/88">v88</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    Clarify if direction of prop 2.5 (locales)

    diff, v88, current

67. • CommentRowNumber67.
    • CommentAuthortphyahoo
    • CommentTimeMay 12th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexsame as last (prop 2.5, locales, if direftion) <a href="https://ncatlab.org/nlab/revision/diff/compact+space/88">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/88">v88</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

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

    diff, v88, current

68. • CommentRowNumber68.
    • CommentAuthortphyahoo
    • CommentTimeMay 12th 2020
    • PermaLink
    Author: tphyahoo
    Format: TextI'm sorry the diff is a mess. Maybe it's because I copy pasted from a desktop editor. I can redo if wanted. I do think the changes make it more understandable.

    I'm sorry the diff is a mess. Maybe it's because I copy pasted from a desktop editor. I can redo if wanted.
    
    I do think the changes make it more understandable.
69. • CommentRowNumber69.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexgive directed open cover as a definition, simplify definition of compact for locales. <a href="https://ncatlab.org/nlab/revision/diff/compact+space/89">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/89">v89</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

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

    diff, v89, current

70. • CommentRowNumber70.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexbreak off definition of directed open cover. simplify statement of compactness for locales. <a href="https://ncatlab.org/nlab/revision/diff/compact+space/89">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/89">v89</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

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

    diff, v89, current

71. • CommentRowNumber71.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexstatement of compactness for locales <a href="https://ncatlab.org/nlab/revision/diff/compact+space/89">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/89">v89</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    statement of compactness for locales

    diff, v89, current

72. • CommentRowNumber72.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexstatement of compactness for locales <a href="https://ncatlab.org/nlab/revision/diff/compact+space/89">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/89">v89</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    statement of compactness for locales

    diff, v89, current

73. • CommentRowNumber73.
    • CommentAuthorGuest
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: Guest
    Format: TextIs it possible to have an open cover without a direction? I don't see how.

    Is it possible to have an open cover without a direction? I don't see how.
74. • CommentRowNumber74.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: Text73 was me. 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."

    73 was me.
    
    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."
75. • CommentRowNumber75.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: MarkdownItexstatement of compactness for locales. <a href="https://ncatlab.org/nlab/revision/diff/compact+space/89">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/89">v89</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    statement of compactness for locales.

    diff, v89, current

76. • CommentRowNumber76.
    • CommentAuthortphyahoo
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: tphyahoo
    Format: TextLooking at the diffs, it appears that there was something done to proposition 2.6. But I don't think this is the case. 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.

    Looking at the diffs, it appears that there was something done to proposition 2.6. But I don't think this is the case.
    
    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.
77. • CommentRowNumber77.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI 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 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.

78. • CommentRowNumber78.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex(By the way, I agree that "diffs" are often hard to read. It might sometimes be easier reading different revisions in different tabs.)

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

79. • CommentRowNumber79.
    • CommentAuthorGuest
    • CommentTimeMay 13th 2020
    • PermaLink
    Author: Guest
    Format: Textokay, I reverted and made only the typo fix for U'. If I have further suggestions given your feedback I will propose here and go lighter on wiki edits.

    okay, I reverted and made only the typo fix for U'. If I have further suggestions given your feedback I will propose here and go lighter on wiki edits.
80. • CommentRowNumber80.
    • CommentAuthortphyahoo
    • CommentTimeMay 24th 2020
    • PermaLink
    Author: tphyahoo
    Format: TextIn compactness for locales,

    In compactness for locales,
81. • CommentRowNumber81.
    • CommentAuthortphyahoo
    • CommentTimeMay 24th 2020
    • PermaLink
    Author: tphyahoo
    Format: TextIn compactness for locales, is the direction always defined by union of opens? IE the join semilattice of opens defined by the union operation? 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.

    In compactness for locales, is the direction always defined by union of opens? IE the join semilattice of opens defined by the union operation?
    
    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.
82. • CommentRowNumber82.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 26th 2020
    • (edited May 26th 2020)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexIt'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’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.

83. • CommentRowNumber83.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 26th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexBy 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.

    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.

84. • CommentRowNumber84.
    • CommentAuthorMike Shulman
    • CommentTimeMay 27th 2020
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

85. • CommentRowNumber85.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 27th 2020
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRight, 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.

    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.

86. • CommentRowNumber86.
    • CommentAuthorMike Shulman
    • CommentTimeMay 27th 2020
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, the distinction isn't relevant for compactness.

    Yes, the distinction isn’t relevant for compactness.

87. • CommentRowNumber87.
    • CommentAuthornLab edit announcer
    • CommentTimeMay 29th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadding 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 <a href="https://ncatlab.org/nlab/revision/diff/compact+space/93">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/93">v93</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    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

    diff, v93, current

88. • CommentRowNumber88.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJun 30th 2023
    • PermaLink
    Author: Dmitri Pavlov
    Format: MarkdownItexAdded: ## History Compact spaces were introduced (under the name of “bicompact spaces”) by [[Paul Alexandroff]] and [[Paul Urysohn]] around 1924, see the 92nd volume of Mathematische Annalen, especially [AU](#AlexandroffUrysohn1924). <a href="https://ncatlab.org/nlab/revision/diff/compact+space/97">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/97">v97</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    Added:

    History

    Compact spaces were introduced (under the name of “bicompact spaces”) by Paul Alexandroff and Paul Urysohn around 1924, see the 92nd volume of Mathematische Annalen, especially AU.

    diff, v97, current

89. • CommentRowNumber89.
    • CommentAuthorZhen Lin
    • CommentTimeSep 6th 2024
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexThe point-free definition given is wrong – the right adjoint to pullback of open subsets always exists; what is needed is that the right adjoint to pullback of subsets restricts to open subsets. <a href="https://ncatlab.org/nlab/revision/diff/compact+space/98">diff</a>, <a href="https://ncatlab.org/nlab/revision/compact+space/98">v98</a>, <a href="https://ncatlab.org/nlab/show/compact+space">current</a>

    The point-free definition given is wrong – the right adjoint to pullback of open subsets always exists; what is needed is that the right adjoint to pullback of subsets restricts to open subsets.

    diff, v98, current