nLab
located subspace

Located subspaces

Located subspaces

Idea

In constructive point-set topology, there are a variety of notions of when a subspace is located. This varies depending on what kind of space one is discussing, and even for a given kind of space, there are sometimes various weaker and stronger notions of locatedness. Typically (if not always), these concepts are trivial in classical mathematics.

A located subspace should be viewed as a nice subspace, ruling out pathological counterexamples that exist for logical rather than topological reasons. For example, given any space XX and any truth value pp, there exists a subspace {x|p}\{x | p\}, and these can seem very strange for undecidable pp; but typically (if not always), this subspace will only be located if pp is true or false.

Definitions

In metric spaces

Given a metric space XX, a subspace SS of XX, and a point xx of XX, we commonly define the distance from xx to SS (or from SS to xx) as an infimum:

d(x,S)inf ySd(x,y). d(x,S) \coloneqq \inf_{y \in S} d(x,y) .

In constructive mathematics, this infimum is generally an upper real number, even if (as is usual) we require the distances d(x,y)d(x,y) to always be a located real number.

The subspace SS is located (or metrically located to be specific) if, for each point xx, d(x,S)d(x,S) is located. (Although we are defining located subspaces in terms of located real numbers, this is backwards historically; the term was first used, by Jan Brouwer, to refer to subsets.)

We should really speak of extended upper/located real numbers, in case SS might be empty or we wish to apply the concept in an extended metric space. But at least if XX is bounded? and inhabited, then a located subspace SS must be empty or inhabited.

Note that there is a smaller complete lattice than the upper reals that contains the located reals and in which we could take the infimum, namely the MacNeille real numbers. However, the inclusion of MacNeille reals into upper reals does not preserve infima (though it does preserve suprema), and in the definition of located subspace we really do want to assert that the upper real infimum, not the MacNeille real infimum, is a located real. This is because upper real infima, unlike MacNeille real infima, have the property that if infA<ε\inf A \lt \varepsilon then there is an aAa\in A such that a<εa\lt\varepsilon, which is crucial for the desired behavior of locatedness.

In uniform spaces

If XX is a uniform space, Bridges et. al. define a subspace SS to be almost located if for any entourage UU, there is an entourage VV such that ¬V[S]U[S]=X\neg V[S] \cup U[S] = X. In other words, every point xXx\in X is either within UU of some point of SS or not within VV of any point of SS.

Since this seems the most natural notion of locatedness for uniform spaces, one might naturally also call such a subspace uniformly located. However, note that even if XX is a metric space, metric locatedness is strictly stronger than uniform locatedness; Bridges et. al. give an example showing that metric locatedness is not a uniform invariant (while uniform locatedness is of course).

In topological spaces

Given a topological space XX and a subspace SS of XX, SS is located (or topologically located to be specific) if, given any point xx and neighbourhood UU of xx, either USU \cap S is inhabited or some other neighbourhood VV of xx is disjoint with SS.

See Section 7.3 of Troelstra & van Dalen.

Examples

Singletons

Any singleton subset of a metric space, or more generally any finite subset, is metrically located, since we can take the minimum of any finite set. A singleton subset of a uniform space is uniformly located if and only if the uniform space is regular.

Covert subsets

Theorem

Suppose XX is a uniformly regular uniform space and that (the underlying set of) SXS\subseteq X is a covert set. Then SS is uniformly located in XX.

Proof

Since XX is uniformly regular, for any entourage UU there is an entourage VV such that ¬VU=X×X\neg V \cup U = X\times X. In particular, for any xXx\in X, for any ySy\in S, we have either (x,y)U(x,y)\in U or (x,y)V(x,y)\notin V. By covertness of SS, it follows that either (x,y)U(x,y)\in U for some ySy\in S, or (x,y)V(x,y)\notin V for all ySy\in S, which is to say that x¬V[S]U[S]x\in \neg V[S] \cup U[S].

Compact subspaces

Theorem

Suppose XX is a uniformly regular uniform space and that SXS\subseteq X is compact in its induced topology. Then SS is uniformly located in XX.

Proof

Given any entourage UU, let VV and WW be entourages such that ¬VU=X×X\neg V \cup U = X\times X (by uniform regularity) and WWWVW\circ W\circ W \subseteq V. Let GG be the interior of ¬W\neg W. Then ¬VG\neg V \subseteq G, since if (x,y)V(x,y)\notin V then W[x]×W[y]W[x] \times W[y] is a neighborhood of (x,y)(x,y) contained in ¬W\neg W (for if x Ww Wz Wyx \approx_W w \approx_W z \approx_W y then (x,y)V(x,y)\in V, which is not the case, hence (w,z)W(w,z)\notin W). Thus, GU=X×XG\cup U = X\times X.

Let i:X×SX×Xi: X\times S \to X\times X be the inclusion and π:X×SX\pi : X\times S \to X the projection. Then i *Gi *U=X×Si^* G \cup i^* U = X\times S. Since XX is uniformly regular, it is regular. Thus SS is compact regular, and hence locally compact, so the locale product X×SX\times S is spatial. Therefore π\pi is both an open map and a proper map of locales. We then have i *Gπ *π !i *U=X×Si^* G \cup \pi^* \pi_! i^* U = X\times S, hence π *(i *Gπ *π !i *U)=X\pi_*(i^* G \cup \pi^* \pi_! i^* U) = X, and so by properness π *i *Gπ !i *U=X\pi_* i^* G \cup \pi_! i^* U = X as well. In other words, for every xXx\in X either (x,y)G(x,y)\in G for all ySy\in S, or there exists a ySy\in S such that (x,y)U(x,y)\in U. Since G¬WG\subseteq \neg W, it follows that SS is almost located.

References

  • Douglas Bridges, Hajime Ishihara, Ray Mines, Fred Richman, Peter Schuster, and Luminiţa Vîţă. Almost locatedness in uniform spaces, Czechoslovak Mathematical Journal, Vol. 57 (2007), No. 1, 1–12, web

  • Anne Sjerp Troelstra & Dirk van Dalen?, Constructivism in Mathematics 2.

Various related notions of locatedness are studied in

Last revised on February 11, 2019 at 19:39:43. See the history of this page for a list of all contributions to it.