topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
A covert space is a topological space such that the unique map to the terminal point space is a closed map.
This should be compared with overt spaces, where is an open map, and compact spaces, where 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 is covert if the unique map is a closed map of locales, i.e. the adjunction satisfies the Frobenius reciprocity condition .
If excluded middle holds, then every locale is covert.
Constructively, covertness is already interesting when is a set with the discrete topology. In this case, since is the poset of truth values (the subobject classifier) and is the powerset of , covertness of can be expressed more logically as
if is a proposition and a predicate on such that , then .
This is always true if is (Kuratowski) finite (in which case the discrete topology on 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 is covert, then for any two predicates on such that , we have either or .
Let be the proposition in the defining property of covertness for .
Note that if and are incompatible (i.e. ), then this becomes the limited principle of omniscience for . Thus, every covert set is omniscient?.
A locale is defined to be compact if its top element is inaccessible by directed joins, i.e. if for some directed set implies for some . Since the right adjoint part of the locale morphism is defined by (a truth value, since is the subobject classifier), this is equivalent to asking that preserve directed joins.
Contrary to a remark in Sketches of an Elephant, this condition implies that is covert, even constructively (and therefore if is compact then is a proper map, without the need to modify the notion of “compact locale”). For suppose and ; we must show that if is true, then so is . As remarked above, is the truth value of the statement “”, while . Suppose , i.e. that . Now consider the set ; this is evidently directed, and our supposition in the last sentence says exactly that its union is . Therefore, if is compact, there exists a such that and . In other words, either or , i.e. either or , which is what we wanted. This proof appears to be due to Vermeulen.
Eduardo Dubuc and Jacques Penon, Objets compacts dans les topos,
Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics, 40(2), 1986, p. 203–217. doi:10.1017/S144678870002718X
Vermeulen, Proper maps of locales, Journal of Pure and Applied Algebra, 92, 1994, p. 79–107. (pdf (core.ac.uk))
Last revised on August 29, 2021 at 17:16:06. See the history of this page for a list of all contributions to it.