Locale ($X,\mathcal{O}(X)$)

A locale is an object of the opposite of the category of frames. A map $f:X\to Y$ is specified by a frame homomorphism $f^{\ast }:\mathcal{O}(Y)\to \mathcal{O}(X)$. This makes open-set algebra primary and allows spaces without enough ordinary points. A point of a frame is the inverse-image map of a point of a locale.

Under classical logic a positive locale is connected when it cannot be written as the union of two disjoint nonzero opens. Equivalently its only complemented opens are $0$ and $1$. An open sublocale uses this criterion relative to its own top element. Positivity of the whole locale excludes the empty locale. This definition is stated with its logical convention; replacing positivity by negated nonemptiness is not a constructive step.

This relation says that the closure of the open $u$ is contained in $v$. A regular locale has $a={\bigvee }_{u\prec a}u$ for every $a$. If $u\prec a$, then $\neg \neg u\le a$ and $\neg \neg u\prec a$.

A locale is regular when every open is the join of opens well inside it. This expresses regularity without reference to points.

A locale is extremally disconnected when the closure of every open is open. Equivalently its regular open elements are complemented, or double negation preserves binary joins, or its Booleanization of a locale is a flat sublocale.

For a compact regular locale $X$, put $B=\mathcal{O}(X{)}_{\neg \neg }$ and $\mathcal{O}(\gamma X)=\mathrm{Idl}(B)$. This locale is extremally disconnected. Its natural surjection to $X$ has inverse imageThe Joyal extension lemma gives the frame homomorphism; its injectivity follows by recovering $a$ as the join of the regular opens in this ideal.

An open, or overt, locale has a positivity map $\mathrm{Pos}:\mathcal{O}(X)\to \Omega$ left adjoint to the scalar inverse image ${!}^{\ast }:\Omega \to \mathcal{O}(X)$, satisfying Frobenius reciprocity. Thus $a\le {!}^{\ast }\mathrm{Pos}(a)$ and positivity preserves arbitrary joins. Classically every locale is overt, with positivity meaning $a\ne 0$.

A positive open locale is totally connected when every positive open of a locale is connected. Under classical logic its positive opens form a completely prime filter, hence specify a dense point. Positivity of the whole locale is essential: the empty locale satisfies the condition on positive opens vacuously but has no point.

An open is positive when its positivity truth value holds. Positivity gives a constructive witness of inhabitedness and must not be replaced by double-negated nonemptiness.

A locale is totally unordered when $f^{\ast }\le g^{\ast }$ for two maps into it implies $f=g$, for every common domain. This tests generalized points rather than just ordinary points. Every Hausdorff locale has this property: comparable maps annihilate the complement of the diagonal and hence factor through the diagonal.

A locale is Hausdorff when its diagonal into its localic square is a closed sublocale. Its complement is the join of rectangles $a\times b$ with $a\wedge b=0$. This is stronger than the underlying space being a Hausdorff space, because the localic square need not be spatial.

A locale is compact when every directed family of opens whose join is $1$ contains $1$. Equivalently every open cover has a finite subcover. The truth-valued test $a\mapsto [a=1]$ is a preframe homomorphism exactly when the locale is compact.

An arbitrary product of compact locales is compact. Finite products correspond to preframe tensor products, whose compactness follows by tensoring the top tests. An arbitrary product is obtained by the filtered colimit of finite frame coproducts; the eventual-top test proves that filtered colimits preserve compactness. No choice of points is required.

A sublocale is determined by a nucleus on a frame $j$ on $\mathcal{O}(X)$. Its frame consists of the fixed elements of $j$, with inherited meets and regularized joins. Increasing the nucleus makes the sublocale smaller.

The double-negation nucleus on a frame gives a dense sublocale whose frame is a complete Boolean algebra. Its elements are regular open elements, with Boolean joins $\neg \neg {\bigvee }_i{a}_i$.

A sublocale is flat when its nucleus on a frame preserves finite joins, including $0$. Equivalently its fixed elements are closed under ambient finite joins. In particular every flat sublocale is a dense sublocale.

Every map from a flat sublocale $A_j$ of $A$ to a compact locale that is also a regular locale extends uniquely to $A$. On frames the extension iswhere the terms are first regarded as fixed elements in the ambient frame. Regularity proves agreement after applying $j$; compactness reduces arbitrary covers to finite subcovers on a well-inside open, and flatness identifies those finite joins with ambient joins. These facts prove that $g^{\ast }$ preserves arbitrary joins and finite meets.

A sublocale is dense when its closure is the whole locale. For a map $f$, its image is dense when $f^{\ast }(a)=0$ implies $a=0$. Classically, a dense point belongs to every nonzero open.

The closed nucleus $c(a)$ determines the complement of the open $a$. A sublocale with nucleus $j$ is dense precisely when $j(0)=0$, since its closure is the closed sublocale defined by $j(0)$.