nLab
covert space

Covert space

Idea

A covert space is a space XX such that the unique map X1X\to 1 to the terminal 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 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.

Definition

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.

Theorem

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

Proof

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.

References

  • Vermeulen, Proper maps of locales

Last revised on December 2, 2016 at 13:18:19. See the history of this page for a list of all contributions to it.