nLab locale

Redirected from "internal locale".
Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

Contents

Idea and motivation

Locale theory is one particular formulation of point-free topology.

A locale is, intuitively, like a topological space that may or may not have enough points (or even any points at all). It contains things we call open subspaces but there may or may not be enough points to distinguish between open subspaces. An open subspace in a locale can be regarded as conveying a bounded amount of information about the (hypothetical) points that it contains.

For example, there is a locale of all surjections from natural numbers (thought of as forming the discrete space NN) to real numbers (forming the real line RR, the locale of real numbers). This locale has no points, since there are no such surjections, but it contains many nontrivial open subspaces. (These open subspaces are generated by a family parametrised by n:Nn\colon N and x:Rx\colon R; the basic open associated to nn and xx may be described as {f:NR|f(n)=x}\{f\colon N \twoheadrightarrow R \;|\; f(n) = x\}. Together with relations internalizing the statements ‘n,!x,f(n)=x\forall\, n,\; \exists!\, x,\; f(n) = x’ and ‘x,n,f(n)=x\forall\, x,\; \exists\, n,\; f(n) = x’, which identify some opens but do not identify all of them, this specifies the locale. This construction is example 1.2.8 from section C1.2 of the Elephant.)

Every topological space can be regarded as a locale (with some lost information if the space is not sober). The locales arising this way are the topological or spatial locales. Conversely, every locale induces a topology on its set of points, but sometimes a great deal of information is lost; in particular, there are many different locales whose set of points is empty.

One motivation for locales is that since they take the notion of open subspace as basic, with the points (if any) being a derived notion, they are exactly what is needed to define sheaves. The notion of sheaf on a topological space only refers to the open subspaces, rather than the points, so it carries over word-for-word to a definition of sheaves on locales. Moreover, passage from locales to their toposes of sheaves is a full and faithful functor, unlike for topological spaces.

Another advantage of locales is that they are better-behaved than topological spaces in alternative foundations of mathematics, including mathematics without the axiom of choice, more generally constructive mathematics, or mathematics internal to an arbitrary topos. For example, constructively the topological space [0,1][0,1] need not be compact, but the locale [0,1][0,1] is always compact (in a suitable sense). It follows that the locale [0,1][0,1], and hence also the locale RR of real numbers, is not necessarily spatial. When it fails to be spatial, because there are “not enough real numbers,” the locale of real numbers is generally a better-behaved object than the topological space of real numbers.

Definitions

Recall that a frame AA is a poset with all joins and all finite meets which satisfies the infinite distributive law:

x( iy i)= i(xy i). x \wedge (\bigvee_i y_i) = \bigvee_i (x\wedge y_i) .

A frame homomorphism ϕ:AB\phi\colon A\to B is a function which preserves finite meets and arbitrary joins. Frames and frame homomorphisms form a category Frm.

Note: By the adjoint functor theorem (AFT) for posets, a frame also has all meets (at least assuming that it is a small set, or more generally that we allow impredicative quantification over it), but a frame homomorphism need not preserve them. Similarly, by the AFT, a frame is automatically a Heyting algebra, but again a frame homomorphism need not preserve the Heyting implication.

By definition, the category Locale of locales is the opposite of the category of frames

LocaleFrm op. Locale \coloneqq Frm^{op} \,.

That is, a locale XX “is” a frame, which we often write as O(X)O(X) and call “the frame of open subspaces of XX”, and a continuous map f:XYf\colon X \to Y of locales is a frame homomorphism f *:O(Y)O(X)f^*\colon O(Y) \to O(X). If you think of a frame as an algebraic structure (a lattice satisfying a completeness condition), then this is an example of the duality of space and quantity.

It is also possible to think of a continuous map f:XYf\colon X \to Y as a map of posets f *:O(X)O(Y)f_*\colon O(X) \to O(Y): a function that preserves all meets (and therefore is monotone and has a left adjoint f *:O(Y)O(X)f^*\colon O(Y) \to O(X)) and such that the left adjoint f *f^* preserves all finite meets. This has the arrow pointing in the “right” direction, at the cost of a less direct definition. (In predicative mathematics, we would have to explicitly add into this definition that f *f_* has a left adjoint; although since few locales even exist predicatively, we usually turn attention to bases of locales anyway.)

Remark

The map f *:O(X)O(Y)f_\ast: O(X) \to O(Y) is of course not the “direct image” along ff, rather it is a kind of dual to direct image, taking an open uO(X)u \in O(X) to the join

vO(Y):f *(v)uv\bigvee_{v \in O(Y): f^\ast(v) \leq u} v

For topological spaces in classical mathematics, denoting the complementation operator by ¬\neg and the interior operator by intint, we have f *(u)=int(¬f(¬u))f_\ast(u) = int(\neg f(\neg u)) where ff on the right denotes the ordinary set-theoretic direct image.

Alternatively, f *(u)f_*(u) can also be described as the largest open subset of YY whose preimage in XX is a subset of uu.

The category LocaleLocale is naturally enhanced to a 2-category:

Definition

The 2-category Locale has

  • as objects XX frames O(X)O(X);

  • as morphisms f:XYf\colon X \to Y frame homomorphisms f *:O(Y)O(X)f^*\colon O(Y) \to O(X);

  • a unique 2-morphism fgf \Rightarrow g whenever for all UO(Y)U \in O(Y) we have f *(U)g *(U)f^*(U) \leq g^*(U).

(See for instance Johnstone, C1.4, p. 514.)

Since parallel 22-morphisms are equal, this 2-category is in fact a (1,2)-category: a Poset-enriched category.

Subsidiary notions

Open and closed subspaces

Given a locale XX, the elements of the frame O(X)O(X) are traditionally thought of as being the open subspaces of XX and are therefore called the opens (or open subspaces, open parts, or open sublocales) of XX. However, one may equally well view them as the closed subspaces of XX and call them the closeds (or closed subspaces, closed parts, or closed sublocales) of XX. When viewed as closed subspaces, the opposite containment relation is used; thus O(X)O(X) is the frame of opens of XX, while the opposite poset O(X) opO(X)^{op} is the coframe of closeds of XX.

An open subspace may be thought of as a potentially verifiable property of a hypothetical point of the space XX. Thus we may verify the intersection of two open subspaces by verifying both properties, and we may verify the union of any family of open subspaces by verifying at least one of them; but it may not necessarily make sense to verify the intersection of infinitely many open subspaces, because this would require us to do an infinite amount of work. (The meet of an arbitrary family of open subspaces does exist, but the construction is impredicative, and it does not match the meet within the lattice of all subspaces.)

Dually, a closed subspace may be thought of as a potentially refutable property. Thus we may refute the union of two closed subspaces by refuting both of them, and we may refute the intersection of any family of closed subspaces by refuting at least one of them; but it may not necessarily make sense to refute the union of infinitely many closed subspaces. (Again, the join of an arbitrary family of closed subspaces does not work right.)

If one views an element of O(X)O(X) as a subspace of XX, one usually means to view it as an open subspace, but we have seen that one may also view it as a closed subspace. This is given by two different maps (one covariant and a frame homomorphism, one contravariant and a coframe homomorphism) from O(X)O(X) to the lattice of all subspaces of XX. See sublocale for further discussion.

Points

As a locale, the abstract point is the locale 11 whose frame of opens is the frame of truth values (classically {<}\{\bot \lt \top\}). This is the terminal object in LocaleLocale, since we must have (for f:X1f\colon X \to 1) f *()= Xf^*(\top) = \top_X and f *()= Xf^*(\bot) = \bot_X (and most generally f *(p)={ X|p}f^*(p) = \bigvee \{\top_X \;|\; p\}, since p={|p}p = \bigvee \{\top \;|\; p\}).

Given a locale XX, a concrete point of XX may be defined in any of the following equivalent ways:

  1. A point of XX is a continuous map f:1Xf\colon 1 \to X;
  2. Unravelling this in terms of f *:O(X)O(1)f^*\colon O(X) \to O(1) and viewing this as a characteristic function, a point of XX is a completely prime filter in O(X)O(X);
  3. Unravelling (1) in terms of f *:O(1)O(X)f_*\colon O(1) \to O(X), which classically (using excluded middle) is determined by f *()f_*(\bot), a point of XX is a prime element of O(X)O(X).

Definition (3) is simpler than (2), being an element of O(X)O(X) satisfying a finitary condition rather than a subset of O(X)O(X) satisfying an infinitary condition. However, it doesn't work in constructive mathematics, which provides much (but by no means all) of the motivation for studying locales.

Properties

Categories of internal locales

Proposition

The category Locale(E)(E) of locales internal to a topos EE is equivalent to the category of localic geometric morphisms Sh E(Σ)ESh_{E}(\Sigma) \to E in Topos.

Locale(E)(Topos/E) loc. Locale(E) \simeq (Topos/E)_{loc} \,.

See localic geometric morphism for more.

Proposition

For every locale XX, the category Locale(Sh(X))Locale(Sh(X)) of locales internal to the sheaf topos over XX is equivalent to the overcategory Locale/XLocale/X

:Locale/XLocale(Sh(X)). \mathcal{I}\colon Locale/X \stackrel{\simeq}{\to} Locale(Sh(X)) \,.

This appears as Johnstone, theorem C1.6.3.

Proposition

For every morphism of locales f:YXf\colon Y \to X the sheaf topos Sh(Y)Sh(Y) is equivalent as a topos over Sh(X)Sh(X) to the topos Sh Sh(X)((Y))Sh_{Sh(X)}(\mathcal{I}(Y)) of internal sheaves over the internal locale (Y)Sh(X)\mathcal{I}(Y) \in Sh(X)

Sh(Y)Sh Sh(X)((Y)). Sh(Y) \simeq Sh_{Sh(X)}(\mathcal{I}(Y)) \,.

This appears as Johnstone, scholium C1.6.4.

Relation to topological spaces

Every topological space XX has a frame of opens O(X)O(X), and therefore gives rise to a locale X LX_L. For every continuous function f:XYf\colon X \to Y between topological spaces, the inverse image map f 1:O(Y)O(X)f^{-1}\colon O(Y) \to O(X) is a frame homomorphism, so ff induces a continuous map f L:X LY Lf_L\colon X_L \to Y_L of locales. Thus we have a functor

() L:(-)_L\colon Top \to Locale.

Conversely, if XX is any locale, we define a point of XX to be a continuous map 1X1 \to X. Here 11 is the terminal locale, which can be defined as the locale 1 L1_L corresponding to the terminal space. Explicitly, we have O(1)=P(1)O(1) = P(1), the powerset of 11 (the initial frame, the set of truth values, which is 22 classically or in a Boolean topos). Since a frame homomorphism O(X)P(1)O(X) \to P(1) is determined by the preimage of 11 (the true truth value), a point can also be described more explicitly as a completely prime filter: an upwards-closed subset FF of O(X)O(X) such that XFX \in F (XX denotes the top element of O(X)O(X)), if U,VFU,V \in F then UVFU \cap V \in F, and if iU iF\bigcup_i U_i \in F then U iFU_i \in F for some ii.

The elements of O(X)O(X) induce a topology on the set of points of XX in an obvious way, thereby giving rise to a topological space X PX_P. Any continuous map f:XYf\colon X \to Y of locales induces a continuous map f P:X PY Pf_P\colon X_P \to Y_P of spaces, so we have another functor

() P:LocaleTop(-)_P\colon Locale \to Top.

One finds that () L(-)_L is left adjoint to () P(-)_P.

In fact, this is an idempotent adjunction:

Proposition

The categories Top of topological spaces and Locale of locales are related by an idempotent adjunction.

(() L() P):Top() P() LLocale. ( (-)_L \dashv (-)_P ) \colon Top \; \underoverset {\underset{(-)_P}{\longleftarrow}} {\overset{(-)_L}{\longrightarrow}} {\bot} \; Locale \,.

This appears for instance as (MacLaneMoerdijk, theorem IX.3 1) or as (Johnstone, lemma C.1.2.2).

Therefore the adjunction restricts to an equivalence between the fixed subcategories on either side.

Definition

A topological space XX with XX LPX \cong X_{L P} is called sober.

A locale with XX PLX \cong X_{P L} is called spatial or topological; one also says that it has enough points.

see also MO here

Corollary

The adjunction from prop. exhibits sober topological spaces as a coreflective subcategory of Locale

(() L() P):SoberTop() P() LLocale ( (-)_L \dashv (-)_P ) \colon SoberTop \underoverset {\underset{(-)_P}{\leftarrow}} {\overset{(-)_L}{\hookrightarrow}} {\bot} Locale

and this restricts to an equivalence of categories between the full subcategory of locales with enough points, and that of sober topological spaces.

This appears for instance as (MacLaneMoerdijk, corollary IX.3 4).

Consequently, we often identify a sober topological space and the corresponding topological locale.

Relation to toposes – localic reflection

The notion of Grothendieck topos can be seen as a categorification of the notion of locale, by relating both notions to the notion of lex totality:

Proposition

A poset PP is a frame if and only if the Yoneda embedding

y:P2 P op y \colon P \to \mathbf{2}^{P^{op}}

has a left exact left adjoint. (Here the poset 2\mathbf{2} of truth values is the base of enrichment for posets seen as enriched categories.)

The analogous result for toposes involves a bit of set theory: under ZFC plus the existence of a strong inaccessible cardinal? κ\kappa, the foundational assumption of MacLane in Categories for the Working Mathematician, call a category moderate if its set of morphisms has size κ\kappa. For example, SetSet is moderate.

Proposition

(Street)

A moderate locally small category CC is a Grothendieck topos if and only if the Yoneda embedding

y:CSet C opy \colon C \to Set^{C^{op}}

has a left exact left adjoint.

These results emphasize frames/toposes as algebras, where the morphisms are left exact left adjoints. The right adjoints to such morphisms are called geometric morphisms, and emphasize locales/toposes as spaces. This analogy, which plays an important but mostly tacit role in Joyal and Tierney, can be developed further along the following lines.

The frame of opens O(X)O(X) corresponding to a locale XX is naturally a site:

Definition

Given a locale XX, with frame of opens O(X)O(X), say that a family of morphisms {U iU}\{U_i \to U\} in O(X)O(X) is a cover if UU is the join of the U iU_i:

U= iU i. U = \vee_i U_i \,.
Proposition

This defines a coverage on O(X)O(X) and hence makes it a site.

See for instance (MacLaneMoerdijk, section 5).

Definition

For XX a locale, write

Sh(X)Sh(O(X)) Sh(X) \coloneqq Sh(O(X))

for the sheaf topos over the category O(X)O(X) equipped with the above canonical structure of a site.

Write Topos for the category of Grothendieck toposes and geometric morphisms.

Proposition

This construction defines a full and faithful functor Sh():Sh(-) : Locale \to Topos.

This appears for instance as MacLaneMoerdijk, section IX.5 prop 2.

Definition

A topos in the image of Sh():LocaleToposSh(-)\colon Locale \to Topos is called a localic topos.

Proposition

The functor Sh():LocaleToposSh(-)\colon Locale \to Topos has a left adjoint

L:ToposLocale L\colon Topos \to Locale

given by sending a topos \mathcal{E} to the locale that is formally dual to the frame of subobjects of the terminal object of \mathcal{E}:

O(L())Sub (*). O(L(\mathcal{E})) \coloneqq Sub_{\mathcal{E}}(*) \,.

This appears for instance as MacLaneMoerdijk, section IX.5 prop 3.

The functor LL here is also called localic reflection.

In summary this means that locales form a reflective subcategory of Topos:

LocaleLTopos. Locale \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow} Topos \,.

In fact this is even a genuine full sub-2-category:

Proposition

For all X,YX,Y \in Locale the 2-functor Sh:Sh\colon Locale \to Topos induces an equivalence of categories

Sh:Locale(X,Y)Topos(Sh(X),Sh(Y)). Sh\colon Locale(X,Y) \stackrel{\simeq}{\to} Topos(Sh(X), Sh(Y)) \,.

This appears as (Johnstone, prop. C1.4.5).

Proposition

The poset of subobjects Sub (*)Sub_{\mathcal{E}}(*) of the terminal object of \mathcal{E} is equivalent to the full subcategory τ 1()\tau_{\leq -1}(\mathcal{E}) of \mathcal{E} on the (1)(-1)-truncated objects of EE:

Sub (*)τ 1. Sub_{\mathcal{E}}(*) \simeq \tau_{\leq -1} \mathcal{E} \,.
Proof

A (-1)-truncated sheaf XX is one whose values over any object are either the singleton set, or the empty set

X(X){*,}=Set. X(X) \in \{*, \emptyset\} = \subset Set \,.

A monomorphism of sheaves is a natural transformation that is degreewise a monomorphism of sets (an injection). Therefore the subobjects of the terminal sheaf (that assigns the singleton set to every object) are precisely the sheaves of this form.

We may think of a frame as a Grothendieck (0,1)-topos. Then localic reflection is reflection of Grothendieck toposes onto (0,1)(0,1)-toposes and is given by (1)(-1)-truncation: for XX a locale, Sh(X)Sh(X) the corresponding localic topos and \mathcal{E} any Grothendieck topos we have a natural equivalence

Gr1Topos(,ShX)Gr(0,1)Topos(τ 1,O(X)) Gr1Topos( \mathcal{E}, Sh X) \simeq Gr(0,1)Topos(\tau_{\leq -1} \mathcal{E}, O(X))

which is

Frame(O(X),Sub (*))Locale(L,X). \cdots \simeq Frame(O(X), Sub_{\mathcal{E}}(*)) \simeq Locale(L \mathcal{E} , X) \,.

This is a small part of a pattern in higher topos theory, described at n-localic (∞,1)-topos.

Examples

General topology

As explained above, the functor from topological spaces to locales provides a very large collection of examples. When restricted to sober topological spaces, this functor becomes fully faithful and its essential images consists of spatial locales.

Without the axiom of excluded middle, many classical examples, such as the locale of real numbers or Cantor space, can cease to be spatial.

Naturally, one is interested in examples of locales that are not spatial, and a few are given below.

Measure theory

An amazing feature of pointfree topology is that it contains not only point-set general topology, but also point-set measure theory, again as a full subcategory.

Specifically, recall from the duality between geometry and algebra that various categories of commutative algebras are contravariantly equivalent to certain corresponding categories of spaces. The category of algebras relevant for measure theory is the category of commutative von Neumann algebras and ultraweakly continuous *-homomorphisms; it is widely accepted that dropping the commutativity condition and passing to the opposite category yields the correct category of noncommutative measurable spaces.

The category of commutative von Neumann algebras is contravariantly equivalent to several other categories:

The last category is particularly interesting: it is a full subcategory of locales. Thus, measure theory embeds into pointfree topology, which means that methods and results from pointfree topology can be used right away in measure theory. This stands in contrast to the traditional point-set treatments, where two rather different formalisms must be developed for point-set topological spaces and point-set measurable spaces.

With the exception of discrete locales, measurable locales are never spatial, and in fact do not have any points other than those in its atomic (discrete) part, which splits off as a coproduct summand.

Intersections of dense sublocales

Another important source of nonspatial sublocales is given by intersections (of arbitrary cardinality) of dense sublocales.

Again, in contrast to the point-set setting, where the Baire category theorem identifies the rather restrictive conditions under which the intersection of dense topological subspaces is again dense, in the pointfree setting arbitrary intersections of dense sublocales are always dense.

In particular, one can intersection all dense sublocales of a given locale, which always produces a nonspatial locale, unless the original locale is discrete. This is the double negation sublocale.

But there are other interesting examples. Connecting to measure theory, we can consider a valuation ν\nu on a given locale LL and take the intersection of all sublocales SS such that ν(S)=ν(1)\nu(S)=\nu(1). The resulting sublocale can be seen as the smallest sublocale with a measure 0 complement.

There is also a notion of internal locale, see also internal site.

References

An early paper, containing much of the basic theory, and in which the term “locale” is introduced:

An introduction to and survey of the use of locales instead of topological spaces (“point-free topology”):

This is, in its own words, to be read as the trailer for the book

that develops, among other things, much of general topology entirely with the notion of locales used in place of that of topological spaces. See also Stone Spaces for more.

Other textbook accounts:

and

  • Steve Vickers, Topology via logic, Cambridge University Press (1989)

where the latter develops topology from the point of view of its internal logic.

An introductory survey is

  • Jorge Picado, Aleš Pultr, Anna Tozzi, Locales, pages 49–101 in Pedicchio&Tholen (eds.), Categorical Foundations , CUP 2004. (draft)

See also

Lex totality is the subject of an article of Street,

  • Ross Street, Notions of Topos, Bull. Australian Math. Soc. 23 (1981), 199–208.

The connection between locales and toposes via lex totality plays a tacit role throughout the influential monograph

  • André Joyal and Myles Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society 51 (1984).

A basic introduction to locale theory can be found in section 1 of

A model category of locales which makes the reflection of sober topological spaces a Quillen adjunction to the sober-restriction of the classical model structure on topological spaces:

Last revised on October 24, 2023 at 09:42:26. See the history of this page for a list of all contributions to it.