CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> locale in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> locale </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/2341/#Item_44" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="topos_theory">Topos Theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a></strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Toposes">Toposes</a></li> </ul> <h2 id="background">Background</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> </ul> </li> </ul> <h2 id="toposes">Toposes</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+presheaves">category of presheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable presheaf</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/site">site</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sieve">sieve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/coverage">coverage</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+pretopology">pretopology</a>, <a class="existingWikiWord" href="/nlab/show/Grothendieck+topology">topology</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheafification">sheafification</a></p> </li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quasitopos">quasitopos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+topos">base topos</a>, <a class="existingWikiWord" href="/nlab/show/indexed+topos">indexed topos</a></p> </li> </ul> <h2 id="toc_internal_logic">Internal Logic</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a></p> </li> </ul> </li> </ul> <h2 id="topos_morphisms">Topos morphisms</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/logical+morphism">logical morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/direct+image">direct image</a>/<a class="existingWikiWord" href="/nlab/show/inverse+image">inverse image</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/global+section">global sections</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/surjective+geometric+morphism">surjective geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/essential+geometric+morphism">essential geometric morphism</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+geometric+morphism">locally connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected+geometric+morphism">connected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/totally+connected+geometric+morphism">totally connected geometric morphism</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%C3%A9tale+geometric+morphism">étale geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+geometric+morphism">open geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proper+geometric+morphism">proper geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/compact+topos">compact topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/separated+geometric+morphism">separated geometric morphism</a>, <a class="existingWikiWord" href="/nlab/show/Hausdorff+topos">Hausdorff topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+geometric+morphism">local geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bounded+geometric+morphism">bounded geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+change">base change</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+geometric+morphism">localic geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperconnected+geometric+morphism">hyperconnected geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/atomic+geometric+morphism">atomic geometric morphism</a></p> </li> </ul> </li> </ul> <h2 id="extra_stuff_structure_properties">Extra stuff, structure, properties</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+locale">topological locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+topos">localic topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/petit+topos">petit topos/gros topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+connected+topos">locally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/connected+topos">connected topos</a>, <a class="existingWikiWord" href="/nlab/show/totally+connected+topos">totally connected topos</a>, <a class="existingWikiWord" href="/nlab/show/strongly+connected+topos">strongly connected topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+topos">local topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+topos">cohesive topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/smooth+topos">smooth topos</a></p> </li> </ul> <h2 id="cohomology_and_homotopy">Cohomology and homotopy</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+groups+in+an+%28infinity%2C1%29-topos">homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/abelian+sheaf+cohomology">abelian sheaf cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+structure+on+simplicial+presheaves">model structure on simplicial presheaves</a></p> </li> </ul> <h2 id="in_higher_category_theory">In higher category theory</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-site">(0,1)-site</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-topos">2-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2-site">2-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-sheaf">2-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/stack">stack</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-site">(∞,1)-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf">(∞,1)-sheaf</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stack">∞-stack</a>, <a class="existingWikiWord" href="/nlab/show/derived+stack">derived stack</a></p> </li> </ul> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Diaconescu%27s+theorem">Diaconescu's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Barr%27s+theorem">Barr's theorem</a></p> </li> </ul> <div> <p> <a href="/nlab/edit/topos+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="topology">Topology</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/topology">topology</a></strong> (<a class="existingWikiWord" href="/nlab/show/point-set+topology">point-set topology</a>, <a class="existingWikiWord" href="/nlab/show/point-free+topology">point-free topology</a>)</p> <p>see also <em><a class="existingWikiWord" href="/nlab/show/differential+topology">differential topology</a></em>, <em><a class="existingWikiWord" href="/nlab/show/algebraic+topology">algebraic topology</a></em>, <em><a class="existingWikiWord" href="/nlab/show/functional+analysis">functional analysis</a></em> and <em><a class="existingWikiWord" href="/nlab/show/topological+homotopy+theory">topological</a> <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a></em></p> <p><a class="existingWikiWord" href="/nlab/show/Introduction+to+Topology">Introduction</a></p> <p><strong>Basic concepts</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/open+subset">open subset</a>, <a class="existingWikiWord" href="/nlab/show/closed+subset">closed subset</a>, <a class="existingWikiWord" href="/nlab/show/neighbourhood">neighbourhood</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/base+for+the+topology">base for the topology</a>, <a class="existingWikiWord" href="/nlab/show/neighbourhood+base">neighbourhood base</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/finer+topology">finer/coarser topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+closure">closure</a>, <a class="existingWikiWord" href="/nlab/show/topological+interior">interior</a>, <a class="existingWikiWord" href="/nlab/show/topological+boundary">boundary</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/separation+axiom">separation</a>, <a class="existingWikiWord" href="/nlab/show/sober+topological+space">sobriety</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/continuous+function">continuous function</a>, <a class="existingWikiWord" href="/nlab/show/homeomorphism">homeomorphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/uniformly+continuous+function">uniformly continuous function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+embedding">embedding</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+map">open map</a>, <a class="existingWikiWord" href="/nlab/show/closed+map">closed map</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sequence">sequence</a>, <a class="existingWikiWord" href="/nlab/show/net">net</a>, <a class="existingWikiWord" href="/nlab/show/sub-net">sub-net</a>, <a class="existingWikiWord" href="/nlab/show/filter">filter</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/convergence">convergence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a><a class="existingWikiWord" href="/nlab/show/Top">Top</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/convenient+category+of+topological+spaces">convenient category of topological spaces</a></li> </ul> </li> </ul> <p><strong><a href="Top#UniversalConstructions">Universal constructions</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/initial+topology">initial topology</a>, <a class="existingWikiWord" href="/nlab/show/final+topology">final topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/subspace">subspace</a>, <a class="existingWikiWord" href="/nlab/show/quotient+space">quotient space</a>,</p> </li> <li> <p>fiber space, <a class="existingWikiWord" href="/nlab/show/space+attachment">space attachment</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/product+space">product space</a>, <a class="existingWikiWord" href="/nlab/show/disjoint+union+space">disjoint union space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cylinder">mapping cylinder</a>, <a class="existingWikiWord" href="/nlab/show/mapping+cocylinder">mapping cocylinder</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cone">mapping cone</a>, <a class="existingWikiWord" href="/nlab/show/mapping+cocone">mapping cocone</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+telescope">mapping telescope</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/colimits+of+normal+spaces">colimits of normal spaces</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/stuff%2C+structure%2C+property">Extra stuff, structure, properties</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/nice+topological+space">nice topological space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/metric+space">metric space</a>, <a class="existingWikiWord" href="/nlab/show/metric+topology">metric topology</a>, <a class="existingWikiWord" href="/nlab/show/metrisable+space">metrisable space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kolmogorov+space">Kolmogorov space</a>, <a class="existingWikiWord" href="/nlab/show/Hausdorff+space">Hausdorff space</a>, <a class="existingWikiWord" href="/nlab/show/regular+space">regular space</a>, <a class="existingWikiWord" href="/nlab/show/normal+space">normal space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sober+space">sober space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+space">compact space</a>, <a class="existingWikiWord" href="/nlab/show/proper+map">proper map</a></p> <p><a class="existingWikiWord" href="/nlab/show/sequentially+compact+topological+space">sequentially compact</a>, <a class="existingWikiWord" href="/nlab/show/countably+compact+topological+space">countably compact</a>, <a class="existingWikiWord" href="/nlab/show/locally+compact+topological+space">locally compact</a>, <a class="existingWikiWord" href="/nlab/show/sigma-compact+topological+space">sigma-compact</a>, <a class="existingWikiWord" href="/nlab/show/paracompact+space">paracompact</a>, <a class="existingWikiWord" href="/nlab/show/countably+paracompact+topological+space">countably paracompact</a>, <a class="existingWikiWord" href="/nlab/show/strongly+compact+topological+space">strongly compact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compactly+generated+space">compactly generated space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/second-countable+space">second-countable space</a>, <a class="existingWikiWord" href="/nlab/show/first-countable+space">first-countable space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/contractible+space">contractible space</a>, <a class="existingWikiWord" href="/nlab/show/locally+contractible+space">locally contractible space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected+space">connected space</a>, <a class="existingWikiWord" href="/nlab/show/locally+connected+space">locally connected space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/simply-connected+space">simply-connected space</a>, <a class="existingWikiWord" href="/nlab/show/locally+simply-connected+space">locally simply-connected space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cell+complex">cell complex</a>, <a class="existingWikiWord" href="/nlab/show/CW-complex">CW-complex</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/pointed+topological+space">pointed space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+vector+space">topological vector space</a>, <a class="existingWikiWord" href="/nlab/show/Banach+space">Banach space</a>, <a class="existingWikiWord" href="/nlab/show/Hilbert+space">Hilbert space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+group">topological group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+vector+bundle">topological vector bundle</a>, <a class="existingWikiWord" href="/nlab/show/topological+K-theory">topological K-theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+manifold">topological manifold</a></p> </li> </ul> <p><strong>Examples</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/empty+space">empty space</a>, <a class="existingWikiWord" href="/nlab/show/point+space">point space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/discrete+space">discrete space</a>, <a class="existingWikiWord" href="/nlab/show/codiscrete+space">codiscrete space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Sierpinski+space">Sierpinski space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/order+topology">order topology</a>, <a class="existingWikiWord" href="/nlab/show/specialization+topology">specialization topology</a>, <a class="existingWikiWord" href="/nlab/show/Scott+topology">Scott topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Euclidean+space">Euclidean space</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/real+line">real line</a>, <a class="existingWikiWord" href="/nlab/show/plane">plane</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cylinder">cylinder</a>, <a class="existingWikiWord" href="/nlab/show/cone">cone</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sphere">sphere</a>, <a class="existingWikiWord" href="/nlab/show/ball">ball</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/circle">circle</a>, <a class="existingWikiWord" href="/nlab/show/torus">torus</a>, <a class="existingWikiWord" href="/nlab/show/annulus">annulus</a>, <a class="existingWikiWord" href="/nlab/show/Moebius+strip">Moebius strip</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/polytope">polytope</a>, <a class="existingWikiWord" href="/nlab/show/polyhedron">polyhedron</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/projective+space">projective space</a> (<a class="existingWikiWord" href="/nlab/show/real+projective+space">real</a>, <a class="existingWikiWord" href="/nlab/show/complex+projective+space">complex</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classifying+space">classifying space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/configuration+space+%28mathematics%29">configuration space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/path">path</a>, <a class="existingWikiWord" href="/nlab/show/loop">loop</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+spaces">mapping spaces</a>: <a class="existingWikiWord" href="/nlab/show/compact-open+topology">compact-open topology</a>, <a class="existingWikiWord" href="/nlab/show/topology+of+uniform+convergence">topology of uniform convergence</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/loop+space">loop space</a>, <a class="existingWikiWord" href="/nlab/show/path+space">path space</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Zariski+topology">Zariski topology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cantor+space">Cantor space</a>, <a class="existingWikiWord" href="/nlab/show/Mandelbrot+space">Mandelbrot space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Peano+curve">Peano curve</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/line+with+two+origins">line with two origins</a>, <a class="existingWikiWord" href="/nlab/show/long+line">long line</a>, <a class="existingWikiWord" href="/nlab/show/Sorgenfrey+line">Sorgenfrey line</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/K-topology">K-topology</a>, <a class="existingWikiWord" href="/nlab/show/Dowker+space">Dowker space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Warsaw+circle">Warsaw circle</a>, <a class="existingWikiWord" href="/nlab/show/Hawaiian+earring+space">Hawaiian earring space</a></p> </li> </ul> <p><strong>Basic statements</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Hausdorff+spaces+are+sober">Hausdorff spaces are sober</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/schemes+are+sober">schemes are sober</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/continuous+images+of+compact+spaces+are+compact">continuous images of compact spaces are compact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+subspaces+of+compact+Hausdorff+spaces+are+equivalently+compact+subspaces">closed subspaces of compact Hausdorff spaces are equivalently compact subspaces</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/open+subspaces+of+compact+Hausdorff+spaces+are+locally+compact">open subspaces of compact Hausdorff spaces are locally compact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quotient+projections+out+of+compact+Hausdorff+spaces+are+closed+precisely+if+the+codomain+is+Hausdorff">quotient projections out of compact Hausdorff spaces are closed precisely if the codomain is Hausdorff</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+spaces+equivalently+have+converging+subnet+of+every+net">compact spaces equivalently have converging subnet of every net</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Lebesgue+number+lemma">Lebesgue number lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sequentially+compact+metric+spaces+are+equivalently+compact+metric+spaces">sequentially compact metric spaces are equivalently compact metric spaces</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+spaces+equivalently+have+converging+subnet+of+every+net">compact spaces equivalently have converging subnet of every net</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sequentially+compact+metric+spaces+are+totally+bounded">sequentially compact metric spaces are totally bounded</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/continuous+metric+space+valued+function+on+compact+metric+space+is+uniformly+continuous">continuous metric space valued function on compact metric space is uniformly continuous</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/paracompact+Hausdorff+spaces+are+normal">paracompact Hausdorff spaces are normal</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/paracompact+Hausdorff+spaces+equivalently+admit+subordinate+partitions+of+unity">paracompact Hausdorff spaces equivalently admit subordinate partitions of unity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/closed+injections+are+embeddings">closed injections are embeddings</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proper+maps+to+locally+compact+spaces+are+closed">proper maps to locally compact spaces are closed</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/injective+proper+maps+to+locally+compact+spaces+are+equivalently+the+closed+embeddings">injective proper maps to locally compact spaces are equivalently the closed embeddings</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+compact+and+sigma-compact+spaces+are+paracompact">locally compact and sigma-compact spaces are paracompact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+compact+and+second-countable+spaces+are+sigma-compact">locally compact and second-countable spaces are sigma-compact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/second-countable+regular+spaces+are+paracompact">second-countable regular spaces are paracompact</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/CW-complexes+are+paracompact+Hausdorff+spaces">CW-complexes are paracompact Hausdorff spaces</a></p> </li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Urysohn%27s+lemma">Urysohn's lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tietze+extension+theorem">Tietze extension theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tychonoff+theorem">Tychonoff theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/tube+lemma">tube lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Michael%27s+theorem">Michael's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Brouwer%27s+fixed+point+theorem">Brouwer's fixed point theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+invariance+of+dimension">topological invariance of dimension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Jordan+curve+theorem">Jordan curve theorem</a></p> </li> </ul> <p><strong>Analysis Theorems</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Heine-Borel+theorem">Heine-Borel theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/intermediate+value+theorem">intermediate value theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extreme+value+theorem">extreme value theorem</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/topological+homotopy+theory">topological homotopy theory</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/left+homotopy">left homotopy</a>, <a class="existingWikiWord" href="/nlab/show/right+homotopy">right homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+equivalence">homotopy equivalence</a>, <a class="existingWikiWord" href="/nlab/show/deformation+retract">deformation retract</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+group">fundamental group</a>, <a class="existingWikiWord" href="/nlab/show/covering+space">covering space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+theorem+of+covering+spaces">fundamental theorem of covering spaces</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+group">homotopy group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weak+homotopy+equivalence">weak homotopy equivalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+theorem">Whitehead's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freudenthal+suspension+theorem">Freudenthal suspension theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/nerve+theorem">nerve theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+extension+property">homotopy extension property</a>, <a class="existingWikiWord" href="/nlab/show/Hurewicz+cofibration">Hurewicz cofibration</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+cofiber+sequence">cofiber sequence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Str%C3%B8m+model+category">Strøm model category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/classical+model+structure+on+topological+spaces">classical model structure on topological spaces</a></p> </li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea_and_motivation'>Idea and motivation</a></li> <li><a href='#definitions'>Definitions</a></li> <li><a href='#Subsidiaries'>Subsidiary notions</a></li> <ul> <li><a href='#open_and_closed_subspaces'>Open and closed subspaces</a></li> <li><a href='#points'>Points</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#CategoryOfLocales'>Categories of internal locales</a></li> <li><a href='#RelationToTopologicalSpaces'>Relation to topological spaces</a></li> <li><a href='#RelationToToposes'>Relation to toposes – localic reflection</a></li> </ul> <li><a href='#Examples'>Examples</a></li> <ul> <li><a href='#general_topology'>General topology</a></li> <li><a href='#ExamplesMeasureTheory'>Measure theory</a></li> <li><a href='#intersections_of_dense_sublocales'>Intersections of dense sublocales</a></li> </ul> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea_and_motivation">Idea and motivation</h2> <p>Locale theory is one particular formulation of <a class="existingWikiWord" href="/nlab/show/point-free+topology">point-free topology</a>.</p> <p>A <em>locale</em> is, intuitively, like a <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> that may or may not have enough <a class="existingWikiWord" href="/nlab/show/points">points</a> (or even any points at all). It contains things we call <a class="existingWikiWord" href="/nlab/show/open+subspaces">open subspaces</a> 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.</p> <p>For example, there is a locale of all <a class="existingWikiWord" href="/nlab/show/surjections">surjections</a> from <a class="existingWikiWord" href="/nlab/show/natural+numbers">natural numbers</a> (thought of as forming the <a class="existingWikiWord" href="/nlab/show/discrete+space">discrete space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>N</mi></mrow><annotation encoding="application/x-tex">N</annotation></semantics></math>) to <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a> (forming the <a class="existingWikiWord" href="/nlab/show/real+line">real line</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math>, the <em><a class="existingWikiWord" href="/nlab/show/locale+of+real+numbers">locale of real numbers</a></em>). 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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo lspace="verythinmathspace">:</mo><mi>N</mi></mrow><annotation encoding="application/x-tex">n\colon N</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>R</mi></mrow><annotation encoding="application/x-tex">x\colon R</annotation></semantics></math>; the basic open associated to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> may be described as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>N</mi><mo>↠</mo><mi>R</mi><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{f\colon N \twoheadrightarrow R \;|\; f(n) = x\}</annotation></semantics></math>. Together with relations internalizing the statements ‘<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mspace width="thinmathspace"></mspace><mi>n</mi><mo>,</mo><mspace width="thickmathspace"></mspace><mo>∃</mo><mo>!</mo><mspace width="thinmathspace"></mspace><mi>x</mi><mo>,</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">\forall\, n,\; \exists!\, x,\; f(n) = x</annotation></semantics></math>’ and ‘<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mspace width="thinmathspace"></mspace><mi>x</mi><mo>,</mo><mspace width="thickmathspace"></mspace><mo>∃</mo><mspace width="thinmathspace"></mspace><mi>n</mi><mo>,</mo><mspace width="thickmathspace"></mspace><mi>f</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mi>x</mi></mrow><annotation encoding="application/x-tex">\forall\, x,\; \exists\, n,\; f(n) = x</annotation></semantics></math>’, 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 <a class="existingWikiWord" href="/nlab/show/Elephant">Elephant</a>.)</p> <p>Every topological space can be regarded as a locale (with some lost information if the space is not <a class="existingWikiWord" href="/nlab/show/sober+space">sober</a>). The locales arising this way are the <em><a class="existingWikiWord" href="/nlab/show/topological+locale">topological</a></em> or <em>spatial</em> 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 <a class="existingWikiWord" href="/nlab/show/empty+set">empty</a>.</p> <p>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 <a class="existingWikiWord" href="/nlab/show/sheaves">sheaves</a>. 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 <a class="existingWikiWord" href="/nlab/show/toposes">toposes</a> of sheaves is a <a class="existingWikiWord" href="/nlab/show/full+and+faithful+functor">full and faithful functor</a>, unlike for topological spaces.</p> <p>Another advantage of locales is that they are better-behaved than topological spaces in alternative <a class="existingWikiWord" href="/nlab/show/foundations+of+mathematics">foundations of mathematics</a>, including mathematics without the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, more generally <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, or mathematics <a class="existingWikiWord" href="/nlab/show/internalization">internal</a> to an arbitrary <a class="existingWikiWord" href="/nlab/show/topos">topos</a>. For example, constructively the topological space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[0,1]</annotation></semantics></math> need not be <a class="existingWikiWord" href="/nlab/show/compact+space">compact</a>, but the <em>locale</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[0,1]</annotation></semantics></math> is always compact (in a suitable sense). It follows that the locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[0,1]</annotation></semantics></math>, and hence also the locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>R</mi></mrow><annotation encoding="application/x-tex">R</annotation></semantics></math> 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.</p> <h2 id="definitions">Definitions</h2> <p>Recall that a <strong><a class="existingWikiWord" href="/nlab/show/frame">frame</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/partial+order">poset</a> with all <a class="existingWikiWord" href="/nlab/show/join">joins</a> and all finite <a class="existingWikiWord" href="/nlab/show/meet">meets</a> which satisfies the <em>infinite distributive law</em>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∧</mo><mo stretchy="false">(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>i</mi></munder><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo><mo>=</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>i</mi></munder><mo stretchy="false">(</mo><mi>x</mi><mo>∧</mo><msub><mi>y</mi> <mi>i</mi></msub><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> x \wedge (\bigvee_i y_i) = \bigvee_i (x\wedge y_i) .</annotation></semantics></math></div> <p>A <strong>frame <a class="existingWikiWord" href="/nlab/show/homomorphism">homomorphism</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">\phi\colon A\to B</annotation></semantics></math> is a function which preserves finite meets and arbitrary joins. Frames and frame homomorphisms form a <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Frm">Frm</a>.</p> <p>Note: By the <a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a> (AFT) for posets, a frame also has all meets (at least assuming that it is a <a class="existingWikiWord" href="/nlab/show/small+set">small set</a>, or more generally that we allow <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">impredicative quantification</a> over it), but a frame homomorphism need not preserve them. Similarly, by the AFT, a frame is automatically a <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a>, but again a frame homomorphism need not preserve the <a class="existingWikiWord" href="/nlab/show/Heyting+implication">Heyting implication</a>.</p> <p>By definition, the <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a> of <strong>locales</strong> is the <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite</a> of the category of frames</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Locale</mi><mo>≔</mo><msup><mi>Frm</mi> <mi>op</mi></msup><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Locale \coloneqq Frm^{op} \,. </annotation></semantics></math></div> <p>That is, a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> “is” a frame, which we often write as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> and call “the frame of open subspaces of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>”, and a <strong><a class="existingWikiWord" href="/nlab/show/continuous+map">continuous map</a></strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f\colon X \to Y</annotation></semantics></math> of locales is a frame homomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*\colon O(Y) \to O(X)</annotation></semantics></math>. If you think of a frame as an algebraic structure (a <a class="existingWikiWord" href="/nlab/show/lattice">lattice</a> satisfying a completeness condition), then this is an example of the <a class="existingWikiWord" href="/nlab/show/duality">duality</a> of <a class="existingWikiWord" href="/nlab/show/space+and+quantity">space and quantity</a>.</p> <p>It is also possible to think of a continuous map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f\colon X \to Y</annotation></semantics></math> as a map of <a class="existingWikiWord" href="/nlab/show/posets">posets</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_*\colon O(X) \to O(Y)</annotation></semantics></math>: a <a class="existingWikiWord" href="/nlab/show/function">function</a> that preserves all <a class="existingWikiWord" href="/nlab/show/meets">meets</a> (and therefore is <a class="existingWikiWord" href="/nlab/show/monotone+function">monotone</a> and has a <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*\colon O(Y) \to O(X)</annotation></semantics></math>) and such that the left adjoint <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">f^*</annotation></semantics></math> preserves all finite meets. This has the arrow pointing in the “right” direction, at the cost of a less direct definition. (In <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative mathematics</a>, we would have to explicitly add into this definition that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub></mrow><annotation encoding="application/x-tex">f_*</annotation></semantics></math> has a left adjoint; although since few locales even exist predicatively, we usually turn attention to <a class="existingWikiWord" href="/nlab/show/base+of+a+locale">bases</a> of locales anyway.)</p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>The map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo>:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_\ast: O(X) \to O(Y)</annotation></semantics></math> is of course <em>not</em> the “direct image” along <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math>, rather it is a kind of dual to direct image, taking an open <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi><mo>∈</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">u \in O(X)</annotation></semantics></math> to the join</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>v</mi><mo>∈</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>:</mo><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>v</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>u</mi></mrow></munder><mi>v</mi></mrow><annotation encoding="application/x-tex">\bigvee_{v \in O(Y): f^\ast(v) \leq u} v</annotation></semantics></math></div> <p>For <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a> in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, denoting the <a class="existingWikiWord" href="/nlab/show/complementation">complementation</a> operator by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>¬</mo></mrow><annotation encoding="application/x-tex">\neg</annotation></semantics></math> and the <a class="existingWikiWord" href="/nlab/show/interior">interior</a> operator by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>int</mi></mrow><annotation encoding="application/x-tex">int</annotation></semantics></math>, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo stretchy="false">(</mo><mi>u</mi><mo stretchy="false">)</mo><mo>=</mo><mi>int</mi><mo stretchy="false">(</mo><mo>¬</mo><mi>f</mi><mo stretchy="false">(</mo><mo>¬</mo><mi>u</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_\ast(u) = int(\neg f(\neg u))</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> on the right denotes the ordinary set-theoretic direct image.</p> <p>Alternatively, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo stretchy="false">(</mo><mi>u</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_*(u)</annotation></semantics></math> can also be described as the largest open subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> whose preimage in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>u</mi></mrow><annotation encoding="application/x-tex">u</annotation></semantics></math>.</p> </div> <p>The category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Locale</mi></mrow><annotation encoding="application/x-tex">Locale</annotation></semantics></math> is naturally enhanced to a <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a>:</p> <div class="num_defn"> <h6 id="definition">Definition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a> has</p> <ul> <li> <p>as <a class="existingWikiWord" href="/nlab/show/objects">objects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/frames">frames</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>;</p> </li> <li> <p>as <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f\colon X \to Y</annotation></semantics></math> frame homomorphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*\colon O(Y) \to O(X)</annotation></semantics></math>;</p> </li> <li> <p>a unique <a class="existingWikiWord" href="/nlab/show/2-morphism">2-morphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>⇒</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f \Rightarrow g</annotation></semantics></math> whenever for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>∈</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">U \in O(Y)</annotation></semantics></math> we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>U</mi><mo stretchy="false">)</mo><mo>≤</mo><msup><mi>g</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>U</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*(U) \leq g^*(U)</annotation></semantics></math>.</p> </li> </ul> </div> <p>(See for instance <a href="#Johnstone">Johnstone, C1.4, p. 514</a>.)</p> <p>Since <a class="existingWikiWord" href="/nlab/show/parallel+morphisms">parallel</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-morphisms are equal, this <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> is in fact a <a class="existingWikiWord" href="/nlab/show/%281%2C2%29-category">(1,2)-category</a>: a <a class="existingWikiWord" href="/nlab/show/Poset">Poset</a>-<a class="existingWikiWord" href="/nlab/show/enriched+category">enriched category</a>.</p> <h2 id="Subsidiaries">Subsidiary notions</h2> <h3 id="open_and_closed_subspaces">Open and closed subspaces</h3> <p>Given a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, the elements of the frame <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> are traditionally thought of as being the <a class="existingWikiWord" href="/nlab/show/open+subspaces">open subspaces</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> and are therefore called the <strong>opens</strong> (or <strong>open subspaces</strong>, <strong>open parts</strong>, or <strong>open sublocales</strong>) of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>. However, one may equally well view them as the <a class="existingWikiWord" href="/nlab/show/closed+subspaces">closed subspaces</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> and call them the <strong>closeds</strong> (or <strong>closed subspaces</strong>, <strong>closed parts</strong>, or <strong>closed sublocales</strong>) of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>. When viewed as closed subspaces, the <a class="existingWikiWord" href="/nlab/show/opposite+relation">opposite</a> containment relation is used; thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> is the <strong>frame of opens</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, while the <a class="existingWikiWord" href="/nlab/show/opposite+poset">opposite poset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><msup><mo stretchy="false">)</mo> <mi>op</mi></msup></mrow><annotation encoding="application/x-tex">O(X)^{op}</annotation></semantics></math> is the <strong><a class="existingWikiWord" href="/nlab/show/coframe">coframe</a> of closeds</strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>.</p> <p>An open subspace may be thought of as a potentially <em>verifiable</em> property of a hypothetical point of the space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>. Thus we may verify the <a class="existingWikiWord" href="/nlab/show/intersection">intersection</a> of two open subspaces by verifying both properties, and we may verify the <a class="existingWikiWord" href="/nlab/show/union">union</a> 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 <a class="existingWikiWord" href="/nlab/show/meet">meet</a> 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.)</p> <p><a class="existingWikiWord" href="/nlab/show/de+Morgan+duality">Dually</a>, a closed subspace may be thought of as a potentially <em>refutable</em> 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 <a class="existingWikiWord" href="/nlab/show/join">join</a> of an arbitrary family of closed subspaces does not work right.)</p> <p>If one views an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> as a <a class="existingWikiWord" href="/nlab/show/subspace">subspace</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, 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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> to the lattice of all subspaces of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>. See <a class="existingWikiWord" href="/nlab/show/sublocale">sublocale</a> for further discussion.</p> <h3 id="points">Points</h3> <p>As a locale, the <strong>abstract <a class="existingWikiWord" href="/nlab/show/point">point</a></strong> is the locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> whose frame of opens is the frame of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a> (classically <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mo>⊥</mo><mo><</mo><mo>⊤</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{\bot \lt \top\}</annotation></semantics></math>). This is the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Locale</mi></mrow><annotation encoding="application/x-tex">Locale</annotation></semantics></math>, since we must have (for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">f\colon X \to 1</annotation></semantics></math>) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mo>⊤</mo><mo stretchy="false">)</mo><mo>=</mo><msub><mo>⊤</mo> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">f^*(\top) = \top_X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mo>⊥</mo><mo stretchy="false">)</mo><mo>=</mo><msub><mo>⊥</mo> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">f^*(\bot) = \bot_X</annotation></semantics></math> (and most generally <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo><mo>=</mo><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo><mo stretchy="false">{</mo><msub><mo>⊤</mo> <mi>X</mi></msub><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>p</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">f^*(p) = \bigvee \{\top_X \;|\; p\}</annotation></semantics></math>, since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>=</mo><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo><mo stretchy="false">{</mo><mo>⊤</mo><mspace width="thickmathspace"></mspace><mo stretchy="false">|</mo><mspace width="thickmathspace"></mspace><mi>p</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">p = \bigvee \{\top \;|\; p\}</annotation></semantics></math>).</p> <p>Given a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, a <strong>concrete <a class="existingWikiWord" href="/nlab/show/point">point</a></strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> may be defined in any of the following equivalent ways:</p> <ol> <li>A point of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/continuous+map">continuous map</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mn>1</mn><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">f\colon 1 \to X</annotation></semantics></math>;</li> <li>Unravelling this in terms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^*\colon O(X) \to O(1)</annotation></semantics></math> and viewing this as a <a class="existingWikiWord" href="/nlab/show/characteristic+function">characteristic function</a>, a point of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/completely+prime+filter">completely prime filter</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>;</li> <li>Unravelling (1) in terms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_*\colon O(1) \to O(X)</annotation></semantics></math>, which classically (using <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>) is determined by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo stretchy="false">(</mo><mo>⊥</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_*(\bot)</annotation></semantics></math>, a point of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/prime+element">prime element</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>.</li> </ol> <p>Definition (3) is simpler than (2), being an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> satisfying a finitary condition rather than a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> satisfying an infinitary condition. However, it doesn't work in <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a>, which provides much (but by no means all) of the motivation for studying locales.</p> <h2 id="properties">Properties</h2> <h3 id="CategoryOfLocales">Categories of internal locales</h3> <div class="num_prop"> <h6 id="proposition">Proposition</h6> <p>The category <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>E</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(E)</annotation></semantics></math> of locales <a class="existingWikiWord" href="/nlab/show/internalization">internal to</a> a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> is equivalent to the category of <a class="existingWikiWord" href="/nlab/show/localic+geometric+morphisms">localic geometric morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Sh</mi> <mi>E</mi></msub><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">Sh_{E}(\Sigma) \to E</annotation></semantics></math> in <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Locale</mi><mo stretchy="false">(</mo><mi>E</mi><mo stretchy="false">)</mo><mo>≃</mo><mo stretchy="false">(</mo><mi>Topos</mi><mo stretchy="false">/</mo><mi>E</mi><msub><mo stretchy="false">)</mo> <mi>loc</mi></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Locale(E) \simeq (Topos/E)_{loc} \,. </annotation></semantics></math></div></div> <p>See <a class="existingWikiWord" href="/nlab/show/localic+geometric+morphism">localic geometric morphism</a> for more.</p> <div class="num_prop"> <h6 id="proposition_2">Proposition</h6> <p>For every locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Locale</mi><mo stretchy="false">(</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Locale(Sh(X))</annotation></semantics></math> of locales internal to the <a class="existingWikiWord" href="/nlab/show/sheaf+topos">sheaf topos</a> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is equivalent to the <a class="existingWikiWord" href="/nlab/show/overcategory">overcategory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Locale</mi><mo stretchy="false">/</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">Locale/X</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ℐ</mi><mo lspace="verythinmathspace">:</mo><mi>Locale</mi><mo stretchy="false">/</mo><mi>X</mi><mover><mo>→</mo><mo>≃</mo></mover><mi>Locale</mi><mo stretchy="false">(</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathcal{I}\colon Locale/X \stackrel{\simeq}{\to} Locale(Sh(X)) \,. </annotation></semantics></math></div></div> <p>This appears as <a href="#Johnstone">Johnstone, theorem C1.6.3</a>.</p> <div class="num_prop"> <h6 id="proposition_3">Proposition</h6> <p>For every morphism of locales <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>Y</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">f\colon Y \to X</annotation></semantics></math> the <a class="existingWikiWord" href="/nlab/show/sheaf+topos">sheaf topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(Y)</annotation></semantics></math> is equivalent as a topos over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(X)</annotation></semantics></math> to the topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Sh</mi> <mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>ℐ</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh_{Sh(X)}(\mathcal{I}(Y))</annotation></semantics></math> of internal sheaves over the internal locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℐ</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{I}(Y) \in Sh(X)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>Sh</mi> <mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>ℐ</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Sh(Y) \simeq Sh_{Sh(X)}(\mathcal{I}(Y)) \,. </annotation></semantics></math></div></div> <p>This appears as <a href="#Johnstone">Johnstone, scholium C1.6.4</a>.</p> <h3 id="RelationToTopologicalSpaces">Relation to topological spaces</h3> <p>Every <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/frame+of+opens">frame of opens</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>, and therefore gives rise to a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>X</mi> <mi>L</mi></msub></mrow><annotation encoding="application/x-tex">X_L</annotation></semantics></math>. For every <a class="existingWikiWord" href="/nlab/show/continuous+function">continuous function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f\colon X \to Y</annotation></semantics></math> between topological spaces, the <a class="existingWikiWord" href="/nlab/show/preimage">inverse image</a> map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msup><mo lspace="verythinmathspace">:</mo><mi>O</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^{-1}\colon O(Y) \to O(X)</annotation></semantics></math> is a frame homomorphism, so <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> induces a continuous map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>L</mi></msub><mo lspace="verythinmathspace">:</mo><msub><mi>X</mi> <mi>L</mi></msub><mo>→</mo><msub><mi>Y</mi> <mi>L</mi></msub></mrow><annotation encoding="application/x-tex">f_L\colon X_L \to Y_L</annotation></semantics></math> of locales. Thus we have a <a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub><mo lspace="verythinmathspace">:</mo></mrow><annotation encoding="application/x-tex">(-)_L\colon</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Top">Top</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Loc">Locale</a>.</p> <p>Conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is any locale, we define a <strong><a class="existingWikiWord" href="/nlab/show/point">point</a></strong> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> to be a <a class="existingWikiWord" href="/nlab/show/continuous+map">continuous map</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">1 \to X</annotation></semantics></math>. Here <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal</a> locale, which can be defined as the locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>1</mn> <mi>L</mi></msub></mrow><annotation encoding="application/x-tex">1_L</annotation></semantics></math> corresponding to the terminal space. Explicitly, we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo><mo>=</mo><mi>P</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(1) = P(1)</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/powerset">powerset</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> (the initial frame, the set of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a>, which is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math> classically or in a <a class="existingWikiWord" href="/nlab/show/Boolean+topos">Boolean topos</a>). Since a frame homomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>→</mo><mi>P</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X) \to P(1)</annotation></semantics></math> is determined by the preimage of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> (the <a class="existingWikiWord" href="/nlab/show/true">true</a> truth value), a point can also be described more explicitly as a <em><a class="existingWikiWord" href="/nlab/show/completely+prime+filter">completely prime filter</a></em>: an upwards-closed subset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">X \in F</annotation></semantics></math> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> denotes the <a class="existingWikiWord" href="/nlab/show/top+element">top element</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>), if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>,</mo><mi>V</mi><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">U,V \in F</annotation></semantics></math> then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>∩</mo><mi>V</mi><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">U \cap V \in F</annotation></semantics></math>, and if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">⋃</mo> <mi>i</mi></msub><msub><mi>U</mi> <mi>i</mi></msub><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">\bigcup_i U_i \in F</annotation></semantics></math> then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>U</mi> <mi>i</mi></msub><mo>∈</mo><mi>F</mi></mrow><annotation encoding="application/x-tex">U_i \in F</annotation></semantics></math> for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>i</mi></mrow><annotation encoding="application/x-tex">i</annotation></semantics></math>.</p> <p>The elements of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> induce a <a class="existingWikiWord" href="/nlab/show/topological+structure">topology</a> on the set of points of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> in an obvious way, thereby giving rise to a topological space <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>X</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">X_P</annotation></semantics></math>. Any continuous map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f\colon X \to Y</annotation></semantics></math> of locales induces a continuous map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mi>P</mi></msub><mo lspace="verythinmathspace">:</mo><msub><mi>X</mi> <mi>P</mi></msub><mo>→</mo><msub><mi>Y</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">f_P\colon X_P \to Y_P</annotation></semantics></math> of spaces, so we have another functor</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub><mo lspace="verythinmathspace">:</mo><mi>Locale</mi><mo>→</mo><mi>Top</mi></mrow><annotation encoding="application/x-tex">(-)_P\colon Locale \to Top</annotation></semantics></math>.</p> <p>One finds that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub></mrow><annotation encoding="application/x-tex">(-)_L</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">(-)_P</annotation></semantics></math>.</p> <p>In fact, this is an <a class="existingWikiWord" href="/nlab/show/idempotent+adjunction">idempotent adjunction</a>:</p> <div class="num_prop" id="TopLocAdjunction"> <h6 id="proposition_4">Proposition</h6> <p>The categories <a class="existingWikiWord" href="/nlab/show/Top">Top</a> of <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a> and <a class="existingWikiWord" href="/nlab/show/Loc">Locale</a> of locales are related by an <a class="existingWikiWord" href="/nlab/show/idempotent+adjunction">idempotent adjunction</a>.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub><mo>⊣</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Top</mi><mspace width="thickmathspace"></mspace><munderover><mo>⊥</mo><munder><mo>⟵</mo><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub></mrow></munder><mover><mo>⟶</mo><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub></mrow></mover></munderover><mspace width="thickmathspace"></mspace><mi>Locale</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> ( (-)_L \dashv (-)_P ) \colon Top \; \underoverset {\underset{(-)_P}{\longleftarrow}} {\overset{(-)_L}{\longrightarrow}} {\bot} \; Locale \,. </annotation></semantics></math></div></div> <p>This appears for instance as (<a href="#MacLaneMoerdijk">MacLaneMoerdijk, theorem IX.3 1</a>) or as (<a href="#Johnstone">Johnstone, lemma C.1.2.2</a>).</p> <p>Therefore the <a class="existingWikiWord" href="/nlab/show/adjunction">adjunction</a> restricts to an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence</a> between the fixed subcategories on either side.</p> <div class="num_defn"> <h6 id="definition_2">Definition</h6> <p>A <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>≅</mo><msub><mi>X</mi> <mrow><mi>L</mi><mi>P</mi></mrow></msub></mrow><annotation encoding="application/x-tex">X \cong X_{L P}</annotation></semantics></math> is called <strong><a class="existingWikiWord" href="/nlab/show/sober+space">sober</a></strong>.</p> <p>A locale with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>≅</mo><msub><mi>X</mi> <mrow><mi>P</mi><mi>L</mi></mrow></msub></mrow><annotation encoding="application/x-tex">X \cong X_{P L}</annotation></semantics></math> is called <strong><a class="existingWikiWord" href="/nlab/show/spatial+locale">spatial</a></strong> or <strong>topological</strong>; one also says that it has <strong>enough points</strong>.</p> </div> <p>see also MO <a href="http://math.stackexchange.com/a/1904289/58526">here</a></p> <div class="num_cor"> <h6 id="corollary">Corollary</h6> <p>The <a class="existingWikiWord" href="/nlab/show/adjunction">adjunction</a> from prop. <a class="maruku-ref" href="#TopLocAdjunction"></a> exhibits <a class="existingWikiWord" href="/nlab/show/sober+topological+spaces">sober topological spaces</a> as a <a class="existingWikiWord" href="/nlab/show/coreflective+subcategory">coreflective subcategory</a> of <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub><mo>⊣</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>SoberTop</mi><munderover><mo>⊥</mo><munder><mo>←</mo><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>P</mi></msub></mrow></munder><mover><mo>↪</mo><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msub><mo stretchy="false">)</mo> <mi>L</mi></msub></mrow></mover></munderover><mi>Locale</mi></mrow><annotation encoding="application/x-tex"> ( (-)_L \dashv (-)_P ) \colon SoberTop \underoverset {\underset{(-)_P}{\leftarrow}} {\overset{(-)_L}{\hookrightarrow}} {\bot} Locale </annotation></semantics></math></div> <p>and this restricts to an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a> between the <a class="existingWikiWord" href="/nlab/show/full+subcategory">full subcategory</a> of locales with enough points, and that of <a class="existingWikiWord" href="/nlab/show/sober+topological+spaces">sober topological spaces</a>.</p> </div> <p>This appears for instance as (<a href="#MacLaneMoerdijk">MacLaneMoerdijk, corollary IX.3 4</a>).</p> <p>Consequently, we often identify a sober topological space and the corresponding topological locale.</p> <h3 id="RelationToToposes">Relation to toposes – localic reflection</h3> <p>The notion of <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a> can be seen as a <a class="existingWikiWord" href="/nlab/show/categorification">categorification</a> of the notion of locale, by relating both notions to the notion of <a class="existingWikiWord" href="/nlab/show/total+category">lex totality</a>:</p> <div class="num_prop"> <h6 id="proposition_5">Proposition</h6> <p>A <a class="existingWikiWord" href="/nlab/show/poset">poset</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/frame">frame</a> if and only if the <a class="existingWikiWord" href="/nlab/show/Yoneda+embedding">Yoneda embedding</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo lspace="verythinmathspace">:</mo><mi>P</mi><mo>→</mo><msup><mstyle mathvariant="bold"><mn>2</mn></mstyle> <mrow><msup><mi>P</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex"> y \colon P \to \mathbf{2}^{P^{op}} </annotation></semantics></math></div> <p>has a <a class="existingWikiWord" href="/nlab/show/exact+functor">left exact</a> <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a>. (Here the poset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mn>2</mn></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{2}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a> is the base of enrichment for posets seen as <a class="existingWikiWord" href="/nlab/show/enriched+categories">enriched categories</a>.)</p> </div> <p>The analogous result for toposes involves a bit of <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>: under <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a> plus the existence of a <span class="newWikiWord">strong inaccessible cardinal<a href="/nlab/new/strong+inaccessible+cardinal">?</a></span> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>κ</mi></mrow><annotation encoding="application/x-tex">\kappa</annotation></semantics></math>, the foundational assumption of MacLane in <em><a class="existingWikiWord" href="/nlab/show/Categories+for+the+Working+Mathematician">Categories for the Working Mathematician</a></em>, call a category <em><a class="existingWikiWord" href="/nlab/show/moderate+category">moderate</a></em> if its set of morphisms has size <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>κ</mi></mrow><annotation encoding="application/x-tex">\kappa</annotation></semantics></math>. For example, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is moderate.</p> <div class="num_prop"> <h6 id="proposition_6">Proposition</h6> <p>(<a href="#Street">Street</a>)</p> <p>A moderate <a class="existingWikiWord" href="/nlab/show/locally+small+category">locally small category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a> if and only if the <a class="existingWikiWord" href="/nlab/show/Yoneda+embedding">Yoneda embedding</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo lspace="verythinmathspace">:</mo><mi>C</mi><mo>→</mo><msup><mi>Set</mi> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex">y \colon C \to Set^{C^{op}}</annotation></semantics></math></div> <p>has a <a class="existingWikiWord" href="/nlab/show/left+exact+functor">left exact</a> <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a>.</p> </div> <p>These results emphasize frames/toposes as algebras, where the morphisms are left exact left adjoints. The <a class="existingWikiWord" href="/nlab/show/right+adjoints">right adjoints</a> to such morphisms are called <a class="existingWikiWord" href="/nlab/show/geometric+morphism">geometric morphisms</a>, and emphasize locales/toposes as <a class="existingWikiWord" href="/nlab/show/spaces">spaces</a>. This analogy, which plays an important but mostly tacit role in <a href="#JT">Joyal and Tierney</a>, can be developed further along the following lines.</p> <p>The <a class="existingWikiWord" href="/nlab/show/frame+of+opens">frame of opens</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> corresponding to a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is naturally a <a class="existingWikiWord" href="/nlab/show/site">site</a>:</p> <div class="num_defn"> <h6 id="definition_3">Definition</h6> <p>Given a locale <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, with <a class="existingWikiWord" href="/nlab/show/frame+of+opens">frame of opens</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math>, say that a family of <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><msub><mi>U</mi> <mi>i</mi></msub><mo>→</mo><mi>U</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{U_i \to U\}</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/cover">cover</a> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/join">join</a> of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>U</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">U_i</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>=</mo><msub><mo>∨</mo> <mi>i</mi></msub><msub><mi>U</mi> <mi>i</mi></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> U = \vee_i U_i \,. </annotation></semantics></math></div></div> <div class="num_prop"> <h6 id="proposition_7">Proposition</h6> <p>This defines a <a class="existingWikiWord" href="/nlab/show/coverage">coverage</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> and hence makes it a <a class="existingWikiWord" href="/nlab/show/site">site</a>.</p> </div> <p>See for instance (<a href="#MacLaneMoerdijk">MacLaneMoerdijk, section 5</a>).</p> <div class="num_defn"> <h6 id="definition_4">Definition</h6> <p>For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> a locale, write</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>≔</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> Sh(X) \coloneqq Sh(O(X)) </annotation></semantics></math></div> <p>for the <a class="existingWikiWord" href="/nlab/show/sheaf+topos">sheaf topos</a> over the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(X)</annotation></semantics></math> equipped with the above canonical structure of a <a class="existingWikiWord" href="/nlab/show/site">site</a>.</p> </div> <p>Write <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a> for the category of <a class="existingWikiWord" href="/nlab/show/Grothendieck+toposes">Grothendieck toposes</a> and <a class="existingWikiWord" href="/nlab/show/geometric+morphisms">geometric morphisms</a>.</p> <div class="num_prop"> <h6 id="proposition_8">Proposition</h6> <p>This construction defines a <a class="existingWikiWord" href="/nlab/show/full+and+faithful+functor">full and faithful functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo>:</mo></mrow><annotation encoding="application/x-tex">Sh(-) : </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a>.</p> </div> <p>This appears for instance as <a href="#MacLaneMoerdijk">MacLaneMoerdijk, section IX.5 prop 2</a>.</p> <div class="num_defn"> <h6 id="definition_5">Definition</h6> <p>A topos in the <a class="existingWikiWord" href="/nlab/show/image">image</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Locale</mi><mo>→</mo><mi>Topos</mi></mrow><annotation encoding="application/x-tex">Sh(-)\colon Locale \to Topos</annotation></semantics></math> is called a <em><a class="existingWikiWord" href="/nlab/show/localic+topos">localic topos</a></em>.</p> </div> <div class="num_prop"> <h6 id="proposition_9">Proposition</h6> <p>The functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Locale</mi><mo>→</mo><mi>Topos</mi></mrow><annotation encoding="application/x-tex">Sh(-)\colon Locale \to Topos</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>L</mi><mo lspace="verythinmathspace">:</mo><mi>Topos</mi><mo>→</mo><mi>Locale</mi></mrow><annotation encoding="application/x-tex"> L\colon Topos \to Locale </annotation></semantics></math></div> <p>given by sending a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> to the locale that is formally dual to the <a class="existingWikiWord" href="/nlab/show/frame">frame</a> of <a class="existingWikiWord" href="/nlab/show/subobjects">subobjects</a> of the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>L</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≔</mo><msub><mi>Sub</mi> <mi>ℰ</mi></msub><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> O(L(\mathcal{E})) \coloneqq Sub_{\mathcal{E}}(*) \,. </annotation></semantics></math></div></div> <p>This appears for instance as <a href="#MacLaneMoerdijk">MacLaneMoerdijk, section IX.5 prop 3</a>.</p> <p>The functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> here is also called <strong>localic reflection</strong>.</p> <p>In summary this means that locales form a <a class="existingWikiWord" href="/nlab/show/reflective+subcategory">reflective subcategory</a> of <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Locale</mi><mover><mo>↪</mo><mover><mo>←</mo><mi>L</mi></mover></mover><mi>Topos</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Locale \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow} Topos \,. </annotation></semantics></math></div> <p>In fact this is even a genuine <a class="existingWikiWord" href="/nlab/show/full+sub-2-category">full sub-2-category</a>:</p> <div class="num_prop"> <h6 id="proposition_10">Proposition</h6> <p>For all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>,</mo><mi>Y</mi><mo>∈</mo></mrow><annotation encoding="application/x-tex">X,Y \in </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a> the <a class="existingWikiWord" href="/nlab/show/2-functor">2-functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo lspace="verythinmathspace">:</mo></mrow><annotation encoding="application/x-tex">Sh\colon</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Locale">Locale</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a> induces an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo lspace="verythinmathspace">:</mo><mi>Locale</mi><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>Y</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mo>≃</mo></mover><mi>Topos</mi><mo stretchy="false">(</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>,</mo><mi>Sh</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Sh\colon Locale(X,Y) \stackrel{\simeq}{\to} Topos(Sh(X), Sh(Y)) \,. </annotation></semantics></math></div></div> <p>This appears as (<a href="#Johnstone">Johnstone, prop. C1.4.5</a>).</p> <div class="num_prop"> <h6 id="proposition_11">Proposition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/poset+of+subobjects">poset of subobjects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Sub</mi> <mi>ℰ</mi></msub><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub_{\mathcal{E}}(*)</annotation></semantics></math> of the terminal object of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> is equivalent to the full <a class="existingWikiWord" href="/nlab/show/subcategory">subcategory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>τ</mi> <mrow><mo>≤</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msub><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\tau_{\leq -1}(\mathcal{E})</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> on the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/truncated">truncated</a> objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Sub</mi> <mi>ℰ</mi></msub><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo><mo>≃</mo><msub><mi>τ</mi> <mrow><mo>≤</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msub><mi>ℰ</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> Sub_{\mathcal{E}}(*) \simeq \tau_{\leq -1} \mathcal{E} \,. </annotation></semantics></math></div></div> <div class="proof"> <h6 id="proof">Proof</h6> <p>A <a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated">(-1)-truncated</a> sheaf <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is one whose values over any object are either the <a class="existingWikiWord" href="/nlab/show/%28-2%29-groupoid">singleton set</a>, or the <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>∈</mo><mo stretchy="false">{</mo><mo>*</mo><mo>,</mo><mi>∅</mi><mo stretchy="false">}</mo><mo>=</mo><mo>⊂</mo><mi>Set</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> X(X) \in \{*, \emptyset\} = \subset Set \,. </annotation></semantics></math></div> <p>A <a class="existingWikiWord" href="/nlab/show/monomorphism">monomorphism</a> of <a class="existingWikiWord" href="/nlab/show/sheaves">sheaves</a> is a <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a> that is degreewise a monomorphism of sets (an <a class="existingWikiWord" href="/nlab/show/injection">injection</a>). Therefore the <a class="existingWikiWord" href="/nlab/show/subobjects">subobjects</a> of the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal</a> sheaf (that assigns the singleton set to every object) are precisely the sheaves of this form.</p> </div> <p>We may think of a <a class="existingWikiWord" href="/nlab/show/frame">frame</a> as a <a class="existingWikiWord" href="/nlab/show/Grothendieck+%280%2C1%29-topos">Grothendieck (0,1)-topos</a>. Then localic reflection is reflection of <a class="existingWikiWord" href="/nlab/show/Grothendieck+toposes">Grothendieck toposes</a> onto <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(0,1)</annotation></semantics></math>-toposes and is given by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-truncation: for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> a locale, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sh</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(X)</annotation></semantics></math> the corresponding <a class="existingWikiWord" href="/nlab/show/localic+topos">localic topos</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> any Grothendieck topos we have a natural equivalence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Gr</mi><mn>1</mn><mi>Topos</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo>,</mo><mi>Sh</mi><mi>X</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>Gr</mi><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo><mi>Topos</mi><mo stretchy="false">(</mo><msub><mi>τ</mi> <mrow><mo>≤</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msub><mi>ℰ</mi><mo>,</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> Gr1Topos( \mathcal{E}, Sh X) \simeq Gr(0,1)Topos(\tau_{\leq -1} \mathcal{E}, O(X)) </annotation></semantics></math></div> <p>which is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>⋯</mi><mo>≃</mo><mi>Frame</mi><mo stretchy="false">(</mo><mi>O</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>Sub</mi> <mi>ℰ</mi></msub><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><mi>Locale</mi><mo stretchy="false">(</mo><mi>L</mi><mi>ℰ</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \cdots \simeq Frame(O(X), Sub_{\mathcal{E}}(*)) \simeq Locale(L \mathcal{E} , X) \,. </annotation></semantics></math></div> <p>This is a small part of a pattern in <a class="existingWikiWord" href="/nlab/show/higher+topos+theory">higher topos theory</a>, described at <a class="existingWikiWord" href="/nlab/show/n-localic+%28%E2%88%9E%2C1%29-topos">n-localic (∞,1)-topos</a>.</p> <h2 id="Examples">Examples</h2> <h3 id="general_topology">General topology</h3> <p>As explained above, the <a class="existingWikiWord" href="/nlab/show/functor">functor</a> from <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a> to locales provides a very large collection of examples. When restricted to <a class="existingWikiWord" href="/nlab/show/sober+topological+spaces">sober topological spaces</a>, this functor becomes <a class="existingWikiWord" href="/nlab/show/fully+faithful+functor">fully faithful</a> and its <a class="existingWikiWord" href="/nlab/show/essential+images">essential images</a> consists of <a class="existingWikiWord" href="/nlab/show/spatial+locales">spatial locales</a>.</p> <p>Without the <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a> of <a class="existingWikiWord" href="/nlab/show/excluded+middle">excluded middle</a>, many classical examples, such as <a class="existingWikiWord" href="/nlab/show/the+locale+of+real+numbers">the locale of real numbers</a> or <a class="existingWikiWord" href="/nlab/show/Cantor+space">Cantor space</a>, can cease to be <a class="existingWikiWord" href="/nlab/show/spatial+locale">spatial</a>.</p> <p>Naturally, one is interested in examples of locales that are not spatial, and a few are given below.</p> <h3 id="ExamplesMeasureTheory">Measure theory</h3> <p>An amazing feature of <a class="existingWikiWord" href="/nlab/show/pointfree+topology">pointfree topology</a> is that it contains not only point-set <a class="existingWikiWord" href="/nlab/show/general+topology">general topology</a>, but also point-set <a class="existingWikiWord" href="/nlab/show/measure+theory">measure theory</a>, again as a <a class="existingWikiWord" href="/nlab/show/full+subcategory">full subcategory</a>.</p> <p>Specifically, recall from the <a class="existingWikiWord" href="/nlab/show/duality+between+geometry+and+algebra">duality between geometry and algebra</a> that various categories of <a class="existingWikiWord" href="/nlab/show/commutative+algebras">commutative algebras</a> are <a class="existingWikiWord" href="/nlab/show/opposite+category">contravariantly</a> <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to certain corresponding categories of spaces. The category of algebras relevant for <a class="existingWikiWord" href="/nlab/show/measure+theory">measure theory</a> is the category of <a class="existingWikiWord" href="/nlab/show/commutative+von+Neumann+algebras">commutative von Neumann algebras</a> and ultraweakly continuous *-homomorphisms; it is widely accepted that dropping the commutativity condition and passing to the <a class="existingWikiWord" href="/nlab/show/opposite+category">opposite category</a> yields the correct category of <a class="existingWikiWord" href="/nlab/show/noncommutative+measurable+spaces">noncommutative measurable spaces</a>.</p> <p>The category of <a class="existingWikiWord" href="/nlab/show/commutative+von+Neumann+algebras">commutative von Neumann algebras</a> is contravariantly <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to several other categories:</p> <ul> <li> <p>compact strictly localizable enhanced measurable spaces and measurable maps;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperstonean+topological+spaces">hyperstonean topological spaces</a> and <a class="existingWikiWord" href="/nlab/show/open+maps">open maps</a>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperstonean+locales">hyperstonean locales</a> and <a class="existingWikiWord" href="/nlab/show/open+maps">open maps</a>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/measurable+locales">measurable locales</a> and maps of locales.</p> </li> </ul> <p>The last category is particularly interesting: it is a <a class="existingWikiWord" href="/nlab/show/full+subcategory">full subcategory</a> of <a class="existingWikiWord" href="/nlab/show/locales">locales</a>. Thus, <a class="existingWikiWord" href="/nlab/show/measure+theory">measure theory</a> embeds into pointfree topology, which means that methods and results from pointfree topology can be used right away in <a class="existingWikiWord" href="/nlab/show/measure+theory">measure theory</a>. This stands in contrast to the traditional point-set treatments, where two rather different formalisms must be developed for point-set <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a> and point-set <a class="existingWikiWord" href="/nlab/show/measurable+spaces">measurable spaces</a>.</p> <p>With the exception of <a class="existingWikiWord" href="/nlab/show/discrete+locales">discrete locales</a>, <a class="existingWikiWord" href="/nlab/show/measurable+locales">measurable locales</a> are <em>never</em> spatial, and in fact do not have any points other than those in its atomic (discrete) part, which splits off as a coproduct summand.</p> <h3 id="intersections_of_dense_sublocales">Intersections of dense sublocales</h3> <p>Another important source of nonspatial sublocales is given by <a class="existingWikiWord" href="/nlab/show/intersections">intersections</a> (of arbitrary cardinality) of <a class="existingWikiWord" href="/nlab/show/dense+sublocales">dense sublocales</a>.</p> <p>Again, in contrast to the point-set setting, where the <a class="existingWikiWord" href="/nlab/show/Baire+category+theorem">Baire category theorem</a> identifies the rather restrictive conditions under which the intersection of dense topological subspaces is again dense, in the pointfree setting arbitrary intersections of <a class="existingWikiWord" href="/nlab/show/dense+sublocales">dense sublocales</a> are always dense.</p> <p>In particular, one can intersection all <a class="existingWikiWord" href="/nlab/show/dense+sublocales">dense sublocales</a> of a given <a class="existingWikiWord" href="/nlab/show/locale">locale</a>, which always produces a nonspatial locale, unless the original locale is discrete. This is the <a class="existingWikiWord" href="/nlab/show/double+negation+sublocale">double negation sublocale</a>.</p> <p>But there are other interesting examples. Connecting to <a class="existingWikiWord" href="/nlab/show/measure+theory">measure theory</a>, we can consider a <a class="existingWikiWord" href="/nlab/show/valuation">valuation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi></mrow><annotation encoding="application/x-tex">\nu</annotation></semantics></math> on a given <a class="existingWikiWord" href="/nlab/show/locale">locale</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>L</mi></mrow><annotation encoding="application/x-tex">L</annotation></semantics></math> and take the intersection of all <a class="existingWikiWord" href="/nlab/show/sublocales">sublocales</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ν</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo><mo>=</mo><mi>ν</mi><mo stretchy="false">(</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\nu(S)=\nu(1)</annotation></semantics></math>. The resulting sublocale can be seen as the smallest sublocale with a measure 0 complement.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p>The notion of locale may be identified with that of a <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck</a> <a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a>. See <a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a> for more on this.</p> </li> <li> <p>An <a class="existingWikiWord" href="/nlab/show/ionad">ionad</a> is to a <a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a> as a <a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">Grothendieck topos</a> is to a <a class="existingWikiWord" href="/nlab/show/locale">locale</a>.</p> </li> <li> <p>A <a class="existingWikiWord" href="/nlab/show/group+object">group object</a> <a class="existingWikiWord" href="/nlab/show/internalization">internal</a> to locales or an <a class="existingWikiWord" href="/nlab/show/internal+groupoid">internal groupoid</a> in locales is a <a class="existingWikiWord" href="/nlab/show/localic+group">localic group</a> or <a class="existingWikiWord" href="/nlab/show/localic+groupoid">localic groupoid</a>, respectively.</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/positive+locale">positive locale</a>, <a class="existingWikiWord" href="/nlab/show/locally+positive+locale">locally positive locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/premetric+locale">premetric locale</a>, <a class="existingWikiWord" href="/nlab/show/metric+locale">metric locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/preuniform+locale">preuniform locale</a>, <a class="existingWikiWord" href="/nlab/show/uniform+locale">uniform locale</a></p> </li> </ul> <p>There is also a notion of <a class="existingWikiWord" href="/nlab/show/internal+locale">internal locale</a>, see also <a class="existingWikiWord" href="/nlab/show/internal+site">internal site</a>.</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+space">topological space</a>, <a class="existingWikiWord" href="/nlab/show/topological+locale">topological locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ionad">ionad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/profinite+space">profinite space</a>, <a class="existingWikiWord" href="/nlab/show/profinite+reflection">profinite reflection</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/localic+homotopy+theory">localic homotopy theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+hyperdoctrine">geometric hyperdoctrine</a></p> </li> </ul> <h2 id="references">References</h2> <p>An early paper, containing much of the basic theory, and in which the term “locale” is introduced:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/John+R.+Isbell">John R. Isbell</a>, <em>Atomless Parts of Spaces</em>, Mathematica Scandinavica <strong>31</strong> (1972) 5–32 [<a href="https://doi.org/10.7146/math.scand.a-11409">doi:10.7146/math.scand.a-11409</a>]</li> </ul> <p>An introduction to and survey of the use of locales instead of topological spaces (“<a class="existingWikiWord" href="/nlab/show/point-free+topology">point-free topology</a>”):</p> <ul> <li id="Johnstone83"><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, <em>The point of pointless topology</em> , Bull. Amer. Math. Soc. (N.S.) <strong>8</strong> 1 (1983), 41-53 [<a href="http://www.ams.org/bull/1983-08-01/S0273-0979-1983-15080-2/home.html">Bulletin AMS</a>, <a href="http://projecteuclid.org/euclid.bams/1183550014">Euclid</a>]</li> </ul> <p>This is, in its own words, to be read as the trailer for the book</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, <em><a class="existingWikiWord" href="/nlab/show/Stone+Spaces">Stone Spaces</a></em>, Cambridge Studies in Advanced Mathematics <strong>3</strong>, Cambridge University Press (1982, 1986) xxi+370 pp. [<a href="http://www.ams.org/mathscinet-getitem?mr=698074">MR85f:54002</a>]</li> </ul> <p>that develops, among other things, much of <a class="existingWikiWord" href="/nlab/show/general+topology">general topology</a> entirely with the notion of locales used in place of that of <a class="existingWikiWord" href="/nlab/show/topological+spaces">topological spaces</a>. See also <em><a class="existingWikiWord" href="/nlab/show/Stone+Spaces">Stone Spaces</a></em> for more.</p> <p>Other textbook accounts:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Francis+Borceux">Francis Borceux</a>, volume 3, chapter 1 of <em><a class="existingWikiWord" href="/nlab/show/Handbook+of+Categorical+Algebra">Handbook of Categorical Algebra</a></em>,</p> </li> <li id="Johnstone"> <p><a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, part C (volume 2) <em><a class="existingWikiWord" href="/nlab/show/Elephant">Sketches of an elephant: a topos theory compendium</a></em>.</p> </li> <li id="MacLaneMoerdijk"> <p><a class="existingWikiWord" href="/nlab/show/Saunders+MacLane">Saunders MacLane</a>, <a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a>, <em><a class="existingWikiWord" href="/nlab/show/Sheaves+in+Geometry+and+Logic">Sheaves in Geometry and Logic</a></em></p> </li> <li> <p>Jorge Picado & Aleš Pultr (2012). <em>Frames and Locales: Topology without points</em>. Springer. <a href="http://www.mat.uc.pt/%7Epicado/publicat/bookpage.html">Web page</a> (with preface, contents, and errata).</p> </li> </ul> <p>and</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Steve+Vickers">Steve Vickers</a>, <em>Topology via logic</em>, Cambridge University Press (1989)</li> </ul> <p>where the latter develops topology from the point of view of its <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>.</p> <p>An introductory survey is</p> <ul> <li>Jorge Picado, Aleš Pultr, Anna Tozzi, <em>Locales</em>, pages 49–101 in Pedicchio&Tholen (eds.), <em>Categorical Foundations</em> , CUP 2004. (<a href="http://www.mat.uc.pt/~picado/publicat/Chapter2.pdf">draft</a>)</li> </ul> <p>See also</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/eom">eom</a>, <em><a href="https://www.encyclopediaofmath.org/index.php/Locale">Locale</a></em></li> </ul> <p>Lex totality is the subject of an article of Street,</p> <ul> <li id="Street"><a class="existingWikiWord" href="/nlab/show/Ross+Street">Ross Street</a>, <em>Notions of Topos</em>, Bull. Australian Math. Soc. 23 (1981), 199–208.</li> </ul> <p>The connection between locales and toposes via lex totality plays a tacit role throughout the influential monograph</p> <ul> <li id="JT"><a class="existingWikiWord" href="/nlab/show/Andr%C3%A9+Joyal">André Joyal</a> and <a class="existingWikiWord" href="/nlab/show/Myles+Tierney">Myles Tierney</a>, <em>An Extension of the Galois Theory of Grothendieck</em>, Memoirs of the American Mathematical Society 51 (1984).</li> </ul> <p>A basic introduction to locale theory can be found in section 1 of</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Ingo+Blechschmidt">Ingo Blechschmidt</a>, <em>Generalized spaces for constructive algebra</em>, (<a href="https://arxiv.org/abs/2012.13850">arXiv:2012.13850</a>)</li> </ul> <p>A <a class="existingWikiWord" href="/nlab/show/model+category">model category</a> of <a class="existingWikiWord" href="/nlab/show/locales">locales</a> which makes the <a class="existingWikiWord" href="/nlab/show/reflective+subcategory">reflection</a> of <a class="existingWikiWord" href="/nlab/show/sober+topological+spaces">sober topological spaces</a> a <a class="existingWikiWord" href="/nlab/show/Quillen+adjunction">Quillen adjunction</a> to the sober-restriction of the <a class="existingWikiWord" href="/nlab/show/classical+model+structure+on+topological+spaces">classical model structure on topological spaces</a>:</p> <ul> <li id="SterlingKapulkin23"><a class="existingWikiWord" href="/nlab/show/Sterling+Ebel">Sterling Ebel</a>, <a class="existingWikiWord" href="/nlab/show/Chris+Kapulkin">Chris Kapulkin</a>, Thm. 4.45 in: <em>Synthetic approach to the Quillen model structure on topological spaces</em> [<a href="https://arxiv.org/abs/2310.14235">arXiv:2310.14235</a>]</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on October 24, 2023 at 09:42:26. See the <a href="/nlab/history/locale" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/locale" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/2341/#Item_44">Discuss</a><span class="backintime"><a href="/nlab/revision/locale/95" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/locale" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/locale" accesskey="S" class="navlink" id="history" rel="nofollow">History (95 revisions)</a> <a href="/nlab/show/locale/cite" style="color: black">Cite</a> <a href="/nlab/print/locale" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/locale" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>