covert space

Covert space



topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Covert space


A covert space is a topological space XX such that the unique map X1X\to 1 to the terminal point space is a closed map.

This should be compared with overt spaces, where X1X\to 1 is an open map, and compact spaces, where X1X\to 1 is a proper map. Since proper maps are closed, all compact spaces are covert.

In classical mathematics, every topological space is covert, just as every space is overt. However, in constructive mathematics, and in particular in synthetic topology, covertness can be a strong condition that already carries much of the power of compactness.


A locale XX is covert if the unique map X1X\to 1 is a closed map of locales, i.e. the adjunction f *:O(1)O(X):f *f^* : O(1) \rightleftarrows O(X) : f_* satisfies the Frobenius reciprocity condition f *(Uf *(V))=f *(U)Vf_*(U\cup f^*(V)) = f_*(U)\cup V.

If excluded middle holds, then every locale is covert.

Covert sets

Constructively, covertness is already interesting when XX is a set with the discrete topology. In this case, since O(1)=P(1)O(1) = P(1) is the poset of truth values (the subobject classifier) and O(X)=P(X)O(X)=P(X) is the powerset of XX, covertness of XX can be expressed more logically as

if PP is a proposition and QQ a predicate on XX such that xX,(PQ(x))\forall x\in X, (P \vee Q(x)), then P(xX,Q(x))P\vee (\forall x\in X, Q(x)).

This is always true if XX is (Kuratowski) finite (in which case the discrete topology on XX is not just covert but compact), but in general it can be quite a strong condition.

In synthetic topology, covertness of sets carries much of the strength of compactness. (Note that here we are talking about covertness of sets — i.e. “spaces” in the sense of synthetic topology, i.e. basic objects of our foundational system — equipped with the “discrete topology” internal to our synthetic-topological formal system; these are quite different from sets whose intrinsic synthetic topology is discrete.) For instance, in various gros toposes of topological, smooth, or algebraic spaces, the covert spaces are precisely the compact ones; see Dubuc-Penon (who call covert sets “compact”).

Covert sets also satisfy the following property.


If XX is covert, then for any two predicates P,QP,Q on XX such that xX,(P(x)Q(x))\forall x\in X, (P(x) \vee Q(x)), we have either xX,P(x)\exists x\in X, P(x) or xX,Q(x)\forall x\in X, Q(x).


Let PP' be the proposition xX,P(x)\exists x\in X, P(x) in the defining property of covertness for XX.

Note that if PP and QQ are incompatible (i.e. ¬(P(x)Q(x))\neg (P(x)\wedge Q(x))), then this becomes the limited principle of omniscience for AA. Thus, every covert set is omniscient?.

Compact locales are covert

A locale XX is defined to be compact if its top element is inaccessible by directed joins, i.e. if X=SX = \bigvee S for some directed set SO(X)S\subseteq O(X) implies XUX\le U for some USU\in S. Since the right adjoint part r *r_* of the locale morphism r:X1r:X\to 1 is defined by r *(U)=(U=X)r_*(U) = (U=X) (a truth value, since O(1)=ΩO(1) = \Omega is the subobject classifier), this is equivalent to asking that r *r_* preserve directed joins.

Contrary to a remark in Sketches of an Elephant, this condition implies that XX is covert, even constructively (and therefore if XX is compact then X1X\to 1 is a proper map, without the need to modify the notion of “compact locale”). For 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. As remarked above, 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, 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. This proof appears to be due to Vermeulen.


Last revised on August 29, 2021 at 13:16:06. See the history of this page for a list of all contributions to it.