Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

(0 2-category 2-category-theory abelian-categories accessible adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cobordism-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology deformation-theory derived-geometry descent differential differential-cohomology differential-geometry duality education elliptic-cohomology enriched fibration foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus gravity group-theory higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration-theory k-theory kan lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure measure-theory modal-logic model model-category-theory model-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology newpage nonassociative noncommutative noncommutative-geometry number number-theory of operads operator operator-algebra order-theory phenomenology philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject super-geometry superalgebra supergeometry symplectic-geometry synthetic-differential-geometry terminology theory topological topology topos topos-theory tqft type type-theory universal

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 16th 2010

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

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 18th 2014

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

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2016
    • (edited Mar 31st 2016)

    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 “XX is compact if…” to make it read more like a text meant for public consumption, and less like a personal note.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 31st 2016

    Looks good!

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2016

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

    If XX is a locale in a Boolean topos, then the unique locale map γ:X1\gamma:X\to 1 is proper iff γ *\gamma_* preserves directed joins… Constructively, the Frobenius reciprocity condition [f *(Uf *(V))=f *(U)Vf_*(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 XX to be compact if X1X\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 EE) that f:FEf: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:XYf:X\to Y, since “f *f_* preserves directed unions” is not internalized to the stack semantics of Sh(Y)Sh(Y). However, when talking about a map X1X\to 1, we should already be in the stack semantics of Sh(1)=SetSh(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:FEf:F\to E to be proper if… f *(Ω F)f_*(\Omega_F) is a compact internal frame in EE. What does it mean to say that an internal frame… is compact in a general topos EE? For the case E=SetE=Set, we saw how to answer this in topos-theoretic terms in 1.5.5: it means that the direct image functor Sh(X)SetSh(X) \to Set… preserves directed colimits of subterminal objects.

    and then proceeds to define f:FEf:F\to E to be proper if “f *f_* preserves directed colimits of subterminal objects” is true in the stack semantics of EE. But C1.5.5 used “f *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 EE. So I am confused; can anyone help?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2016

    Ok, I found Vermeulen’s paper, and I believe he has a constructive proof that if r:X1r:X\to 1 preserves directed joins then it satisfies the Frobenius condition. Suppose UO(X)U\in O(X) and VO(1)=ΩV\in O(1) = \Omega; we must show that if r *(Ur *(V))r_\ast(U \cup r_\ast(V)) is true, then so is r *(U)Vr_\ast(U) \cup V. Note that r *(W)r_\ast(W) is the truth value of the statement “W=XW=X”, while r *(P)={XP}r^*(P) = \bigcup \{ X \mid P \} . Suppose r *(Ur *(V))r_\ast(U \cup r_\ast(V)), i.e. that U{XV}=XU\cup \bigcup \{ X \mid V \} = X. Now consider the set {WO(X)V(WU)}\{ 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 XX. Therefore, if XX is compact in the sense that its top element is inaccessible by directed joins, there exists a WW such that V(WU)V \vee (W\le U) and XWX\le W. In other words, either VV or XUX\le U, i.e. either VV or r *(U)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.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 1st 2016

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

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2017
    • (edited Apr 23rd 2017)

    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]

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 23rd 2017
    • (edited Apr 23rd 2017)

    How are closed sets being defined here?

    If we are defining closed sets to be precisely the complements of open sets (in symbols, ¬U\neg U), then I can see that the usual open set formulation implies the closed set formulation you just mentioned: if iIU i=X\bigcup_{i \in I} U_i = X, then surely iI¬U i=¬( iU i)=¬X=\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 UU would be the complement of a closed set.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2017

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

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2017

    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.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeApr 23rd 2017

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

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2017

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

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 15th 2017

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