\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{local geometric morphism} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory} [[!include topos theory - contents]] \hypertarget{discrete_and_concrete_objects}{}\paragraph*{{Discrete and concrete objects}}\label{discrete_and_concrete_objects} [[!include discrete and concrete objects - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{local_geometric_morphism_and_relative_local_topos}{Local geometric morphism and relative local topos}\dotfill \pageref*{local_geometric_morphism_and_relative_local_topos} \linebreak \noindent\hyperlink{LocalTopos}{Local topos}\dotfill \pageref*{LocalTopos} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{EquivalentCharacterizations}{Equivalent characterizations}\dotfill \pageref*{EquivalentCharacterizations} \linebreak \noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak \noindent\hyperlink{HomotopyDimension}{Homotopy dimension}\dotfill \pageref*{HomotopyDimension} \linebreak \noindent\hyperlink{concrete_sheaves}{Concrete sheaves}\dotfill \pageref*{concrete_sheaves} \linebreak \noindent\hyperlink{homotopy_equivalence}{Homotopy equivalence}\dotfill \pageref*{homotopy_equivalence} \linebreak \noindent\hyperlink{ElementaryAxiomatization}{Elementary Axiomatization}\dotfill \pageref*{ElementaryAxiomatization} \linebreak \noindent\hyperlink{SetupForAxiomatization}{The setup}\dotfill \pageref*{SetupForAxiomatization} \linebreak \noindent\hyperlink{the_axioms}{The axioms}\dotfill \pageref*{the_axioms} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{EasyExamples}{Easy examples}\dotfill \pageref*{EasyExamples} \linebreak \noindent\hyperlink{sheaves_on_a_local_site}{Sheaves on a local site}\dotfill \pageref*{sheaves_on_a_local_site} \linebreak \noindent\hyperlink{relative_realizability}{Relative Realizability}\dotfill \pageref*{relative_realizability} \linebreak \noindent\hyperlink{localization}{Localization}\dotfill \pageref*{localization} \linebreak \noindent\hyperlink{LocalOverTopoes}{Local over-toposes}\dotfill \pageref*{LocalOverTopoes} \linebreak \noindent\hyperlink{gros_toposes}{Gros toposes}\dotfill \pageref*{gros_toposes} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} \hypertarget{local_geometric_morphism_and_relative_local_topos}{}\subsubsection*{{Local geometric morphism and relative local topos}}\label{local_geometric_morphism_and_relative_local_topos} \begin{defn} \label{}\hypertarget{}{} A \textbf{local geometric morphism} $f : E \to S$ between [[topos]]es $E,S$ is \begin{itemize}% \item a [[geometric morphism]] \begin{displaymath} (f^* \dashv f_*) \colon E \stackrel{\overset{f^*}{\leftarrow}}{\underset{f_*} {\to}} S \end{displaymath} \item such that a further [[right adjoint]] $f^! : S \to E$ exists \begin{displaymath} (f^* \dashv f_* \dashv f^!) : E \stackrel{\overset{f^*}{\longleftarrow}}{\stackrel{\underset{f_*}{\longrightarrow}}{\underset{f^!}{\longleftarrow}}} S \end{displaymath} \item and such that one, hence all, of the following equivalent conditions hold: \begin{enumerate}% \item The right adjoint $f^!$ is an $S$-[[indexed functor]]. \item $f$ is [[connected geometric morphism|connected]], i.e. $f^*$ is [[full and faithful functor|fully faithful]]. \item The right adjoint $f^!$ is fully faithful. \item The right adjoint $f^!$ is [[cartesian closed functor|cartesian closed]]. \end{enumerate} \end{itemize} \end{defn} When we regard $E$ as a topos over $S$, so that $f$ is regarded as its [[global section]] geometric morphism in the category of toposes over $S$, then we say that $E$ is a \textbf{local $S$-topos}. In this case we may label the functors involved as \begin{displaymath} (Disc \dashv \Gamma \dashv Codisc) : E \stackrel{\overset{Disc}{\longleftarrow}}{\stackrel{\underset{\Gamma}{\longrightarrow}}{\underset{Codisc}{\longleftarrow}}} S \end{displaymath} to indicate that if we think of $\Gamma$ as sending a [[space]] to its underlying $S$-object of points by forgetting [[cohesive topos|cohesion]], then $Disc$ creates the [[discrete space]]/[[discrete object]] and $Codisc$ the [[codiscrete space]]/[[codiscrete object]] on an object in $S$. This is especially common when $S=$ [[Set]], in which case the final condition is automatic since all functors are $Set$-indexed. Hence in that case we have the following simpler \href{local}{definition}. \hypertarget{LocalTopos}{}\subsubsection*{{Local topos}}\label{LocalTopos} \begin{defn} \label{local}\hypertarget{local}{} A [[sheaf topos]] $\mathcal{T}$ is a \textbf{local topos} if the [[global section]] [[geometric morphism]] $\mathcal{T} \stackrel{\overset{LConst}{\leftarrow}}{\underset{\Gamma}{\to}} Set$ has a further [[right adjoint]] $CoDisc$, making an [[adjoint triple]] $(LConst \dashv \Gamma \dashv CoDisc)$ \begin{displaymath} CoDisc \colon Set \hookrightarrow \mathcal{T}. \end{displaymath} (As just stated, it is automatic in the case over $Set$ that this is furthermore a [[full and faithful functor]].) \end{defn} \begin{remark} \label{}\hypertarget{}{} Another way of stating this is that a Grothendieck topos is local if and only if the terminal object $1$ is [[connected object|connected]] and [[projective object|projective]] (since this means precisely that $\Gamma = \hom(1, -)$ preserves colimits, and therefore has a right adjoint by virtue of an [[adjoint functor theorem]]). Another term for this: we say $1$ is \emph{[[tiny object|tiny]]} ([[atomic object|atomic]]). Notice the similarity to the concept of \emph{[[amazing right adjoint]]} (the difference being that this is a right adjoint not to the external but to the [[internal hom]] out of 1.) \end{remark} Note also that in an infinitary-[[extensive category]] an object is connected as soon as $\hom(X,-)$ preserves \emph{binary} coproducts (see [[connected object]]). Moreover, a coproduct-preserving functor between toposes preserves coequalizers as soon as it preserves epimorphisms, since any coequalizer can be constructed as the quotient of an equivalence relation generated using images and countable coproducts and quotients of equivalence relations are effective. Thus, we can say that a Grothendieck topos is local iff $\hom(1,-)$ preserves binary coproducts and epis. Moreover, a cospan $A \to C \leftarrow B$ in a topos is a coproduct diagram iff $A$ and $B$ are disjoint monos whose union is all of $C$; thus $\hom(1,-)$ preserves binary coproducts as soon as it preserves the initial object and binary unions. This leads to the following equivalent form of ``locality'' that makes sense even for elementary toposes: \begin{defn} \label{}\hypertarget{}{} An [[elementary topos]] $E$ is \emph{local} if the terminal object $1$ is \begin{itemize}% \item nonempty: $1\ncong 0$, \item connected: $1 = p \vee q$ implies $1 = p$ or $1 = q$, and \item projective: every epi $U \to 1$ admits a section $t: 1 \to U$. \end{itemize} \end{defn} \begin{remark} \label{}\hypertarget{}{} Some authors have instead used the term ``local'' to refer just to the condition that $1$ is connected; note this is equivalent to $Sub_E(1)$ being a [[local ring|local rig]]. In his \hyperlink{Awodey}{thesis}, Steve Awodey upgraded this, saying that a topos is \emph{hyperlocal} if both connectivity and projectivity are satisfied. As argued above, for a Grothendieck topos this is slightly \emph{weaker} than locality, although the difference is only in the inclusion of the trivial topos (for if $1\cong 0$ then $E\simeq 1$). Note that a local elementary topos, as defined above, is [[well-pointed topos|constructively well-pointed]] if and only if $1$ is additionally a [[generator]]. \end{remark} \begin{example} \label{}\hypertarget{}{} The [[free topos]] is a local elementary topos. \end{example} \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{EquivalentCharacterizations}{}\subsubsection*{{Equivalent characterizations}}\label{EquivalentCharacterizations} \begin{prop} \label{}\hypertarget{}{} A geometric morphism $f : E \to S$ is local precisely if \begin{enumerate}% \item there exists a geometric morphism $c : S \to E$ such that $f \circ c \simeq id$; \item for every other geometric morphism $g : G \to S$ the composite $c\circ g$ is an [[initial object]] in the hom-category $Topos_{/S}(g,f)$ of the [[slice category|slice]] [[2-category]] of [[Topos]] over $S$. \end{enumerate} \end{prop} This is (\hyperlink{Johnstone}{Johnstone, theorem 3.6.1 vi)}). \begin{remark} \label{}\hypertarget{}{} In particular this means that the category of [[topos points]] of a local topos has a [[contractible]] [[nerve]]. \end{remark} \hypertarget{general}{}\subsubsection*{{General}}\label{general} \begin{prop} \label{}\hypertarget{}{} The [[global section]] geometric morphism of any local $\mathcal{S}$-topos (over a [[base topos]] $\mathcal{S}$) is a [[Grothendieck fibration]] and a [[Grothendieck opfibration]]. \end{prop} This appears in (\hyperlink{Shulman}{Shulman}). \begin{prop} \label{}\hypertarget{}{} The [[Freyd cover]] of a [[topos]] is a [[local topos]], and in fact freely so. Every local topos is a [[retract]] of a Freyd cover. \end{prop} This appears as (\hyperlink{Johnstone}{Johnstone, lemma C3.6.4}). \hypertarget{HomotopyDimension}{}\subsubsection*{{Homotopy dimension}}\label{HomotopyDimension} \begin{prop} \label{}\hypertarget{}{} In a local [[sheaf topos]] over [[Set]], every [[inhabited object]] is globally inhabited: every object $X$ for which the unique morphism $X \to *$ to the [[terminal object]] is an [[epimorphism]] has a [[global point]] $* \to X$. \end{prop} \begin{proof} Since in a local topos the [[global section]] functor $\Gamma$ is a [[left adjoint]], it preserves [[epimorphisms]]. Since it is a right adjoint it preserves the terminal object. Therefore $\Gamma(X) \to \Gamma(*) \simeq *$ is an epimorphism in [[Set]], hence a [[surjection]], meaning that $\Gamma(X)$ is [[inhabited]]. Since $\Gamma(X) \simeq Hom(*,X)$ (see [[global section geometric morphism]]), the claim follows. \end{proof} \begin{remark} \label{}\hypertarget{}{} In a [[topos]] every [[epimorphism]] is an [[effective epimorphism]]. Therefore $X \to *$ being an epi means that $X$ is a [[(-1)-connected]] object. Therefore the above statement says in terms of [[(infinity,1)-category theory]] that a non-trivial local topos has [[homotopy dimension]] 0. The same is true for any [[local (infinity,1)-topos]]. \end{remark} \hypertarget{concrete_sheaves}{}\subsubsection*{{Concrete sheaves}}\label{concrete_sheaves} Every local topos $\Gamma : E \to S$ comes with a notion of [[concrete sheaves]], a [[reflective subcategory]] $Conc_\Gamma(E) \hookrightarrow E$ which factors the topos inclusion of $S$: \begin{displaymath} S \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{Codisc}{\hookrightarrow}} Conc_\Gamma(E) \stackrel{\overset{Conc}{\leftarrow}}{\hookrightarrow} E \end{displaymath} and is a [[quasitopos]]. See [[concrete sheaf]] for details. \hypertarget{homotopy_equivalence}{}\subsubsection*{{Homotopy equivalence}}\label{homotopy_equivalence} Since a local geometric morphism has a [[left adjoint]] in the [[2-category]] [[Topos]], it is necessarily a [[homotopy equivalence of toposes]]. \hypertarget{ElementaryAxiomatization}{}\subsection*{{Elementary Axiomatization}}\label{ElementaryAxiomatization} For any local topos $\Gamma \colon \mathcal{E} \to \mathcal{S}$, the base topos $\mathcal{S}$ is equivalent to the [[category of sheaves]] for a [[Lawvere-Tierney topology]] $j$ on $\mathcal{E}$. A sound and complete elementary [[axiomatization]] of local maps of (bounded) toposes can be given in terms of properties of topos $E$ and topology $j$ (\hyperlink{AwodeyBirkedal}{AwodeyBirkedal}) We discuss first \begin{itemize}% \item \hyperlink{SetupForAxiomatization}{the setup} \end{itemize} and then \begin{itemize}% \item \hyperlink{TheAxioms}{the axioms} \end{itemize} themselves. \hypertarget{SetupForAxiomatization}{}\subsubsection*{{The setup}}\label{SetupForAxiomatization} Let $\mathcal{E}$ be an [[elementary topos]] equipped with a [[Lawvere-Tierney topology]] $j : \Omega \to \Omega$. Write $V \mapsto \sharp V$ for the $j$-[[closure operation]] on [[subobjects]] $V \hookrightarrow X$, the \emph{[[sharp modality]]} \begin{displaymath} \itexarray{ V &\to& {*} \\ \downarrow && \downarrow \\ \sharp V &\to& &\to& {*} \\ \downarrow && \downarrow && \downarrow \\ X &\stackrel{\chi_V}{\to}& \Omega &\stackrel{j}{\to}& \Omega } \end{displaymath} Write \begin{displaymath} (\Gamma \dashv coDisc) : Sh_j(\mathcal{E}) \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\to}} \mathcal{E} \end{displaymath} for the [[reflective subcategory]] [[category of sheaves|of j-sheaves]]. \begin{defn} \label{EssentialTopology}\hypertarget{EssentialTopology}{} We say that $j$ is an \textbf{[[essential geometric morphism|essential]] topology} if for all objects $X$ the closure operation $\sharp : Sub(X) \to Sub(X)$ on [[posets of subobjects]] has a [[left adjoint]] $\flat \dashv \sharp$: \begin{displaymath} (U \hookrightarrow \sharp V) \Leftrightarrow (\flat U \hookrightarrow V) \,. \end{displaymath} \end{defn} This appears under the term ``principal'' in (\hyperlink{AwodeyBirkedal}{Awodey-Birkedal, def. 2.1}). \begin{remark} \label{}\hypertarget{}{} We use the notation ``$\flat$'' and ``$\sharp$'' oppositely to the use on p.14 of \hyperlink{AwodeyBirkedal}{Awodey-Birkedal}. Our convention is such that it harmonizes with the terminology at \emph{[[cohesive topos]]} and \emph{[[cohesive (infinity,1)-topos]]}, where it makes interpretational sense to pronounce ``$\flat$'' as ``flat''. \end{remark} \begin{observation} \label{}\hypertarget{}{} The left adjoints $\flat : Sub(X) \to Sub(X)$ for all $X \in \mathcal{E}$ extend to a functor $\flat : \mathcal{E} \to \mathcal{E}$ on all of $\mathcal{E}$. \end{observation} \begin{proof} (\ldots{}) \end{proof} \begin{prop} \label{InternalCharacterizationOfLocalReflection}\hypertarget{InternalCharacterizationOfLocalReflection}{} A [[Lawvere-Tierney topology]] $j$ is \hyperlink{EssentialTopology}{essential}, $(\flat \dashv \sharp )$, precisely if for all objects $X$ there exists a least $\sharp$-[[dense subobject]] $U_X \hookrightarrow X$. \end{prop} This appears as (\hyperlink{AwodeyBirkedal}{AwodeyBirkedal, lemma 2.3}). \begin{proof} By the discussion at [[category of sheaves]] we have that $\sharp$ is given by the composite \begin{displaymath} \sharp : \mathcal{E} \stackrel{\Gamma}{\to} Sh_j(\mathcal{E}) \stackrel{coDisc}{\hookrightarrow} \mathcal{E} \,, \end{displaymath} where the first morphism is [[sheafification]] and the second is [[full and faithful functor|full and faithful]]. If now the [[left adjoint]] $\flat$ exists, it follows that this comes from a left adjoint $Disc$ to $\Gamma$ as \begin{displaymath} \flat : \mathcal{E} \stackrel{\overset{Disc}{\hookleftarrow}}{\underset{\Gamma} {\to}} Sh_j(\mathcal{E}) \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\hookrightarrow}} \mathcal{E} : \sharp \,. \end{displaymath} Therefore the $(Disc \dashv \Gamma)$-[[counit of an adjunction|counit]] provides morphisms \begin{displaymath} (\flat X \to X) = (\flat X \to U_x \hookrightarrow X) \,, \end{displaymath} whose [[image]] factorization $U_x \hookrightarrow X$ we claim provides the least dense subobjects. To show that $U_X$ is dense it is sufficient to show that \begin{displaymath} \sharp (\flat X \to X) = (coDisc \Gamma Disc \Gamma \to coDisc \Gamma X) \end{displaymath} is an [[isomorphism]]. Composing this morphism with $CoDisc$ of the $(Disc \dashv\Gamma)$-unit on $\Gamma X$ (which is an [[isomorphism]] since $Disc$ is a [[full and faithful functor]] by the discussion at \emph{\href{adjoint+triple#FullyFaithFulAdjointTriples}{fully faithful adjoint triples}}) and using the $(Disc \dashv \Gamma)$ [[triangle identity]] we have \begin{displaymath} coDisc( \Gamma X \stackrel{\simeq}{\to} \Gamma Disc \Gamma X \stackrel{}{\to} \Gamma X ) = coDisc ( \Gamma X \stackrel{Id}{\to} \Gamma X) \,. \end{displaymath} Using that also $coDisc$ is full and faithful and then [[2-out-of-3]] for [[isomorphisms]] it follows that $coDisc \Gamma Disc \Gamma X \stackrel{\simeq}{\to} coDisc \Gamma X$ hence \begin{displaymath} \sharp \flat X \stackrel{\simeq}{\to} \sharp X \end{displaymath} is indeed an isomorphism. Moreover, by one of the equivalent characterizations of [[reflective subcategories]] we have (\ldots{}) \end{proof} \begin{defn} \label{DiscreteObjects}\hypertarget{DiscreteObjects}{} An object $X \in \mathcal{E}$ is called \textbf{discrete} if for all $\Gamma$-[[local isomorphisms]] $f : A \to B$ the induced morphism \begin{displaymath} \mathcal{E}(X,A) \to \mathcal{E}(X,B) \end{displaymath} is an [[isomorphism]] (of sets, hence a bijection). \end{defn} \begin{defn} \label{ODiscreteObjects}\hypertarget{ODiscreteObjects}{} An object $X \in \mathcal{E}$ is called \textbf{o-discrete} if $\flat X \simeq X$. \end{defn} \begin{lemma} \label{}\hypertarget{}{} Every discrete object is o-discrete. \end{lemma} \hypertarget{the_axioms}{}\subsubsection*{{The axioms}}\label{the_axioms} \begin{defn} \label{}\hypertarget{}{} On $\mathcal{E}$ a [[elementary topos]] with [[Lawvere-Tierney topology]] $j$ consider the following axioms. \begin{itemize}% \item \textbf{Axiom 1}. $j$ is \hyperlink{EssentialTopology}{essential}. \item \textbf{Axiom 2 a}. There is an object $G \in \mathcal{E}$ such that every object is a [[subquotient]] of the [[product]] of a \hyperlink{DiscreteObjects}{discrete object} with $G$. \item \textbf{Axiom 2 b}. With $G$ as above, there is a discrete object $G'$ and an [[epimorphism]] $G' \to \flat G$. \item \textbf{Axiom 3}. For all \hyperlink{DiscreteObjects}{discrete objects} $D$, if the [[internal hom]] $[X,D]$ is \hyperlink{ODiscreteObjects}{o-discrete}, then $X$ is also discrete. \item \textbf{Axiom 4}. \hyperlink{DiscreteObjects}{Discrete objects} are closed under binary [[products]]. \end{itemize} \end{defn} \begin{theorem} \label{}\hypertarget{}{} These axioms characterize local geometric morphisms $\mathcal{E} \to Sh_j(\mathcal{E}) \simeq D_j(\mathcal{E})$. If $G$ is fixed to be the terminal object (in which case Axiom 2 b becomes empty), then they characterize local and [[localic geometric morphisms]]. \end{theorem} This is (\hyperlink{AwodeyBirkedal}{Awodey-Birkedal, theorem 3.1}) together with the discussion around remark 3.7. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{EasyExamples}{}\subsubsection*{{Easy examples}}\label{EasyExamples} \begin{example} \label{PresheafToposOverSiteWithTerminal}\hypertarget{PresheafToposOverSiteWithTerminal}{} If $C$ is a [[small category]] with a [[terminal object]] $* \in C$, then the [[presheaf topos]] $[C^{op},Set]$ is a local topos. \end{example} \begin{proof} Notice that $Set \simeq [*,Set]$ is the presheaf topos over the point category, the category with a single object and a single morphism. Therefore the constant presheaf functor \begin{displaymath} Const : Set \to [C^{op}, Set] \end{displaymath} can be thought of as sending a set $S \in Set$, hence a functor $S : * \to Set$ to the composite functor \begin{displaymath} Const(S) \colon C \to * \stackrel{S}{\to} Set \,. \end{displaymath} Notice that in the presence of a terminal object in $C$, $Const$ is a [[full and faithful functor]]: a [[natural transformation]] $Const(S_1) \to Const(S_2)$ has components \begin{displaymath} \itexarray{ S_1 = & Const(S_1)(*) &\stackrel{f}{\to}& Const(S_2)(*) & = S_2 \\ & \downarrow^{\mathrm{id}} && \downarrow^{\mathrm{id}} \\ & Const(S_1)(U) &\to& Const(S_2)(U) } \end{displaymath} where the vertical morphisms are $Const(U \to *)$, the point being that they exist for every $U \in C$ given the presence of the terminal object. It follows that such a natural transformation is given by any and one and the same [[function]] $f \colon S_1 \to S_2$. The functor $Const$ has a [[left adjoint]] and a [[right adjoint]], and these are -- essentially by definition -- the [[colimit]] and the [[limit]] operations \begin{displaymath} (\underset{\rightarrow}{\lim} \vdash Const \vdash \underset{\leftarrow}{\lim}) \end{displaymath} which send a presheaf/functor $F \colon C^{op} \to Set$ to its [[colimit]] $\underset{\rightarrow}{\lim} F \in Set$ or [[limit]] $\underset{\leftarrow}{\lim} F \in Set$, respectively. Since adjoints are essentially unique, it follows that the [[global section]] functor $\Gamma \colon [C^{op}, Set]$ is given by taking the limit, $\Gamma \simeq \underset{\leftarrow}{\lim}$. Observe that the [[terminal object]] $* \in C$ is the [[initial object]] in the [[opposite category]] $C^{op}$. But the limit over a [[diagram]] with initial object is given simply by evaluation at that object, and so we have for any $F \in [C^{op}, Set]$ that \begin{displaymath} \begin{aligned} \Gamma(F) & \simeq \underset{\leftarrow}{\lim} F \\ & \simeq F(*) \in Set \end{aligned} \end{displaymath} hence that the global section functor is simply given by evaluating a presheaf on the terminal object of $C$. Limits and colimit \emph{in} a presheaf category $[C^{op}, Set]$ are computed objectwise over $C$ (see at \emph{[[limits and colimits by example]]}). Therefore evaluation at any object in $C$ preserves in limits and colimits, and in particular evaluation at the terminal object does. Therefore $\Gamma$ preserves all colimits. Hence by the [[adjoint functor theorem]] it has a further [[right adjoint]] $CoDisc$. We can compute it explicitly by the [[Yoneda lemma]] and using the defining Hom-isomorphism of adjoints to be the functor $CoDisc \colon Set \to [C^{op}, Set]$ such that for $S \in Set$ the presheaf $CoDisc(S)$ is given over $U \in C$ by \begin{displaymath} \begin{aligned} CoDisc(S)(U) & \underoverset{Yoneda}{\simeq}{\to} Hom_{[C^{op}, Set]}(U,CoDisc(S)) \\ & \underoverset{adjunction}{\simeq}{\to} Hom_{Set}(\Gamma(U), S) \,. \end{aligned} \end{displaymath} So in conclusion we have an [[adjoint triple]] $(Const \vdash \Gamma \vdash CoDisc)$ where $Const$ is a [[full and faithful functor]]. By the discussion at \emph{\href{adjoint+triple#FullyFaithFulAdjointTriples}{fully faithful adjoint triples}} it follows then that also $CoDisc$ is full and faithful. \end{proof} \begin{prop} \label{}\hypertarget{}{} The converse to prop. \ref{PresheafToposOverSiteWithTerminal} is true if $C$ is [[Cauchy complete category|Cauchy complete]]. \end{prop} \begin{example} \label{}\hypertarget{}{} If $X$ is a [[topological space]], or more generally a [[locale]], then $Sh(X)$ is local (over Set) iff $X$ has a [[focal point]] $x$, i.e. a point whose only [[neighborhood]] is the whole space. In this case, the extra right adjoint $f^! : Set \to Sh(X)$ to the global sections functor $f_* : Sh(X) \to Set$ is given by the functor which computes the stalk at $x$. This can also be given without reference to $x$, by the formula \begin{displaymath} \Gamma(U, f^!(M)) = Hom(\{\star|U=X\}, M) \cong \begin{cases} M, & U = X, \\ \{\star\}, & U \neq X, \end{cases} \end{displaymath} for sets $M$ and open subsets $U \subseteq X$. \end{example} \hypertarget{sheaves_on_a_local_site}{}\subsubsection*{{Sheaves on a local site}}\label{sheaves_on_a_local_site} For $C$ a [[local site]], the [[category of sheaves]] $Sh(C)$ is a local topos over $Set$. For instance [[CartSp]] is a local site. Objects in $Sh(C)$ are [[generalized smooth spaces]] such as [[diffeological space]]s. The further right adjoint \begin{displaymath} Codisc : Set \to Sh(CartSp) \end{displaymath} is the functor that sends a set to the [[diffeological space]] on that set with \emph{[[codiscrete space|codiscrete]]} smooth structure (every map of sets is smooth). \hypertarget{relative_realizability}{}\subsubsection*{{Relative Realizability}}\label{relative_realizability} Let $A$ be a partial combinatory algebra and let $A\sharp\subseteq A$ be a sub partial combinatory algebra of $A$. Then there is a (localic) local geometric morphism from the [[relative realizability topos]] $\mathrm{RT}(A,A\sharp)$ to the standard [[realizability topos]] $\mathrm{RT}(A\sharp)$. \hypertarget{localization}{}\subsubsection*{{Localization}}\label{localization} Let $LocTopos$ denote the 2-category of local [[Grothendieck toposes]] (over Set) with all geometric morphisms between them. Let $PTopos$ denote the 2-category whose objects are [[pointed topos|pointed toposes]] (i.e. (Grothendieck) toposes $E$ equipped with a geometric morphism $s\colon Set\to E$), and whose morphisms are pairs $(f,\alpha)$ such that $f\colon E\to E'$ is a geometric morphism and $\alpha\colon s'\to f s$ is a (not necessarily invertible) geometric transformation. Note that if $E$ is a local topos with global sections geometric morphism $e^*\dashv e_*$, then the adjunction $e_*\dashv e^!$ is also a geometric morphism $Set\to E$. In this way we have a functor $LocTopos \to PTopos$, which is a full embedding, and turns out to have a [[right adjoint]]: this right adjoint is called the \textbf{localization} of a pointed topos at its specified point. For example: \begin{prop} \label{LocalizationOfPresheafTopos}\hypertarget{LocalizationOfPresheafTopos}{} If $C$ is a [[small category]] and $U$ is an object of $C$, then the localization of the [[presheaf topos]] $[C^{op},Set]$ at the point induced by $U\colon 1\to C$ can be identified with the [[presheaf topos]] $[(C/U)^{op},Set]$ over the [[over category]] of $C$ over $U$. By the general properties of [[over topos]]es, this is equivalently the over-topos $PSh(C)/U$ (where $U$ is regarded in $PSh(C)$ by the [[Yoneda embedding]]). \end{prop} \begin{prop} \label{}\hypertarget{}{} If $X=Spec(A)$ is the [[Zariski spectrum]] of a [[commutative ring]] $A$, and $P\subset A$ is a prime ideal of $A$ (i.e. a point of $X$), then the localization of $Sh(X)$ at $P\colon 1\to X$ can be identified with $Sh(Spec(A_P))$, where $A_P$ denotes the [[localization]] of $A$ at $P$. Of course, this is the origin of the terminology. \end{prop} A similar construction is possible for [[bounded geometric morphism|bounded]] toposes over any base (not just Set). \hypertarget{LocalOverTopoes}{}\subsubsection*{{Local over-toposes}}\label{LocalOverTopoes} \begin{prop} \label{}\hypertarget{}{} For $\mathcal{E}$ a [[Grothendieck topos]] and $X \in \mathcal{E}$ an object, the [[over topos]] $\mathcal{E}/X$ is local if $X$ is a [[tiny object]] ([[atomic object]]). \end{prop} \begin{proof} We check that the [[global section]] [[geometric morphism]] $\Gamma : \mathcal{E}/X \to Set$ preserves [[colimit]]s. It is given by the [[hom-functor]] out of the [[terminal object]] of $\mathcal{E}/X$, which is $(X \stackrel{Id}{\to} X)$: \begin{displaymath} \Gamma : (A \stackrel{f}{\to} X) \mapsto Hom_{\mathcal{E}/X}(Id_X, f) \,. \end{displaymath} The [[hom-set]]s in the [[over category]] are [[fiber]]s of the hom-sets in $\mathcal{E}$: we have a [[pullback]] diagram \begin{displaymath} \itexarray{ Hom_{\mathcal{E}/X}(Id_X, (A \to X)) &\to& Hom_{\mathcal{E}}(X,A) \\ \downarrow && \downarrow^{f_*} \\ * &\stackrel{Id_x}{\to}& Hom_{\mathcal{E}}(X,X) } \,. \end{displaymath} Moreover, overserve that [[colimit]]s in the [[over category]] are computed in $\mathcal{E}$. \begin{displaymath} {\lim_{\to}}_i (A_i \stackrel{f_i}{\to} X) \simeq ({\lim_\to}_i A_i) \to X \,. \end{displaymath} If $X$ is a [[tiny object]] then by definition we have \begin{displaymath} Hom_{\mathcal{E}}(X, {\lim}_i A_i) \simeq {\lim_\to}_i Hom_{\mathcal{E}}(X, A_i) \,, \end{displaymath} Inserting all this into the above pullback gives the pullback \begin{displaymath} \itexarray{ Hom_{\mathcal{E}/X}(Id_X, {\lim_\to}_i (A_i \to X)) &\to& {\lim_\to}_i Hom_{\mathcal{E}}(X, A_i) \\ \downarrow && \downarrow^{f_*} \\ * &\stackrel{Id_x}{\to}& Hom_{\mathcal{E}}(X,X) } \,. \end{displaymath} By [[universal colimits]] in the topos [[Set]], this pullback of a colimit is the colimit of the separate pullbacks, so that \begin{displaymath} \Gamma({\lim_\to}_i (A_i \to X))) \simeq Hom_{\mathcal{E}/X}(Id_X, {\lim_\to}_i (A_i \to X)) \simeq {\lim_\to}_i Hom_{\mathcal{E}/X}(Id_X,(A_i \to X)) \simeq {\lim_\to}_i \Gamma(A_i \to X) \,. \end{displaymath} So $\Gamma$ does commute with colimits if $X$ is tiny. By the [[adjoint functor theorem]] then the [[right adjoint]] $\nabla : Set \to \mathcal{E}/X$ does exist and so $\mathcal{E}/X$ is a local topos. \end{proof} \begin{remark} \label{}\hypertarget{}{} As a special case this reproduces the \hyperlink{LocalizationOfPresheafTopos}{above statement} that slices $PSh(C)/j(U)$ of presheaf toposes over objects in the image of the [[Yoneda embedding]] are local: every [[representable functor]] is [[tiny object|tiny]] (see there). \end{remark} \hypertarget{gros_toposes}{}\subsubsection*{{Gros toposes}}\label{gros_toposes} Let $A$ be a [[commutative ring]] (such as $\mathbb{Z}$ or a [[field]]), let $Spec A$ be the [[prime spectrum]] of $A$, and let $\mathcal{Z}_A$ be the [[big and little toposes|big]] [[Zariski site|Zariski topos]] for $A$ (i.e. the [[classifying topos]] for [[local ring|local $A$-algebras]]). For each element $a$ of $A$, we have an open subset $D (a) = \{ \mathfrak{p} \in Spec A : a \notin \mathfrak{p} \}$, and these open subsets constitute a basis for the topology on $Spec A$. The full subcategory of the frame of open subsets of $Spec A$ spanned by these basic open subsets admits a contravariant [[full and faithful functor|full embedding]] in the category of finitely-presented $A$-algebras via the functor $D (a) \mapsto A [a^{-1}]$ (the well-definedness of this functor requires a non-trivial check!), and this functor moreover has the cover lifting property, so induces a local geometric morphism $\mathcal{Z}_A \to Sh (Spec A)$. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[essential geometric morphism]] \item [[locally connected topos]] / [[locally ∞-connected (∞,1)-topos]] \begin{itemize}% \item [[connected topos]] / [[∞-connected (∞,1)-topos]] \item [[strongly connected topos]] / [[strongly ∞-connected (∞,1)-topos]] \item [[totally connected topos]] / [[totally ∞-connected (∞,1)-topos]] \end{itemize} \item \textbf{local topos} / [[local (∞,1)-topos]] \begin{itemize}% \item [[Pi modality]] $\dashv$ [[flat modality]] $\dashv$ [[sharp modality]] \end{itemize} \item [[cohesive topos]] / [[cohesive (∞,1)-topos]] \end{itemize} and \begin{itemize}% \item [[locally connected site]], [[locally ∞-connected site]] \item [[connected site]] \item [[local site]] \item [[cohesive site]], [[(∞,1)-cohesive site]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} Standard references include \begin{itemize}% \item [[Peter Johnstone]], [[Ieke Moerdijk]], \emph{Local maps of toposes} Proc. London Math. Soc. (1989) s3-58 (2): 281-305. (\href{http://plms.oxfordjournals.org/content/s3-58/2/281.full.pdf+html}{pdf}) \end{itemize} and Chapter C3.6 of \begin{itemize}% \item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]]} \end{itemize} A completely [[internal logic|internal]] characterization of local toposes is discussed in \begin{itemize}% \item [[Steve Awodey]], [[Lars Birkedal]], \emph{Elementary axioms for local maps of toposes}, Journal of Pure and Applied Algebra, 177(3):215-230, (2003) (\href{http://www.itu.dk/people/birkedal/papers/elealm.ps.gz}{ps}, [[AwodeyBirkedalLocalTopos.pdf:file]]) \end{itemize} This is based on part 2 of \begin{itemize}% \item [[Lars Birkedal]], \emph{Developing Theories of Types and Computability via Realizability} PhD Thesis (\href{http://itu.dk/people/birkedal/papers/devttc.pdf}{pdf}) \end{itemize} Free local constructions are considered in \begin{itemize}% \item [[Mike Shulman]], \emph{Discreteness, Concreteness, Fibrations, and Scones} (\href{http://golem.ph.utexas.edu/category/2011/11/discreteness_concreteness_fibr.html}{blog post}) \end{itemize} Notions of local topos, with a view to logical completeness theorems, appear in Steve Awodey's thesis: \begin{itemize}% \item [[Steve Awodey]], \emph{Logic in topoi: functorial semantics for higher-order logic}, Thesis, University of Chicago (1997). \end{itemize} [[!redirects local geometric morphisms]] [[!redirects local topos]] [[!redirects local topoi]] [[!redirects local toposes]] \end{document}