Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2017elephant.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017elephant.tex"))
% (defun d () (interactive) (find-xpdfpage "~/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"))
% (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-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-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.8»	(to "elephant-A4.4.8")
% «.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.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]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\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{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()}}

\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\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")

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-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}
% $$





\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")
% (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")
% (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")
% (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.
%
%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")
% (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")
% (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.

\bsk

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

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:

\msk

\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).




\newpage

%  _  _    _____ 
% | || |  |___ / 
% | || |_   |_ \ 
% |__   _| ___) |
%    |_|(_)____/ 
%                
% «elephant-A4.3» (to ".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")
% (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")
% (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")
% (find-elephantpage (+ 17 186) "Lemma 4.3.2")

\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")
% (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")
% (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")
% (find-elephantpage (+ 17 195) "A4.4 Local Operators")

\BF{A4.4 Local Operators}

\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")
% (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.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")
% (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")

\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)")





\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»"
% End: