nLab dense subspace




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



Given a topological space (or locale) XX, a subspace AA of XX is dense if its closure is all of XX: cl(A)=Xcl(A)=X.

Since cl(A)cl(A) is the set of all points xx such that every open neighborhood of xx intersects AA, this can equivalently be written as “every open neighborhood of every point intersects AA”, or equivalently “every inhabited open set intersects AA”, i.e. AUA\cap U is inhabited for all inhabited open sets UU.

Contraposing this, we obtain another equivalent definition “the only open subset not intersecting AA is the empty set”, or “if AU=A\cap U=\emptyset for some open set UU, then U=U=\emptyset”. This is the definition usually given when XX is a locale: a nucleus jj is dense if j(0)=0j(0)=0 (since j(0)j(0) is the union of all opens whose “intersection with jj” is 00).


  • If AXA \subseteq X is a dense subset of a topological space XX and f:XYf: X \to Y is an epimorphism, then the image f(A)f(A) is dense in YY.

  • If i: AXA \hookrightarrow X and j:XBj: X \hookrightarrow B are dense subspace inclusions, then so is the composite ji:ABj \circ i: A \to B.

  • If AXA\subseteq X is a dense subset of topological space XX and AA is connected, so is XX.

  • In point-set topology, a space is separable if and only if it has a dense subspace with countably many points.

  • In locale theory, we have the curious property that any intersection of dense subspaces is still dense. (This of course fails rather badly for topological spaces, where the intersection of all dense topological subspaces is the space of isolated points.) One consequence is that every locale has a smallest dense sublocale, the double negation sublocale.


In the category of Hausdorff topological spaces (with continuous functions between them), the inclusion of a dense subspace

AiX A \overset{\;\;i\;\;}{\hookrightarrow} X

is an epimorphism.


We have to show that for (f,g)(f,g) any pair of parallel morphisms out of XX

AiXgfY A \overset{\;\;i\;\;}{\hookrightarrow} X \underoverset {\;\;g\;\;} {\;\;f\;\;} {\rightrightarrows} Y

into a Hausdorff space YY, the equality fi=gif \circ i = g \circ i implies f=gf = g. With classical logic we may equivalently show the contrapositive: That fgf \neq g implies figif \circ i \neq g \circ i.

So assume that fgf \neq g. This means that there exists yYy \in Y with f(y)g(y)f(y) \neq g(y). But since YY is Hausdorff, there exist disjoint open neighbourhoods O f(y),O g(y)YO_{f(y)},\;O_{g(y)} \subset Y, i.e. f(x)O f(x)f(x) \in O_{f(x)} and g(x)O g(x)g(x) \in O_{g(x)} with O f(x)O g(x)=O_{f(x)} \cap O_{g(x)} = \varnothing.

But their preimages must intersect at least in xf 1(O f(x))g 1(O g(x))x \in f^{-1}\big( O_{f(x)} \big) \cap g^{-1}\big( O_{g(x)} \big). Since this intersection is an open subset (as preimages of open subsets are open by definition of continuous functions, and since finite intersections of open subsets are open by the definition of topological spaces) there exists a point aAa \in A with i(a)f 1(O f(x))g 1(O g(x))i(a) \in f^{-1}\big( O_{f(x)} \big) \cap g^{-1}\big( O_{g(x)} \big) (by definition of dense subset). But since then f(i(a))O f(x)f(i(a)) \in O_{f(x)} and g(i(a))O g(x)g(i(a)) \in O_{g(x)} while O f(x)O_{f(x)} is disjoint from O g(x)O_{g(x)}, it follows that f(i(a))g(i(a))f(i(a)) \neq g(i(a)). This means that figif \circ i \neq g \circ i.

In constructive mathematics

In constructive mathematics, the law of contraposition is not an equivalence, so we obtain two inequivalent notions of density:

  • AXA\subseteq X is strongly dense if AUA\cap U is inhabited for all inhabited open sets UXU\subseteq X.
  • AXA\subseteq X is weakly dense if AU=A\cap U = \emptyset for some open UXU\subseteq X implies U=U=\emptyset.

Of course, strong density implies weak density, since emptiness is non-inhabitation (whereas inhabitation is stronger than non-emptiness). The two notions of density are related dually to the corresponding notions of closed subspace: AA is strongly dense iff its weak closure is all of XX, and weakly dense iff its strong closure is all of XX.

Note that the usual notion of density for sublocales j(0)=0j(0)=0 is an analogue of weak density, and could be called such. There is also a notion of strong density for sublocales. Since strong density refers to inhabited sets, one might expect strong density for sublocales to refer to positive elements, and thus only be sensible for overt locales; but in fact it can be reformulated to make sense in all cases.


A nucleus jj on a locale XX is strongly dense if j(P^)=P^j(\hat{P})=\hat{P} for any truth value PP, where P^={XP}\hat{P} = \bigvee \{ X \mid P \}.

With classical logic, every truth value is either \top or \bot, and we have ^=X\hat{\top}=X (and any nucleus satisfies j(X)=Xj(X)=X) while ^=0\hat{\bot}=0. Thus classically strong and weak density coincide. To see that this is really a notion of strong density, we prove:


If i:AXi:A\subseteq X is a sublocale such that AA and XX are both overt, then AA is strongly dense if and only if for any positive open UO(X)U\in O(X), the intersection AU=i *UO(A)A\cap U = i^*U \in O(A) is also positive.


First suppose AA is strongly dense, and let UO(X)U\in O(X) be positive. Let PP be the truth value of the statement “i *UO(A)i^*U \in O(A) is positive”. We want to show that PP is true, for which it suffices to show that P^={XP}\hat{P} = \bigvee \{ X \mid P \} is positive, since then its covering {XP}\{ X \mid P \} would be inhabited and thus PP would be true. And since UU is positive, it suffices to show UP^U \subseteq \hat{P}.

Now since AA is strongly dense, j A(P^)=P^j_A(\hat{P}) = \hat{P}, which is to say that P^=i *(i *P^)\hat{P} = i_*(i^*\hat{P}). By adjointness, therefore, to show UP^U \subseteq \hat{P} it suffices to show i *Ui *P^={AP}i^*U \subseteq i^*\hat{P} = \bigvee \{ A \mid P\}. Now since AA is overt, i *Ui^*U can be covered by positive opens, so it suffices to show that for any positive Vi *UV\subseteq i^*U we have V{AP}V\subseteq \bigvee \{ A \mid P\}. But if Vi *UV\subseteq i^*U is positive, then i *Ui^*U is also positive, i.e. PP is true, and thus {AP}=A\bigvee \{ A \mid P\} = A, which contains VV.

Now suppose conversely that for any positive UO(X)U\in O(X), i *Ui^*U is also positive, and let PP be any truth value; we must show i *i *P^P^i_* i^*\hat{P} \subseteq \hat{P}. Since XX is overt, i *i *P^i_* i^*\hat{P} can be covered by positive opens, so it suffices to show that for any positive Ui *i *P^U\subseteq i_* i^*\hat{P} we have UP^U\subseteq \hat{P}. But by adjointness, Ui *i *P^U\subseteq i_* i^*\hat{P} is equivalent to i *Ui *P^i^*U \subseteq i^*\hat{P}, and by assumption i *Ui^*U is also positive. Thus, i *P^={AP}i^*\hat{P} = \bigvee \{ A \mid P\} is positive, which means that PP is true, and hence P^=X\hat{P} = X and so UP^U\subseteq \hat{P}.

Since spatial locales are overt, and their positivity predicate coincides with inhabitedness, we have in particular:


If i:AXi:A\subseteq X is a subspace of a topological space, then AA is strongly dense as a topological subspace if and only if it is strongly dense as a sublocale.

Strong density for sublocales gives rise to a corresponding notion of weakly closed sublocale. It is also the specialization of the notion of fiberwise dense sublocale? to the case of locale maps X1X\to 1.


Strongly dense sublocales are discussed in

  • Sketches of an Elephant, C1.1 and C1.2

  • Peter Johnstone, A constructive ‘closed subgroup theorem’ for localic groups and groupoids, Cahiers de Topologie et Géométrie Différentielle Catégoriques (1989), Volume: 30, Issue: 1, page 3-23 link

  • Mamuka Jibladze, Peter Johnstone, The frame of fibrewise closed nuclei, Cahiers de Topologie et Géométrie Différentielle Catégoriques (1991), Volume: 32, Issue: 2, page 99-112, link

  • Peter Johnstone, Fiberwise separation axioms for locales

Last revised on May 31, 2022 at 15:57:09. See the history of this page for a list of all contributions to it.