% (find-angg "LATEX/istanbulquotes.tex")
% (find-angg "LATEX/istanbulquotes.lua")
% (defun c () (interactive) (find-LATEXsh "lualatex istanbulquotes.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/istanbulquotes.pdf"))
% (defun e () (interactive) (find-LATEX "istanbulquotes.tex"))
% (find-xpdfpage "~/LATEX/istanbulquotes.pdf")
%
% (find-istfile "glyphs.el")
% (load "~/LATEX/istanbulglyphs.el")
% (eev-uc-set-composes)
%
% (find-books "__cats/__cats.el" "johnstone-elephant")


% «.chars»		(to "chars")
%
% «.lua»		(to "lua")
% «.fourman»		(to "fourman")
% «.mmoe»		(to "mmoe")
% «.elephant-A4»	(to "elephant-A4")
% «.elephant-A4.1.1»	(to "elephant-A4.1.1")
% «.elephant-A4.1.4»	(to "elephant-A4.1.4")
% «.elephant-A4.1.5»	(to "elephant-A4.1.5")
% «.elephant-A4.1.8»	(to "elephant-A4.1.8")
% «.elephant-A4.1.10»	(to "elephant-A4.1.10")
% «.elephant-A4.2.6»	(to "elephant-A4.2.6")
% «.elephant-A4.2.7»	(to "elephant-A4.2.7")
% «.elephant-A4.2.9»	(to "elephant-A4.2.9")
% «.elephant-A4.2.10»	(to "elephant-A4.2.10")
% «.elephant-A4.2.12»	(to "elephant-A4.2.12")
% «.elephant-A4.3.6»	(to "elephant-A4.3.6")
% «.elephant-A4.3.9»	(to "elephant-A4.3.9")
% «.elephant-A4.5.2»	(to "elephant-A4.5.2")
% «.elephant-A4.5.8»	(to "elephant-A4.5.8")
% «.elephant-A4.5.9»	(to "elephant-A4.5.9")
% «.elephant-A4.5.10»	(to "elephant-A4.5.10")
% «.elephant-A4.5.20»	(to "elephant-A4.5.20")
% «.elephant-A4.6.2»	(to "elephant-A4.6.2")
% «.elephant-A4.6.5»	(to "elephant-A4.6.5")
% «.elephant-A4.6.6»	(to "elephant-A4.6.6")
% «.elephant-A4.6.10»	(to "elephant-A4.6.10")


\documentclass[oneside]{book}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{luacode}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\begin{document}

% \directlua{dofile "\jobname.lua"}

\widemtos


% «chars» (to ".chars")
\input istanbuldefs % (find-istfile "defs.tex")

\catcode`°=13 \def°{^\degree}
\catcode`¹=13 \def¹{^{-1}}
\catcode`²=13 \def²{^2}
\catcode`³=13 \def³{^3}
%\catcode`¼=13 \def¼{}
%\catcode`½=13 \def½{}
%\catcode`¾=13 \def¾{}
\catcode`±=13 \def±{\pm}
\catcode`÷=13 \def÷{\div}
\catcode`·=13 \def·{\cdot}
\catcode`×=13 \def×{\times}
\catcode`¬=13 \def¬{\neg}
\catcode`§=13 \def§{\S}

\catcode`Δ=13 \defΔ{\Delta}
\catcode`Θ=13 \defΘ{\Theta}
\catcode`Ω=13 \defΩ{\Omega}
\catcode`α=13 \defα{\alpha}
\catcode`β=13 \defβ{\beta}
\catcode`γ=13 \defγ{\gamma}
\catcode`δ=13 \defδ{\delta}
\catcode`ε=13 \defε{\epsilon}
\catcode`η=13 \defη{\eta}
\catcode`θ=13 \defθ{\theta}
\catcode`λ=13 \defλ{\lambda}
\catcode`π=13 \defπ{\pi}
\catcode`ω=13 \defω{\omega}
\catcode`←=13 \def←{\ot}
\catcode`↑=13 \def↑{\upto}
\catcode`→=13 \def→{\to}
\catcode`↓=13 \def↓{\dnto}
\catcode`↔=13 \def↔{\bij}
\catcode`↕=13 \def↕{\updownarrow}
\catcode`↖=13 \def↖{\nwarrow}
\catcode`↗=13 \def↗{\nearrow}
\catcode`↘=13 \def↘{\searrow}
\catcode`↙=13 \def↙{\swarrow}
\catcode`↣=13 \def↣{\epito}
\catcode`↣=13 \def↣{\twoheadrightarrow}
\catcode`↦=13 \def↦{\mapsto}
\catcode`⇒=13 \def⇒{\funto}
\catcode`∀=13 \def∀{\forall}
\catcode`∃=13 \def∃{\exists}
\catcode`∈=13 \def∈{\in}
\catcode`∘=13 \def∘{\circ}
\catcode`∞=13 \def∞{\infty}
\catcode`∧=13 \def∧{\land}
\catcode`∨=13 \def∨{\lor}
\catcode`∩=13 \def∩{\cap}
\catcode`∪=13 \def∪{\cup}
\catcode`≃=13 \def≃{\simeq}
\catcode`≅=13 \def≅{\cong}
\catcode`≤=13 \def≤{\le}
\catcode`≥=13 \def≥{\ge}
\catcode`⊂=13 \def⊂{\subset}
\catcode`⊃=13 \def⊃{\supset}
\catcode`⊆=13 \def⊆{\subseteq}
\catcode`⊇=13 \def⊇{\supseteq}
\catcode`⊢=13 \def⊢{\vdash}
\catcode`⊣=13 \def⊣{\dashv}
\catcode`⊤=13 \def⊤{\top}
\catcode`⊥=13 \def⊥{\bot}
\catcode`♭=13 \def♭{\flat}
\catcode`♯=13 \def♯{\sharp}

%\catcode`=13 \def{\ensuremath{\bullet}}
%\catcode`=13 \def{\mathscr}
%\catcode`=13 \def{\mathbf}
%\catcode`=13 \def{\par\noindent}
%\catcode`=13 \def{\par}
%\catcode`=13 \def{\mathcal}

\def\bfy{\mathbf{y}}
\def\bfyU{\mathbf{y}U}

\def\BF#1{\noindent{\bf#1}\quad}
\def\liml{\underleftarrow {\lim}{}}
\def\limr{\underrightarrow{\lim}{}}
\def\frakCat{\mathfrak{Cat}}
\def\frakTop{\mathfrak{Cat}}
\def\elephantpage#1{((page #1))}
\def\ob{{\operatorname{ob}}}
\def\sh{\mathbf{sh}}
\def\Sh{\mathbf{Sh}}
\def\Sp{\mathbf{Sp}}
\def\Lop{\mathbf{Lop}}
\def\Hom{\mathrm{Hom}}

\def\sdd{\ssk{\scriptsize (...)}\ssk}
\def\mdd{\msk{\scriptsize (...)}\msk}



% «lua» (to ".lua")
% (find-LATEX "2015logicandcats.lua")
% \directlua{
% dednat6dir = "/home/edrx/dednat5/"
% dofile(dednat6dir.."dednat6.lua")
% dofile(os.getenv("LUA_INIT"):sub(2))
% }
% %
% \catcode`\^^J=10                     % (find-es "luatex" "spurious-omega")
% \directlua{dofile "istanbulall.lua"} % (find-ist "all.lua")
% \directlua{output = mytexprint}      % (find-ist "all.lua" "output")
% \directlua{output =  printboth}      % (find-ist "all.lua" "output")
% \directlua{tf = TexFile.read(tex.jobname..".tex")}
% \def\Diag#1{\directlua{tf:processuntil()}\diag{#1}}
% \def\Ded #1{\directlua{tf:processuntil()}\ded{#1}}
% \def\Expr#1{\directlua{tf:processuntil() output(#1)}}
% \def\Expr#1{\directlua{tf:processuntil() output(tostring(#1))}}
% %L output(preamble1)                -- (find-dn5 "preamble6.lua")
% \directlua{tf:processuntil()}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}




% -------------------------------------------
%  _____                                      
% |  ___|__  _   _ _ __ _ __ ___   __ _ _ __  
% | |_ / _ \| | | | '__| '_ ` _ \ / _` | '_ \ 
% |  _| (_) | |_| | |  | | | | | | (_| | | | |
% |_|  \___/ \__,_|_|  |_| |_| |_|\__,_|_| |_|
%                                             
% «fourman» (to ".fourman")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 329)   "2.18 Elementary J-operators")

This is an excerpt -- pages 329-331 -- from M.P. Fourman and D.S.
Scott's ``Sheaves and Logic'', that was published in SLNM0753
(``Applications of Sheaves: Proceedings of the Research Symposium on
Applications of Sheaf Theory to Logic, Algebra and Analysis - Durham,
july 9-21, 1977'').

\bsk


\BF{2.18. ELEMENTARY J-OPERATORS.} In these examples $Ω$ is a given cHa.

(i) {\sl The closed quotient.} The operator is defined by
%
$$J_a p = a ∨ p.$$
%
This is obviously a J-operator, and the congruence relation is:
%
$$a∨p = a∨q.$$
%
The set of fixed points (quotient lattice) is:
%
$$\setofst{p ∈ Ω}{a≤p}.$$

Classically speaking in the spatial case where $Ω=\Opens(X)$, the
quotient corresponds to the topology on the {\sl closed} subspace
complementary to the open set $a$.

This quotient makes the element $a$ ``false'' and is the least such.

\msk

(ii) {\sl The open quotient.} The operator is defined by:
%
% (find-slnm0753page (+ 14 330))
%
$$J^a p = a→p.$$
%
The congruence relation is:
%
$$a∧p = a∧q \qquad \text{(equivalently, $a ≤ p↔q$)}.$$
%
The set of fixed points is thus isomorphic to
%
$$Ω_a = \setofst{p∈Ω}{p≤a}.$$

Intuitionistically speaking in the spatial case, this quotient
corresponds to the topology on the open subspace $a$. This quotient
makes $a$ ``true'' and is the leat such.

\msk

(iii) {\sl The Boolean quotient}. The operator is defined by:
%
$$B_a p = (p→a)→a.$$
%
The congruence relation is:
%
$$p→a = q→ a.$$
%
The set of fixed points is 
%
$$\setofst{p∈Ω}{(p→a)→a≤p}.$$

In case $a=⊥$, this is the well-known $¬¬$-quotient giving the
(complete) Boolean algebra of ``stable'' elements. For arbitrary $a$,
we could first form $Ω/J_a$ and follow this by the $¬¬$-quotient to
obtain $Ω/B_a$. (In general, if $J≤K$, then $Ω/K$ is a quotient of
$Ω/J$.)

We remark that in general $Ω/J$ is a cBa iff $J=B_{J_⊥}$. Further, is
$Ω$ is already Boolean, then {\sl every} J-operator on $Ω$ is of the
form $B_a = J_a$.

\msk

(iv) {\sl The forcing quotient}. The operator is a combination of
previous ones:
%
$$(J_a∧J^b)p = (a∨p)∧(b→p).$$
%
The congruence relation is a conjunction:
%
$$a∨b=a∨q \quad \text{and} \quad b∧p=b∧q.$$
%
The set of fixed points is:
%
$$\setofst{p∈Ω}{b→p≤ a→p}.$$

The point of the quotient is that it provides the {\sl least}
J-operator such that $Ja≤Jb$; that is, we take the least quotient that
``forces'' $a→b$ to be true. If we want to force a sequence of
statements $a_i→b_i$, for $i<n$, the operator needed is $\bigvee_{i<n}
(J_{a_i}∧J{b_i})$. It is important to note that in general sup's of
J-operators cannot be calculated pointwise. We shall see below,
however, that it is possible to find a finite expression for this
particular sup. (We owe this remark to John Cartmell).

\msk

% (find-slnm0753page (+ 14 331))

(vi) {\sl A mixed quotient.} The interest of this example lies in the fact
that it has a neat finite definition:
%
$$(B_a∧J^a)p = (p→a)→p.$$
%
The congruence relation is:
%
$$(p→a)→p = (q→a)→q,$$
%
which is equivalent to the conjunction:
%
$$a∧p = a∧q \quad\text{and}\quad p→a = q→a.$$
%
The set of fixed points is:
%
$$\setofst{p∈Ω}{(p→a)→p ≤ p}.$$

It is difficult to make this set vivid except to say that it is the
set of elements p satisfying Pierce's law (for a fixed a).

\msk

If we take a polynomial in $→$, $∧$, $∨$, $⊥$, say $f(p,a,b,\ldots)$,
it is a decidable question whether for all $a$, $b$, $\ldots$ it
defines a J-operator. This does not, however, help us very much in
cataloguing such operators (nor in seeing what good they are!) Some
techniques can be developed from the following formulae, which were
pointed out to us by Cartmell, see also [33] and [47].

\msk

\BF{2.19. PROPOSITION.} In the following, $K$ is an arbitrary
J-operator, $⊤$ is the constant function (the greatest J-operator with
the most trivial quotient), and $⊥$ is the least J-operator (namely,
the identity function on $Ω$):

$$
\def\li#1 #2 #3 #4    #5 #6 #7 #8 {\text{#1}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\}
\begin{array}{rlclcrlclc}
\li   (i) J_a∨J_b = J_{a∨b}    (ii)   J^a∨J^b = J^{a∧b}
\li (iii) J_a∧J_b = J_{a∧b}    (iv)   J^a∧J^b = J^{a∨b}
\li   (v) J_a∧J^a = ⊥          (vi)   J_a∨J^a = ⊤
\li (vii) J_a∨K   = K∘J_a      (viii) J^a∨K   = J^a∘K
\li  (ix) J_a∨B_a = B_a        (x)    J^a∨B_b = B_{a→b}
\end{array}
$$

Proof. Equations (i)-(iv) are easy calculations; while (v) comes down
to showing $p=(a∨p)∧(a→p)$. Formula (vi) is a direct consequence of
(vii) (equally, of (viii)).


\newpage



% -------------------------------------------------------
%  __  __ _        ____  __                    _ _  _ _    
% |  \/  | |      / /  \/  | ___   ___ _ __ __| (_)(_) | __
% | |\/| | |     / /| |\/| |/ _ \ / _ \ '__/ _` | || | |/ /
% | |  | | |___ / / | |  | | (_) |  __/ | | (_| | || |   < 
% |_|  |_|_____/_/  |_|  |_|\___/ \___|_|  \__,_|_|/ |_|\_\
%                                                |__/      
% «mmoe» (to ".mmoe")
% (find-books "__cats/__cats.el" "moerdijk")
% (find-maclanemoerdijkpage (+  -29  69) "2. Sieves and Sheaves")
% (find-maclanemoerdijktext (+  -29  69))

This is an excerpt -- pages 69-71 -- from MacLane and Moerdijk's
``Sheaves in Geometry and Logic - A First Introduction to Topos
Theory'' (1992).

\bsk

\BF{2. Sieves and Sheaves}

On any space $X$, each open set $U$ determines a presheaf $\Hom(-, U)$ 
defined, for each open set $V$, by 
%
% (find-maclanemoerdijkpage (+  -29  70))
%
$$
  \Hom(V, U) =
  \begin{cases}
    1      & \text{if} \quad $V ⊂ U$, \\
    \empty & \text{otherwise,} \\
  \end{cases}
  %
  \qquad\qquad(1)
$$
%
where 1 is the one-point set. This presheaf is clearly a sheaf; it is
the representable presheaf $\bfy(U) = \Hom(—, U)$ on the category
$\Opens(X)$. Recall from §1.4 that a {\sl sieve} $S$ on $U$ in this
category is defined to be a subfunctor of $\Hom(—, U)$. Replacing the
sieve $S$ by the set (call it $S$ again) of all those $V ⊂ U$ with $SV
= 1$, we may also describe a sieve on $U$ as a subset $S ⊂ \Opens(U)$
of objects such that $V_0 ⊂ V ∈ S$ implies $V_0 ∈ S$. Each indexed
family $\setofst{V_i ⊂ U}{i ∈ I}$ of subsets of U generates ($=$
``spans'') a sieve $S$ on $U$; namely, the set $S$ consisting of all
those open $V$ with $V ∈ V_i$ for some $i$; in particular, each $V_0 ∈
U$ determines a {\sl principal sieve} $(V_0)$ on $U$, consisting of
all $V$ with $V ⊂ V_0$. It is not difficult to see that a sieve $S$ on
$U$ is principal iff the subfunctor $S$ of $\bfy(U)$ is a subsheaf
(Exercise 1). A sieve $S$ on $U$ is said to be a {\sl covering} sieve
for $U$ when $U$ is the union of all the open sets $V$ in $S$.

In the definition of a sheaf, we may replace {\sl open coverings} by
{\sl covering sieves}, as follows:

\msk

\BF{Proposition 1.} A presheaf P on X is a sheaf if and only if, for
every open set $U$ of $X$ and every covering sieve $S$ on $U$, the
inclusion $i_s: S → \bfyU$ of functors induces an isomorphism,
%
$$\Hom(\bfyU, P) ≅ \Hom(S, Р). \qquad\qquad   (2)$$
%
(Here each $\Hom$ is the set of natural transformations.) 

\msk

\BF{Proof:} For any presheaf $P$ on the space $X$ and any covering of
an open set $U$ by $U_i$, we can construct the equalizer $E$ in the
diagram
%
% (find-es "xypic" "two-and-three")
% $$ (B ↓ f) \diagxyto/->/^U \calC \diagxyto/->/^F \Set $$
%
$$ E \diagxyto/->/^d \prod_i PU_i \two/->`->/ \prod_{i,j} P(U_i,U_j)$$
%
Specifically, $E$ consists of those families of elements $x_i ∈ PU_i$
with $x_i|_{U_i∩U_j} = x_j|_{U_i∩U_j}$ for all pairs of indices
$(i,j)$. Now replace the covering $U_i$ by the corresponding sieve
$S$, consisting of all open sets $V$ with $V ⊂ U_i$ for some $i$, and
for each $V$ define $x_V$ to be $x_i|_V$. By the assumption that the
$x_i$ match on intersections $U_i∩U_j$, the $x_V$ so defined are
independent of the choice of the index $i$ with $V ⊂ U_i$. Therefore,
the equalizer $E$ can be described as the set of those families of
elements $x_V ∈ PV$ for $V ∈ S$ with $x_V|_{V'} = x_{V'}$ whenever $V'
⊂ V$. Now regard $S$ as a functor $\Opens(X)^\op → \Sets$ with $SV =
1$ for those $V ∈ S$ and $SV = \empty$ otherwise. Each element $x_V ∈
PV$ is then a map $SV → PV$, so the equalizer $E$ is now described as
the set of natural transformations
%
% (find-maclanemoerdijkpage (+  -30  71))
%
$θ: S → P$ [where $θ_V(1)$ is $x_V$]. Next use the inclusion $i_S: S →
\bfyU$ to form the diagram
%
%D diagram mmoe-p71
%D 2Dx     100   +60  +60
%D 2D  100 A     B    B'     
%D 2D
%D 2D  +40 C     D
%D 2D
%D (( A .tex= \Hom(S,P)    B .tex= \prod_{i}PU_i   B' .tex= \prod_{i,j}P(U_i∩U_j)
%D    C .tex= \Hom(\bfyU,P)  D .tex= PU,
%D    A B  ->     .plabel= a d
%D    B B' -> sl^ .plabel= a p
%D    B B' -> sl_ .plabel= b q
%D    C A  ->     .plabel= l (i_S)^*
%D    D B  ->     .plabel= r e
%D    C D  ->     .plabel= a \bfy 
%D    C D  ->     .plabel= b ≅
%D ))
%D enddiagram
%D
$$\Diag{mmoe-p71} \qquad\qquad (3)$$
%
where $\bfy$ is the isomorphism given by the Yoneda lemma, while the
maps $e$, $p$, and $q$ are described as before in (1.2), and the
equalizer $d$ is the function which sends each natural transformation
$θ: S → P$ to the family $θ_{U_i}(1) ∈ PU_i$ of its values, for $i ∈
I$.


For this diagram, one verifies that the square in the middle always
commutes, so that $e$ does, in fact, always factor through the
equalizer $d$ of $p$ and $q$. Therefore, $P$ is a sheaf (i.e., $e$ is
the equalizer) if and only if, for every covering $U_i$, the left-hand
vertical map $(i_S)*$ is an isomorphism, where $S$ is the
corresponding covering sieve.

This proposition has the theoretical advantage of describing sheaves 
wholly in terms of objects (presheaves and sieves) of the category of 
presheaves. It also slightly simplifies some proofs of facts about sheaves. 
Moreover, it will be used as a definition of sheaves in terms of a more 
general notion of covering (Chapter III). 

As said before, the category $\Sh(X)$ for the space $X$ is a full
subcategory of the functor category (the category of presheaves)
$\Sets^{\Opens(X)^\op}$:
%
$$ \Sh(X) ↣ \Opens(X) = \Sets^{\Opens(X)^\op} \qquad\qquad (4) $$ 
 
We will soon see (§5) that this inclusion functor has a left adjoint.
This will imply the second part of

\BF{Proposition 2.} For any space X the category Sh(X) has all small 
limits, and the inclusion of sheaves in presheaves preserves all these 
limits. 

% \end{document}



% (find-854 "" "yoneda-lemma")
% (find-854 "" "yoneda-lemma-2")
% (find-854page 32 "yoneda-lemma")
% (find-854page 33 "yoneda-lemma-2")


\newpage


% -----------------------------------------
%  _____ _            _                 _   
% | ____| | ___ _ __ | |__   __ _ _ __ | |_ 
% |  _| | |/ _ \ '_ \| '_ \ / _` | '_ \| __|
% | |___| |  __/ |_) | | | | (_| | | | | |_ 
% |_____|_|\___| .__/|_| |_|\__,_|_| |_|\__|
%              |_|                          

All the extracts below are from Peter Johstone's ``Sketches of an
Elephant'', vol.1, section A4: ``Geometric Morphisms - Basic Theory''.

% (setq last-kbd-macro (kbd "M-A 2*<up> C-a C-SPC <down> C-w M-o C-y M-o <down>"))

% «elephant-A4» (to ".elephant-A4")
% «elephant-A4.1.1» (to ".elephant-A4.1.1")
% (find-elephanttext (+ 17 161))
% (find-elephantpage (+ 17 161) "A4 Geometric Morphisms - Basic Theory")
% (find-elephantpage (+ 17 161) "Definition 4.1.1")

\msk

\BF{Definition 4.1.1} (a) Let $\calE$ and $\calF$ be toposes. A geometric
morphism $f: \calF → \calE$ consists of a pair of functors $f_*: \calF → \calE$
(the direct image of f) and $f^*: \calE → \calF$ (the inverse image of $f$)
together with an adjunction ($f^* ⊣ f_*$), such that $f^*$ is cartesian
(i.e. preserves finite limits).

\ssk

(b) Let $f$ and $g: \calF → \calE$ be geometric morphisms. A geometric
transformation $α: f → g$ is defined to be a natural
transformation $α: f^* → g^*$.

\bsk

% «elephant-A4.1.4» (to ".elephant-A4.1.4")
% (find-elephanttext (+ 17 163))
% (find-elephantpage (+ 17 163) "Example 4.1.4")

\BF{Example 4.1.4} Let $f: \calC → \calD$ be a functor between small
categories. Then composition with $f$ defines a functor $f^*: [\calD,
  \Set] → [\calC, \Set]$, which has adjoints on both sides, the left
and right {\sl Kan extensions} along $f$: for example, the right Kan
extension $\liml_f$ sends a functor $F: \calC → \Set$ to the functor
whose value at an object $B$ of $\calD$ is the limit of the diagram
%
% (find-es "xypic" "two-and-three")
$$ (B ↓ f) \diagxyto/->/^U \calC \diagxyto/->/^F \Set $$
%
(here $(B ↓ f)$ is the comma category whose objects are pairs
$(A,\phi)$ with $\phi: B → fA$ in $\calD$, and $U$ is the forgetful
functor from this category to $\calC$). Thus $f^*$ is the inverse image
of a geometric morphism $[\calC, \Set] → [\calD, \Set]$, whose direct image
is $\liml_f$. Moreover, any natural transformation $α: f → g$ between
functors $\calC → \calD$ induces a natural transformation $f^* → g^*$ (whose
value at $F$ is the natural transformation $Fα: Ff → Fg$), i.e. a
geometric transformation \elephantpage{164} $(\liml_f,f^*) →
(\liml_g,g^*)$. Thus the assignment $\calC \mto [\calC,\Set]$ can be made
into a functor (that is, a 2-functor) from the 2-category $\frakCat$
of small categories, functors and natural transformations into
$\frakTop$ (in fact into $\frakTop/\Set$).

\sdd

We note that the geometric morphisms which arise as in 4.1.4, though
not as special as those of 4.1.2, still have the property that their
inverse image functors have left adjoints as well as right adjoints.
We call a geometric morphism $f$ {\it essential} if it has this
property; we normally write $f_!$ for the left adjoint of $f^*$. With
the aid of this notion, we can prove a partial converse to 4.1.4:

\bsk

% «elephant-A4.1.5» (to ".elephant-A4.1.5")
% (find-elephanttext (+ 17 164))
% (find-elephantpage (+ 17 164) "Lemma 4.1.5")

\BF{Lemma 4.1.5} Let $\calC$ and $\calD$ be small categories such that $\calD$ is
Cauchy-complete (cf.\ 1.1.10). Then every essential geometric morphism
$f: [\calC,\Set] → [\calD, \Set]$ is induced as in 4.1.4 by a functor $\calC →
\calD$.

\bsk

% «elephant-A4.1.8» (to ".elephant-A4.1.8")
% (find-elephanttext (+ 17 165))
% (find-elephantpage (+ 17 165) "Example 4.1.8")

\BF{Example 4.1.8} Let $(\calC,T)$ be a small site, as defined in 2.1.9.
The inclusion functor $\Sh(\calC,T) → [\calC^\op,\Set]$ has a cartesian left
adjoint (the {\it associated sheaf functor} --- this is a special case
of a result which we shall prove in 4.4.8 below), so it is the direct
image of a geometric morphism.

\bsk

% «elephant-A4.1.10» (to ".elephant-A4.1.10")
% (find-elephanttext (+ 17 165))
% (find-elephantpage (+ 17 165) "Example 4.1.10")

\BF{Example 4.1.10} Let $\calC$ and $\calD$ be small cartesian categories,
and $f:\calC→\calD$ a cartesian functor. We shall show that in this case the
left Kan extension functor $\limr_f [\calC^\op,\Set], [\calD^\op,\Set]$,
whose {\it direct} image is $f^*$ (compare 4.1.4). To verify this,
note that for any $B ∈ \ob \calD$, the functor $\limr_f(-)(B)
[\calC^\op,\Set] → \Set$ may be described as the composite
%
$$ [\calC^\op,\Set]
   \diagxyto/->/^{U^*}
   [(B ↓ f)^\op, \Set]
   \diagxyto/->/^{\limr}
   \Set
$$
%
\elephantpage{166} where $U:(B ↓ f) → \calC$ is the forgetful functor, as
before.

\bsk

% «elephant-A4.2.6» (to ".elephant-A4.2.6")
% (find-elephanttext (+ 17 180))
% (find-elephantpage (+ 17 180) "Lemma 4.2.6 (iii) and (iv)")

\BF{Lemma 4.2.6} Let $f: \calF → \calE$ be a geometric morphism. The
following conditions are equivalent:

\sdd

(iii) $f^*$ is faithful. 

(iv) The unit $η$ of the adjunction $(f^* ⊣ f_*)$ is monic. 

\sdd

A geometric morphism satisfying the equivalent conditions of Lemma
4.2.6 is called a {\it surjection}. We next list some typical
examples.

% «elephant-A4.2.7» (to ".elephant-A4.2.7")
% (find-elephanttext (+ 17 181))
% (find-elephantpage (+ 17 181) "Examples 4.2.7 (b) and (c)")
% (find-elephantpage (+ 17 182) "inclusion")

\ssk

\BF{Examples 4.2.7} (...)

(b) Let $f: \calC → \calD$ be a functor between small categories. If $f$ is
surjective on objects, then it is easily verified that the functor
$f^*: [\calD, \Set] → [\calC, \Set]$ is conservative; for a natural
transformation a between functors $\calD → \Set$ is an isomorphism iff
$α_B$ is bijective for every object $B$ of $\calD$. So the geometric
morphism $[\calC, \Set] → [\calD, \Set]$ induced by $f$ as in 4.1.4 is
surjective.

\sdd

(c) Let $f: X → Y$ be a continuous map of topological spaces. If $f$
is surjective, then the geometric morphism $\Sh(X) → \Sh(Y)$ induced
by $f$ as in 4.1.11 is a surjection.

\bsk

% «elephant-A4.2.9» (to ".elephant-A4.2.9")
% (find-elephanttext (+ 17 182))
% (find-elephantpage (+ 17 182) "Lemma 4.2.9")

\BF{Lemma 4.2.9} A geometric morphism is an inclusion iff its direct
image is a cartesian closed functor (i.e. preserves exponentials).

\bsk

% «elephant-A4.2.10» (to ".elephant-A4.2.10")
% (find-elephanttext (+ 17 183))
% (find-elephantpage (+ 17 183) "Theorem 4.2.10")

\BF{Theorem 4.2.10} Every geometric morphism can be factored, uniquely
up to canonical equivalence, as a surjection followed by an inclusion.

\bsk

% «elephant-A4.2.12» (to ".elephant-A4.2.12")
% (find-elephanttext (+ 17 184))
% (find-elephantpage (+ 17 184) "Examples 4.2.12 (b) and (c)")
% (find-elephantpage (+ 17 189) "Grothendieck coverages")

\BF{Examples 4.2.12} (...)

(b) Let $f: \calC → \calD$ be a functor between small categories. If $f$ is
full and faithful, then the induced geometric morphism $[\calC, \Set] →
[\calD, \Set]$ is an inclusion; (...)

(c) Let $f:X→Y$ be a continuous map of topological spaces. Then it is
straightforward to verify that $f_*: \Sh(X) → \Sh(F)$ is faithful iff
it is full and faithful, iff $f¹: \Opens(Y) → \Opens(X)$ is
surjective. If $X$ is a subspace of $Y$ and $f$ is the inclusion, then
the latter condition is satisfied; the converse holds (up to
homeomorphism) provided $Y$ satisfies the $T_0$ separation axiom, in
which case the surjectivity of $f¹$ forces $f$ to be injective.
Combining this with 4.2.7(c), we see that if we apply the
factorization of 4.2.10 to the morphism $\Sh(X) → \Sh(F)$ induced by
an arbitrary continuous $f:X→Y$, we obtain $\Sh(I)$, where $I$ is the
image of $f$ topologized as a subspace of $Y$ (that is, we obtain the
coimage factorization in $\Sp$, rather than the image factorization).


\bsk

% «elephant-A4.3.6» (to ".elephant-A4.3.6")
% (find-elephanttext (+ 17 189))
% (find-elephantpage (+ 17 189) "Lemma 4.3.6")
% (find-elephantpage (+ 17 190) "(b) (i) and (ii)")

\BF{Lemma 4.3.6} Let $L$ be a cartesian reflector on a cartesian
category $\calE$, corresponding to a reflective subcategory $\calL$, and let
$c_L$ denote the universal closure derived from $L$ as in 4.3.2. Let A be an object of €. Then 

\ssk

(a) The following are equivalent: 

(i) A is $c_L$-separated. 

(ii) The unit map $η_A: A → LA$ is monic. 

(iii) $A$ is a subobject of an object of $C$. 

(iv) The diagonal map $A \mto A × A$ is $c_L$ -closed. 

\ssk

(b) The following are equivalent: 

(i) A is a $c_L$-sheaf. 

(ii) The unit $η_a : A → LA$ is an isomorphism. 

(iii) $A$ is an object of $C$. 

\bsk

% «elephant-A4.3.9» (to ".elephant-A4.3.9")
% (find-elephanttext (+ 17 192))
% (find-elephantpage (+ 17 192) "Theorem 4.3.9")

\BF{Theorem 4.3.9} Let $\calE$ be a topos, and $L$ a cartesian reflector
on $\calE$, corresponding to a reflective subcategory $\calL$. Then $\calL$ is
a topos, and the inclusion $\calL → \calE$ is the direct image of a
geometric morphism, whose inverse image is (the factorization through
$\calL$ of) L.

% «elephant-A4.5.2» (to ".elephant-A4.5.2")
% (find-elephanttext (+ 17 205))
% (find-elephantpage (+ 17 205) "Example 4.5.2")

\bsk

\BF{Example 4.5.2} Let $\calC$ be a small category, and $\calD$ a full
subcategory of $\calC$. Then the geometric morphism $[\calD, \Set] → [\calC,
  \Set]$ induced by the inclusion $\calD → \calD$ is an inclusion by
4.2.12(b); so it corresponds to a local operator on $[\calC, Set]$.

\bsk

% «elephant-A4.5.8» (to ".elephant-A4.5.8")
% (find-elephanttext (+ 17 209))
% (find-elephantpage (+ 17 209) "Proposition 4.5.8 (i)")

\BF{Proposition 4.5.8} Let $j$ be a local operator on a topos $\calE$. The following 
conditions are equivalent: 

(i) The associated sheaf functor $L: \calE → \sh_j(\calE)$ preserves the subobject 
classifier. 

(ii) The canonical monomorphism $Ω_j → Ω$ is $j$-dense. 

(iii) For any $\phi: A → Ω$, the equalizer of $\phi$ and $j\phi$ is a
$j$-dense subobject of $A$.

(iv) Every monomorphism in $\calE$ may be factored (not necessarily
uniquely) as a $j$-closed monomorphism followed by a $j$-dense one.

(v) $j$ commutes with implication, i.e. the diagram (...) commutes.

% (vi) The diagram (...) commutes.

\bsk

% «elephant-A4.5.9» (to ".elephant-A4.5.9")
% (find-elephanttext (+ 17 211))
% (find-elephantpage (+ 17 211) "Example 4.5.9")
% (find-elephantpage (+ 17 211) "We write Lop(E)")

Example 4.5.9 Let $¬: Ω → Ω$ be the Heyting negation map, i.e. the
classifying map of $⊥: 1 \monicto Ω$. It is straightforward to verify
that the composite $¬¬$ is a local operator, i.e. that it satisfies
the conditions of 4.4.1. Moreover, it satisfies the conditions of
4.5.8: to see this, observe that for any element $x$ of a Heyting
algebra if, we have $x ≤ (¬¬x ⇒ x)$ and $¬x ≤ (¬¬x ⇒ x)$ (the latter
since $(¬x ∧ ¬¬x) = ⊥ ≤ x$), and so $(¬¬x ⇒ x) ≥ (x ∨ ¬x)$; hence
$¬¬(¬¬x ⇒ x) ≥ ¬¬(x∨¬x) = ⊤$. But this is just the statement that the
diagram in (vi) of 4.5-8 commutes. Alternatively, we could use
condition (iv): given a subobject $A' \monicto A$, if we set
$A'' = A' ∪ ¬A'$, then $A' \monicto A''$ is $¬¬$-closed (since it is
complemented) and $A'' \monicto A$ is $¬¬$-dense (cf. the proof of
1.4.14).

We note that the subtopos $\sh_{¬¬}(\calE)$ is Boolean; for if $A$ is any
$¬¬$-sheaf, its subobjects in $\sh_{¬¬}(\calE)$ are its $¬¬$-closed
subobjects in $\calE$, and these form a Boolean algebra. It is easy to
see that it is not an open subtopos in general; for example, if $X$ is
a $T_0$-space (such as $\R$) in which no nonempty open subspace is
discrete, then $\sh_{¬¬}(\Sh(X))$ cannot be open. We shall have more
to say about Boolean subtoposes in 4.5.21 below.

\msk

We write $\Lop(\calE)$ for the class of all local operators on a topos
$\calE$ (note that it is a set if $\calE$ is locally small). $\Lop(\calE)$
carries a natural partial order, defined by $j_1 ≤ j_2$ iff $∧(j_1,
j_2) = j_1$; this is equivalent to saving that $J_1 < J_2$ in
$\Sub(Ω)$, or that $Ω_{j_2} ≤ Ω_{j_1}$, or that $\sh_{j_2}(\calE) ⊆
\sh_{j_1}(\calE)$ as subcategories of $\calE$ (the more dense monomorphisms
we have, the more conditions an object has to satisfy to be a sheaf).
We shall see eventually that $\Lop(\calE)$ is a Heyting algebra; for the
moment, we note

\msk

% «elephant-A4.5.10» (to ".elephant-A4.5.10")
% (find-elephanttext (+ 17 211))
% (find-elephantpage (+ 17 211) "Lemma 4.5.10")
% (find-elephantpage (+ 17 215) "(e)")

\BF{Lemma 4.5.10} The partial ordering $\Lop(\calE)$ has greatest and
least elements, and binary meets.

\bsk

% «elephant-A4.5.20» (to ".elephant-A4.5.20")
% (find-elephanttext (+ 17 219))
% (find-elephantpage (+ 17 219) "Corollary 4.5.20")
% (find-elephantpage (+ 17 219) "the local operator ¬¬ of 4.5.9 is dense")

\BF{Corollary 4.5.20} Any geometric inclusion $\calE' → \calE$ has a unique
factorization $\calE' → \calE'' → \calE$, where $\calE' → \calE''$ is dense and
$\calE'' → \calE$ is closed.

\bsk

% «elephant-A4.6.2» (to ".elephant-A4.6.2")
% (find-elephanttext (+ 17 224))
% (find-elephantpage (+ 17 224) "Examples 4.6.2 (a), (c), (f)")

\BF{Examples 4.6.2} (a) Every inclusion is localic, for if $f$ is an
inclusion then every object of its domain is isomorphic to one of the
form $f^* A$. More generally, if $f_*$ is merely faithful, then the
counit $f^*f_*B → B$ is epic for all $B$, and so $f$ is localic.

\sdd

(c) Let $f: \calC → \calD$ be a functor between small categories. If $f$ is
faithful, then the induced geometric morphism $[\calC, \Set] → [\calD,
  \Set]$ of 4.1.4 is localic. For every functor $\calC → Set$ is a
quotient of a coproduct of representable functors; if $f$ is faithful
then the representable functor $\calC (A, —)$ is a subfunctor of
$f^*(\calD(f(A),—))$; and $f^*$ preserves coproducts. The converse is
also true: if $\calC (A, —)$ appears as a subquotient of some $f^*(F)$,
then (being projective) it actually occurs as a subobject of $f^*(F)$,
and this can only happen if there exists $x ∈ F(f(A))$ such that
$F(fα)(x) \neq F(fβ)(x)$ whenever $α, β: A \rightrightarrows B$ are
distinct morphisms of $\calC -$ which in particular forces $fα \neq fβ$.

(d) In particular, if $\calC$ is a preorder (so that the unique functor
from $\calC$ to the terminal category $\mathbf{1}$ is faithful), then the
unique geometric morphism $[\calC, \Set] → \Set$ of 4.1.9 is localic.

(e) It is easy to verify that a composite of localic morphisms is
localic, since the subquotient relation is transitive and inverse
image functors preserve monomorphisms and epimorphisms. So, combining
(a) and (d), we see that if $(\calC, T)$ is a small site whose underlying
category is a preorder, then the unique geometric morphism $\Sh(\calC, T)
→ \Set$ is localic. (We shall prove a converse to this result in
B3.3.5.) In particular, for any topological space $X$, $\Sh(X) → \Set$
is localic. Similarly, combining (a) and (b), we note that the
surjection with Boolean domain constructed in the proof of 4.5.23 is
localic.

(f) It is even easier to verify that, if
%
$$ \calG \diagxyto/->/^{g} \calF \diagxyto/->/^{f} \calE $$
%
is a composable pair of geometric morphisms and the composite $fg$ is
localic, then $g$ is localic. Hence if $\calF$ and $\calG$ both admit
localic morphisms to $\Set$, then any geometric morphism between them
is localic. For example, the geometric morphism $\Sh(X) → \Sh(Y)$
induced by a continuous map of spaces $X → Y$, as in 4.1.11, is always
localic.

\bsk

% «elephant-A4.6.5» (to ".elephant-A4.6.5")
% (find-elephanttext (+ 17 226))
% (find-elephantpage (+ 17 226) "Theorem 4.6.5")

\BF{Theorem 4.6.5} Any geometric morphism can be factored, uniquely up
to equivalence, as a hyperconnected morphism followed by a localic
one.

% «elephant-A4.6.6» (to ".elephant-A4.6.6")
% (find-elephanttext (+ 17 226))
% (find-elephantpage (+ 17 226) "Proposition 4.6.6 (i) and (iv)")

\bsk

\BF{Proposition 4.6.6} Let $f:\calF→\calE$ be a geometric morphism. The
following are equivalent:

(i) $f$ is hyperconnected. 

(ii) $f^*$ is full and faithful, and its image is closed under
subobjects in $\calF$.

(iii) $f^*$ is full and faithful, and its image is closed under
quotients in $\calF$.

(iv) The unit and counit of $(f^* ⊣ f_*)$ are both monic. 

(v) $f_*$ preserves $Ω$, i.e. the comparison map $\tau: f_*(Ω_{\calF}) →
Ω_{\calE}$ (the classifying map of $f_*(⊤_{\calF})$) is an isomorphism.

(vi) For each object $A$ of $\calE$, $f^*$ induces an equivalence
$\Sub_{\calE}(A) ≃ Sub_{\calF}(f^*A)$.

% «elephant-A4.6.10» (to ".elephant-A4.6.10")
% (find-elephanttext (+ 17 231))
% (find-elephantpage (+ 17 231) "Proposition 4.6.10 (i) and (iii)")


\end{document}







\end{document}


% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End:
