\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{locale} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory} [[!include topos theory - contents]] \hypertarget{topology}{}\paragraph*{{Topology}}\label{topology} [[!include topology - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea_and_motivation}{Idea and motivation}\dotfill \pageref*{idea_and_motivation} \linebreak \noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak \noindent\hyperlink{Subsidiaries}{Subsidiary notions}\dotfill \pageref*{Subsidiaries} \linebreak \noindent\hyperlink{open_and_closed_subspaces}{Open and closed subspaces}\dotfill \pageref*{open_and_closed_subspaces} \linebreak \noindent\hyperlink{points}{Points}\dotfill \pageref*{points} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{CategoryOfLocales}{Categories of internal locales}\dotfill \pageref*{CategoryOfLocales} \linebreak \noindent\hyperlink{RelationToTopologicalSpaces}{Relation to topological spaces}\dotfill \pageref*{RelationToTopologicalSpaces} \linebreak \noindent\hyperlink{RelationToToposes}{Relation to toposes -- localic reflection}\dotfill \pageref*{RelationToToposes} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea_and_motivation}{}\subsection*{{Idea and motivation}}\label{idea_and_motivation} Locale theory is one particular formulation of [[point-free topology]]. A \emph{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]] $N$) to [[real numbers]] (forming the [[real line]] $R$, the \emph{[[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\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\}$. Together with relations internalizing the statements ‘$\forall\, n,\; \exists!\, x,\; f(n) = x$’ and ‘$\forall\, x,\; \exists\, n,\; f(n) = x$’, which identify some opens but do not identify all of them, this specifies the locale.) Every topological space can be regarded as a locale (with some lost information if the space is not [[sober space|sober]]). The locales arising this way are the \emph{[[topological locale|topological]]} or \emph{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 set|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 [[internalization|internal]] to an arbitrary [[topos]]. For example, constructively the topological space $[0,1]$ need not be [[compact space|compact]], but the \emph{locale} $[0,1]$ is always compact (in a suitable sense). It follows that the locale $[0,1]$, and hence also the locale $R$ 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. \hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions} Recall that a \textbf{[[frame]]} $A$ is a [[partial order|poset]] with all [[join|joins]] and all finite [[meet|meets]] which satisfies the \emph{infinite distributive law}: \begin{displaymath} x \wedge (\bigvee_i y_i) = \bigvee_i (x\wedge y_i) . \end{displaymath} A \textbf{frame [[homomorphism]]} $\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 [[predicative mathematics|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 \textbf{locales} is the [[opposite category|opposite]] of the category of frames \begin{displaymath} Locale \coloneqq Frm^{op} \,. \end{displaymath} That is, a locale $X$ ``is'' a frame, which we often write as $O(X)$ and call ``the frame of open subspaces of $X$'', and a \textbf{[[continuous map]]} $f\colon X \to Y$ of locales is a frame homomorphism $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\colon X \to Y$ as a map of [[posets]] $f_*\colon O(X) \to O(Y)$: a [[function]] that preserves all [[meets]] (and therefore is [[monotone function|monotone]] and has a [[left adjoint]] $f^*\colon O(Y) \to O(X)$) and such that the left adjoint $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 must explicitly add into this definition that $f_*$ has a left adjoint; compare the definition of [[geometric morphism]] one level up.) This category is naturally enhanced to a [[2-category]]: \begin{defn} \label{}\hypertarget{}{} The [[2-category]] [[Locale]] has \begin{itemize}% \item as [[objects]] $X$ [[frames]] $O(X)$; \item as [[morphisms]] $f\colon X \to Y$ frame homomorphisms $f^*\colon O(Y) \to O(X)$; \item a unique [[2-morphism]] $f \Rightarrow g$ whenever for all $U \in O(Y)$ we have $f^*(U) \leq g^*(U)$. \end{itemize} \end{defn} (See for instance \hyperlink{Johnstone}{Johnstone, C1.4, p. 514}.) Since [[parallel morphisms|parallel]] $2$-morphisms are equal, this [[2-category]] is in fact a [[(1,2)-category]]: a [[Poset]]-[[enriched category]]. \hypertarget{Subsidiaries}{}\subsection*{{Subsidiary notions}}\label{Subsidiaries} \hypertarget{open_and_closed_subspaces}{}\subsubsection*{{Open and closed subspaces}}\label{open_and_closed_subspaces} Given a locale $X$, the elements of the frame $O(X)$ are traditionally thought of as being the [[open subspaces]] of $X$ and are therefore called the \textbf{opens} (or \textbf{open subspaces}, \textbf{open parts}, or \textbf{open sublocales}) of $X$. However, one may equally well view them as the [[closed subspaces]] of $X$ and call them the \textbf{closeds} (or \textbf{closed subspaces}, \textbf{closed parts}, or \textbf{closed sublocales}) of $X$. When viewed as closed subspaces, the [[opposite relation|opposite]] containment relation is used; thus $O(X)$ is the \textbf{frame of opens} of $X$, while the [[opposite poset]] $O(X)^{op}$ is the \textbf{coframe of closeds} of $X$. An open subspace may be thought of as a potentially \emph{verifiable} property of a hypothetical point of the space $X$. 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.) [[de Morgan duality|Dually]], a closed subspace may be thought of as a potentially \emph{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)$ as a [[subspace]] of $X$, 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)$ to the lattice of all subspaces of $X$. See [[sublocale]] for further discussion. \hypertarget{points}{}\subsubsection*{{Points}}\label{points} As a locale, the \textbf{abstract [[point]]} is the locale $q$ whose frame of opens is the frame of [[truth values]] (classically $\{\bot \lt \top\}$). This is the [[terminal object]] in $Locale$, since we must have (for $f\colon X \to 1$) $f^*(\top) = \top_X$ and $f^*(\bot) = \bot_X$ (and most generally $f^*(p) = \bigvee \{\top_X \;|\; p\}$, since $p = \bigvee \{\top \;|\; p\}$). Given a locale $X$, a \textbf{concrete [[point]]} of $X$ may be defined in any of the following equivalent ways: \begin{enumerate}% \item A point of $X$ is a [[continuous map]] $f\colon 1 \to X$; \item Unravelling this in terms of $f^*\colon O(X) \to O(1)$ and viewing this as a [[characteristic function]], a point of $X$ is a [[completely prime filter]] in $O(X)$; \item Unravelling (1) in terms of $f_*\colon O(1) \to O(X)$, which classically (using [[excluded middle]]) is determined by $f_*(\bot)$, a point of $X$ is a [[prime element]] of $O(X)$. \end{enumerate} Definition (3) is simpler than (2), being an element of $O(X)$ satisfying a finitary condition rather than a subset of $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. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{CategoryOfLocales}{}\subsubsection*{{Categories of internal locales}}\label{CategoryOfLocales} \begin{prop} \label{}\hypertarget{}{} The category [[Locale]]$(E)$ of locales [[internalization|internal to]] a [[topos]] $E$ is equivalent to the category of [[localic geometric morphisms]] $Sh_{E}(\Sigma) \to E$ in [[Topos]]. \begin{displaymath} Locale(E) \simeq (Topos/E)_{loc} \,. \end{displaymath} \end{prop} See [[localic geometric morphism]] for more. \begin{prop} \label{}\hypertarget{}{} For every locale $X$, the category $Locale(Sh(X))$ of locales internal to the [[sheaf topos]] over $X$ is equivalent to the [[overcategory]] $Locale/X$ \begin{displaymath} \mathcal{I}\colon Locale/X \stackrel{\simeq}{\to} Locale(Sh(X)) \,. \end{displaymath} \end{prop} This appears as \hyperlink{Johnstone}{Johnstone, theorem C1.6.3}. \begin{prop} \label{}\hypertarget{}{} For every morphism of locales $f\colon Y \to X$ the [[sheaf topos]] $Sh(Y)$ is equivalent as a topos over $Sh(X)$ to the topos $Sh_{Sh(X)}(\mathcal{I}(Y))$ of internal sheaves over the internal locale $\mathcal{I}(Y) \in Sh(X)$ \begin{displaymath} Sh(Y) \simeq Sh_{Sh(X)}(\mathcal{I}(Y)) \,. \end{displaymath} \end{prop} This appears as \hyperlink{Johnstone}{Johnstone, scholium C1.6.4}. \hypertarget{RelationToTopologicalSpaces}{}\subsubsection*{{Relation to topological spaces}}\label{RelationToTopologicalSpaces} Every [[topological space]] $X$ has a [[frame of opens]] $O(X)$, and therefore gives rise to a locale $X_L$. For every [[continuous function]] $f\colon X \to Y$ between topological spaces, the [[preimage|inverse image]] map $f^{-1}\colon O(Y) \to O(X)$ is a frame homomorphism, so $f$ induces a continuous map $f_L\colon X_L \to Y_L$ of locales. Thus we have a [[functor]] $(-)_L\colon$ [[Top]] $\to$ [[Loc|Locale]]. Conversely, if $X$ is any locale, we define a \textbf{[[point]]} of $X$ to be a [[continuous map]] $1 \to X$. Here $1$ is the [[terminal object|terminal]] locale, which can be defined as the locale $1_L$ corresponding to the terminal space. Explicitly, we have $O(1) = P(1)$, the [[powerset]] of $1$ (the initial frame, the set of [[truth values]], which is $2$ classically or in a [[Boolean topos]]). Since a frame homomorphism $O(X) \to P(1)$ is determined by the preimage of $1$ (the [[true]] truth value), a point can also be described more explicitly as a \emph{[[completely prime filter]]}: an upwards-closed subset $F$ of $O(X)$ such that $X \in F$ ($X$ denotes the [[top element]] of $O(X)$), if $U,V \in F$ then $U \cap V \in F$, and if $\bigcup_i U_i \in F$ then $U_i \in F$ for some $i$. The elements of $O(X)$ induce a [[topological structure|topology]] on the set of points of $X$ in an obvious way, thereby giving rise to a topological space $X_P$. Any continuous map $f\colon X \to Y$ of locales induces a continuous map $f_P\colon X_P \to Y_P$ of spaces, so we have another functor $(-)_P\colon Locale \to Top$. One finds that $(-)_L$ is [[left adjoint]] to $(-)_P$. In fact, this is an [[idempotent adjunction]]: \begin{prop} \label{TopLocAdjunction}\hypertarget{TopLocAdjunction}{} The categories [[Top]] of [[topological spaces]] and [[Loc|Locale]] of locales are related by an [[idempotent adjunction]]. \begin{displaymath} ( (-)_L \dashv (-)_P ) \colon Top \; \underoverset {\underset{(-)_P}{\longleftarrow}} {\overset{(-)_L}{\longrightarrow}} {\bot} \; Locale \,. \end{displaymath} \end{prop} This appears for instance as (\hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, theorem IX.3 1}) or as (\hyperlink{Johnstone}{Johnstone, lemma C.1.2.2}). Therefore the [[adjunction]] restricts to an [[equivalence of categories|equivalence]] between the fixed subcategories on either side. \begin{defn} \label{}\hypertarget{}{} A [[topological space]] $X$ with $X \cong X_{L P}$ is called \textbf{[[sober space|sober]]}. A locale with $X \cong X_{P L}$ is called \textbf{[[spatial locale|spatial]]} or \textbf{topological}; one also says that it has \textbf{enough points}. \end{defn} see also MO \href{http://math.stackexchange.com/a/1904289/58526}{here} \begin{cor} \label{}\hypertarget{}{} The [[adjunction]] from prop. \ref{TopLocAdjunction} exhibits [[sober topological spaces]] as a [[coreflective subcategory]] of [[Locale]] \begin{displaymath} ( (-)_L \dashv (-)_P ) \colon SoberTop \underoverset {\underset{(-)_P}{\leftarrow}} {\overset{(-)_L}{\hookrightarrow}} {\bot} Locale \end{displaymath} and this restricts to an [[equivalence of categories]] between the [[full subcategory]] of locales with enough points, and that of [[sober topological spaces]]. \end{cor} This appears for instance as (\hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, corollary IX.3 4}). Consequently, we often identify a sober topological space and the corresponding topological locale. \hypertarget{RelationToToposes}{}\subsubsection*{{Relation to toposes -- localic reflection}}\label{RelationToToposes} The notion of [[Grothendieck topos]] can be seen as a [[categorification]] of the notion of locale, by relating both notions to the notion of [[total category|lex totality]]: \begin{prop} \label{}\hypertarget{}{} A [[poset]] $P$ is a [[frame]] if and only if the [[Yoneda embedding]] \begin{displaymath} y \colon P \to \mathbf{2}^{P^{op}} \end{displaymath} has a [[exact functor|left exact]] [[left adjoint]]. (Here the poset $\mathbf{2}$ of [[truth values]] is the base of enrichment for posets seen as [[enriched categories]].) \end{prop} 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 \emph{[[Categories for the Working Mathematician]]}, call a category \emph{[[moderate category|moderate]]} if its set of morphisms has size $\kappa$. For example, $Set$ is moderate. \begin{prop} \label{}\hypertarget{}{} (\hyperlink{Street}{Street}) A moderate [[locally small category]] $C$ is a [[Grothendieck topos]] if and only if the [[Yoneda embedding]] \begin{displaymath} y \colon C \to Set^{C^{op}} \end{displaymath} has a [[left exact functor|left exact]] [[left adjoint]]. \end{prop} These results emphasize frames/toposes as algebras, where the morphisms are left exact left adjoints. The [[right adjoints]] to such morphisms are called [[geometric morphism|geometric morphisms]], and emphasize locales/toposes as [[spaces]]. This analogy, which plays an important but mostly tacit role in \hyperlink{JT}{Joyal and Tierney}, can be developed further along the following lines. The [[frame of opens]] $O(X)$ corresponding to a locale $X$ is naturally a [[site]]: \begin{defn} \label{}\hypertarget{}{} Given a locale $X$, with [[frame of opens]] $O(X)$, say that a family of [[morphisms]] $\{U_i \to U\}$ in $O(X)$ is a [[cover]] if $U$ is the [[join]] of the $U_i$: \begin{displaymath} U = \vee_i U_i \,. \end{displaymath} \end{defn} \begin{prop} \label{}\hypertarget{}{} This defines a [[coverage]] on $O(X)$ and hence makes it a [[site]]. \end{prop} See for instance (\hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, section 5}). \begin{defn} \label{}\hypertarget{}{} For $X$ a locale, write \begin{displaymath} Sh(X) \coloneqq Sh(O(X)) \end{displaymath} for the [[sheaf topos]] over the category $O(X)$ equipped with the above canonical structure of a [[site]]. \end{defn} Write [[Topos]] for the category of [[Grothendieck toposes]] and [[geometric morphisms]]. \begin{prop} \label{}\hypertarget{}{} This construction defines a [[full and faithful functor]] $Sh(-) :$ [[Locale]] $\to$ [[Topos]]. \end{prop} This appears for instance as \hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, section IX.5 prop 2}. \begin{defn} \label{}\hypertarget{}{} A topos in the [[image]] of $Sh(-)\colon Locale \to Topos$ is called a \emph{[[localic topos]]}. \end{defn} \begin{prop} \label{}\hypertarget{}{} The functor $Sh(-)\colon Locale \to Topos$ has a [[left adjoint]] \begin{displaymath} L\colon Topos \to Locale \end{displaymath} 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}$: \begin{displaymath} O(L(\mathcal{E})) \coloneqq Sub_{\mathcal{E}}(*) \,. \end{displaymath} \end{prop} This appears for instance as \hyperlink{MacLaneMoerdijk}{MacLaneMoerdijk, section IX.5 prop 3}. The functor $L$ here is also called \textbf{localic reflection}. In summary this means that locales form a [[reflective subcategory]] of [[Topos]]: \begin{displaymath} Locale \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow} Topos \,. \end{displaymath} In fact this is even a genuine [[full sub-2-category]]: \begin{prop} \label{}\hypertarget{}{} For all $X,Y \in$ [[Locale]] the [[2-functor]] $Sh\colon$ [[Locale]] $\to$ [[Topos]] induces an [[equivalence of categories]] \begin{displaymath} Sh\colon Locale(X,Y) \stackrel{\simeq}{\to} Topos(Sh(X), Sh(Y)) \,. \end{displaymath} \end{prop} This appears as (\hyperlink{Johnstone}{Johnstone, prop. C1.4.5}). \begin{prop} \label{}\hypertarget{}{} The [[poset of subobjects]] $Sub_{\mathcal{E}}(*)$ of the terminal object of $\mathcal{E}$ is equivalent to the full [[subcategory]] $\tau_{\leq -1}(\mathcal{E})$ of $\mathcal{E}$ on the $(-1)$-[[truncated]] objects of $E$: \begin{displaymath} Sub_{\mathcal{E}}(*) \simeq \tau_{\leq -1} \mathcal{E} \,. \end{displaymath} \end{prop} \begin{proof} A [[(-1)-truncated]] sheaf $X$ is one whose values over any object are either the [[(-2)-groupoid|singleton set]], or the [[empty set]] \begin{displaymath} X(X) \in \{*, \emptyset\} = \subset Set \,. \end{displaymath} A [[monomorphism]] of [[sheaves]] is a [[natural transformation]] that is degreewise a monomorphism of sets (an [[injection]]). Therefore the [[subobjects]] of the [[terminal object|terminal]] sheaf (that assigns the singleton set to every object) are precisely the sheaves of this form. \end{proof} We may think of a [[frame]] as a [[Grothendieck (0,1)-topos]]. Then localic reflection is reflection of [[Grothendieck toposes]] onto $(0,1)$-toposes and is given by $(-1)$-truncation: for $X$ a locale, $Sh(X)$ the corresponding [[localic topos]] and $\mathcal{E}$ any Grothendieck topos we have a natural equivalence \begin{displaymath} Gr1Topos( \mathcal{E}, Sh X) \simeq Gr(0,1)Topos(\tau_{\leq -1} \mathcal{E}, O(X)) \end{displaymath} which is \begin{displaymath} \cdots \simeq Frame(O(X), Sub_{\mathcal{E}}(*)) \simeq Locale(L \mathcal{E} , X) \,. \end{displaymath} This is a small part of a pattern in [[higher topos theory]], described at [[n-localic (∞,1)-topos]]. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item [[the locale of real numbers]] \item [[Cantor space]] \end{itemize} \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item The notion of locale may be identified with that of a [[Grothendieck topos|Grothendieck]] [[(0,1)-topos]]. See [[Heyting algebra]] for more on this. \item An [[ionad]] is to a [[topological space]] as a [[Grothendieck topos]] is to a [[locale]]. \item A [[group object]] [[internalization|internal]] to locales or an [[internal groupoid]] in locales is a [[localic group]] or [[localic groupoid]], respectively. \end{itemize} There is also a notion of [[internal locale]], see also [[internal site]]. \begin{itemize}% \item [[topological space]], [[topological locale]] \item [[ionad]] \item [[topos]] \item [[profinite space]], [[profinite reflection]] \item [[localic homotopy theory]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} An introduction to and survey of the use of locales instead of topological spaces (``[[point-free topology]]'') is in \begin{itemize}% \item [[Peter Johnstone]], \emph{The point of pointless topology} , Bull. Amer. Math. Soc. (N.S.) Volume 8, Number 1 (1983), 41-53. (\href{http://www.ams.org/bull/1983-08-01/S0273-0979-1983-15080-2/home.html}{Bulletin AMS}, \href{http://projecteuclid.org/euclid.bams/1183550014}{Euclid}) \end{itemize} This is, in its own words, to be read as the trailer for the book \begin{itemize}% \item [[Peter Johnstone]], \emph{[[Stone Spaces]]}, Cambridge Studies in Advanced Mathematics \textbf{3}, Cambridge University Press 1982. xxi+370 pp. \href{http://www.ams.org/mathscinet-getitem?mr=698074}{MR85f:54002}, reprinted 1986. \end{itemize} that develops, among other things, much of standard [[topology]] entirely with the notion of locale used in place of that of [[topological space]]s. See [[Stone Spaces]] for details. Other textbook accounts include \begin{itemize}% \item [[Francis Borceux]], volume 3, chapter 1 of \emph{[[Handbook of Categorical Algebra]]}, \item [[Peter Johnstone]], part C (volume 2) \emph{[[Elephant|Sketches of an elephant: a topos theory compendium]]}. \item [[Saunders MacLane]], [[Ieke Moerdijk]], \emph{[[Sheaves in Geometry and Logic]]} \item Jorge Picado \& Aleš Pultr (2012). \emph{Frames and Locales: Topology without points}. Springer. \href{http://www.mat.uc.pt/%7Epicado/publicat/bookpage.html}{Web page} (with preface, contents, and errata). \end{itemize} and \begin{itemize}% \item [[Steve Vickers]], \emph{Topology via logic}, Cambridge University Press (1989) \end{itemize} where the latter develops topology from the point of view of its [[internal logic]]. An introductory survey is \begin{itemize}% \item Jorge Picado, Ale\v{s} Pultr, Anna Tozzi, \emph{Locales} , pp.49-101 in Pedicchio\&Tholen (eds.), \emph{Categorical Foundations} , CUP 2004. (\href{http://www.mat.uc.pt/~picado/publicat/Chapter2.pdf}{draft}) \end{itemize} See also \begin{itemize}% \item [[eom]], \emph{\href{https://www.encyclopediaofmath.org/index.php/Locale}{Locale}} \end{itemize} Lex totality is the subject of an article of Street, \begin{itemize}% \item [[Ross Street]], \emph{Notions of Topos}, Bull. Australian Math. Soc. 23 (1981), 199-208. \end{itemize} The connection between locales and toposes via lex totality plays a tacit role throughout the influential monograph \begin{itemize}% \item [[André Joyal]] and [[Myles Tierney]], \emph{An Extension of the Galois Theory of Grothendieck}, Memoirs of the American Mathematical Society 51 (1984). \end{itemize} [[!redirects locale]] [[!redirects locales]] [[!redirects internal locale]] [[!redirects internal locales]] [[!redirects localic reflection]] [[!redirects localic reflections]] [[!redirects locale theory]] \end{document}