Locale

Etymology and the key move

The word locale was introduced as a mathematical term by J.R. Isbell in “Atomless Parts of Spaces” (Mathematica Scandinavica 31, 1972, pp. 5–32). The naming is deliberate: locale derives from Latin locus (place, position, topic) — the same root as topology (from Greek topos). A locale is a place in the mathematical sense — a structured site of relations — but defined without assuming any occupants.

In ordinary language, locale entered English in 1816 as a false spelling of French local used as a noun, with the terminal e added to indicate stress (as in morale). The etymological content: a locale is a positioned particular — something with a definite character derived from its relational structure, not from what it contains.

The key move (Isbell, Johnstone, Vickers): A topological space is classically defined as a set of points equipped with a topology (a distinguished collection of subsets called opens). But this gets the priority backwards. What matters about a space is not which points inhabit it but which observable properties it supports — which propositions about it are semidecidable, which conditions can be verified by finite observation. The opens (observable properties) are primary; the points (complete consistent families of properties) are secondary — and may not exist at all.

This is the pointfree move: define a space entirely by its logic of observation, without assuming a prior point set. The resulting object is a locale.

Formal definition

A frame is a complete lattice satisfying the infinite distributive law:

$$a \wedge \bigvee_{i \in I} b_i \;=\; \bigvee_{i \in I} (a \wedge b_i)$$

for all $a \in L$ and all $\{b_i\}_{i \in I} \subseteq L$. Equivalently: a frame is a complete Heyting algebra — the implication $a \to b = \bigvee\{c \mid a \wedge c \leq b\}$ exists by the adjoint functor theorem. Finite meets distribute over infinite joins; this is the frame axiom.

A locale is a frame viewed as a space. The elements of the frame are the opens of the locale — its observable properties. The category $\mathbf{Loc}$ is defined as $\mathbf{Frm}^{\mathrm{op}}$: locale morphisms $f : L \to M$ are frame homomorphisms $f^* : O(M) \to O(L)$ going in the opposite direction (pulling back opens, as continuous maps pull back open sets). This reversal is essential: a continuous function sends points forward but pulls observations backward.

A nucleus on a frame $L$ is a map $j : L \to L$ satisfying:

1. $j(a \wedge b) = j(a) \wedge j(b)$ (meet-preservation)
2. $a \leq j(a)$ (extensiveness)
3. $j(j(a)) = j(a)$ (idempotence)

A sublocale of a locale $L$ is a subset $S \subseteq L$ that is closed under arbitrary meets and under residuation from the left: for every $a \in L$ and $s \in S$, the element $a \to s \in S$. Equivalently (and this equivalence is the content of the nucleus-sublocale theorem): $S = \mathrm{Fix}(j) = \{a \in L \mid j(a) = a\}$ for a unique nucleus $j$ on $L$.

Four structural results

Theorem 1 — The nucleus-sublocale bijection (Johnstone, Stone Spaces, Theorem II.2.3, 1982). For any locale $L$, there is a bijection:

$$\{\text{nuclei } j : L \to L\} \;\longleftrightarrow\; \{\text{sublocales of } L\}$$

given by $j \mapsto \mathrm{Fix}(j)$ and $S \mapsto j_S$ where $j_S(a) = \bigwedge\{s \in S \mid s \geq a\}$. The lattice of sublocales $\mathrm{Sl}(L)$ (ordered by inclusion) is anti-isomorphic to the lattice of nuclei $N(L)$ (ordered pointwise): $\mathrm{Sl}(L) \cong N(L)^{\mathrm{op}}$. Meets of sublocales are set-theoretic intersections; joins are the sublocale generated by the union (strictly larger than the union in general).

Theorem 2 — Sublocales form a coframe. The lattice $\mathrm{Sl}(L)$ is a coframe: binary meets distribute over arbitrary joins. But $\mathrm{Sl}(L)$ is generally not a frame — it is the opposite of a frame. Consequently, the complementation in $\mathrm{Sl}(L)$ is not Boolean: the complement $\neg S$ of a sublocale $S$ is the largest sublocale disjoint from $S$ (the pseudo-complement), and $S \vee \neg S$ need not equal the top sublocale $L$.

This is a sharp departure from classical topology: open subsets of a topological space form a frame; sublocales of a locale form a coframe. The two structures are dual.

Theorem 3 — Tychonoff’s theorem without choice (Johnstone, 1981). An arbitrary product of compact locales is compact — with no use of the axiom of choice. In classical point-set topology, Tychonoff’s theorem (product of compact spaces is compact) is equivalent to the axiom of choice over ZF. The localic version requires no choice whatsoever and is provable in constructive mathematics. This is not a quirk but a structural feature: compactness for locales is intrinsic to the lattice structure (it is the condition $\bigvee S = \top \Rightarrow \exists$ finite $T \subseteq S$ with $\bigvee T = \top$), independent of point selection.

Theorem 4 — The logical interpretation (Vickers, Topology via Logic, Cambridge University Press, 1988). The frame $O(L)$ of a locale is a geometric theory: its generators are the basic observable properties and its relations are the axioms of the frame (finite conjunction, infinite disjunction). The infinite distributive law $a \wedge \bigvee b_i = \bigvee(a \wedge b_i)$ encodes the logic of finitary hypothesis, infinitary witness: you can only make finitely many observations at once (finite $\wedge$), but you can verify that some element of an infinite disjunction holds by finding a witness ($\bigvee$ allowed infinitely). A point of $L$ is a frame homomorphism $p : O(L) \to \{0, 1\}$ — equivalently, a completely prime filter in $O(L)$. Under the logical interpretation: a point is a classical model of the geometric theory $O(L)$.

A locale without points is therefore a consistent geometric theory with no classical models — a situation that cannot arise under the axiom of choice (every consistent theory has a model, by the ultrafilter lemma), but that arises constructively and within any topos where AC fails internally. The locale of Dedekind reals in certain constructive foundations, the locale of surjections from $\mathbb{N}$ to $\mathbb{R}$ (which has no points because no such surjection exists, yet has a rich frame of observable conditions), and the classifying locale of any consistent but non-realizable geometric theory are all instances.

Stone duality and the spectrum

The full framework sits inside a web of Stone-type dualities.

Stone’s theorem (1936): The category of Boolean algebras is dually equivalent to the category of Stone spaces (compact Hausdorff totally disconnected topological spaces): $\mathbf{Bool} \simeq \mathbf{Stone}^{\mathrm{op}}$. The duality sends a Boolean algebra $B$ to its spectrum $\mathrm{Spec}(B)$ — the set of ultrafilters on $B$ with the topology generated by $\{U_a : a \in B\}$ where $U_a = \{F : a \in F\}$.

Priestley’s theorem (1970): The category of bounded distributive lattices is dually equivalent to the category of Priestley spaces (compact ordered spaces that are totally order-disconnected).

The general locale-space duality: For the category $\mathbf{Loc}$ of locales and the category $\mathbf{Top}$ of topological spaces, there is an adjunction:

$$\mathbf{Top} \;\underset{\mathrm{Pt}}{\overset{O}{\rightleftharpoons}}\; \mathbf{Loc}$$

where $O$ sends a space $X$ to its locale of open sets and $\mathrm{Pt}$ sends a locale $L$ to its space of points $\mathrm{Pt}(L)$ with the topology generated by $\{\hat{a} : a \in L\}$ where $\hat{a} = \{p \in \mathrm{Pt}(L) : p(a) = 1\}$. The adjunction restricts to an equivalence between sober spaces (spaces where every irreducible closed set has a unique generic point) and spatial locales (locales with enough points to separate opens). The full category $\mathbf{Loc}$ is strictly larger than the sober-space side.

The classifying locale. For any geometric theory $\mathbb{T}$, the classifying locale $\mathcal{L}[\mathbb{T}]$ is the locale whose frame is the Lindenbaum-Tarski algebra of $\mathbb{T}$ (formulae modulo provable equivalence under $\wedge$ and $\bigvee$). Points of $\mathcal{L}[\mathbb{T}]$ = classical models of $\mathbb{T}$. The locale is spatial iff $\mathbb{T}$ has enough models to witness all logical distinctions (a completeness condition). Every locale is, up to isomorphism, the classifying locale of some geometric theory.

The genius loci: mathematical and phenomenological convergence

In Roman religion, the genius loci (guardian spirit of a place) named the qualitative identity of a location — what made this place this place, independent of its temporary occupants. Christian Norberg-Schulz (Genius Loci: Towards a Phenomenology of Architecture, 1980), drawing on Heidegger’s “Building Dwelling Thinking” (1951), formalized this: a place is constituted by its character — by what can be experienced and observed there — not by which persons happen to inhabit it at any moment.

The mathematical locale makes precisely the same move. A locale $L$ is constituted by its frame $O(L)$ — its logic of observable properties — independently of whether any classical points (actual occupants) exist. Two locales with isomorphic frames are the same locale regardless of their point sets. The locale is the character; the points are secondary.

This convergence is not metaphorical. Both structures answer the same question: What makes a space this space? The phenomenological answer: its gathering of relations (Heidegger’s Versammlung) — how light, materiality, history, and social practice cohere there. The mathematical answer: its frame of observable opens — which semidecidable propositions the space supports, how they combine, what counts as covering.

The institutional implication: a normative institution is a locale. It is constituted by what can be legally recognized and acted upon within it — its frame of observable normative properties — not by which specific agents happen to occupy its roles. The corporation as a legal entity is defined by its articles of incorporation (the frame) and exists as a locale even before any officer, director, or shareholder is named. The judicial system is defined by its procedures, jurisdictions, and recognitions; which judges happen to hold office is secondary.

Locale vs. adjacent concepts

Concept	Constituted by	Points required	Distributive law	Category
Topological space	Point set + open sets	Yes — primary	Finite	$\mathbf{Top}$
Sober space	Point set, every irred. closed has generic point	Yes	Finite	$\mathbf{Top}_{\mathrm{sob}}$
Locale	Frame (complete distributive lattice)	No — secondary	Infinite	$\mathbf{Loc} = \mathbf{Frm}^{\mathrm{op}}$
Spatial locale	Frame with enough points to separate opens	Yes (enough)	Infinite	$\mathbf{Loc}_{\mathrm{sp}}$
Frame	Algebraic object	N/A	Infinite	$\mathbf{Frm}$
Scott domain	Directed-complete partial order + Scott topology	Optional	Directed	$\mathbf{DCPO}$

The adjunction $\mathbf{Top} \rightleftharpoons \mathbf{Loc}$ restricts to an equivalence on $\mathbf{Top}_{\mathrm{sob}} \simeq \mathbf{Loc}_{\mathrm{sp}}$. The gap between $\mathbf{Loc}$ and $\mathbf{Loc}_{\mathrm{sp}}$ is precisely the pointless locales — the consistent theories without classical models.

Scott domains (Vickers shows explicitly) form a full subcategory of $\mathbf{Loc}$: the Scott topology on any domain is a locale, and the continuous maps between domains are exactly the locale morphisms of their Scott topologies. Domain theory is locale theory restricted to a particularly well-behaved class of frames.

In this system

Definitions. Each fiber $H_t$ of the relational history presheaf is a locale: it is a complete Heyting algebra (the infinite distributive law holds, and the Heyting implication $a \to b = \bigvee\{c \mid a \wedge c \leq b\}$ exists). The saturation nucleus $\mathrm{RelationalHistoryFiberSaturatingNucleus}(t)$ and transferring nucleus $\mathrm{RelationalHistoryFiberTransferringNucleus}(t)$ satisfy all three nucleus axioms; by the definition of Lawvere-Tierney topology on a locale, they are the two canonical LT-topologies on $H_t$.

Proposition 1 (The two canonical sublocales and their coframe structure). By the nucleus-sublocale bijection (Johnstone, Theorem II.2.3): the saturation nucleus and transferring nucleus correspond to two sublocales:

$$\mathrm{Fix}(\sigma_t) \;\in\; \mathrm{Sl}(H_t), \qquad \mathrm{Fix}(\Delta_t) \;\in\; \mathrm{Sl}(H_t)$$

Their meet in $\mathrm{Sl}(H_t)$ is their set-theoretic intersection:

$$H^*_t \;=\; \mathrm{Fix}(\sigma_t) \cap \mathrm{Fix}(\Delta_t) \;=\; \mathrm{Fix}(\sigma_t) \wedge \mathrm{Fix}(\Delta_t) \;\in\; \mathrm{Sl}(H_t)$$

Their join in $\mathrm{Sl}(H_t)$ is the smallest sublocale of $H_t$ containing both — the sublocale generated by $\mathrm{Fix}(\sigma_t) \cup \mathrm{Fix}(\Delta_t)$. This is NOT the set-theoretic union; it is the closure of the union under arbitrary meets and left-residuation. It may be strictly larger than the union.

Proof. Meets in $\mathrm{Sl}(H_t)$ are set-theoretic intersections by definition of sublocales. The intersection of two sublocales is a sublocale (closed under meets and residuation by both). $\square$

Proposition 2 (Asymmetric locales: backward-seeing vs. forward-stable). The two canonical sublocales have fundamentally different characters as locales in their own right:

$\mathrm{Fix}(\sigma_t)$ is the backward-seeing sublocale: its elements are those propositions of $H_t$ that are maximally settled by the restriction profiles from predecessor histories. As a locale, $\mathrm{Fix}(\sigma_t) \cong H_t / {\sim_{\sigma_t}}$ (the quotient frame by the kernel of $\sigma_t$, which is a HA homomorphism by meet-preservation and surjectivity onto its image). Its points are those frame homomorphisms $H_t \to \{0,1\}$ that factor through $\sigma_t$ — agents whose observational profiles agree with the backward-recognized structure.

$\mathrm{Fix}(\Delta_t)$ is the forward-stable sublocale: its elements are those propositions present in the image of every one-step independent extension restriction $H(i_{s,t}) : H_{t \star s} \to H_t$, for every step $s \perp t$. Since each such image is a sub-Heyting-algebra of $H_t$ (images of HA homs are sub-HAs, by the sub-HA lemma), and the intersection of sub-HAs is a sub-HA, $\mathrm{Fix}(\Delta_t)$ is a sub-HA — in particular closed under implication $\to$. As a locale, $\mathrm{Fix}(\Delta_t)$ is the terminal object among locales over $H_t$ that are simultaneously sub-locales of every one-step extension.

Caution. The restriction $\sigma_t|_{\mathrm{Fix}(\Delta_t)} : \mathrm{Fix}(\Delta_t) \to H^*_t$ is a surjection but is not a Heyting algebra homomorphism in general — it does not preserve $\mathrm{Fix}(\Delta_t)$-joins. Therefore $H^*_t \cong \mathrm{Fix}(\Delta_t)/{\sim_{\sigma_t|_{\mathrm{Fix}(\Delta_t)}}}$ only as a poset, not as a locale. The joint sublocale $H^*_t$ has less frame structure than either $\mathrm{Fix}(\sigma_t)$ or $\mathrm{Fix}(\Delta_t)$ individually. (Source: relational-history-fiber-heyting-algebra-first-isomorphism-theorem.md.)

Proposition 3 (Pseudo-complementation in the sublocale lattice). Since $\mathrm{Sl}(H_t)$ is a coframe, it has pseudo-complements: for each sublocale $S \in \mathrm{Sl}(H_t)$, there is a largest sublocale $\neg S$ disjoint from $S$. However, $S \vee \neg S$ need not equal $H_t$ (the top sublocale): the sublocale lattice is not Boolean. In particular:

$$\mathrm{Fix}(\sigma_t) \vee \neg\mathrm{Fix}(\sigma_t) \;\subsetneq\; H_t \quad \text{in general}$$

The gap $H_t \setminus (\mathrm{Fix}(\sigma_t) \vee \neg\mathrm{Fix}(\sigma_t))$ has a normative interpretation: it consists of propositions that are neither backward-recognized nor classifiably not backward-recognized — a zone of genuine normative indeterminacy that is a structural feature of the locale, not resolvable by classical complementation.

Proposition 4 (Pointedness of $H_t$ and institutional instantiability). $H_t$ is a spatial locale iff it has enough points: iff frame homomorphisms $H_t \to \{0,1\}$ (classical agents fully specifying which propositions hold) exist in sufficient number to separate all opens. Under the logical interpretation: $H_t$ is spatial iff the normative theory it presents has enough classical models (instantiations by concrete agents) to distinguish all its propositions.

In classical mathematics (with the axiom of choice), every nontrivial locale has at least one point (ultrafilter lemma). The only pointless locale classically is $H_t = \{\top\}$ (the degenerate locale where all propositions are identified). Constructively and internally in a non-Boolean topos, genuine pointlessness arises: a history $t$ may represent a consistent normative state whose full instantiation requires structures not available in the ambient mathematical universe — an institutional configuration that is coherently defined but not yet (or not currently) concretely realized.

Proposition 5 (The Joyal-Tierney theorem and the hyperverse topos). The category $\mathrm{Sh}(T, J)$ of sheaves on the relational history site $(T, J)$ is a Grothendieck topos. By the Joyal-Tierney theorem (Joyal and Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs AMS 51(309), 1984): every Grothendieck topos $\mathcal{E}$ is equivalent to the topos of equivariant sheaves on some localic groupoid $G$:

$$\mathcal{E} \;\simeq\; \mathrm{Sh}(G)$$

Applied to $\mathrm{Sh}(T, J)$: the relational hyperverse corresponds to sheaves on a localic groupoid $G_{(T,J)}$. The localic groupoid encodes the symmetries and transition structure of the site in purely locale-theoretic terms — without reference to a set of points in the site. Whether $G_{(T,J)}$ has a normative interpretation (whether its object locale is one of the fibers $H_t$, whether its morphism locale encodes nuclear commutation) is an open structural question.

Open questions

• Whether the pseudo-complement $\neg \mathrm{Fix}(\sigma_t)$ in $\mathrm{Sl}(H_t)$ — the largest sublocale of $H_t$ disjoint from the backward-seeing sublocale — has a formal normative reading: what does it mean to be in the “forward-only” zone, maximally separated from backward recognition?

• Whether the classifying-locale perspective gives a direct construction of each fiber $H_t$: is there a geometric theory $\mathbb{T}_t$ whose classifying locale $\mathcal{L}[\mathbb{T}_t]$ is precisely $H_t$? If so, what are the generators and axioms of $\mathbb{T}_t$, and how do history steps $t_0 \to t$ correspond to geometric morphisms between the classifying toposes?

• Whether the Tychonoff theorem for locales (no choice required) yields a product result for relational universes: if $H_t$ and $H_s$ are compact locales, is the localic product $H_t \otimes H_s$ (the coproduct of frames) compact without choice? This would imply that joint normative closure is achievable without a choice principle selecting which propositions are settled in the joint system.

• Whether the non-spatiality of $H_t$ (if it occurs) corresponds to a specific class of normative configurations — whether there is a structural condition on the history site $(T, J)$ that guarantees spatiality of all fibers, and whether this condition has an institutional interpretation (e.g., sufficient diversity of agents, or sufficient concreteness of the covering families in $J$).

• Whether the localic groupoid $G_{(T,J)}$ from the Joyal-Tierney representation is a known structure: whether it is related to the nucleus-commutation groupoid, the history monoid as a localic category, or some combination. The morphism locale of $G_{(T,J)}$ would encode the transition structure of the entire relational hyperverse in purely pointfree terms.

• Whether the institutional corruption scenario from Enterprise — where the nucleus pair $(\sigma_t, \Delta_t)$ is weakened to $(\sigma'_t, \Delta'_t)$ — corresponds to a sublocale shrinkage in $\mathrm{Sl}(H_t)$: the fixed sublocale $H^{*'}_t = \mathrm{Fix}(\sigma'_t \circ \Delta'_t)$ is nominally larger (more elements declared settled) but its locale structure is impoverished — the new sublocale has fewer observable distinctions, a coarser topology on the space of recognitions.