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> Grothendieck topos 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> Grothendieck topos </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/6753/#Item_32" 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="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> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#definition'>Definition</a></li> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#general'>General</a></li> <li><a href='#Giraud'>Giraud's axiomatic characterization</a></li> <li><a href='#Streetcharacterization'>Street’s axiomatic characterization</a></li> <li><a href='#as_lex_reflections_of_categories_of_presheaves'>As lex reflections of categories of presheaves</a></li> <li><a href='#AsLocalicGroupoids'>As localic groupoids</a></li> <li><a href='#internal_logic'>Internal logic</a></li> <li><a href='#2monadicity_over_locally_presentable_categories'>2-monadicity over locally presentable categories</a></li> <li><a href='#enrichment_over_accessible_categories_with_directed_colimits'>Enrichment over accessible categories with directed colimits</a></li> </ul> <li><a href='#in_weak_foundations'>In weak foundations</a></li> <li><a href='#examples_and_nonexamples'>Examples and non-examples</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#History'>History</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="definition">Definition</h2> <p>Classically, we have:</p> <div class="num_defn"> <p>A <strong>Grothendieck topos</strong> <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{T}</annotation></semantics></math> is a category that admits a <a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>𝒯</mi><mover><mo>↪</mo><mover><mo>←</mo><mi>lex</mi></mover></mover><mi>PSh</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \mathcal{T} \stackrel{\stackrel{lex}{\leftarrow}}{\hookrightarrow} PSh(C) </annotation></semantics></math></div> <p>in a <a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a> category, i.e., a full and faithful functor that has a left exact left adjoint.</p> <p>This is equivalently the <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a> (<a class="existingWikiWord" href="/nlab/show/Set">Set</a>-valued <a class="existingWikiWord" href="/nlab/show/presheaves">presheaves</a> satisfying the sheaf condition) over a <a class="existingWikiWord" href="/nlab/show/small+category">small</a> <a class="existingWikiWord" href="/nlab/show/site">site</a>.</p> </div> <p>See at <em><a class="existingWikiWord" href="/nlab/show/sheaf+toposes+are+equivalently+the+left+exact+reflective+subcategories+of+presheaf+toposes">sheaf toposes are equivalently the left exact reflective subcategories of presheaf toposes</a></em> for discussion of this characterization.</p> <p>Since smallness can be relative, we also have:</p> <div class="num_defn"> <p>For a given fixed <a class="existingWikiWord" href="/nlab/show/ETCS">category of sets</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>, a <strong>Grothendieck topos</strong> over <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> is a <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</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>-valued <a class="existingWikiWord" href="/nlab/show/presheaves">presheaves</a> satisfying the sheaf condition) over a <a class="existingWikiWord" href="/nlab/show/site">site</a> which is <a class="existingWikiWord" href="/nlab/show/small+category">small</a> relative to <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>, that is a site <a class="existingWikiWord" href="/nlab/show/internal+category">internal</a> to <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>.</p> </div> <p>Note that a Grothendieck topos is a <a class="existingWikiWord" href="/nlab/show/topos">topos</a> because (or if) <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> is.</p> <p>The <a class="existingWikiWord" href="/nlab/show/site">site</a> is not considered part of the structure; different sites may give rise to <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> category of sheaves.</p> <p>By the general theory of <a class="existingWikiWord" href="/nlab/show/geometric+morphisms">geometric morphisms</a>, every Grothendieck topos sits inside a category of <a class="existingWikiWord" href="/nlab/show/presheaf">presheaves</a> by a <a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</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>S</mi><mo stretchy="false">)</mo><mo>↪</mo><mi>PSh</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sh(S) \hookrightarrow PSh(S)</annotation></semantics></math>.</p> <ul> <li> <p>This may be taken as an alternative definition of <a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a>: since <a class="existingWikiWord" href="/nlab/show/Lawvere-Tierney+topology">Lawvere-Tierney topologies</a> are bijectively given by <a class="existingWikiWord" href="/nlab/show/geometric+embeddings">geometric embeddings</a>, instead of explicitly defining a sheaf as a presheaf satisfying <a class="existingWikiWord" href="/nlab/show/descent">descent</a>, one may define categories of sheaves as geometric embeddings into presheaf categories.</p> </li> <li> <p>For details on the relation between the two perspectives see <a class="existingWikiWord" href="/nlab/show/geometric+embedding">geometric embedding</a>.</p> </li> <li> <p>This perspective is useful for defining the <a class="existingWikiWord" href="/nlab/show/vertical+categorification">vertical categorification</a> of sheaves: <a class="existingWikiWord" href="/nlab/show/stacks">stacks</a> and <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stacks">∞-stacks</a>: the higher categories of these may be defined as geometric embeddings into higher categories of presheaves. This has been worked out in detail for <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-categories">(∞,1)-categories</a>. See <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category+of+%28%E2%88%9E%2C1%29-sheaves">(∞,1)-category of (∞,1)-sheaves</a>.</p> </li> <li> <p>Sometimes it is useful to distinguish between <a class="existingWikiWord" href="/nlab/show/petit+topos">petit topos</a> and <a class="existingWikiWord" href="/nlab/show/gros+topos">gros topos</a>.</p> </li> </ul> <h2 id="properties">Properties</h2> <h3 id="general">General</h3> <div class="num_prop" id="LocallyPresentable"> <h6 id="proposition">Proposition</h6> <p>Every Grothendieck topos is a <a class="existingWikiWord" href="/nlab/show/locally+presentable+category">locally presentable category</a>.</p> </div> <p>(<a href="#Borceux94">Borceux 94, vol 3, prop. 3.4.16</a>)</p> <div class="num_prop" id="total"> <h6 id="proposition_2">Proposition</h6> <p>Every Grothendieck topos is a <a class="existingWikiWord" href="/nlab/show/total+category">total category</a> and a <a class="existingWikiWord" href="/nlab/show/cototal+category">cototal category</a>.</p> </div> <div class="proof"> <h6 id="proof">Proof</h6> <p>From the page <a class="existingWikiWord" href="/nlab/show/total+category">total category</a>, totality follows from the fact that a Grothendieck topos is</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/cocomplete+category">Cocomplete</a>,</li> <li><a class="existingWikiWord" href="/nlab/show/well-powered+category">Well-copowered</a> (because <a class="existingWikiWord" href="/nlab/show/quotient">quotient</a> objects of an <a class="existingWikiWord" href="/nlab/show/object">object</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> are in <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relations">equivalence relations</a> on <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 there is a <a class="existingWikiWord" href="/nlab/show/small+set">small set</a> of these because a Grothendieck topos is well-powered), and</li> <li>Has a <a class="existingWikiWord" href="/nlab/show/generator">generator</a> (e.g., the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> of all <a class="existingWikiWord" href="/nlab/show/representable+functor">representables</a> for a <a class="existingWikiWord" href="/nlab/show/small+site">small site</a> presentation).</li> </ul> <p>Dually, a Grothendieck topos is</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/complete+category">Complete</a>,</li> <li><a class="existingWikiWord" href="/nlab/show/well-powered+category">Well-powered</a> (because <a class="existingWikiWord" href="/nlab/show/subobjects">subobjects</a> of an <a class="existingWikiWord" href="/nlab/show/object">object</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> are in <a class="existingWikiWord" href="/nlab/show/bijection">bijection</a> with elements of a <a class="existingWikiWord" href="/nlab/show/small+set">small</a> <a class="existingWikiWord" href="/nlab/show/hom-set">hom-set</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>Ω</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\hom(X, \Omega)</annotation></semantics></math>), and</li> <li>Has a <a class="existingWikiWord" href="/nlab/show/cogenerator">cogenerator</a> (e.g., the <a class="existingWikiWord" href="/nlab/show/product">product</a> of <a class="existingWikiWord" href="/nlab/show/power+objects">power objects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>Ω</mi> <mi>c</mi></msup></mrow><annotation encoding="application/x-tex">\Omega^c</annotation></semantics></math> where <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> ranges over representables for a small site presentation).</li> </ul> <p>Therefore a Grothendieck topos is also cototal.</p> </div> <h3 id="Giraud">Giraud's axiomatic characterization</h3> <p>Giraud characterized Grothendieck toposes as categories satisfying certain <a class="existingWikiWord" href="/nlab/show/exactness+property">exactness</a> and <a class="existingWikiWord" href="/nlab/show/small+set">small</a> <a class="existingWikiWord" href="/nlab/show/complete+category">completeness</a> properties (where “small” is again relative to the given category of sets <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>). The exactness properties are elementary (not depending on <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>), and are satisfied in any elementary <a class="existingWikiWord" href="/nlab/show/topos">topos</a>, or even a <a class="existingWikiWord" href="/nlab/show/pretopos">pretopos</a>.</p> <p><a class="existingWikiWord" href="/nlab/show/Giraud%27s+theorem">Giraud's theorem</a> characterises a Grothendieck topos as follows:</p> <ol> <li>a <a class="existingWikiWord" href="/nlab/show/locally+small">locally small</a> <a class="existingWikiWord" href="/nlab/show/category">category</a> with a small <a class="existingWikiWord" href="/nlab/show/generating+set">generating set</a>,</li> <li>with all finite <a class="existingWikiWord" href="/nlab/show/limits">limits</a>,</li> <li>with all small <a class="existingWikiWord" href="/nlab/show/coproducts">coproducts</a>, which are <a class="existingWikiWord" href="/nlab/show/disjoint+coproduct">disjoint</a>, and <a class="existingWikiWord" href="/nlab/show/pullback+stability">pullback-stable</a>,</li> <li>where all <a class="existingWikiWord" href="/nlab/show/congruences">congruences</a> have effective <a class="existingWikiWord" href="/nlab/show/quotient+objects">quotient objects</a>, which are also pullback-stable.</li> </ol> <p>These conditions are equivalent to</p> <ul> <li>a <a class="existingWikiWord" href="/nlab/show/locally+small">locally small</a> <a class="existingWikiWord" href="/nlab/show/infinitary+pretopos">infinitary pretopos</a> with a small generating set.</li> </ul> <p>See the <a class="existingWikiWord" href="/nlab/show/Elephant">Elephant</a>, theorem C.2.2.8. (There, the assumption of local smallness is not stated explicitly, but it is included in the definition of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-pretopos by way of <a class="existingWikiWord" href="/nlab/show/well-powered+category">well-poweredness</a>; on the nLab it is not so included, so we have to state it explicitly. To see that it is necessary, note that 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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/Grothendieck+universes">Grothendieck universes</a> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">U\in V</annotation></semantics></math>, then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mi>V</mi></msub></mrow><annotation encoding="application/x-tex">Set_V</annotation></semantics></math> satisfies all the other conditions relative to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mi>U</mi></msub></mrow><annotation encoding="application/x-tex">Set_U</annotation></semantics></math>, but is not locally small and is not a Grothendieck topos.) See also <a href="https://secure.wikimedia.org/wikipedia/en/wiki/Topos#Giraud.27s_axioms">Wikipedia</a>.</p> <p>Sometimes (3,4) are combined and strengthened to the statement that the category has all small <a class="existingWikiWord" href="/nlab/show/colimits">colimits</a>, which are effective and pullback-stable. However, this is a mistake for two reasons: it is a significantly stronger axiomatisation (since without the small generating set, not every infinitary pretopos has this property), and it is not valid in weak foundations (while the definition given above is).</p> <h3 id="Streetcharacterization">Street’s axiomatic characterization</h3> <p>Augmenting the aforementioned Proposition <a class="maruku-ref" href="#total"></a> that Grothendieck toposes are total categories, <a href="#Street">Street</a> more or less characterizes Grothendieck toposes as <em>lex total</em> categories having the same “size” as <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>.</p> <p>In more detail: we take as background set theory ZFC + “there is a strongly inaccessible cardinal” <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>; equivalently, the existence of a single <a class="existingWikiWord" href="/nlab/show/Grothendieck+universe">Grothendieck universe</a> <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> (a set of “small sets”). Supposing given a model <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ZFC</mi><mo>+</mo><mi>universe</mi></mrow><annotation encoding="application/x-tex">ZFC+universe</annotation></semantics></math>, “category” shall then refer to category theory interpreted in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>. Let <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> be the category of small sets; note that the set of morphisms of <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> 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>.</p> <p>Recall that locally small category <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 <a class="existingWikiWord" href="/nlab/show/lex+total+category">lex total</a> if the <a class="existingWikiWord" href="/nlab/show/Yoneda+embedding">Yoneda embedding</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>E</mi><mo>→</mo><mo stretchy="false">[</mo><msup><mi>E</mi> <mi>op</mi></msup><mo>,</mo><mi>Set</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">y: E \to [E^{op}, Set]</annotation></semantics></math> 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 class="num_theorem"> <h6 id="theorem">Theorem</h6> <p><strong>(Street)</strong> A category <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 a Grothendieck topos iff it is lex total and the size of the set of isomorphism classes of objects is <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> or less.</p> </div> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>This result is in the spirit of saying “every Grothendieck topos is the category of <a class="existingWikiWord" href="/nlab/show/sheaves">sheaves</a> with respect to the <a class="existingWikiWord" href="/nlab/show/canonical+topology">canonical topology</a> on itself”. Putting aside set-theoretic issues, it suggests that Grothendieck toposes be seen as analogous to <a class="existingWikiWord" href="/nlab/show/frames">frames</a>, which may be defined as lex total objects in <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>-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>. In this setting, the appropriate morphisms are left exact left adjoints, so that Grothendieck toposes and <a class="existingWikiWord" href="/nlab/show/geometric+morphisms">geometric morphisms</a> between them would be analogous to <a class="existingWikiWord" href="/nlab/show/locales">locales</a> and <a class="existingWikiWord" href="/nlab/show/continuous+maps">continuous maps</a> between them.</p> <p>One can deduce formally that lex total categories are <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed</a> <a class="existingWikiWord" href="/nlab/show/Heyting+pretoposes">Heyting pretoposes</a>.</p> </div> <h3 id="as_lex_reflections_of_categories_of_presheaves">As lex reflections of categories of presheaves</h3> <p><a class="existingWikiWord" href="/nlab/show/sheaf+toposes+are+equivalently+the+left+exact+reflective+subcategories+of+presheaf+toposes">sheaf toposes are equivalently the left exact reflective subcategories of presheaf toposes</a></p> <h3 id="AsLocalicGroupoids">As localic groupoids</h3> <p>Every Grothendieck topos is equivalent to the <a class="existingWikiWord" href="/nlab/show/classifying+topos+of+a+localic+groupoid">classifying topos of a localic groupoid</a>, every Grothendieck topos <a class="existingWikiWord" href="/nlab/show/point+of+a+topos">with enough points</a> is equivalent to the classifying topos of a <a class="existingWikiWord" href="/nlab/show/topological+groupoid">topological groupoid</a>, and in fact the 2-category <a class="existingWikiWord" href="/nlab/show/Topos">Topos</a> of Grothendieck toposes is equivalent to a localization of that of <a class="existingWikiWord" href="/nlab/show/localic+groupoids">localic groupoids</a>.</p> <p>See at <em><a class="existingWikiWord" href="/nlab/show/classifying+topos+of+a+localic+groupoid">classifying topos of a localic groupoid</a></em> for more.</p> <h3 id="internal_logic">Internal logic</h3> <p>Being an <a class="existingWikiWord" href="/nlab/show/elementary+topos">elementary topos</a>, a Grothendieck topos has an <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> that can be taken to be <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a> or a form of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>. It is also useful to take its internal <a class="existingWikiWord" href="/nlab/show/geometric+logic">geometric logic</a>, in particular because that is preserved by <a class="existingWikiWord" href="/nlab/show/geometric+morphisms">geometric morphisms</a> and because every geometric theory has a Grothendieck <a class="existingWikiWord" href="/nlab/show/classifying+topos">classifying topos</a>.</p> <p>Although the internal logic of a Grothendieck topos is <a class="existingWikiWord" href="/nlab/show/constructive+logic">constructive logic</a>, there are a number of principles that are true in every Grothendieck topos (at least, assuming the base topos <a class="existingWikiWord" href="/nlab/show/Set">Set</a> is <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical</a>) but are not constructively provable (and in particular can fail in other toposes). Roughly speaking, many of these axioms assert that classicality fails “in only a <a class="existingWikiWord" href="/nlab/show/small+category">small</a> way”. These include:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/WISC">WISC</a>: every set has a weakly initial set of covers.</li> <li>The (constructive) <a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a> (AMC).</li> <li>The <a class="existingWikiWord" href="/nlab/show/axiom+of+stack+completions">axiom of stack completions</a>.</li> <li>(allegedly) the local <a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a> (SCSA).</li> <li>Every <a class="existingWikiWord" href="/nlab/show/complete+small+category">complete small category</a> is a preorder.</li> </ul> <h3 id="2monadicity_over_locally_presentable_categories">2-monadicity over locally presentable categories</h3> <p>The <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> of Grothendieck toposes and <a class="existingWikiWord" href="/nlab/show/logical+morphisms">logical morphisms</a> is <a class="existingWikiWord" href="/nlab/show/2-monad">2-monadic</a> over the 2-category of <a class="existingWikiWord" href="/nlab/show/locally+presentable+categories">locally presentable categories</a> and <a class="existingWikiWord" href="/nlab/show/cocontinuous+functors">cocontinuous functors</a>. This is proven in <a href="#BungeCarboni1995">Bunge and Carboni 1995</a>. See <a class="existingWikiWord" href="/nlab/show/symmetric+topos">symmetric topos</a> for more details.</p> <h3 id="enrichment_over_accessible_categories_with_directed_colimits">Enrichment over accessible categories with directed colimits</h3> <p>The <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> of Grothendieck toposes and <a class="existingWikiWord" href="/nlab/show/geometric+morphisms">geometric morphisms</a> is <a class="existingWikiWord" href="/nlab/show/enriched+bicategory">enriched as a bicategory</a> over the 2-category of <a class="existingWikiWord" href="/nlab/show/accessible+categories">accessible categories</a> with <a class="existingWikiWord" href="/nlab/show/directed+colimits">directed colimits</a> (note that accessible categories always have <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>-filtered colimits for some cardinal <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>, but not necessarily directed colimits unless they are <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ω</mi></mrow><annotation encoding="application/x-tex">\omega</annotation></semantics></math>-accessible) and functors preserving <a class="existingWikiWord" href="/nlab/show/directed+colimits">directed colimits</a>. This is proven in <a href="#DiLiberti22">Di Liberti 2022</a>.</p> <h2 id="in_weak_foundations">In weak foundations</h2> <p>We have two definitions of a Grothendieck topos:</p> <ul> <li>the category of sheaves on some small site,</li> <li>a category that satisfies Giraud's axioms (as listed above).</li> </ul> <p>The theorem that these are equivalent can be proved in quite weak foundations, whether <a class="existingWikiWord" href="/nlab/show/finitist+mathematics">finitist</a>, <a class="existingWikiWord" href="/nlab/show/predicative+mathematics">predicative</a>, or <a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive</a> (or all three at once), as long as we axiomatize correctly given the caveats listed in the previous section. Some hard-nosed predicativists (and even hard-nosed ZFC fundamentalists) may object to the language (on the ground that large categories such as <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> and other nontrivial Grothendieck toposes don't really exist), but they should accept the theorems when suitably phrased.</p> <p>In predicative mathematics, however, we cannot prove that every Grothendieck topos is in fact a <a class="existingWikiWord" href="/nlab/show/topos">topos</a>! In fact, it is immediate that <a class="existingWikiWord" href="/nlab/show/the+category+of+sets">the category of sets</a> is a Grothendieck topos, but <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 an elementary topos if and only if <a class="existingWikiWord" href="/nlab/show/power+sets">power sets</a> are small, which is precisely what predicativists doubt. One can use the term <strong>Grothendieck pretopos</strong> to avoid implying that we have an elementary topos. On the other hand, since Grothendeick toposes came first, perhaps it is the definition of ‘elementary topos’ that is too strong.</p> <p>Similarly, in finitist mathematics, we cannot prove that every Grothendieck topos has a <a class="existingWikiWord" href="/nlab/show/natural+numbers+object">natural numbers object</a>; while in strongly predicative mathematics, we cannot prove that every Grothendieck topos is <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed</a>. In each case, once a property is accepted of <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> (the <a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a> and small <a class="existingWikiWord" href="/nlab/show/function+sets">function sets</a>, in these examples), it can be proved for all Grothendieck toposes.</p> <p>Constructivism as such is irrelevant; even in <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, most Grothendieck toposes are not <a class="existingWikiWord" href="/nlab/show/boolean+topos">boolean</a>. However, for an analogous result, try the theorem that the <a class="existingWikiWord" href="/nlab/show/category+of+presheaves">category of presheaves</a> on a <a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a> (and hence any category of sheaves contained within it) is boolean. (Again, <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> itself is an example of this.)</p> <p>The theorem that every Grothendieck topos is <a class="existingWikiWord" href="/nlab/show/cocomplete+category">cocomplete</a> is a subtle point; it fails only in finitist predicative mathematics. (The key point in the proof is to generate the <a class="existingWikiWord" href="/nlab/show/transitive+relation">transitive closure</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mo>∼</mo> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">\sim^*</annotation></semantics></math> of a binary relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math>. One proof defines <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><msup><mo>∼</mo> <mo>*</mo></msup><mi>b</mi></mrow><annotation encoding="application/x-tex">a \sim^* b</annotation></semantics></math> to mean that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∼</mo><msub><mi>x</mi> <mn>0</mn></msub><mo>∼</mo><mi>⋯</mi><mo>∼</mo><msub><mi>x</mi> <mrow><mi>n</mi><mo>−</mo><mn>1</mn></mrow></msub><mo>∼</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \sim x_0 \sim \cdots \sim x_{n-1} \sim b</annotation></semantics></math> for some <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>, which is predicative but infinitary; another defines <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><msup><mo>∼</mo> <mo>*</mo></msup><mi>b</mi></mrow><annotation encoding="application/x-tex">a \sim^* b</annotation></semantics></math> to mean that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∼</mo><mo>′</mo><mi>b</mi></mrow><annotation encoding="application/x-tex">a \sim' b</annotation></semantics></math> for every transitive relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo><mo>′</mo></mrow><annotation encoding="application/x-tex">\sim'</annotation></semantics></math> that contains <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∼</mo></mrow><annotation encoding="application/x-tex">\sim</annotation></semantics></math>, which is finitary but impredicative.)</p> <h2 id="examples_and_nonexamples">Examples and non-examples</h2> <p>By definition, every <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a> is a Grothendieck topos. Examples include:</p> <ul> <li> <p>Every <a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a> category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSh</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>=</mo><msup><mi>Set</mi> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex">PSh(C) = Set^{C^{op}}</annotation></semantics></math> is a Grothendieck topos.</p> </li> <li> <p>In particular <a class="existingWikiWord" href="/nlab/show/Set">Set</a> is a Grothendieck topos, because it is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>PSh</mi><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">PSh(\ast)</annotation></semantics></math>.</p> </li> <li> <p>Broadly, most of the <a class="existingWikiWord" href="/nlab/show/toposes">toposes</a> that people have worked with are Grothendieck.</p> </li> </ul> <p>On the other hand, there are <a class="existingWikiWord" href="/nlab/show/topos#ElementaryTopos">(elementary) toposes</a> that fail to be Grothendieck toposes:</p> <ul> <li> <p>Because a Grothendieck topos <a class="existingWikiWord" href="/nlab/show/complete+category">has all small limits</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinSet</mi></mrow><annotation encoding="application/x-tex">FinSet</annotation></semantics></math> is not Grothendieck.</p> </li> <li> <p>More generally, the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mrow><mo><</mo><mi>π</mi></mrow></msub></mrow><annotation encoding="application/x-tex">Set_{\lt \pi}</annotation></semantics></math> of sets with <a class="existingWikiWord" href="/nlab/show/cardinality">cardinality</a> below any bound <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> is not a Grothendieck topos, even when <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/strong+limit+cardinal">strong limit cardinal</a> so that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Set</mi> <mrow><mo><</mo><mi>π</mi></mrow></msub></mrow><annotation encoding="application/x-tex">Set_{\lt \pi}</annotation></semantics></math> is an (elementary) topos.</p> </li> <li> <p>Similarly, any category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>FinSet</mi> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msup></mrow><annotation encoding="application/x-tex">FinSet^{C^{op}}</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinSet</mi></mrow><annotation encoding="application/x-tex">FinSet</annotation></semantics></math>-valued presheaves is a topos but not a Grothendieck topos, and the same goes more generally for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>Set</mi> <mrow><mo><</mo><mi>π</mi></mrow> <mrow><msup><mi>C</mi> <mi>op</mi></msup></mrow></msubsup></mrow><annotation encoding="application/x-tex">Set_{\lt \pi}^{C^{op}}</annotation></semantics></math> for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>π</mi></mrow><annotation encoding="application/x-tex">\pi</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/strong+limit+cardinal">strong limit cardinal</a>.</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a>, the maps in which can be thought of as computable functions, is not Grothendieck.</p> </li> <li> <p>Other non-Grothendieck toposes occur in the topos-theoretic approach to <a class="existingWikiWord" href="/nlab/show/nonstandard+analysis">nonstandard analysis</a>.</p> </li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a></p> <ul> <li> <p><strong>Grothendieck topos</strong>, <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/geometric+logic">geometric logic</a>, <a class="existingWikiWord" href="/nlab/show/geometric+type+theory">geometric type theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-topos">2-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf+%28%E2%88%9E%2C1%29-topos">(∞,1)-sheaf (∞,1)-topos</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lex+total+category">lex total category</a></p> </li> </ul> <div> <p><strong>Locally presentable categories:</strong> <a class="existingWikiWord" href="/nlab/show/cocomplete+category">Cocomplete</a> possibly-<a class="existingWikiWord" href="/nlab/show/large+categories">large categories</a> generated under <a class="existingWikiWord" href="/nlab/show/filtered+colimits">filtered colimits</a> by <a class="existingWikiWord" href="/nlab/show/small+object">small</a> <a class="existingWikiWord" href="/nlab/show/generators">generators</a> under <a class="existingWikiWord" href="/nlab/show/small+colimit">small</a> <a class="existingWikiWord" href="/nlab/show/relations">relations</a>. Equivalently, <a class="existingWikiWord" href="/nlab/show/accessible+functor">accessible</a> <a class="existingWikiWord" href="/nlab/show/reflective+localizations">reflective localizations</a> of <a class="existingWikiWord" href="/nlab/show/free+cocompletions">free cocompletions</a>. Accessible categories omit the cocompleteness requirement; toposes add the requirement of a <a class="existingWikiWord" href="/nlab/show/left+exact+functor">left exact</a> localization.</p> <table><thead><tr><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/%28n%2Cr%29-categories">(n,r)-categories</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></th><th><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/toposes">toposes</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mphantom><mi>A</mi></mphantom></mrow><annotation encoding="application/x-tex">\phantom{A}</annotation></semantics></math></th><th>locally presentable</th><th>loc finitely pres</th><th>localization theorem</th><th><a class="existingWikiWord" href="/nlab/show/free+cocompletion">free cocompletion</a></th><th>accessible</th></tr></thead><tbody><tr><td style="text-align: left;"><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category+theory">(0,1)-category theory</a></strong></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/locales">locales</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/suplattice">suplattice</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/algebraic+lattices">algebraic lattices</a></td><td style="text-align: left;"><a href="algebraic+lattice#RelationToLocallyFinitelyPresentableCategories">Porst’s theorem</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/powerset">powerset</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/poset">poset</a></td></tr> <tr><td style="text-align: left;"><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Grothendieck+topos">toposes</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/locally+presentable+categories">locally presentable categories</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/locally+finitely+presentable+categories">locally finitely presentable categories</a></td><td style="text-align: left;"><a href="locally+presentable+category#AsLocalizationsOfPresheafCategories">Gabriel–Ulmer’s theorem</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/presheaf+category">presheaf category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/accessible+categories">accessible categories</a></td></tr> <tr><td style="text-align: left;"><strong><a class="existingWikiWord" href="/nlab/show/model+category">model category theory</a></strong></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/model+toposes">model toposes</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/combinatorial+model+categories">combinatorial model categories</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Dugger%27s+theorem">Dugger's theorem</a></td><td style="text-align: left;">global <a class="existingWikiWord" href="/nlab/show/model+structures+on+simplicial+presheaves">model structures on simplicial presheaves</a></td><td style="text-align: left;">n/a</td></tr> <tr><td style="text-align: left;"><strong><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category+theory">(∞,1)-category theory</a></strong></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-toposes">(∞,1)-toposes</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/locally+presentable+%28%E2%88%9E%2C1%29-categories">locally presentable (∞,1)-categories</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a href="locally+presentable+infinity-category#Definition">Simpson’s theorem</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-presheaf+%28%E2%88%9E%2C1%29-categories">(∞,1)-presheaf (∞,1)-categories</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/accessible+%28%E2%88%9E%2C1%29-categories">accessible (∞,1)-categories</a></td></tr> </tbody></table> </div> <h2 id="History">History</h2> <p>From <a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a> (sent to the <a href="https://www.mta.ca/~cat-dist/">Categories mailing list</a> on Apr 14, 2018):</p> <blockquote> <p>At the start of 1958 <a class="existingWikiWord" href="/nlab/show/Grothendieck">Grothendieck</a> believed the correct <a class="existingWikiWord" href="/nlab/show/Weil+cohomology">Weil cohomology</a> of a <a class="existingWikiWord" href="/nlab/show/scheme">scheme</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> would be the <a class="existingWikiWord" href="/nlab/show/abelian+sheaf+cohomology">derived functor cohomology</a> of some <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ab(S)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/sheaf+of+abelian+groups">sheaves of Abelian groups</a> on <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> —and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ab</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ab(S)</annotation></semantics></math> was likely to be the category of all Abelian <a class="existingWikiWord" href="/nlab/show/group+objects">group objects</a> in some <a class="existingWikiWord" href="/nlab/show/category+of+sheaves">category of sheaves</a> of <a class="existingWikiWord" href="/nlab/show/sets">sets</a> on <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>. He had no name yet for such conjectural categories of sheaves of sets but for later reference I will call this category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(S)</annotation></semantics></math>. It would require some new notion of sheaves of sets more general than the existing notion using topological spaces. He had no concrete idea what this new notion of sheaf might be. His experience in Kansas in 1955 suggested it was likely to come from some new notion of espace etale over a scheme. and it should have some good exactness properties.</p> <p>On April 21, 1958 Grothendieck went to the Seminaire Chevalley to hear <a class="existingWikiWord" href="/nlab/show/Serre">Serre</a> describe isotrivial fiber bundles on a variety V, which are bundles that become trivial when pulled back to some surjective family of finite, unramified maps to V. Serre showed this gave the expected one-dimensional Weil cohomology groups of V. Grothendieck immediately told Serre it would work in all dimensions–which Serre found “very optimistic”“ at the time.</p> <p>All of this is well documented in familiar sources.</p> <p>Grothendieck’s 1973 topos lectures in Buffalo show that during Serre’s talk Grothendieck saw the Weil espaces etales over a scheme <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> should be patched together from Serre’s unramified maps to <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>. That is, the sought category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(S)</annotation></semantics></math> of sheaves of sets on S should be generated by the unramified maps to S, and should have arbitrary colimits of these, and finite limits. He first sought to axiomatize this roughly the way his Tohoku paper had axiomatized sheaves of groups.</p> <p>A few changes came soon: He realized finite unramified maps should be replaced by flat unramified maps (just as topological espaces etales are trivial locally in the fiber and not on the base). He abandoned the axiomatic approach to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>S</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(S)</annotation></semantics></math> as too vague and shifted to construction by sites. And for sites he began treating sheaves as a kind of functor, rather than as espaces etales. Only after the notion ot site developed would Giraud give his topos axioms, and no one has yet really taken a precise notion of espace etale much beyond the topological case.</p> <p>But April 21 1958 was the birth of <a class="existingWikiWord" href="/nlab/show/topos+theory">topos theory</a>. The term topos came later. (Lots of people are not named on the day they are born.)</p> <p>As of the summer of 1973 Grothendieck’s stated preferred definition of topos was still: a category with arbitrary <a class="existingWikiWord" href="/nlab/show/colimits">colimits</a>, <a class="existingWikiWord" href="/nlab/show/finite+limits">finite limits</a>, and a small generating set. He says over and over this is not quite adequate for proofs. He says proofs require the notion of <a class="existingWikiWord" href="/nlab/show/site">site</a>, or else the <a class="existingWikiWord" href="/nlab/show/Giraud+axioms">Giraud axioms</a>, but he calls the vaguer idea more intuitive and says that is the way to think about a topos.</p> <p>Also in 1973 Grothendieck says the objects in any topos should be seen as <a class="existingWikiWord" href="/nlab/show/espaces+etales">espaces etales</a> over the <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> of the topos, in a generalized sense that includes saying any orbit of a group action lies “etale” over a <a class="existingWikiWord" href="/nlab/show/fixed+point">fixed point</a>. Today, it is not obvious that this can work well in general. In <a class="existingWikiWord" href="/nlab/show/SGA4">SGA4</a> Grothendieck had already given evidence that it would work for <a class="existingWikiWord" href="/nlab/show/petit+topos">petit topos</a> but not <a class="existingWikiWord" href="/nlab/show/gros+topos">gros topos</a>. But still in 1973 he did say it. And it works perfectly for petit etale toposes—as long as we generalize the notion of espace etale to include a Galois orbit (in an extension field) lying over a single point (in the ground field).</p> </blockquote> <h2 id="references">References</h2> <p>Basic exposition:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Michael+Barr">Michael Barr</a>, <a class="existingWikiWord" href="/nlab/show/Colin+McLarty">Colin McLarty</a>, <a class="existingWikiWord" href="/nlab/show/Charles+Wells">Charles Wells</a>, <em>Variable set theory</em>, prepared for <em>Scientific American</em> but unpublished (~1985) [<a href="https://www.math.mcgill.ca/barr/papers/vst.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/BarrMcLartyWells-VariableSetTheory.pdf" title="pdf">pdf</a>]</li> </ul> <p>A quick introduction of the basic facts of sheaf-topos theory is chapter I, “Background in topos theory” in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Ieke+Moerdijk">Ieke Moerdijk</a>, <em>Classifying Spaces and Classifying Topoi</em> Lecture Notes in Mathematics 1616, Springer (1995)</li> </ul> <p>Textbook accounts include</p> <ul> <li id="Borceux94"> <p><a class="existingWikiWord" href="/nlab/show/Francis+Borceux">Francis Borceux</a>, vol 3 of <em><a class="existingWikiWord" href="/nlab/show/Handbook+of+Categorical+Algebra">Handbook of Categorical Algebra</a></em>, Cambridge University Press (1994)</p> </li> <li> <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> </ul> <p>Grothendieck topoi appear around section III,4 there. A proof of Giraud’s theorem is in appendix A.</p> <p>The proof of Giraud’s theorem for <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topoi">(∞,1)-topoi</a> is section 6.1.5 of</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Jacob+Lurie">Jacob Lurie</a>, <em><a class="existingWikiWord" href="/nlab/show/Higher+Topos+Theory">Higher Topos Theory</a></em></li> </ul> <p>Street’s characterization of Grothendieck toposes is given in</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; MR83a:18014. (<a href="http://journals.cambridge.org/download.php?file=%2FBAZ%2FBAZ23_02%2FS000497270000705Xa.pdf&code=c6248e4fa6a517c9bb451e4f5abcf862">pdf link</a>)</li> </ul> <p>These are also called Giraud frames in</p> <ul> <li id="Vickers22"><a class="existingWikiWord" href="/nlab/show/Steven+Vickers">Steven Vickers</a>, <em>Generalized point-free spaces, pointwise</em> [<a href="https://arxiv.org/abs/2206.01113">arXiv:2206.01113</a>]</li> </ul> <p>On 2-monadicity of the opposite of the 2-category of Grothendieck toposes:</p> <ul> <li id="BungeCarboni1995"><a class="existingWikiWord" href="/nlab/show/Marta+Bunge">Marta Bunge</a>, <a class="existingWikiWord" href="/nlab/show/Aurelio+Carboni">Aurelio Carboni</a>, <em>The Symmetric Topos</em> , JPAA <strong>105</strong> (1995) pp.233-249.</li> </ul> <p>On enrichment of the 2-category of Grothendieck toposes:</p> <ul> <li id="DiLiberti2022"><a class="existingWikiWord" href="/nlab/show/Ivan+Di+Liberti">Ivan Di Liberti</a>, <em>General facts on the Scott Adjunction</em>, Applied Categorical Structures 30.3 (2022): 569-591.</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on April 30, 2024 at 19:44:02. See the <a href="/nlab/history/Grothendieck+topos" 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/Grothendieck+topos" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/6753/#Item_32">Discuss</a><span class="backintime"><a href="/nlab/revision/Grothendieck+topos/64" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/Grothendieck+topos" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/Grothendieck+topos" accesskey="S" class="navlink" id="history" rel="nofollow">History (64 revisions)</a> <a href="/nlab/show/Grothendieck+topos/cite" style="color: black">Cite</a> <a href="/nlab/print/Grothendieck+topos" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/Grothendieck+topos" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>