# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJan 3rd 2011
• (edited Jan 3rd 2011)

added to locale a section relation to toposes stating localic reflection

• CommentRowNumber2.
• CommentAuthorDavidRoberts
• CommentTimeJan 3rd 2011

locale, not ocale

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJan 3rd 2011

thanks, fixed.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 3rd 2011

Added to locale remakrs on how the frame of subobjects $Sub_{\mathcal{E}}(*) \simeq \tau_{\leq -1}$ is the subcategory of $(-1)$-truncated objects and how this is the beginning of a pattern continued at n-localic (infinity,1)-topos.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMar 16th 2011

Have added to locale in the section Category of locales two theorems from the Elephant on the externalization of internal locales (needed in the discussion of Bohrification)

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJul 8th 2011

At locale in the section relation to topological spaces I have tried to make some of the statements more pronounced.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeJul 25th 2011

I have made more explicit in the discussion of localic reflection at locale that $Sh : Locale \to Topos$ is fully faithful in fact as a 2-functor.

The discussion of this point in the entry would deserve a bit of expansion. Maybe I find time to expand on it later.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJul 25th 2011

I realized that we never stated the definition of the 2-category (or (1,2)-category) of locales. So I have now added it to the Definition-section at Locale.

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeJul 25th 2011

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeJul 25th 2011
• (edited Jul 25th 2011)

Oh. dear, I should take a break :-) I did look for it, but didn’t see it! Thanks.

Anyway, I have now added to Locale, too, the precise definition, and some more pointers.

• CommentRowNumber11.
• CommentAuthorTodd_Trimble
• CommentTimeDec 6th 2011

Added to locale the observation that frames are the same as lex total posets, by way of introducing connections between locales and toposes.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeDec 6th 2011

Nice, thanks! Should we have a page lex-total category with Street’s theorem on it?

• CommentRowNumber13.
• CommentAuthorCharles Rezk
• CommentTimeMay 20th 2019

The second paragraph of Locale says:

For example, there is a locale of all surjections from natural numbers (thought of as forming the discrete space $N$) to real numbers (forming the real line $R$): the locale of real numbers. This local 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\colon N$ and $x\colon R$; the basic open associated to $n$ and $x$ may be described as $\{f\colon N \twoheadrightarrow R \;|\; f(n) = x\}$.

Can someone explain exactly what this means, or at least give a reference?

• CommentRowNumber14.
• CommentAuthorDavid_Corfield
• CommentTimeMay 20th 2019

Capitalised ’Locale’ is redirected to Loc, the category. So you mean the lower case version locale.

Does the description at locale of real numbers help? It seems to be largely the work of Toby.

• CommentRowNumber15.
• CommentAuthorCharles Rezk
• CommentTimeMay 20th 2019

Yes I mean locale. The locale of real numbers doesn’t help at all. In any case I would guess that the particular sets (locales?) $N$ and $R$ are basically irrelevant for this example. (Except for having $|N|\lt|R|$, which is supposed to imply there are no points.) I just want to know what definition is underlying this example.

• CommentRowNumber16.
• CommentAuthorCharles Rezk
• CommentTimeMay 20th 2019
• (edited May 20th 2019)

Here’s my speculation, though it doesn’t seem to work right. Let $X$ and $Y$ be sets, and let $\mathcal{P}$ be the poset of “finite partial graphs” in $X\times Y$, i.e., finite subsets $\Gamma\subseteq X\times Y$ such that the composite $\Gamma\to X\times Y \to X$ is injective. Let $\mathcal{O}$ be the collection of upward-closed subsets of $\mathcal{P}$: this set is supposed to be the collection of “opens” in the locale.

Given any function $f\colon X\to Y$ let $U_f\in \mathcal{O}$ be the set of all $\Gamma\in \mathcal{P}$ such that $\Gamma\cup \Gamma_f$ is not the graph of any function: it’s the set of finite partial graphs inconsistent with $f$. Note that $U_f\neq \mathcal{P}$ since $\varnothing\notin U_f$, and I can show that $U_f$ is non-trivially an intersection of non-maximal elements of $\mathcal{O}$ if and only if $f$ is not surjective. That is, surjective functions give rise to points in the locale $\mathcal{O}$. What I can’t prove is that these are the only points in the locale.

Edit. Nevermind that doesn’t make sense anyway. But I expect they mean some kind of example along these lines.

• CommentRowNumber17.
• CommentAuthorMike Shulman
• CommentTimeMay 20th 2019

The locale of surjections $X\to Y$ is the classifying locale of the propositional geometric theory of surjections $X\to Y$. There are basic propositions “$f(x)=y$” (an atomic formula) for each $x\in X$ and $y\in Y$, and then axioms like $\vdash_{x\in X} \bigvee_{y\in Y} f(x)=y$ and $(f(x)=y) \wedge (f(x)=y') \vdash_{x\in X,y\neq y'\in Y} \bot$ to make it a function and $\vdash_{y\in Y} \bigvee_{x\in X} f(x)=y$ to make it surjective. So the opens of the locale are generated by these propositions “$f(x)=y$” under finite meet and arbitrary join, modulo those axioms. This can be re-expressed in terms of partial functions in a way kind of like you say, but I don’t remember (and don’t have time to work out) exactly how it goes. But with this description, the points of the locale are, by the universal property of classifying locales (or equivalently, by the universal property of a frame presented by generators and relations), precisely surjections $X\to Y$.

• CommentRowNumber18.
• CommentAuthorCharles Rezk
• CommentTimeMay 23rd 2019

Thanks Mike. I would still love a reference for this. It looks to me that what I was describing above is the locale of “partial graphs in $X\times Y$”; at least, the points are precisely the partial graphs. I assume the additional axioms are imposed by choosing appropriate sublocales.

• CommentRowNumber19.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2019

It’s C1.2.8 in Sketches of an Elephant.

• CommentRowNumber20.
• CommentAuthorCharles Rezk
• CommentTimeJun 7th 2019

Thanks Mike.

Here’s a brief sketch of the construction (where I’ve unwound most of the terminology Johnstone uses here).

Fix discrete spaces $X$ and $Y$, and let $M=\prod_X Y$ with the usual product topology. For a finite subset $S\subseteq Y$ write $M_S=\{f\in M\;|\; S\subseteq f(X)\}$, the subset of functions which map onto $S$. Let $\mathcal{O}$ be the collection of open subsets $U\subseteq M$ such that

for all open $V\subseteq M$ and finite $S\subseteq Y$, we have that $V\cap M_S\subseteq U$ implies $V\subseteq U$.

The claims are that:

1. $\mathcal{O}$ is a complete lattice satisfying the infinite distributive law, i.e., it corresponds to a locale.

2. If $X$ is infinite then $\varnothing\in \mathcal{O}$ and $M\in \mathcal{O}$, e.g., $\mathcal{O}$ is a non-trivial locale when $X$ is infinite and $Y$ is non-empty.

3. The points of $\mathcal{O}$ correspond exactly to surjective functions $X\to Y$.

In particular, if $\infty\leq |X| \lt |Y|$ then $\mathcal{O}$ is a non-trivial pointless locale. (Johnstone in the example assumes $X=\mathbb{N}$, but as far as I can tell the construction is entirely general.)

It is easy to see that $\mathcal{O}$ is closed under pairwise intersections of open sets and contains $M$, so has pairwise meets and a top element. To show it is a locale, you need to know that for every open set $U$ there is a smallest open set $j(U)$ which contains $U$ and is an element of $\mathcal{O}$. The recipe for $j$ is to define for any open set $U$,

$h(U) := \bigcup_{V\cap M_S\subseteq U} V,$

where the union ranges over all open $V\subseteq U$ and finite $S\subseteq Y$ satisfying the condition. Then iterate $h$ some possibly transfinite number of times to get $j(U)$. Then $j(\varnothing)$ is the bottom element and $\bigvee U_i = j(\bigcup U_i)$. The key observation is that $h$ preserves pairwise intersection and has exactly elements of $\mathcal{O}$ as its fixed points, whence $j$ has these same properties.

More conceptually: $\mathcal{O}$ is the limit in Locale of the family of subspaces $M_S$ of $M$ indexed by the poset of all finite $S\subseteq Y$; compare with the limit in Top, which is just the subspace $\bigcap_S M_S$ of surjective functions. (Johnntone says “intersection of sublocales” here, but I think it is also an example of a limit in Locale this context, as is the intersection subspace in Top.)

Unrelated remark: Apparently the TeX engine on this thing displays the same character for $\backslash varnothing$ ($\varnothing$) and $\backslash emptyset$ ($\emptyset$), which is unfortunate since $\emptyset$ is so ugly.

• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeJun 8th 2019

Thanks for writing that out! It would be useful to add it to some nlab page, maybe locale?

I generally prefer \emptyset to \varnothing; I find the latter uglier than the former. But if you really want the latter you may be able to get it with unicode &#8709; (∅).

• CommentRowNumber22.
• CommentAuthorTobyBartels
• CommentTimeSep 25th 2019

Web page for Picado & Pultr 2012.

• CommentRowNumber23.
• CommentAuthorTobyBartels
• CommentTimeSep 25th 2019

I added a bit about the locale of surjections discussed in comments #13–#21, only at the level of detail of Mike #17 (actually less detail than that), not Charles #20.

• CommentRowNumber24.
• CommentAuthorTobyBartels
• CommentTimeFeb 2nd 2020

The direct-image functor preserves joins, not meets.

• CommentRowNumber25.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 2nd 2020
• (edited Feb 2nd 2020)

Toby: no. This is not “direct image”, since direct image maps do not (generally) take opens to opens. Rather, we are taking an adjoint $O(X) \to O(Y)$ to a frame map $O(Y) \to O(X)$, and since frame maps are left exact left adjoints, we want here its right adjoint, playing a role analogous to geometric morphisms between toposes.

• CommentRowNumber26.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 2nd 2020

(Rolled back to previous version.)

• CommentRowNumber27.
• CommentAuthorTobyBartels
• CommentTimeFeb 7th 2020

Sorry, I thought that it was a typo (well, something analogous to that, involving thinking about things backwards), but it was me who was thinking backwards! (left vs right adjoint).

• CommentRowNumber28.
• CommentAuthorTobyBartels
• CommentTimeFeb 7th 2020
• (edited Feb 7th 2020)

Although a rollback is a dangerous tool, since I also made some other (more minor) edits. I just used that tool myself to restore my other edits; but if all that you did was to roll back my edit and add your remark (edit: and change ‘This category’ to ‘The category $Locale$’), then everything is OK now.

• CommentRowNumber29.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 8th 2020

Sorry if I missed those other edits. Looks good now.

• CommentRowNumber30.
• CommentAuthorDmitri Pavlov
• CommentTimeMar 22nd 2020

Added another description of localic direct images for topological spaces.

1. Added reference for the construction of the locale of surjections N -> R.

Alfredo Álvarez

• CommentRowNumber32.
• CommentAuthorDmitri Pavlov
• CommentTimeFeb 24th 2021

Redirects: map of locales, morphism of locales, etc.

• CommentRowNumber33.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 3rd 2021

## 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 faihtful and its essential images consists of spatial locales.

If excluded middle fails, many classical examples, such as the locale of real numbers, 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 ultraweak *-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:

• compact strictly localizable enhanced measurable spaces and measurable maps;

• measurable locales and maps of locales.

The last category is particularly interesting: it is a full subcategory of locales, which means that 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 for point-set measurable spaces.

With the exception of discrete locales, measurable locales are never spatial.

### 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 $L$ and take the intersection of all sublocales $S$ such that $\nu(S)=\nu(1)$. The resulting sublocale can be seen as the smallest sublocale with a measure 0 complement.

• CommentRowNumber34.
• CommentAuthorUrs
• CommentTimeJul 3rd 2021

Thanks!! That’s excellent.

(We should really have an entry noncommutative measure theory…)