% (find-angg "LATEX/2017elephant.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017elephant.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2017elephant.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2017elephant.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2017elephant; makeindex 2017elephant"))
% (defun e () (interactive) (find-LATEX "2017elephant.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017elephant"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-xpdfpage "~/LATEX/2017elephant.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017elephant.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017elephant.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017elephant.pdf
%               file:///tmp/2017elephant.pdf
%           file:///tmp/pen/2017elephant.pdf
% http://angg.twu.net/LATEX/2017elephant.pdf
%
% «.title-page»			(to "title-page")
% «.surj-incl»			(to "surj-incl")
% «.dense-closed»		(to "dense-closed")
%
% «.elephant-A1.1.1»		(to "elephant-A1.1.1")
% «.elephant-A2.1.3»		(to "elephant-A2.1.3")
% «.elephant-A2.1.8»		(to "elephant-A2.1.8")
% «.elephant-A2.1.9»		(to "elephant-A2.1.9")
% «.elephant-A2.1.10»		(to "elephant-A2.1.10")
% «.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.8»		(to "elephant-A4.2.8")
% «.elephant-A4.2.9»		(to "elephant-A4.2.9")
% «.elephant-fact-p.182»	(to "elephant-fact-p.182")
% «.elephant-A4.2.10»		(to "elephant-A4.2.10")
% «.elephant-A4.2.12»		(to "elephant-A4.2.12")
% «.elephant-A4.3»		(to "elephant-A4.3")
% «.elephant-A4.3.1»		(to "elephant-A4.3.1")
% «.elephant-A4.3.1-cL»		(to "elephant-A4.3.1-cL")
% «.elephant-A4.3.2»		(to "elephant-A4.3.2")
% «.elephant-A4.3.3»		(to "elephant-A4.3.3")
% «.elephant-A4.3.4»		(to "elephant-A4.3.4")
% «.elephant-A4.3.5»		(to "elephant-A4.3.5")
% «.elephant-A4.3.6»		(to "elephant-A4.3.6")
% «.elephant-A4.3.7»		(to "elephant-A4.3.7")
% «.elephant-A4.3.8»		(to "elephant-A4.3.8")
% «.elephant-A4.3.9»		(to "elephant-A4.3.9")
% «.elephant-A4.3.10»		(to "elephant-A4.3.10")
% «.elephant-A4.3.11»		(to "elephant-A4.3.11")
%
% «.elephant-A4.4»		(to "elephant-A4.4")
% «.elephant-A4.4.1»		(to "elephant-A4.4.1")
% «.elephant-A4.4.2»		(to "elephant-A4.4.2")
% «.elephant-A4.4.4»		(to "elephant-A4.4.4")
% «.elephant-A4.4.8»		(to "elephant-A4.4.8")
% «.elephant-A4.5.2»		(to "elephant-A4.5.2")
% «.elephant-A4.5.3»		(to "elephant-A4.5.3")
% «.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.19»		(to "elephant-A4.5.19")
% «.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")
%
% «.my-old-diagrams»		(to "my-old-diagrams")
%
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx17}               % (find-angg "LATEX/edrx17.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end


\def\ph{\phantom}
\def\ovl{\overline}

\def\bbG{{\mathbb{G}}}

\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\elephantpage#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\calS{\mathcal{S}}
\def\Ran{\text{Ran}}

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

%L sections = {}
%L addsection = function (p, title) table.insert(sections, {p, title}) end

\def\BFT#1{\noindent{\bf#1}\quad}
\def\BF#1{\directlua{addsection(\the\count0, "#1")}\BFT{#1}}
\pu

% (find-LATEXgrep "grep -nH -e pbsy *")
% (find-LATEX "edrx17.sty" "pbsymbol")
\def\pbsymbol#1{\vcenter{\hbox{\unitlength=#1pt%
  \begin{picture}(1,1)(0,0)
    \Line(0,0)(1,0)(1,1)
  \end{picture}}}}

% (find-dn4 "experimental.lua" "relplace")
% (find-dn6file "diagforth.lua" "forths[\"place\"] =")
% (find-dn6 "diagtex.lua" "DxyPlace")
% (find-dn6file "diagtex.lua" "node_to_TeX =")
%L
%L forths["relplace"] = function ()
%L     local x, y = ds:pick(0).x, ds:pick(0).y
%L     local dx, dy = getwordasluaexpr(), getwordasluaexpr()
%L     local TeX = getword()
%L     ds:push(storearrow(DxyPlace {{x=x+dx, y=y+dy, tex=TeX}}))
%L   end
%
% Usage: NODE relplace 7 7 \pbsymbol{7}



% ---------------------------------------------
%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title-page» (to ".title-page")


{\setlength{\parindent}{0em}

{\bf Notes on notation: Elephant}

Eduardo Ochs, 2017

Version at the bottom of the page.

eduardoochs@gmail.com

\url{http://angg.twu.net/LATEX/2017elephant.pdf}

\url{http://angg.twu.net/math-b.html\#notes-on-notation}

\bsk

All the extracts from page 3 onwards are from Peter Johstone's
``Sketches of an Elephant'', vol.1, sections A1 (``Regular and
Cartesian Closed Categories'') and A4 (``Geometric Morphisms - Basic
Theory''). They are interspersed with my notes about what are the
``missing diagrams'' in the book; the idea of ``missing diagrams'' is
explained here:

\url{http://angg.twu.net/math-b.html\#logic-for-children-unilog-2018}

\url{http://angg.twu.net/LATEX/2017vichy-workshop.pdf}

\url{http://www.uni-log.org/wk6-logic-for-children.html}

\msk

The diagrams in the first pages are for the third paper in this series:

\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}

}

\newpage



% ---------------------
%  ____             _       _            _ 
% / ___| _   _ _ __(_)     (_)_ __   ___| |
% \___ \| | | | '__| |_____| | '_ \ / __| |
%  ___) | |_| | |  | |_____| | | | | (__| |
% |____/ \__,_|_| _/ |     |_|_| |_|\___|_|
%                |__/                      
%
% «surj-incl» (to ".surj-incl")

Surjections (defined in A4.2.6(iv)),

inclusions (defined in A4.2.9),

and some examples:

%D diagram surj-1
%D 2Dx     100 +25    +25 +25
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> f^*D D
%D ren A2  A3  ==> E f_*E
%D ren A0' A2' ==> f^*f_*E E
%D ren A1' A3' ==> D f_*f^*D
%D ren A4  A5  ==> \calF \calE
%D
%D (( # A0' A2' -> .plabel= l \sm{ε_B\\=\id}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a f
%D    A4 A5 -> .plabel= b \text{(surj)}
%D ))
%D enddiagram
%D
%D diagram surj-2
%D 2Dx     100 +25    +40 +30
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fool{D_{12}}{D_{12}} D_{12}
%D ren A2  A3  ==> \fool{E_1}{E_2} E_1{×}E_2
%D ren A0' A2' ==> f^*f_*E E
%D ren A1' A3' ==> D_{12} D_{12}{×}D_{12}
%D ren A4  A5  ==> \Set^\fool{1}{2} \Set^{(12)}
%D
%D (( # A0' A2' -> .plabel= l \sm{ε_B\\=\id}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a f
%D    A4 A5 -> .plabel= b \text{(surj)}
%D ))
%D enddiagram
%D
%D diagram surj-3
%D 2Dx     100 +25    +50 +50
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fool{D_3}{D_4} \foor{D_3}{D_4}
%D ren A2  A3  ==> \fool{E_3}{E_4} \foor{E_3{×}E_4}{E_4}
%D ren A0' A2' ==> f^*f_*E E
%D ren A1' A3' ==> \foor{D_3}{D_4} \foor{D_3{×}D_4}{D_4}
%D ren A4  A5  ==> \Set^\fool{3}{4} \Set^\foor{3}{4}
%D
%D (( # A0' A2' -> .plabel= l \sm{ε_B\\=\id}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a f
%D    A4 A5 -> .plabel= b \text{(surj)}
%D ))
%D enddiagram
%D
%D
%D
%D
%D diagram incl-1
%D 2Dx     100 +20    +25 +25
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> h^*D D
%D ren A2  A3  ==> E h_*E
%D ren A0' A2' ==> h^*h_*E E
%D ren A1' A3' ==> D h_*h^*D
%D ren A4  A5  ==> \calF \calE
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    # A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%D
%D diagram incl-2
%D 2Dx     100 +20    +45 +25
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fool{D_6} \foor{D_5}{D_6}{D_7}
%D ren A2  A3  ==> \fool{E_6} \foor{E_6}{E_6}{1}
%D ren A0' A2' ==> \fool{E_6} \fool{E_6}
%D ren A1' A3' ==> D h_*h^*D
%D ren A4  A5  ==> \Set^\fool{6} \Set^\foor{5}{6}{7}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    # A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%D
%D diagram incl-3
%D 2Dx     100 +20    +35 +25
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fool{D_8} \foor{D_8}{D_9}
%D ren A2  A3  ==> \fool{E_8} \foor{E_8}{1}
%D ren A0' A2' ==> \fool{E_8} \fool{E_8}
%D ren A1' A3' ==> D h_*h^*D
%D ren A4  A5  ==> \Set^\fool{8} \Set^\foor{8}{9}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    # A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%D
$$\pu
  \begin{array}{ccc}
  \diag{surj-1}
  &
  \diag{incl-1}
  \\
  \\
  \def\fool#1#2{{(#1\ph{M}#2)}}
  \def\foor#1{{#1}}
  \diag{surj-2}
  &
  \def\fool#1{{(#1)}}
  \def\foor#1#2#3{{(#1→#2→#3)}}
  \diag{incl-2}
  \\
  \\
  \def\fool#1#2{{(#1\ph{M}#2)}}
  \def\foor#1#2{{(#1→#2)}}
  \diag{surj-3}
  &
  \def\fool#1{{(#1)}}
  \def\foor#1#2{{(#1\ph{M}#2)}}
  \diag{incl-3}
  \end{array}
$$

\bsk
\bsk

The factorization (theorem A4.2.10),

and an example:

%D diagram facto
%D 2Dx     100 +50 +50
%D 2D  100 A0      A2
%D 2D
%D 2D  +20 B0  B1  B2
%D 2D
%D ren A0 ==> \Set^\fool
%D ren A2 ==> \Set^\foor
%D ren B0 ==> \Set^\fool
%D ren B1 ==> \Set^\foom
%D ren B2 ==> \Set^\foor
%D
%D (( A0 A2 -> .plabel= a f
%D    B0 B1 -> .plabel= a g
%D    B0 B1 -> .plabel= b \text{(surj)}
%D    B1 B2 -> .plabel= a h
%D    B1 B2 -> .plabel= b \text{(incl)}
%D    
%D ))
%D enddiagram
%D
$$\pu
  \def\fool{{\psm{1&&2\\3& &4\\5}}}
  \def\foom{{\psm{12  \\3&→&4\\5}}}
  \def\foor{{\psm{12  \\3&→&4\\5&&6}}}
  \diag{facto}
$$

%D diagram facto-2
%D 2Dx     100 +55 +55 +60
%D 2D  100 A0          A3
%D 2D
%D 2D  +20 B0  B1      B3
%D 2D
%D 2D  +20     C1  C2  C3 
%D 2D
%D ren A0 ==> \Set^\fool
%D ren A3 ==> \Set^\foor
%D ren B0 ==> \Set^\fool
%D ren B1 ==> \Set^\foom
%D ren B3 ==> \Set^\foor
%D ren C1 ==> \Set^\foom
%D ren C2 ==> \Set^\fooM
%D ren C3 ==> \Set^\foor
%D
%D (( A0 A3 -> .plabel= a f
%D    B0 B1 -> .plabel= a g
%D    B0 B1 -> .plabel= b \text{(surj)}
%D    B1 B3 -> .plabel= a h
%D    B1 B3 -> .plabel= b \text{(incl)}
%D    C1 C2 -> .plabel= a i
%D    C1 C2 -> .plabel= b \text{(dense)}
%D    C2 C3 -> .plabel= a j
%D    C2 C3 -> .plabel= b \text{(closed)}
%D    
%D ))
%D enddiagram
%D
$$\pu
  \def\fool{{\psm{1&&2\\3& &4\\ &&6}}}
  \def\foom{{\psm{12  \\3&→&4\\ &&6}}}
  \def\fooM{{\psm{12  \\3&→&4\\ & &6&→7}}}
  \def\fooM{{\psm{12  \\3&→&4\\5&→&6}}}
  \def\foor{{\psm{12  \\3&→&4\\5&→&6&→7}}}
  \diag{facto-2}
$$











\newpage

\def\fooone    #1{{(#1)}}
\def\footwo  #1#2{{(#1→#2)}}
\def\foothr#1#2#3{{(#1→#2→#3)}}
\def\Setone    #1{\Set^{(#1)}}
\def\Settwo  #1#2{\Set^{(#1→#2)}}
\def\Setthr#1#2#3{\Set^{(#1→#2→#3)}}


$\Setone{6}→\Setthr{5}{6}{7}$:

$ηcD: cD→g_*g^*cD$ is $\foothr{D_6}{D_6}{D_6} → \foothr{D_6}{D_6}{1}$ (not monic)

$\Ran_g\fooone{0} = \foothr{0}{0}{0}$ (not initial)

%D diagram incl-5-567
%D 2Dx     100 +20    +45 +60
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     a4 <=> a5
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fooone{D_6} \foothr{D_5}{D_6}{D_7}
%D ren A2  A3  ==> \fooone{E_6} \foothr{E_6}{E_6}{1}
%D ren A0' A2' ==> \fooone{E_6} \fooone{E_6}
%D ren A1' A3' ==> \foothr{D_6}{D_6}{D_6} \foothr{D_6}{D_6}{1}
%D ren a4  a5  ==> \fooone{0} \foothr{0}{0}{1}
%D ren A4  A5  ==> \Set^\fooone{6} \Set^\foothr{5}{6}{7}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{not\,monic\,=(}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    a4 a5 -> .plabel= b =(
%D
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%
$$\pu
  \def\fool#1{{(#1)}}
  \def\foor#1#2#3{{(#1→#2→#3)}}
  \diag{incl-5-567}
$$

\bsk
\bsk

$\Setone{6}→\Settwo{5}{6}$ is dense:

$ηcD: cD→g_*g^*cD$ is $\footwo{D_6}{D_6} → \footwo{D_6}{D_6}$ (monic)

$\Ran_g\fooone{0} = \footwo{0}{0}$ (initial)
%
%D diagram incl-6-56
%D 2Dx     100 +20    +45 +45
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     a4 <=> a5
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fooone{D_6} \footwo{D_5}{D_6}
%D ren A2  A3  ==> \fooone{E_6} \footwo{E_6}{E_6}
%D ren A0' A2' ==> \fooone{E_6} \fooone{E_6}
%D ren A1' A3' ==> \footwo{D_6}{D_6} \footwo{D_6}{D_6}
%D ren a4  a5  ==> \fooone{0} \footwo{0}{0}
%D ren A4  A5  ==> \Set^\fooone{6} \Set^\footwo{5}{6}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    a4 a5 -> .plabel= b =)
%D
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%
$$\pu
  \diag{incl-6-56}
$$

\bsk
\bsk

$\Setone{6}→\Settwo{6}{7}$ is not dense:

$ηcD: cD→g_*g^*cD$ is $\footwo{D_6}{D_6} → \footwo{D_6}{1}$ (not monic)

$\Ran_g\fooone{0} = \footwo{0}{1}$ (not initial)
%
%D diagram incl-6-67
%D 2Dx     100 +20    +45 +45
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     a4 <=> a5
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \fooone{D_6} \footwo{D_6}{D_7}
%D ren A2  A3  ==> \fooone{E_6} \footwo{E_6}{1}
%D ren A0' A2' ==> \fooone{E_6} \fooone{E_6}
%D ren A1' A3' ==> \footwo{D_6}{D_6} \footwo{D_6}{1}
%D ren a4  a5  ==> \fooone{0} \footwo{0}{1}
%D ren A4  A5  ==> \Set^\fooone{6} \Set^\footwo{6}{7}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{not\,monic\,=(}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    a4 a5 -> .plabel= b =(
%D
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%
$$\pu
  \diag{incl-6-67}
$$



\newpage

$\Settwo{5}{6}→\Setthr{5}{6}{7}$:

$ηcD: cD→g_*g^*cD$ is $\foothr{D_6}{D_6}{D_6} → \foothr{D_6}{D_6}{1}$ (not monic)

$\Ran_g\footwo{0}{0} = \foothr{0}{0}{1}$ (not initial)

%D diagram incl-56-567
%D 2Dx     100 +40    +55 +60
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     a4 <=> a5
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \footwo{D_5}{D_6} \foothr{D_5}{D_6}{D_7}
%D ren A2  A3  ==> \footwo{E_5}{E_6} \foothr{E_6}{E_6}{1}
%D ren A0' A2' ==> \footwo{E_5}{E_6} \footwo{E_5}{E_6}
%D ren A1' A3' ==> \foothr{D_6}{D_6}{D_6} \foothr{D_6}{D_6}{1}
%D ren a4  a5  ==> \footwo{0}{0} \foothr{0}{0}{1}
%D ren A4  A5  ==> \Set^\footwo{5}{6} \Set^\foothr{5}{6}{7}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{not\,monic\,=(}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    a4 a5 -> .plabel= b =(
%D
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%
$$\pu
  \diag{incl-56-567}
$$

\bsk
\bsk

$\Settwo{6}{7}→\Setthr{5}{6}{7}$:

$ηcD: cD→g_*g^*cD$ is $\foothr{D_6}{D_6}{D_6} \foothr{D_6}{D_6}{D_6}$ (monic)

$\Ran_g\footwo{0}{0} = \foothr{0}{0}{0}$ (initial)

%D diagram incl-67-567
%D 2Dx     100 +40    +55 +60
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |  |  
%D 2D      v   v       v  v  
%D 2D  +20 A2' A2 |-> A3  A3'
%D 2D         
%D 2D  +15     a4 <=> a5
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0  A1  ==> \footwo{D_6}{D_7} \foothr{D_5}{D_6}{D_7}
%D ren A2  A3  ==> \footwo{E_6}{E_7} \foothr{E_6}{E_6}{E_7}
%D ren A0' A2' ==> \footwo{E_6}{E_7} \footwo{E_6}{E_7}
%D ren A1' A3' ==> \foothr{D_6}{D_6}{D_6} \foothr{D_6}{D_6}{D_6}
%D ren a4  a5  ==> \footwo{0}{0} \foothr{0}{0}{0}
%D ren A4  A5  ==> \Set^\footwo{6}{7} \Set^\foothr{5}{6}{7}
%D
%D (( A0' A2' -> .plabel= l \sm{\ph{so}ε\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{monic}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    a4 a5 -> .plabel= b =)
%D
%D    A4 A5 -> .plabel= a h
%D    A4 A5 -> .plabel= b \text{(incl)}
%D ))
%D enddiagram
%
$$\pu
  \diag{incl-67-567}
$$


\newpage




%  ____                                 _                    _ 
% |  _ \  ___ _ __  ___  ___        ___| | ___  ___  ___  __| |
% | | | |/ _ \ '_ \/ __|/ _ \_____ / __| |/ _ \/ __|/ _ \/ _` |
% | |_| |  __/ | | \__ \  __/_____| (__| | (_) \__ \  __/ (_| |
% |____/ \___|_| |_|___/\___|      \___|_|\___/|___/\___|\__,_|
%                                                              
% «dense-closed» (to ".dense-closed")
% (elep 5 "dense-closed")
% (ele    "dense-closed")
% (find-elephantpage (+ 1104  66) "General Index" "Local operator")
% (find-elephantpage (+ 1104  66) "General Index" "Local operator" "A4.5.3")
% (find-elephantpage (+ 1104  66) "General Index" "Local operator" "A4.5.20")
% https://ncatlab.org/nlab/show/%28dense%2Cclosed%29-factorization
% https://ncatlab.org/nlab/show/dense+subtopos

Dense-closed factorization (A4.5.20)

A geometric morphism $f$ is an inclusion when all counit maps $εE:
f^*f_*E→E$ are isos (A4.2.9); a geometric inclusion is dense exactly
when all the unit maps on constant presheaves, $ηcD: cD→ g_*g^*cD$,
are monics, and closed when all the counit maps, $εE: h^*h_*E→E$, are
isos (Peter Arndt, 5.pdf, p.8)...

Problems (Peter, help, please!):

1) I can't find these characterizations of dense and closed in the Elephant,

2) ``closed inclusion'' {\sl should be} stricter than ``inclusion''!...

\url{http://angg.twu.net/LATEX/5.pdf}

%D diagram dense-closed-1
%D 2Dx     100 +20    +25 +20    +25 +20    +25 +25
%D 2D  100 A0' A0 <-----------------------| A1  A1'
%D 2D      |   |                             |  |  
%D 2D      v   v                             v  v  
%D 2D  +20 A2' A2 |-----------------------> A3  A3'
%D 2D                        
%D 2D  +15     A4 <=======================> A5     
%D 2D
%D 2D  +20 B0' B0 <-| B1  B1'    C0' C0 <-| C1  C1'    
%D 2D      |   |       |  |      |   |       |  |      
%D 2D      v   v       v  v      v   v       v  v      
%D 2D  +20 B2' B2 |-> B3  B3'    C2' C2 |-> C3  C3'    
%D 2D                                                  
%D 2D  +15     B4 <=> B5             c4 <=> c5
%D 2D
%D 2D  +15                           C4 <=> C5         
%D 2D
%D ren A0  A1  ==> f^*D D
%D ren A2  A3  ==> E f_*E
%D ren A0' A2' ==> f^*f_*E E
%D ren A1' A3' ==> D f_*f^*D
%D ren A4  A5  ==> \calE' \calE
%D
%D ren B0  B1  ==> g^*D D
%D ren B2  B3  ==> E g_*E
%D ren B0' B2' ==> g^*g_*E E
%D ren B1' B3' ==> cD g_*g^*cD
%D ren B4  B5  ==> \calE' \calE''
%D
%D ren C0  C1  ==> h^*D D
%D ren C2  C3  ==> E h_*E
%D ren C0' C2' ==> h^*h_*E E
%D ren C1' C3' ==> D h_*h^*D
%D ren C4  C5  ==> \calE'' \calE
%D ren c4  c5  ==> 0 h_*0{=}0
%D
%D (( A0' A2' -> .plabel= l \sm{ε\\\text{(iso)}}
%D    # A1' A3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    A4 A5 -> .plabel= a f
%D    A4 A5 -> .plabel= b \text{(inclusion)}
%D    
%D    # B0' B2' -> .plabel= l \sm{ε_B\\=\id}
%D    B1' B3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    B0 B1 <-| B0 B2 -> B1 B3 -> B2 B3 |->
%D    B4 B5 -> .plabel= a g
%D    B4 B5 -> .plabel= b \text{(dense)}
%D    
%D    # C0' C2' -> .plabel= l \sm{ε\\\text{(iso)}}
%D    # C1' C3' -> .plabel= r \sm{η\ph{monic}\\\text{(monic)}}
%D    C0 C1 <-| C0 C2 -> C1 C3 -> C2 C3 |->
%D    C4 C5 -> .plabel= a h
%D    C4 C5 -> .plabel= b \text{(closed)}
%D    c4 c5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{dense-closed-1}
$$






\newpage

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


% -----------
%     _    _ 
%    / \  / |
%   / _ \ | |
%  / ___ \| |
% /_/   \_\_|
%            
% «elephant-A1.1.1» (to ".elephant-A1.1.1")
% (find-books "__cats/__cats.el" "johnstone-elephant")
% (find-elephantpage (+  17    3) "A1.1 Preliminary assumptions")
% (find-elephantpage (+  17    4) "Lemma 1.1.1")

\BF{A1.1 Preliminary assumptions}

\sdd

A {\sl full} subcategory, of course, is one whose inclusion functor is
full; but when dealing with subcategories we shall generally assume
(sometimes without saying so explicitly) that they are also {\sl
  replete}, i.e., that any object of the ambient category isomorphic
to one in the subcategory is itself in the subcategory. The full
subcategories of $\calC$ correspond to classes of objects of $\calC$
which are closed under isomorphism. In particular, for us a {\sl
  reflective} subcategory will always mean a full, replete subcategory
whose inclusion functor has a left adjoint.

We use the term {\sl reflection} for an adjunction whose right adjoint
is full and faithful, and {\sl reflector} for a monad which is
idempotent (i.e., one whose multiplication is an isomorphism); it is
well known that these three concepts are essentially the same. The
following, related, result seems not to be widely known, however; and
since we shall need it occasionally, we sketch its proof here.

\BF{Lemma 1.1.1} Let $F:\calC→\calD$ be a functor having a right
adjoint $G$. If there is any natural isomorphism (nor necessarily the
counit of the adjunction) between $FG$ and the identity functor on
$\calD$, then $(F⊣G)$ is a reflection.
%
%D diagram reflective
%D 2Dx     100    +25
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> LD D
%D ren A2 A3 ==> S S
%D ren B0 B1 ==> \calS \calD
%D ren C0 C1 ==> \calF \calE
%D
%D (( A0 A1 <-|
%D    A2 A3 |->
%D    A0 A2 ->  A1 A3 ->
%D    B0 B1 <- sl^ .plabel= a L
%D    B0 B1 -> sl_ .plabel= b \text{(inc)}
%D    # C0 C1 -> .plabel= m f
%D ))
%D enddiagram
%D
%D diagram reflector
%D 2Dx     100    +30    +40
%D 2D  100 A0 --> A1 <-- A2
%D 2D
%D 2D  +20
%D 2D
%D ren A0 A1 A2 ==> A TA TTA
%D ren A0 A1 A2 ==> C TC TTC
%D ren A0 A1 A2 ==> C GFC GFGFC
%D
%D (( A0 A1 -> .plabel= a ηC
%D    # A1 A2 <- .plabel= a \sm{μC=\\GεFC\\\text{(iso)}}
%D    A1 A2 <- .plabel= a \sm{μC:=\\GεFC}
%D    A1 A2 <- .plabel= b \text{(iso)}
%D ))
%D enddiagram
%D
%D diagram reflection
%D 2Dx     100    +25
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> FGD GD
%D ren A2 A3 ==> D GD
%D ren B0 B1 ==> \calD \calC
%D ren C0 C1 ==> \calF \calE
%D
%D (( A0 A1 <-|
%D    A2 A3 |->
%D    A0 A2 -> .plabel= l \sm{εD\\\text{(iso)}} A1 A3 ->
%D    B0 B1 <- sl^ .plabel= a F
%D    B0 B1 -> sl_ .plabel= b G
%D    # C0 C1 -> .plabel= m f
%D ))
%D enddiagram
%D
$$\pu
  \begin{array}{ccc}
  \text{Reflective:} &
  \text{Reflector:} &
  \text{Reflection:} \\
  \\
  %
  \diag{reflective}
  &
  \diag{reflector}
  &
  \diag{reflection} \\
  \end{array}
$$

% $$\pu
%   \diag{reflective}
%   \qquad
%   \diag{reflector}
%   \qquad
%   \diag{reflection}
% $$



\bsk
\bsk

%     _    ____  
%    / \  |___ \ 
%   / _ \   __) |
%  / ___ \ / __/ 
% /_/   \_\_____|
%                
% «elephant-A2.1.3»  (to ".elephant-A2.1.3")
% (find-elephantpage (+ 17 70) "Example 2.1.3")
% (elep 6 "elephant-A2.1.3")
% (ele    "elephant-A2.1.3")

\BF{Definition 2.1.3} For any small category $\calC$, the functor
category $[\calC,\Set]$ is a topos, as we saw in 1.5.5 and 1.6.6.

\newpage

% «elephant-A2.1.8»  (to ".elephant-A2.1.8")
% (elep 8 "elephant-A2.1.8")
% (ele    "elephant-A2.1.8")
% (find-elephantpage (+ 17 72) "Example 2.1.8")
% (find-elephantpage (+ 1104 55) "Index of Notation")
% (find-elephantpage (+ 17 13) "Example A1.2.5" "Sp")

\BF{Example 2.1.8} Let $X$ be a topological space, and let $\Opens(X)$
denote the lattice of open sets of $X$, considered as a (small)
preorder. A {\sl presheaf} (of sets) on $X$ is, by definition, a
functor $\Opens(X)^\op→\Set$; thus the category $[\Opens(X)^\op,\Set]$
of presheaves on $X$ is a topos. If $F$ is a presheaf on $X$, we call
the elements of $F(U)$ (for $U$ an open set of $X$) {\sl sections} of
$F$ over $U$, and we describe the map $F(U)→F(V)$ induced by an
inclusion $V⊆U$ in $\Opens(X)$ as a {\sl restriction} of sections from
$U$ to $V$. The example we have in mind is that, for any object
$p:Y→X$, of $\Sp(X)$, we may define a presheaf $Γ(p)$ by taking
$Γ(p)(U)$ to be the set of sections of $p$ over $U$ (i.e., continuous
maps $s:U→Y$ such that $ps$ is the inclusion map $U→X$); in fact, as
is easily seen, $Γ$ defines a functor $\Sp/X→[\Opens(X)^\op,\Set]$.
%
%D diagram ??
%D 2Dx     100 +20 +25 +25 +25 +40 +40 +30
%D 2D  100 A0      B0  B1  C0  C1  D0  D1
%D 2D  +10     A1
%D 2D  +10 A2      B2  B3  C2  C3  D2  D3
%D 2D  +12                         D4'
%D 2D  +8  A4      B4  B5  C4  C5  D4  D5
%D 2D
%D ren A0 A1 A2 A4       ==> Y X Z \Sp
%D ren B0 B1 B2 B3 B4 B5 ==> (Y,p) Y (Z,q) Z \Sp/X \Sp
%D ren C0 C1 C2 C3 C4 C5 ==> (Y,p) Γ(p) (Z,q) Γ(q) \Sp/X [\Opens(X)^\op,\Set]
%D ren D0 D1 D2 D3 D4' D4 D5 ==> U Γ(p)(U) V Γ(p)(V) \Opens(X)\phantom{!!!} \Opens(X)^\op \Set
%D
%D (( A0 A1 -> .plabel= a p
%D    A0 A2 -> .plabel= l f
%D    A2 A1 -> .plabel= b q
%D    A4 xy+= 10 0 place
%D
%D    B0 B1 |->
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r f
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil |->
%D    B4 B5  ->
%D
%D    C0 C1 |->
%D    C0 C2  -> .plabel= l f
%D    C1 C3  -> .plabel= r Γ(f)
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil |->
%D    C4 C5  -> .plabel= a Γ
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

$Γ(p):=\setofst{(U∈\Opens(X),s:U→Y)}{ps=(U \ito X)}$

$Γ(p)(U):=\setofst{s:U→Y}{ps=(U \ito X)}$
%
%D diagram Gamma-diamond
%D 2Dx     100 +25 +25
%D 2D  100     AZ
%D 2D        ->  ->
%D 2D  +15 A2 ---> A3
%D 2D      ^___  ___^
%D 2D  +15  \  A1  /
%D 2D        \ ^  /
%D 2D  +20     A0
%D 2D
%D 2D  +15     B0
%D 2D
%D ren A0 A1 A2 A3 AZ B0 ==> V U Y X Z \Sp
%D
%D (( A0 A1 `->
%D    A1 A2  -> .plabel= a s
%D    A2 A3  -> .plabel= a p
%D    A0 A2  -> .plabel= b r
%D    A0 A3 `-> sl_
%D    A1 A3 `-> sl_
%D    B0 place
%D
%D    A2 AZ -> .plabel= l f
%D    AZ A3 -> .plabel= r q
%D ))
%D enddiagram
%D
%D diagram Gamma-1
%D 2Dx     100 +30 +40 +45 +25 +40 +40 +30
%D 2D  100 D0  D1  D1' E0
%D 2D  +10 
%D 2D  +10 D2  D3  D3' E1
%D 2D  +12 D4'
%D 2D  +8  D4  D5
%D 2D
%D ren D0 D1 D1' ==> U Γ(p)(U) \setofi{s}
%D ren D2 D3 D3' ==> V Γ(p)(V) \setofi{r}
%D ren D4'   D4 D5 ==> \Opens(X)\phantom{!!!} \Opens(X)^\op \Set
%D ren E0 E1 ==> s s∘(V{\ito}U)
%D
%D (( D0 D1 |->
%D    D2 D0 `->
%D    D1 D3  -> # .plabel= r Γ(p)(V{\ito}U)
%D    D2 D3 |->
%D    D1 D1' = D3 D3' = D1' D3' ->
%D    D0 D3 harrownodes nil 20 nil |->
%D    D4' place
%D    D4 D5  -> .plabel= a Γ(p)
%D    E0 E1 |->
%D ))
%D enddiagram
%D
$$\pu
  \def\setofi#1{\{#1|p#1{=}(\ito)\}}
  \diag{Gamma-diamond}
  \qquad
  \diag{Gamma-1}
$$
%
%D diagram Gamma-2
%D 2Dx     100 +25 +35 +35 +45 +40 +50
%D 2D  100 A0  B0  B1  D0  D1  E0  E1
%D 2D  +10 
%D 2D  +10 A1  B2  B3  D2  D3  E2  E3
%D 2D  +12 A2
%D 2D  +8  A3  C0  C1
%D 2D
%D ren A0 A1 A2 A3 ==> U V \Opens(X)\phantom{!!!} \Opens(X)^\op
%D ren B0 B1 B2 B3 ==> Γ(p)(U) Γ(q)(U) Γ(p)(V) Γ(q)(V)
%D ren C0 C1       ==> Γ(p)    Γ(q)
%D ren D0 D1 D2 D3 ==> \setofps{p}{s} \setofps{q}{s'} \setofps{p}{r} \setofps{q}{r'}
%D ren E0 E1 E2 E3 ==> f f∘s s∘(V{\ito}V) f∘s∘(V{\ito}V)
%D
%D (( A1 A0 `-> A2 place A3 place
%D    B0 B1  ->
%D    B0 B2  ->
%D    B1 B3  ->
%D    B2 B3  ->
%D    C0 C1  -> .plabel= a Γ(f)
%D    D0 D1  ->
%D    D0 D2  ->
%D    D1 D3  ->
%D    D2 D3  ->
%D    E0 E1 |->
%D    E0 E2 |->
%D    E1 E3 |->
%D    E2 E3 |->
%D ))
%D enddiagram
%D
$$\pu
  \def\setofps#1#2{\{#2|#1#2{=}(\ito)\}}
  \diag{Gamma-2}
$$


\newpage

% «elephant-A2.1.9»  (to ".elephant-A2.1.9")
% (elep 6 "elephant-A2.1.9")
% (ele    "elephant-A2.1.9")
% (find-elephantpage (+ 17 73) "Definition 2.1.9")

\BF{Definition 2.1.9} Let $\calC$ be a small category. By a {\sl
  coverage} on $\calC$, we mean a function assigning to each object
$A$ of $\calC$ a collection $T(A)$ of families $(f_i: A_i→A \,|\,
i∈I)$ of morphisms with common codomain $A$ (called {\sl $T$-covering
  families}), such that

\begin{itemize}

\item[(C)] if $(f_i: A_i→A \,|\, i∈I)$ is a $T$-covering family and
  $g:B→A$ is any morphism with codomain $A$, there exists a
  $T$-covering family $(h_j: B_j→B \,|\, j∈J)$ such that each $gh_j$
  factors through some $f_i$.

  \msk

  (...) and replaces (C) with the stronger condition:

\item[(C')] if $(f_i: A_i→A \,|\, i∈I)$ is a $T$-covering family and
  $g:B→A$ is any morphism with codomain $A$, then the family
  $(g^*(f_i) \,|\, i∈I)$ is $T$-covering.

\end{itemize}

A {\sl site} is a small category equipped with a coverage.

\msk

We say a functor $F: \calC^\op → \Set$ {\sl satisfies the sheaf axiom}
for a family of morphisms $(f_i: A_i→A \,|\, i∈I)$ if, whenever we are
given a family of elements $s_i∈F(A_i)$ which are {\sl compatible} in
the sense that, whenever $g: B→A_i$ and $h:B→A_j$ satisfy $f_ig =
f_jh$ (here $i$ and $j$ need not be distinct), we have $F(g)(s_i) =
F(h)(s_j)$, then there exists a unique $s∈F(A)$ such that $F(f_i)(s) =
s_i$ for each $i∈I$. (Once again, this definition may be simplified if
$\calC$ has pullbacks; it then suffices to check the compatibility of
$s_i$ and $s_j$ on the pullback of $f_i$ against $f_j$, rather than on
arbitrary pairs $(g,h)$ as above. in this case, the condition may
conveniently be expressed diagrammatically: $F$ satisfies the sheaf
axiom for $(A_i→A \,|\, i∈I)$ iff
%
% (find-es "xypic" "two-and-three")
$$ F(A) \diagxyto/->/ \prod_{i∈I} F(A_i) \two/->`->/ F(A_i ×_A A_j)$$
%
is an equalizer diagram.) We say that $F$ is a {\sl $T$-sheaf} if it
satisfies the sheaf axiom for every $T$-covering family; and we write
$\Sh(\calC,T)$ (or simply $\Sh(C)$, if $T$ is obvious from the
context) for the full subcategory of $[\calC^\op,\Set]$ whose objects
are $T$-sheaves.

% «elephant-A2.1.10»  (to ".elephant-A2.1.10")
% (find-elephantpage (+ 17 74) "Lemma 2.1.10")
% (elep 8 "elephant-A2.1.10")
% (ele    "elephant-A2.1.10")

\bsk

\BF{Lemma 2.1.10} {\sl If $(C,T)$ is a site, then $\Sh(C,T)$ is a
  topos.}



\newpage

% (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")
% (elep 9 "elephant-A4.1.1")
% (ele    "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")

% \bsk

\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^*$.

%D diagram gm0
%D 2Dx     100    +25
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> f^*E E
%D ren A2 A3 ==> F f_*F
%D ren B0 B1 ==> \calF \calE
%D ren C0 C1 ==> \calF \calE
%D
%D (( A0 A1 <-|
%D    A2 A3 |->
%D    A0 A2 ->  A1 A3 ->
%D    B0 B1 <- sl^ .plabel= a f^*
%D    B0 B1 -> sl_ .plabel= b f_*
%D    C0 C1 -> .plabel= m f
%D ))
%D enddiagram
%D
$$\pu
  \diag{gm0}
$$



\bsk

% «elephant-A4.1.4» (to ".elephant-A4.1.4")
% (elep 7 "elephant-A4.1.4")
% (ele    "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$.
%
%D diagram gm-induced-by-f
%D 2Dx     100    +40  +30
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3 = A4
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> f^*D D
%D ren A2 A3 A4 ==> F f_*F \liml_f{}F
%D ren B0 B1 ==> [\calC,\Set] [\calD,\Set]
%D ren C0 C1 ==> \calC \calD
%D
%D (( A0 A1 <-|
%D    A2 A3 |-> A3 A4 =
%D    A0 A2 ->  A1 A3 ->
%D    B0 B1 <- sl^ .plabel= a f^*
%D    B0 B1 -> sl_ .plabel= b f_*
%D    C0 C1 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\pu
  \diag{gm-induced-by-f}
  \qquad
  (f_*F)(B) = \Lim((B↓f)\xton{FU}\Set)
$$
%
%D diagram Ran0
%D 2Dx     100 +50 +30
%D 2D  100 A0  A1  A2
%D 2D
%D 2D  +20 B0  B1  B2
%D 2D  +15 BC
%D 2D  +15 C0  C1  C2
%D 2D
%D ren A0 A1 A2 ==> (•↦B\ton{φ}fA↤A) A FA
%D ren B0 B1 B2 ==> (•↦B\ton{φ'}fA'↤A') A' FA'
%D ren C0 C1 C2 ==> (B↓f) \calC \Set
%D ren BC ==> (1→\calD=\calD←\calC)
%D
%D (( A0 A1 |-> A1 A2 |->
%D    A0 B0 -> .plabel= r (\_,α)
%D    A1 B1 -> .plabel= r α
%D    A2 B2 -> .plabel= r Fα
%D    B0 B1 |-> B1 B2 |->
%D    C0 C1 -> .plabel= a U C1 C2 -> .plabel= a F
%D    BC place
%D ))
%D enddiagram
%D
$$\pu
  \diag{Ran0}
$$
%
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")
% (elep 8 "elephant-A4.1.5")
% (ele    "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")
% (elep 8 "elephant-A4.1.8")
% (ele    "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.
%
%D diagram asf
%D 2Dx     100    +50
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D
%D ren A0 A1 ==> f^*P P
%D ren A2 A3 ==> S f_*P
%D ren B0 B1 ==> \Sh(\calC,T) [\calC^\op,\Set]
%D
%D (( A0 A1 <-|
%D    A0 A2 -> A1 A3 ->
%D    A2 A3 |->
%D    B0 B1 <- sl^ .plabel= a f^*\;\text{(asf)}
%D    B0 B1 -> sl_ .plabel= b f_*\;\text{(inc)}
%D ))
%D enddiagram
%D
$$\pu
  \diag{asf}
$$



\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]$ is also cartesian, so that it is
the inverse image of a geometric morphism $[\calD^\op,\Set] →
[\calC^\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")
% (elep 8 "elephant-A4.2.6" "surjection")
% (ele    "elephant-A4.2.6" "surjection")
% (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.

%D diagram gm-surj
%D 2Dx     100    +40
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> f^*E E
%D ren A2 A3 ==> f^*E f_*f^*E
%D ren B0 B1 ==> \calF \calE
%D ren C0 C1 ==> \calF \calE
%D
%D (( A0 A1 <-| .plabel= a \text{(faithful)}
%D    A2 A3 |->
%D    A0 A2 ->  A1 A3 -> .plabel= r \sm{η\phantom{mmm}\\\text{(monic)}}
%D    B0 B1 <- sl^ .plabel= a f^*
%D    B0 B1 -> sl_ .plabel= b f_*
%D    C0 C1 -> .plabel= a f
%D    C0 C1 -> .plabel= b \text{(surjection)}
%D ))
%D enddiagram
%D
$$\pu
  \diag{gm-surj}
$$




% «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.

%D diagram F-FG-E-p182
%D 2Dx     100 +30 +30
%D 2D  100 A0  A1  A2
%D 2D
%D 2D  +15 B0      B2
%D 2D
%D ren A0 A1 A2 ==> \calF \calF_\bbG \calE
%D ren B0    B2 ==> \calF            \calE
%D
%D (( A0 A1 <- sl^ .plabel= a g^*
%D    A0 A1 -> sl_ .plabel= b g_*
%D    A1 A2 <- sl^ .plabel= a h^*
%D    A1 A2 -> sl_ .plabel= b h_*
%D    B0 B2 <- sl^ .plabel= a f^*
%D    B0 B2 -> sl_ .plabel= b f_*
%D    
%D ))
%D enddiagram
%D
$$\pu
  \diag{F-FG-E-p182}
$$

\bsk

% «elephant-A4.2.8» (to ".elephant-A4.2.8")
% (elep 9 "elephant-A4.2.8")
% (ele    "elephant-A4.2.8")
% (find-elephantpage (+ 17 182) "Proposition 4.2.8")

\BF{Proposition 4.2.8} With the notation established above, the counit
$h^*h_*→1$ is an isomorphism.

(...)

A geometric morphism $h$ satisfying the condition that the counit
$h^*h_*→1$ is an isomorphism, or the equivalent condition that $h_*$
is full and faithful, is called an {\sl inclusion} (though some
authors prefer the term {\sl embedding}). We shall study inclusions in
greater detail in the next three sections; for the present, we digress
briefly to note an alternative characterization of them:

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

\bsk

\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

\pagebreak[2] % (find-es "tex" "pagebreak")

% «elephant-fact-p.182» (to ".elephant-fact-p.182")
% (elep 10 "elephant-fact-p.182")
% (ele     "elephant-fact-p.182")
% (find-elephanttext (+ 17 182))
% (find-elephantpage (+ 17 182) "Thus we have a factorization")

{\sl (The factorization at p.182):}

Now let $f:\calF→\calE$ be an arbitrary geometric morphism. Write
$\bbG$ for the comonad on $\calF$ induced by $(f^*⊣f_*)$ and
$g:\calF→\calF_\bbG$ for the surjection of 4.4.2. The comparison
functor $h^*:\calE→\calF_\calG$ satisfies $g^*h^*=f^*$, and is
therefore cartesian since $g^*$ creates finite limits. Moreover, since
$\calE$ has equalizers, $h^*$ has a right adjoint $h_*$, which sends a
$\bbG$-coalgebra $(B,β)$ to the equalizer of
%
$$ f_*B \two/->`->/<300>^{f_*β}_{η_{f_*β}} f_*f^*f_*B $$
%
(where $η$ is the unit of $(f^*⊣f_*)$), and $h_*g_* ≅ f_*$ by the
uniqueness of adjoints (or by direct calculation, if you prefer). Thus
we have a factorization $f ≅ hg$ of our original geometric morphism.

\bsk

% «elephant-A4.2.10» (to ".elephant-A4.2.10")
% (elep 10 "elephant-A4.2.10" "surjection followed by an inclusion")
% (ele     "elephant-A4.2.10" "surjection followed by an inclusion")
% (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).




\newpage

%  _  _    _____ 
% | || |  |___ / 
% | || |_   |_ \ 
% |__   _| ___) |
%    |_|(_)____/ 
%                
% «elephant-A4.3» (to ".elephant-A4.3")
% (elep 11 "elephant-A4.3")
% (ele     "elephant-A4.3")
% (find-elephantpage (+ 17 184) "4.3 Cartesian Reflectors and Sheaves")

\BF{4.3 Cartesian Reflectors and Sheaves}

\bsk

% «elephant-A4.3.1» (to ".elephant-A4.3.1")
% (elep 14 "elephant-A4.3.1")
% (ele     "elephant-A4.3.1")
% (find-elephantpage (+ 17 185) "Proposition 4.3.1")

\BF{Proposition 4.3.1} Let $\calE$ be a cartesian closed category, and
$\calL$ a reflective subcategory of $\calE$, corresponding to a
reflector $L$ on $\calE$. Then $L$ preserves finite products iff (the
class of objects of) $\calE$ is an exponential ideal in $\calE$.
Moreover, if these conditions hold then $B^η:B^{LA}→B^A$ is an
isomorphism for every object $B$ of $\calL$, where $η: 1_\calE → L$ is
the unit of the reflection.

\bsk

% (phap 39 "J-ops-and-connectives")
% (pha     "J-ops-and-connectives")

{\bf My way to visualize 4.3.1:} choose a ZHA $H$ and a J-operator $J$
on it. Then $H$ is a (posetal) CCC, and $J(H)$ is a reflective
subcategory of $H$, corresponding to a reflector $J:H→J(H)⊆H$. If
$Q∈J(H)$, i.e., $Q=Q^*$, then we have this; note that in the obvious
$(→)$-cube we have $(P^*→Q^*)→(P→Q^*)$, but in the full $(→)$-cube we
have $(P^*→Q^*)→(P→Q^*)$.
%
%D diagram 4.3.1
%D 2Dx     100 +15    +25 +15    +20  +15
%D 2D  100 A0' A0 <-| A1  A1'         B1'
%D 2D      |   |       |  |   \       ^  
%D 2D      v   v       v  v    v      |  
%D 2D  +20 A2' A2 |-> A3  A3' -> A3'' B3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0 A1 A2 A3 ==> LA A B B
%D ren A0' A2'      => LB B
%D ren A1' A3' A3'' => A LA B
%D ren B1' B3'      => B^A B^{LA}
%D ren A4 A5 ==> \calL \calE
%D
%D (( A0' A2' -> .plabel= l \sm{ε_B\\=\id}
%D    A1' A3' -> .plabel= l η_A
%D    A3' A3'' --> A1' A3'' -->
%D    B1' B3' <- .plabel= r \sm{B^{ηA}\\\text{(iso)}}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 <- sl^ .plabel= a L
%D    A4 A5 -> sl_ .plabel= b \text{(inc)}
%D ))
%D enddiagram
%D
%D diagram 4.3.1-my
%D 2Dx     100 +15    +25 +15 +20
%D 2D  100 A0' A0 <-| A1  A1' B1'
%D 2D      |   |       |   |  ^  
%D 2D      v   v       v   v  |  
%D 2D  +20 A2' A2 |-> A3  A3' B3'
%D 2D         
%D 2D  +15     A4 <=> A5
%D 2D
%D ren A0 A1 A2 A3 ==> P^* P Q Q 
%D ren A0' A2' => Q^* Q
%D ren A1' A3' => P P^*
%D ren B1' B3' => (P{→}Q) (P^*{→}Q)
%D ren A4 A5 ==> J(H) H
%D
%D (( A0' A2' -> .plabel= l \sm{ε_Q\\=\id}
%D    A1' A3' -> .plabel= r η_P
%D    B1' B3' <- .plabel= r \text{(iso)}
%D    
%D    A0 A1 <-| A0 A2 -> A1 A3 -> A2 A3 |->
%D    
%D    A4 A5 <- sl^ .plabel= a J
%D    A4 A5 -> sl_ .plabel= b \text{(inc)}
%D ))
%D enddiagram
%D
$$\pu
  \diag{4.3.1}
  \qquad
  \diag{4.3.1-my}
$$

% \bsk
% {\bf My way of viewing 4.2.12:}

\def\ms{\mathstrut}
\def\ms{\phantom{a}}
\def\fooabc#1#2#3{{\psm{#1\\↓\\#2\\↓\\#3\\}}}
\def\foob#1{{\psm{\ms\\\ms\\#1\\\ms\\\ms\\}}}
\def\fooABC#1#2#3{\fooabc{\{#1\}}{\{#2\}}{\{#3\}}}
\def\Fooabc#1#2#3{{\pmat{#1\\#2\\#3\\}}}
\def\FooABC#1#2#3{\Fooabc{\{#1\}}{\{#2\}}{\{#3\}}}

Here is a typical non-trivial inclusion, and a map $A→LA$ on it:
%
%D diagram reflective
%D 2Dx     100 +30    +45 +30
%D 2D  100 A0' A0 <-| A1  A1'
%D 2D      |   |       |   |
%D 2D      v   v       v   v
%D 2D  +40 A2' A2 |-> A3  A3'
%D 2D          
%D 2D  +40     B0 <=> B1
%D 2D
%D 2D  +25     C0 <=> C1
%D 2D  
%D ren A0 A1 ==> \foob{D_2} \fooabc{D_1}{D_2}{D_3}
%D ren A2 A3 ==> \foob{E_2} \fooabc{E_2}{E_2}{1}
%D ren B0 B1 ==> \Set^\foob2 \Set^\fooabc123
%D ren C0 C1 ==> \foob2 \fooabc123
%D ren A0' A2' ==> \foob{E_2} \foob{E_2}
%D ren A1' A3' ==> \fooabc{D_1}{D_2}{D_3} \fooabc{D_2}{D_2}{1}
%D
%D (( A0 A1 <-|
%D    A2 A3 |->
%D    A0 A2 ->  A1 A3 ->
%D    B0 B1 <- sl^ .plabel= a f^*
%D    B0 B1 -> sl_ .plabel= b f_*
%D    C0 C1 -> .plabel= m f
%D
%D    A0' A2' -> .plabel= l \sm{η\\\text{(iso)}}
%D    A1' A3' -> .plabel= r \sm{η\\\text{(iso)}}
%D ))
%D enddiagram
%D
$$\pu
  \diag{reflective}
  \qquad
  \begin{array}{cc}  
    \fooABC   {47,48}{14,15,16}{1,2,3} \ton{η}
    \fooABC{14,15,16}{14,15,16}{0} \\
    \\
    A \ton{η} LA \\
  \end{array}
$$


% \def\foosub#1#2#3#4#5#6{\sm{#1#2\\#3#4\\#5#6}}
% \foosub000000,
% \foosub000001,
% \foosub000010,
% \foosub000011,





\bsk

% «elephant-A4.3.1-cL» (to ".elephant-A4.3.1-cL")
% (elep 15 "elephant-A4.3.1-cL")
% (ele     "elephant-A4.3.1-cL")
% (find-elephantpage (+ 17 186) "Now suppose that E")

Now suppose that $\calE$ has pullbacks, and let $L$ be a reflector on
$\calE$ which preserves pullbacks. Then, for any object $A$ of
$\calE$, we may define a unary operation $c_{L,A}$ (or simply $c_L$)
on subobjects of $A$, as follows: if $A' \monicto A$ is monic, then so
is $LA' \monicto LA$, and we define $c_L(A')$ by the pullback diagram:
%
%D diagram cL-pullback
%D 2Dx     100 +30
%D 2D  100 A0  A1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D ren A0 A1 A2 A3 ==> c_L(A') LA' A LA
%D
%D (( A0 A1 ->
%D    A0 A2 >-> A1 A3 >-> 
%D    A2 A3 -> .plabel= a η_A
%D    A0 relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
%D diagram cL-pullback-my
%D 2Dx     100 +25 +30
%D 2D  100 A0.
%D 2D
%D 2D  +15 A00 A0  A1
%D 2D
%D 2D  +30     A2  A3
%D 2D
%D ren A00 A0 A1 A2 A3 ==> A00 c_L(A') LA' A LA
%D ren A00 A0 A1 A2 A3 ==> Q c_L(Q) JQ R JR
%D ren A00 A0 A1 A2 A3 ==> Q JQ{∧}R JQ R JR
%D
%D (( A00 A0 >-> A00 A2 >-> A00 A1 >-> .slide= 10pt .plabel= a η_Q
%D    A0 A1 ->
%D    A0 A2 >-> A1 A3 >-> 
%D    A2 A3 -> .plabel= a η_R
%D    A0 relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\pu
  \diag{cL-pullback}
  \qquad
  \diag{cL-pullback-my}
  \;\;
  \begin{array}{rcl}
  c_{J,R}(Q) &=& c_J(Q) \\ 
             &=& JQ ×_{JR} R \\ 
             &=& JQ × R \\ 
             &=& Q^* ∧ R \\ 
             &=:& Q^{(R)} \\ 
  \end{array}
$$
%
%D diagram cL-pullback-three
%D 2Dx     100 +40 +40
%D 2D  100 A00 A0  A1
%D 2D
%D 2D  +40     A2  A3
%D 2D
%D ren A00 ==> \Fooabc{P_1}{P_2}{P_3}
%D ren  A0 ==> \Fooabc{P_2{×_{R_2}}R_1}{P_2}{R_3}
%D ren  A1 ==> \Fooabc{P_2}{P_2}{1}
%D ren  A2 ==> \Fooabc{R_1}{R_2}{R_3}
%D ren  A3 ==> \Fooabc{R_2}{R_2}{1} 
%D
%D (( A00 A0 >-> A00 A2 >-> A00 A1 >-> .slide= 24pt .plabel= a η
%D    A0 A1 ->
%D    A0 A2 >-> A1 A3 >-> 
%D    A2 A3 -> .plabel= a η
%D    A0 relplace 12 12 \pbsymbol{7}
%D ))
%D enddiagram
%D
%D diagram cL-pullback-three-n
%D 2Dx     100 +40 +40
%D 2D  100 A00 A0  A1
%D 2D
%D 2D  +40     A2  A3
%D 2D
%D ren A00 ==> \FooABC{35}{13}{1}
%D ren  A0 ==> \FooABC{35,36}{13}{1,2}
%D ren  A1 ==> \FooABC{13}{13}{0}
%D ren  A2 ==> \FooABC{35,36}{13,14}{1,2}
%D ren  A3 ==> \FooABC{13,14}{13,14}{0} 
%D
%D (( A00 A0 >-> A00 A2 >-> A00 A1 >-> .slide= 24pt .plabel= a η
%D    A0 A1 ->
%D    A0 A2 >-> A1 A3 >-> 
%D    A2 A3 -> .plabel= a η
%D    A0 relplace 12 12 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\pu
  \diag{cL-pullback-three}
  \qquad
  \diag{cL-pullback-three-n}
$$

A way to understand how it works:
%
$$\left( \FooABC{35}{13}{1} ↣ \FooABC{35,36}{13,14}{1,2} \right)
  ↦ \Fooabc{1,0}{1,0}{1,0}
  ↦ \Fooabc{}{1,0}{}
  ↦ \Fooabc{1,1}{1,0}{1,1}
  ↦ \FooABC{35,36}{13}{1,2}
$$

\bsk
    
    




% «elephant-A4.3.2» (to ".elephant-A4.3.2")
% (elep 15 "elephant-A4.3.2")
% (ele     "elephant-A4.3.2")
% (find-elephantpage (+ 17 186) "Lemma 4.3.2")
% (find-elephantpage (+ 1104  71) "General Index" "Universal closure")

\BF{Lemma 4.3.2} The operation $c_L$ just defined is a closure
operation on $\Sub(A)$; that is, it is order-preserving and satisfies
$A' ≤ c_L(A') ≅ c_Lc_L(A')$ for any $A'$. Moreover, $c_L$ commutes (up
to isomorphism) with pullback along an arbitrary morphism of $\calE$.

\bsk

% «elephant-A4.3.3» (to ".elephant-A4.3.3")
% (find-elephantpage (+ 17 187) "Lemma 4.3.3")

\BF{Lemma 4.3.3} Let $c$ be a universal closure operation on a
cartesian closed category $\calE$. Then

(i) Given a commutative square (...) where $m$ is a dense object and
$n$ is closed, there is a unique morphism $g:A→B'$ satisfying $ng=f$
and $gm=f'$.
%
%D diagram 4.3.3i
%D 2Dx     100 +30
%D 2D  100 A0  A1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D ren A0 A1 A2 A3 ==> A' B' A B
%D
%D (( A0 A1  -> .plabel= a f
%D    A0 A2 >-> .plabel= l \sm{m\\\text{(dense)}}
%D    A1 A3 >-> .plabel= r \sm{n\\\text{(closed)}}
%D    A2 A3  -> .plabel= b f
%D    A2 A1 -> .plabel= m ∃!g
%D ))
%D enddiagram
%D
%D diagram 4.3.3i-my
%D 2Dx     100 +30
%D 2D  100 A0  A1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D ren A0 A1 A2 A3 ==> P R Q S
%D
%D (( A0 A1  -> .plabel= a f
%D    A0 A2 >-> .plabel= l \sm{m\\P^{(Q)}=Q}
%D    A1 A3 >-> .plabel= r \sm{n\\R^{(S)}=R}
%D    A2 A3  -> .plabel= b f
%D    A2 A1 -> .plabel= m ∃!g
%D ))
%D enddiagram
%D
$$\pu
  \diag{4.3.3i}
  \qquad
  \diag{4.3.3i-my}
$$

(ii) For any $A'↣A$, $c(A')$ may be characterized as the unique
  subobject $A''$ of $A$ such that $A'↣A''$ is dense and $A''↣A$ is
  closed.
%
%D diagram dense-closed
%D 2Dx     100 +15  +20  +20 +15  +20
%D 2D  100 A2            C2              
%D 2D        <-            <-            
%D 2D  +15     A1 = A1'      C1 = C1'    
%D 2D         ^             ^            
%D 2D        /             /             
%D 2D  +20 A0            C0              
%D 2D
%D ren A0 A1 A2 A1' ==> A' A'' A c(A')
%D ren C0 C1 C2 C1' ==> P Q R P^{(R)}
%D
%D (( A0 A1 >-> .plabel= r \text{(dense)}
%D    A1 A2 >-> .plabel= r \text{(closed)}
%D    A0 A2 >->
%D    A1 A1' =
%D    
%D    # B0 B1 >-> .plabel= r \text{(dense)}
%D    # B1 B2 >-> .plabel= r \text{(closed)}
%D    # B0 B2 >->
%D    # B1 B1' =
%D    
%D    C0 C1 >-> .plabel= r \text{(dense)}
%D    C1 C2 >-> .plabel= r \text{(closed)}
%D    C0 C2 >->
%D    C1 C1' =
%D ))
%D enddiagram
%D
$$\pu
  \diag{dense-closed}
$$

(iii) For subobjects $A'↣A$ and $A''↣A$, we have
  $c(A'∩A'')≅c(A')∩c(A'')$.

\bsk

{\bf My way to visualize 4.3.3}

Fix a ZHA $H$, a J-operator $J:H→H$ and an element $Q∈H$; remember
that we can write $[00,Q]∩H$ for the set of elements of $H$ below $Q$.
The operation
%
$$\begin{array}{rcrclcl}
  ·^{(Q)} &:& [00,Q]∩H &→& [00,Q]∩H \\
           &&        P &↦& P^{(Q)} \\
           &&          &:=& P^*∧Q \\
  \end{array}
$$
%
is a J-operator $J'$ on the ZHA $H':=[00,Q]∩H$, whose cuts are the
same as the ones in $J$, except, of course, that we don't use the cuts
above $Q$; note that some regions of $J$ may be partly inside $H'$ and
partly outside it --- if $P$ belongs to one of these regions then
$J'(P) = J(P)∧Q ≠ J(P)$.

\bsk

% «elephant-A4.3.4» (to ".elephant-A4.3.4")
% (elep 13 "elephant-A4.3.4" "$c$-dense")
% (ele     "elephant-A4.3.4" "$c$-dense")
% (find-elephantpage (+ 17 188) "Definition 4.3.4")

\BF{Definition 4.3.4} Let $c$ be a universal closure operator on a
cartesian category $\calE$.

(a) We say an object $A$ of $\calE$ is {\sl ($c$-)separated} if,
whenever we have a diagram
%
%D diagram separated
%D 2Dx     100    +20    +40   +20
%D 2D  100 B' --> A      P --> R
%D 2D      v             v
%D 2D      |             |
%D 2D      v             v
%D 2D  +20 B             Q
%D 2D
%D # ren ==>
%D
%D (( B' B >-> .plabel= l \sm{m\\\text{(dense)}}
%D    B' A -> .plabel= a f'
%D    B A --> .plabel= r f
%D 
%D    P Q >-> .plabel= l P^{(Q)}=Q
%D    P R ->
%D    Q R -->
%D ))
%D enddiagram
%D
%D diagram separated-2
%D 2Dx     100 +20  +20
%D 2D  100 C2              
%D 2D        <-            
%D 2D  +15     C1 = C1'    
%D 2D         ^            
%D 2D        /             
%D 2D  +20 C0              
%D 2D
%D ren C0 C1 C2 C1' ==> P Q R P^{(R)}
%D
%D (( C0 C1 >->  .plabel= r \text{(dense)}
%D    C1 C2 >--> .plabel= r !\,/\,∃! # \text{(closed)}
%D    C0 C2 >->
%D    C1 C1' =
%D ))
%D enddiagram
%D
$$\pu
  \diag{separated}
  \qquad
  \diag{separated-2}
$$
%
where $m$ is $c$-dense, there is at most one $f:B→A$ with $fm=f'$.

(b) We say $A$ is a ($c$-)sheaf if, whenever we have a diagram as
above, there is exactly one $f$ with $fm=f'$.

\bsk

{\bf My way to visualize 4.3.4}

All objects $R∈H$ are $J$-separated.

All objects $R∈J(H)$ are $J$-sheaves.

An object $R\not∈J(H)$ is not a $J$-sheaf. The map $R↣R^*$ is not an
iso, and we can't build the diagonal map when $P:=R$ and $Q:=R^*$:
%
%D diagram not-sheaf
%D 2Dx     100   +20
%D 2D  100 R --> R{}
%D 2D      v
%D 2D      |
%D 2D      v
%D 2D  +20 R^*
%D 2D
%D
%D (( R R{} -> .plabel= a \text{(iso)}
%D    R R^* >-> .plabel= l \text{(not\,iso)}
%D    R^* R{} --> .plabel= r =(
%D ))
%D enddiagram
%D
$$\pu
  \diag{not-sheaf}
$$
%



\bsk

% «elephant-A4.3.5» (to ".elephant-A4.3.5")
% (find-elephantpage (+ 17 188) "Example 4.3.5")

\BF{Example 4.3.5}

\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 $\calE$. 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.7» (to ".elephant-A4.3.7")
% (find-elephantpage (+ 17 191) "Lemma 4.3.7")

\BF{Lemma 4.3.7}

\bsk

% «elephant-A4.3.8» (to ".elephant-A4.3.8")
% (find-elephantpage (+ 17 191) "Lemma 4.3.8")

\BF{Lemma 4.3.8}



\bsk


% «elephant-A4.3.9» (to ".elephant-A4.3.9")
% (elep 14 "elephant-A4.3.9")
% (ele     "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.

\bsk

% «elephant-A4.3.10» (to ".elephant-A4.3.10")
% (find-elephantpage (+ 17 193) "Remark 4.3.10")

\BF{Remark 4.3.10} 

\bsk

% «elephant-A4.3.11» (to ".elephant-A4.3.11")
% (find-elephantpage (+ 17 193) "Proposition 4.3.11")

\BF{Proposition 4.3.11} Let $f:\calF→\calE$ be a geometric morphism.
and $L$ a cartesian reflector on $\calE$. The following are
equivalent:

(i) $f$ factors (uniquely) through the inclusion $h:\calL→\calE$ which
corresponds to $L$ under 4.3.9.


\newpage





%  _  _   _  _   
% | || | | || |  
% | || |_| || |_ 
% |__   _|__   _|
%    |_|(_) |_|  
%                
% «elephant-A4.4» (to ".elephant-A4.4")
% (elep 19 "elephant-A4.4")
% (ele     "elephant-A4.4")
% (find-elephantpage (+ 17 195) "A4.4 Local Operators")
% (find-elephanttext (+ 17 195))

\BF{A4.4 Local Operators}

\bsk

% «elephant-A4.4.1»  (to ".elephant-A4.4.1")
% (elep 19 "elephant-A4.4.1")
% (ele     "elephant-A4.4.1")
% (find-elephantpage (+ 17 195) " Definition 4.4.1")
% (find-elephanttext (+ 17 195))

\bsk

\BF{Definition 4.4.1} Let $\calE$ be a topos, with subobject
classifier $Ω$. A {\sl local operator} on $\catE$ (or on $Ω$) is a
morphism $j:Ω→Ω$ such that the diagrams

(...)

commute (where $∧$ is the binary meet operation on $Ω$ defined in
1.6.3).

\bsk

% «elephant-A4.4.2»  (to ".elephant-A4.4.2")
% (elep 15 "elephant-A4.4.2")
% (ele     "elephant-A4.4.2")
% (find-elephantpage (+ 17 195) "Lemma 4.4.2")
% (find-elephanttext (+ 17 195))

\BF{Lemma 4.4.2} For any topos $\calE$, there is a bijection between
universal closure and local operators on $\calE$.

\bsk

% «elephant-A4.4.4»  (to ".elephant-A4.4.4")
% (elep 15 "elephant-A4.4.4")
% (ele     "elephant-A4.4.4")
% (find-elephantpage (+ 17 197) "Proposition 4.4.4")
% (find-elephanttext (+ 17 197))

\BF{Proposition 4.4.4} Let $c$ be a proper universal closure operation
on a quasitopos $\calE$. Then the subcategories $𝐬{sep}_c(\calE)$ and
$\sh_c(\calE)$ are both reflective in $\calE$.

(Construction):

%L addabbrevs(">->", "\\monicto ")
%:
%:     A∈\calE
%:    ---------
%:    Δ:A>->A×A
%:  -------------
%:  \ovl{A}>->A×A
%:  -------------
%:   d:A→P_j(A)
%:  -------------
%:   MA>->P_j(A)
%:  -------------
%:   LA>->P_j(A)
%:
%:   ^constr-4.4.4
%:
$$\pu
  \ded{constr-4.4.4}
$$


% (find-elephantpage (+ 17 201) "Theorem 4.4.8")
% (find-elephanttext (+ 17 201))

\bsk

% «elephant-A4.4.8» (to ".elephant-A4.4.8")
% (find-elephanttext (+ 17 201))
% (find-elephantpage (+ 17 201) "Theorem 4.4.8")

\BF{Example 4.4.8} For a quasitopos $\calE$, there is a bijection
between reflective subcategories of $\calE$ with cartesian reflector,
and proper universal closure operations on $\calE$. In particular, if
$\calE$ is a topos, there is a bijection between subtoposes of $\calE$
and local operators on $\calE$.

\bsk

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

\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.3» (to ".elephant-A4.5.3")
% (elep 15 "elephant-A4.5.3")
% (ele     "elephant-A4.5.3")
% (find-elephanttext (+ 17 205))
% (find-elephantpage (+ 17 206) "Proposition 4.5.3")
% closed subtoposes:

\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.19» (to ".elephant-A4.5.19")
% (find-elephantpage (+ 17 219) "Lemma 4.5.19")

\BF{Lemma 4.5.19} 


\bsk

% «elephant-A4.5.20» (to ".elephant-A4.5.20")
% (elep 16 "elephant-A4.5.20" "factorization" "dense" "closed")
% (ele     "elephant-A4.5.20" "factorization" "dense" "closed")
% (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")
% (find-xpdfpage "~/LATEX/5.pdf")
% (find-xpdfpage "~/LATEX/5.pdf" 8 "Density part")

% closure of j:
% dense local operator:

\def\ext{\mathrm{ext}}
\def\cextj{{c(\ext(j))}}

The local operator $\cextj$ is of course called the {\sl closure} of
$j$. We note that the inclusion $\sh_j(\calE) → \sh_\cextj(\calE)$
corresponding to the inequality $\cextj≤j$ has the property that its
direct image preserves the initial object (equivalently, the local
operator on $\sh_\cextj(\calE)$ which corresponds to it has exterior
0), since the initial object of $\sh_j(\calE)$ is simply $\ext(j)$. Of
course, we call a subtopos or local operator {\sl dense} if its has
this property; we may thus conclude

\msk

\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")
% (elep 16 "elephant-A4.6.2")
% (ele     "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)")





\newpage

%  __  __               _     _       _ _                 
% |  \/  |_   _    ___ | | __| |   __| (_) __ _  __ _ ___ 
% | |\/| | | | |  / _ \| |/ _` |  / _` | |/ _` |/ _` / __|
% | |  | | |_| | | (_) | | (_| | | (_| | | (_| | (_| \__ \
% |_|  |_|\__, |  \___/|_|\__,_|  \__,_|_|\__,_|\__, |___/
%         |___/                                 |___/     
%
% «my-old-diagrams» (to ".my-old-diagrams")

% (find-books "__cats/__cats.el" "johnstone-elephant")
% (find-elephantpage (+  17  161) "A4 Geometric Morphisms - Basic Theory")
% (find-elephantpage (+  17  164) "essential geometric morphism")
% (find-elephanttext (+  17  164) "essential geometric morphism")
% (find-elephantpage (+  17  188) "separated")
% (find-elephantpage (+  17  195) "A4.4 Local Operators")

% (find-elephantpage (+  17  163) "4.1.4  Let f:C->D be a functor between small categories")
% (iquo 1 "elephant-A4.1.4")
% (iquop 1 "elephant-A4.1.4")


Inclusion:

A4.2.8: The counit $h^*h_*→1$ is an iso:
%
%D diagram inclusion
%D 2Dx     100    +30
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3
%D 2D
%D 2D  +15 B0 <=> B1
%D 2D
%D 2D  +15 C0 <=> C1
%D 2D  
%D ren A0 A1 ==> h^*D D
%D ren A2 A3 ==> h^*D h_*h^*D
%D ren B0 B1 ==> \Set^A \Set^B
%D ren C0 C1 ==> A B
%D
%D (( A0 A1 <-|
%D    A2 A3 |->
%D    A0 A2 ->  A1 A3 -> .plabel= r \sm{ε\\\text{(iso)}}
%D    B0 B1 <- sl^ .plabel= a h^*
%D    B0 B1 -> sl_ .plabel= b h_*
%D    C0 C1 -> .plabel= a h
%D ))
%D enddiagram
%D
$$\pu
  \diag{inclusion}
$$




%L PPV(sections)
\pu




\end{document}

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