Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% (find-LATEX "2020maclane-moerdijk.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020maclane-moerdijk.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2020maclane-moerdijk.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2020maclane-moerdijk.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020maclane-moerdijk.pdf"))
% (defun e () (interactive) (find-LATEX "2020maclane-moerdijk.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020maclane-moerdijk"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2020maclane-moerdijk.pdf"))
%          (code-eec-LATEX "2020maclane-moerdijk")
% (find-pdf-page   "~/LATEX/2020maclane-moerdijk.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020maclane-moerdijk.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020maclane-moerdijk.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020maclane-moerdijk.pdf
%               file:///tmp/2020maclane-moerdijk.pdf
%           file:///tmp/pen/2020maclane-moerdijk.pdf
% http://angg.twu.net/LATEX/2020maclane-moerdijk.pdf
% (find-LATEX "2019.mk")

% «.title»			(to "title")
% «.Set-C-op»			(to "Set-C-op")
% «.yoneda»			(to "yoneda")
% «.Omega-in-presheaf»		(to "Omega-in-presheaf")
% «.sieve-on-C»			(to "sieve-on-C")
% «.cat-of-elements»		(to "cat-of-elements")
% «.sieves-and-sheaves»		(to "sieves-and-sheaves")
% «.O-Bottle»			(to "O-Bottle")
% «.OO-House»			(to "OO-House")
% «.sieves»			(to "sieves")
% «.top-sheaves-in-my-notation»	(to "top-sheaves-in-my-notation")
% «.sheaves-on-a-site»		(to "sheaves-on-a-site")
% «.LT-subsumes-groth»		(to "LT-subsumes-groth")
% «.localic-topoi»		(to "localic-topoi")
% «.spaces-from-locales»	(to "spaces-from-locales")
% «.5._localic_topoi»		(to "5._localic_topoi")


\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{indentfirst}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-u.bib}            % (find-LATEX "catsem-u.bib")
%\addbibresource{2019notes-yoneda.bib}    % (find-LATEX "2019notes-yoneda.bib")
\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}

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

\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}

%\def\Sets    {\mathbf{Sets}}
\def\Nat     {\text{Nat}}
\def\phop    {{}^{\phantom{\op}}}
\def\Cop     {{\catC^\op}}
\def\SetsCop {\Sets^{\catC^\op}}
\def\hatC    {{\widehat\catC}}
\def\OXop    {\Opens(X)^\op}
\def\SetsOXop{\Sets^{\Opens(X)^\op}}
\def\univ    {\mathsf{univ}}
\def\Spaces  {\mathbf{Spaces}}
\def\Locales {\mathbf{Locales}}
\def\Frames  {\mathbf{Frames}}
\def\Top     {\mathbf{Top}}
\def\Bund    {\mathbf{Bund}}
\def\Loc     {\mathrm{Loc}}
\def\Ker     {\operatorname{Ker}}
\def\Pt      {\operatorname{pt}}
\def\Sh      {\operatorname{Sh}}
\def\PSh     {\operatorname{PSh}}
\def\acz     {\setlength{\arraycolsep}{0pt}}

%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title»  (to ".title")

{\setlength{\parindent}{0em}
\footnotesize

Notes on MacLane and Moerdijk's

``Sheaves in Geometry and Logic - A First Introduction to Topos Theory'' (1994)

\url{https://www.springer.com/gp/book/9780387977102}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020maclane-moerdijk.pdf}

\ssk

See:

\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}

\url{http://angg.twu.net/math-b.html\#favorite-conventions}

I wrote these notes mostly to test if the conventions above
are good enough.

}









\section*{1. Categories of functors}

%  ____       _     /\    ____   /\               
% / ___|  ___| |_  |/\|  / ___| |/\|   ___  _ __  
% \___ \ / _ \ __|      | |           / _ \| '_ \ 
%  ___) |  __/ |_       | |___       | (_) | |_) |
% |____/ \___|\__|       \____|       \___/| .__/ 
%                                          |_|    
%
% «Set-C-op»  (to ".Set-C-op")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 25) "(viii)")

(Page 25):

(viii) $\Set^{\catC^\op}$, where...

%D diagram p25-a
%D 2Dx     100 +25 +20 +25 +25 +15 +25
%D 2D  100 A0  A1  C0  C1  E0  F0  F1
%D 2D
%D 2D  +20 A2  A3  C2  C3  E1  F2  F3
%D 2D
%D 2D  +12 B0      D0
%D 2D  +8  B1  B2  D1  D2      G0  G1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 B2 ==> C PC  D PD  \catC \phop\catC^\op \Set
%D ren C0 C1 C2 C3 D0 D1 D2 ==> C P'C D P'D \catC \phop\catC^\op \Set
%D ren E0 E1 F0 F1 F2 F3 G0 G1 ==> C D PC P'C PD P'D P P'
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l f
%D    A1 A3  -> .plabel= r Pf
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 place
%D    B1 B2 -> .plabel= a P
%D
%D    C0 C1 |->
%D    C0 C2 <-  .plabel= l f
%D    C1 C3  -> .plabel= r P'f
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil |->
%D    D0 place
%D    D1 D2  -> .plabel= a P'
%D
%D    E0 E1 <-  .plabel= l f
%D    F0 F1  -> .plabel= a θ_C
%D    F0 F2  -> .plabel= l Pf
%D    F1 F3  -> .plabel= r P'f
%D    F2 F3  -> .plabel= a θ_D
%D    G0 G1  -> .plabel= a θ
%D ))
%D enddiagram
%D
$$\pu
  \diag{p25-a}
$$

\bsk

%D diagram p25-b
%D 2Dx     100 +25 +25 +40
%D 2D  100 A0  A1  C0
%D 2D
%D 2D  +20 A2  A3  C2  C3
%D 2D
%D 2D  +20 A4  A5  C4  C5
%D 2D
%D 2D  +12 B0
%D 2D  +8  B1  B2
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> C PC D PD E PE
%D ren B0 B1 B2 ==> \catC \phop\catC^\op \Set
%D ren C0 C2 C4 ==> x x·f (x·f)·g
%D ren C3 C5    ==>  =x|f  =x·(f∘g) 
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l f
%D    A1 A3  -> .plabel= r Pf
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    A2 A4 <-  .plabel= l g
%D    A3 A5  -> .plabel= r Pg
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    B0 place
%D    B1 B2  -> .plabel= a P
%D
%D    C0 C2 |-> C2 C4 |->
%D    C3 place C5 place
%D ))
%D enddiagram
%D
$$\pu
  \diag{p25-b}
$$



\newpage

% __   __                   _       
% \ \ / /__  _ __   ___  __| | __ _ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |
%   | | (_) | | | |  __/ (_| | (_| |
%   |_|\___/|_| |_|\___|\__,_|\__,_|
%                                   
% «yoneda»  (to ".yoneda")
% (mmop 3 "yoneda")
% (mmoa   "yoneda")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 26) "Each object C of C gives rise")

(Page 26):

Each object $C$ of $\catC$ gives rise to a presheaf $𝐛y(C)$ on
$\catC$...

%D diagram p26-a
%D 2Dx     100 +30 +40 +35 +20 +20
%D 2D  100 A0  A1  C0  D0  E0  E1
%D 2D
%D 2D  +20 A2  A3  C1  D1  E2
%D 2D
%D 2D  +12 B0
%D 2D  +8  B1  B2
%D 2D
%D ren A0 A1 A2 A3 ==> D 𝐛y(C)(D) D' 𝐛y(C)(D')
%D ren B0 B1 B2 ==> \catC \phop\catC^\op \Set
%D ren C0 C1 ==> =\Hom_\catC(D,C) =\Hom_\catC(D',C)
%D ren D0 D1 ==> u u∘α
%D ren E0 E1 E2 ==> D C D'
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l α
%D    A1 A3  -> .plabel= r 𝐛y(C)(α)
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 place
%D    B1 B2  -> .plabel= a 𝐛y(C)
%D
%D    C0 C1  -> .plabel= r (∘α)
%D    D0 D1 |->
%D    E0 E1  -> .plabel= a u
%D    E0 E2 <-  .plabel= l α
%D    E1 E2 <-  .plabel= r u∘α
%D ))
%D enddiagram
%D
$$\pu
  \diag{p26-a}
$$

%D diagram p26-b
%D 2Dx     100 +25 +35 +50 +35 +20 +20
%D 2D  100 A0  A1  C0  D0  E0  F0  F1
%D 2D
%D 2D  +20 A2  A3  C1  D1  E1      F2
%D 2D
%D 2D  +12 B0
%D 2D  +8  B1  B2
%D 2D
%D ren A0 A1 A2 A3 ==> C_1 𝐛y(C_1) C_2 𝐛y(C_2)
%D ren B0 B1 B2 ==> \catC \catC \Set^{\catC^\op}
%D ren C0 C1 ==> =\Hom_\catC(-,C_1) =\Hom_\catC(-,C_2)
%D ren D0 D1 ==>  \Hom_\catC(D,C_1)  \Hom_\catC(D,C_2)
%D ren E0 E1 ==> v f∘v
%D ren F0 F1 F2 ==> D C_1 C_2
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r 𝐛y(f)
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 place
%D    B1 B2  -> .plabel= a 𝐛y
%D    C0 C1  -> .plabel= r (f∘)
%D    D0 D1  -> .plabel= r (f∘)
%D    E0 E1 |->
%D    F0 F1  -> .plabel= a v
%D    F1 F2  -> .plabel= r f
%D    F0 F2  -> .plabel= l f∘v
%D ))
%D enddiagram
%D
$$\pu
  \diag{p26-b}
$$
%
%D diagram p26-yoneda
%D 2Dx     100 +45
%D 2D  100     A1
%D 2D
%D 2D  +20 A2  A3
%D 2D
%D 2D  +20 A4  A5
%D 2D
%D 2D  +20 B0  B1
%D 2D
%D 2D  +15 C0  C1
%D 2D
%D 2D  +20     C2
%D 2D
%D 2D  +20
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 C PC D PD
%D ren B0 B1 ==> \phop\catC^\op \Set
%D ren C0 C1 C2 ==> \Hom_\catC(-,C) \Set(1,P-) P
%D
%D (( A1 A3  -> .plabel= r \sm{\nameof{θ_α}=\\\nameof{α_C(1_C)}}
%D    A2 A3 |->
%D    A2 A4 <-
%D    A3 A5  ->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    B0 relplace 0 -8 \catC
%D    B0 B1  -> .plabel= a P
%D    C0 C1  ->
%D    C1 C2 <->
%D    C0 C2  -> .plabel= b α
%D    C0 relplace -35 0 𝐛y(C)=
%D ))
%D enddiagram
%D
$$\pu
  \diag{p26-yoneda}
$$



\newpage

(Page 37):

% «Omega-in-presheaf»  (to ".Omega-in-presheaf")
% (mmop 3 "Omega-in-presheaf")
% (mmoa   "Omega-in-presheaf")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 37) "For an arbitrary presheaf category hatC")

For an arbitrary presheaf category $\hatC = \SetsCop$, if there is a
subobject classifier $Ω$, it must, in particular, classify the
subobjects of each representable presheaf $𝐛yC = \Hom_\catC(-,C): \Cop
→ \Sets$. Therefore,
%
$$\begin{array}{rcl}
  \Sub_\hatC(\Hom_\catC(-,C)) & ≅ & \Hom_\hatC(\Hom_\catC(-,C),Ω) \\
                              & ≅ &       \Nat(\Hom_\catC(-,C),Ω) \\
  \end{array}
$$
%
By the Yoneda Lemma [see \S1(6) above], the set on the right is (up to
isomorphism) $Ω(C)$. Thus the subobject classifier $Ω$, if it exists,
must be the functor $Ω: \Cop → \Sets$ with object function
%
$$\begin{array}{rcl}
  Ω(C) & = & \Sub_\hatC(\Hom_\catC(-,C)) \\
       & = & \setofst{S}{S \text{ is a subfunctor of }\Hom_\catC(-,C)}, \\
  \end{array}
$$
%
and with a suitable mapping function.


%D diagram p37-1
%D 2Dx     100 +50 +50 +55
%D 2D  100     A1      D1
%D 2D
%D 2D  +20 A2  A3  D2  D3
%D 2D
%D 2D  +20 A4  A5  D4  D5
%D 2D
%D 2D  +20 B0  B1  E0  E1
%D 2D
%D 2D  +15 C0  C1  F0  F1
%D 2D
%D 2D  +20     C2      F2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 C Ω(C) D Ω(D)
%D ren B0 B1 C0 C1 C2 ==> \phop\Cop \Sets \Hom_\catC(-,C) \Set(1,Ω(-)) Ω(-)=Ω
%D ren D1 D2 D3 D4 D5 ==> 1 Ω \Sub(Ω) X \Sub(X)
%D ren E0 E1 F0 F1 F2 ==> \phop\hatC^\op \Sets \Hom_\hatC(-,Ω) \Sets(1,\Sub(-)) \Sub(-)
%D
%D (( A1 A3  ->
%D    A2 A3 |->
%D    A2 A4 <-
%D    A3 A5  ->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    B0 B1  -> .plabel= a Ω
%D    C0 C1  ->
%D    C1 C2 <->
%D    C0 C2  ->
%D    B0 relplace 0 -8 \catC
%D    C0 relplace -30 0 𝐛yC=
%D ))
%D (( D1 D3  -> .plabel= r \sm{\nameof{⊤}\\(\univ)}
%D    D2 D3 |->
%D    D2 D4 <-
%D    D3 D5  ->
%D    D2 D5 harrownodes nil 20 nil |->
%D    D4 D5 |->
%D    E0 E1  -> .plabel= a \Sub
%D    F0 F1 <->
%D    F1 F2 <->
%D    F0 F2 <->
%D    E0 relplace 0 -8 \hatC
%D ))
%D enddiagram
%D
$$\pu
  \diag{p37-1}
$$

\bsk

$$\begin{array}{rcl}
  Ω(C) & ≅ & \Sets(1,Ω(C)) \\
       & ≅ & \Hom_\hatC(𝐛yC,Ω) \\
       & ≅ & \Sub_\hatC(𝐛yC) \\
       & = & \Sub_\hatC(\Hom_\catC(-,C)) \\
       & = & \setofst{S}{S \text{ is a subfunctor of }\Hom_\catC(-,C)}, \\
  \end{array}
$$


\newpage

% «sieve-on-C»  (to ".sieve-on-C")
% (mmop 4 "sieve-on-C")
% (mmoa   "sieve-on-C")
% (find-maclanemoerdijkpage (+   11  38)     "Sieve on C =")

(Page 38:)

A sieve on $C$ is...

\def\cod{\mathop{\text{cod}}}
%\def\thinpsm            #1{\setlength{\arraycolsep}{0pt}\psm{#1}}
%\def\thinpsm            #1{\setlength{\arraycolsep}{-10pt}\psm{#1}}
\def\thinpsm             #1{\psm{#1}}
\def\thinpsmtwo      #1#2#3{\thinpsm{ &#1 \\ #2 \!\!\! &↑ \\ &#3 }}
\def\thinpsmthree#1#2#3#4#5{\thinpsm{ &#1 \\ #2 \!\!\! &↑ \\ &#3 \\ #4 \!\!\! &↑ \\ &#5 }}

$$\begin{array}{rcl}
  t_C &=& \setofst{g}{\cod g = C} \\
      &=& \setofst{ \thinpsmtwo{C}{g}{D} }{\cod g = C} \\
  S \text{ is a sieve on } C
      &=& (S⊂t_C \text{ and } S \text{ is downward-closed} ) \\
      &=& (S⊂t_C \text{ and }
           ∀\thinpsmthree{C}{g}{D}{h}{D'}.
           \pmat{g∈S \\ ↓ \\ g∘h∈S}
          ) \\
  Ω(C) &=& \setofst{S⊂t_C}{S \text{ is a sieve on } C} \\
       &=& \setofst{S⊂t_C}{S \text{ is downward-closed}} \\
  \end{array}
$$


%D diagram ??
%D 2Dx     100    +30 +30 +55
%D 2D  100 A0 |-> A1  C0  D0
%D 2D      |       |   |   |
%D 2D      |  |->  |   |   |
%D 2D      |       |   |   |
%D 2D  +25 A2 |-> A3  C1  D1
%D 2D
%D 2D  +13 B0'
%D 2D  +7  B0 --> B1
%D 2D
%D ren A0 A1 A2 A3 ==> C Ω(C) B Ω(B)
%D ren B0' B0 B1 ==> \catC \phantom{{}^\op}\catC^\op \Set
%D ren C0 C1 ==> S g^*S=S·g
%D ren D0 D1 ==> \inOmC \inOmB
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l g
%D    A1 A3  -> .plabel= r g^*
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D
%D    B0' place
%D    B0 B1 -> .plabel= a Ω
%D
%D    C0 C1 |->
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \def\inOmC{\setofst{ \thinpsmtwo{C}{g}{D} }{ g∈S }}
  \def\inOmB{\setofst{ \thinpsmtwo{B}{h}{D} }{ g∘h∈S }}
  \diag{??}
$$




\newpage

% «cat-of-elements»  (to ".cat-of-elements")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 41) "Given P, the index category J")

(Page 41):

Given $P$, the index category $J$ which serves to prove the
proposition is the so-called {\sl category of elements} of $P$,
denoted by $∫_\catC P$ or, more briefly, $∫P$. Its objects are all
pairs $(C,p)$ where $C$ is an object of $\catC$ and $p$ is an element
$p∈P(C)$. Its morphisms $(C',p)→(C,p)$ are those morphisms $u:C'→C$ of
$\catC$ for which $pu=p'$; in other words, $u$ must take the chosen
element $p$ in $P(C)$ ``back'' into $p'$ in $P(C')$:
%
$$(C',p)→(C,p) \qquad \text{by $u:C'→C$ with $pu=p'$.}$$

These morphisms ar composed by composing the underlying arrows $u$ of
$\catC$. This category has an evident projection functor
%
$$π_P: ∫_\catC P → \catC, \qquad (C,p) \mapsto C.
$$

%D diagram ??
%D 2Dx     100 +30 +65 +35 +20 +20 +20
%D 2D  100     A1
%D 2D
%D 2D  +20 A2  A3  C0  C1
%D 2D
%D 2D  +20 A4  A5  C2  C3
%D 2D
%D 2D  +20 B0  B1  D0  D1
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 C P(C) C' P(C')
%D ren B0 B1 ==> \phop\Cop \Sets
%D ren C0 C1 C2 C3 ==> (C,p) C (C',p') C'
%D ren D0 D1 ==> ∫_{\catC}P=∫P \catC
%D
%D (( A1 A3  -> .plabel= r \nameof{p}
%D    A2 A3 |->
%D    A2 A4 <-  .plabel= l u
%D    A3 A5  -> .plabel= r P(u)
%D    A4 A5 |->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A1 A5  -> .slide= 25pt .plabel= r \sm{\nameof{pu}:=\\\nameof{P(u)(p)}\;=\\\nameof{p'}}
%D    B0 relplace 0 -8 \catC
%D    B0 B1  -> .plabel= a P
%D ))
%D (( C0 C1 |->
%D    C0 C2 <-  .plabel= l u
%D    C1 C3 <-  .plabel= r u
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil |->
%D    D0 D1  -> .plabel= a π_P
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage

(Page 41):

Colimits over the category of elements can be used to construct a pair
of adjoint functors which will have many uses, as follows.

{\bf Theorem 2.} {\sl If $A: \catC→\calE$ is a functor from a small
  category $\catC$ to a cocomplete category $\calE$, the functor $R$
  from $\calE$ to presheaves given by
  %
  $$R(E): C \mapsto \Hom_\calE(A(C),E)$$
  %
  has a left adjoint $L:\SetsCop → \calE$ defined for each presheaf
  $P$ in $\SetsCop$ as the colimit
  %
  $$L(P) = \Colim(∫ P \ton{π_P} \catC \ton{A} \calE).$$

}

\bsk

Here's how I found the type and a precise definition of $R_1$...

(It's too big! How do other people do this?)
%
\def\HomE{\Hom_\calE}
%
%D diagram ??
%D 2Dx     100  +25 +40  +35 +40 +20  +30
%D 2D  100 A0 - A1  C0 - C1  E0  F0 - F1
%D 2D      |     |  |     |  |   |     |
%D 2D  +20 A2 - A3  C2 - C3  E1  F2 - F3
%D 2D            |
%D 2D  +20      A4
%D 2D  +7           D0'          G0'
%D 2D  +8  B0 - B1  D0 - D1      G0 - G1
%D 2D
%D ren A0 A1 A2 A3 A4 ==> C A(C) C' A(C') E
%D ren       B0 B1    ==> \catC \calE
%D ren   D0' D0 D1    ==> \catC \phop\Cop \Sets
%D ren C0 C1 C2 C3    ==> C \HomE(A(C),E) C' \HomE(A(C'),E)
%D ren       E0 E1    ==> f{∘}Ag f
%D ren F0 F1 F2 F3    ==> C R(E)(C) C' R(E)(C')
%D ren   G0' G0 G1    ==> \catC \phop\Cop \Sets
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l g
%D    A1 A3  -> .plabel= r Ag
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    A3 A4  -> .plabel= r f
%D    A1 A4  -> .slide= 20pt .plabel= r f∘Ag
%D    B0 B1  -> .plabel= a A
%D
%D    C0 C1 |->
%D    C0 C2  -> .plabel= l g
%D    C1 C3 <-  .plabel= r (∘Ag)
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil |->
%D    D0' place
%D    D0 D1 -> .plabel= a R(E)
%D
%D    E0 E1 <-|
%D
%D    F0 F1 |->
%D    F0 F2  -> .plabel= l g
%D    F1 F3 <-  .plabel= r (∘Ag)
%D    F2 F3 |->
%D    F0 F3 harrownodes nil 20 nil |->
%D    G0' place
%D    G0 G1 -> .plabel= a R(E)
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

%D diagram ??
%D 2Dx     100 +30  +45 +30  +30 +30 +25  +40 +25
%D 2D  100 A0  B0 - B1  D0 - D1  E0  F0 - F1
%D 2D      |   |     |  |     |  |   |     |
%D 2D  +20 A1  B2 - B3  D2 - D3  E1  F2 - F3
%D 2D
%D 2D  +15                           G0 - G1  H0
%D 2D                                |     |   |
%D 2D  +20     C0 - C1               G2 - G3  H1
%D 2D
%D ren A0 A1       ==> C C'
%D ren B0 B1 B2 B3 ==> \HomE(A(C),E) \HomE(A(C),E') \HomE(A(C'),E) \HomE(A(C'),E')
%D ren C0 C1       ==> E E'
%D ren D0 D1 D2 D3 ==> f{∘}AG h{∘}f{∘}Ag f h{∘}f
%D ren E0 E1       ==> C C'
%D ren F0 F1 F2 F3 ==> R(E)(C) R(E')(C) R(E)(C') R(E')(E')
%D ren G0 G1 G2 G3 ==> R(E) R(E') E E'
%D ren H0 H1       ==> \SetsCop \calE
%D
%D (( A0 A1  -> .plabel= a g
%D    B0 B1  -> .plabel= a (h∘)
%D    B0 B2 <-  .plabel= l (∘Ag)
%D    B1 B3 <-  .plabel= r (∘Ag)
%D    B2 B3  -> .plabel= a (h∘) 
%D    C0 C1  -> .plabel= a h
%D
%D    D0 D1 |->
%D    D0 D2 <-|
%D    D1 D3 <-|
%D    D2 D3 |->
%D
%D    E0 E1 <-  .plabel= l g
%D
%D    F0 F1  -> .plabel= a (h∘)
%D    F0 F2 <-  .plabel= l (∘Ag)
%D    F1 F3 <-  .plabel= r (∘Ag)
%D    F2 F3  -> .plabel= a (h∘)
%D
%D    G0 G1  -> .plabel= a Rh
%D    G0 G2 <-|
%D    G1 G3 <-|
%D    G2 G3  -> .plabel= b h
%D    G0 G3 varrownodes nil 15 nil <-|
%D
%D    H0 H1 <- .plabel= r R
%D ))
%D enddiagram
%D
$$\pu
  \def\HomE{\Hom_\calE}
  \def\HomE{\calE}
  \diag{??}
$$




\newpage

% «sieves»  (to ".sieves")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11  24) "I. Categories of functors")
% (find-maclanemoerdijkpage (+   11  37)   "a sieve on C")
% http://angg.twu.net/MINICATS/sheaves_for_children__1_to_7.pdf

\cite{MacLaneMoerdijk}, (Page 37):

Given an object $C$ in the category $\catC$, a {\sl sieve} on $C$ is a
set $S$ of arrows with codomain $C$ such that $f∈S$ implies $f∘h∈S$.

A sieve $S$ can be seen as a subfunctor $S: \catC^\op → \Set$ of
$\Hom(-,C): \catC^\op → \Set$ --- or, more explicitly, as a natural
transformation $ι: S → \Hom(-,C)$ such that each $ι_A$ is an
inclusion.
%
%D diagram sieve-on-C
%D 2Dx     100 +20 +35 +20 +40 +35 +25
%D 2D  100     C
%D 2D
%D 2D  +20 B       A0  B0  B1  D0  D1
%D 2D
%D 2D  +20     A   A1  B2  B3  D2  D3
%D 2D
%D 2D  +15             C0  C1
%D 2D
%D ren A0 B0 B1 ==> B S(B) \Hom(B,C)
%D ren A1 B2 B3 ==> A S(A) \Hom(A,C)
%D ren    C0 C1 ==>   S(-) \Hom(-,C)
%D ren    D0 D1 ==>    f      f
%D ren    D2 D3 ==>   f∘h    f∘h
%D
%D (( B C -> .plabel= l f∈S
%D    A B -> .plabel= l h
%D    A C -> .plabel= r f∘h∈S
%D    C relplace -7 14 \dashrightarrow
%D    
%D    A0 A1 <-  .plabel= l h
%D    B0 B1 `-> .plabel= a ι_B
%D    B0 B2  -> .plabel= l ∘h
%D    B1 B3  -> .plabel= r ∘h
%D    B2 B3 `-> .plabel= a ι_A
%D    C0 C1 `-> .plabel= a ι
%D
%D    D0 D1 |-> D0 D2 |-> D1 D3 |-> D2 D3 |-> 
%D ))
%D enddiagram
%D
$$\pu
  \diag{sieve-on-C}
$$


\newpage

% (find-maclanemoerdijkpage (+ 11 70) "a sieve S on U")

(Page 70):

A sieve $S$ on an object $U$ of $\Opens(X)$ is a subfunctor of
$\Hom(-,U)$:
%
%D diagram sieve-on-a-topology
%D 2Dx     100 +20 +35 +20 +40 +35 +25
%D 2D  100 X
%D 2D
%D 2D  +20     U
%D 2D
%D 2D  +20 V       A0  B0  B1  D0  D1
%D 2D
%D 2D  +20     W   A1  B2  B3  D2  D3
%D 2D
%D 2D  +15             C0  C1
%D 2D
%D ren A0 B0 B1 ==> V S(V) \Hom(V,U)
%D ren A1 B2 B3 ==> W S(W) \Hom(W,U)
%D ren    C0 C1 ==>   S(-) \Hom(-,U)
%D ren    D0 D1 ==>  ι_{V,U} ι_{V,U}
%D ren    D2 D3 ==>  ι_{W,U} ι_{W,U}
%D
%D (( U X ->
%D    V U -> .plabel= l ι_{V,U}∈S
%D    W V -> .plabel= l ι_{W,V}
%D    W U -> .plabel= r ι_{W,U}∈S
%D    U relplace -7 14 \dashrightarrow
%D    
%D    A0 A1 <-  .plabel= l ι_{W,V}
%D    B0 B1 `-> .plabel= a ι_V
%D    B0 B2  -> .plabel= l ∘ι_{W,V}
%D    B1 B3  -> .plabel= r ∘ι_{W,V}
%D    B2 B3 `-> .plabel= a ι_W
%D    C0 C1 `-> .plabel= a ι
%D
%D    D0 D1 |-> D0 D2 |-> D1 D3 |-> D2 D3 |-> 
%D ))
%D enddiagram
%D
$$\pu
  \diag{sieve-on-a-topology}
$$


% «sieves-and-sheaves»  (to ".sieves-and-sheaves")
% (find-maclanemoerdijkpage (+ 11 69) "2. Sieves and Sheaves")
% (find-maclanemoerdijkpage (+ 11 70) "a sieve S on U")

\subsection*{2. Sieves and Sheaves}

(From pages 69--70):

\begin{quotation}

On any space $X$, each open set $U$ determines a presheaf $\Hom(-,U)$ defined, for each open set $V$, by
%
$$\Hom(V,U) = \begin{cases}
              1 & \text{if $V⊂U$,} \\
              ∅ & \text{otherwise.} \\
              \end{cases}
$$

This presheaf is clearly a sheaf; it is the representable presheaf
$𝐛y(U) = \Hom(-,U)$ on the category $\Opens(X)$. Recall from section
I.4 that a {\sl sieve} $S$ on $U$ in this category is defined to be a
subfunctor of $\Hom(-,U)$. Replacing the sieve $S$ by the set (call it
$S$ again) of all those $V⊂U$ with $SV=1$, we may also describe a
sieve on $U$ as a subset $S⊂\Opens(U)$ of objects such that $V_0 ⊂ V ∈
S$ implies $V_0 ∈ S$. Each indexed family $\setofst{V_i⊂U}{i∈I}$ of
subsets of $U$ generates (= ``spans'') a sieve $S$ on $U$; namely, the
set $S$ consisting of all those open $V$ with $V ⊆ V_i$ for some $i$;
in particular, each $V_0 ⊂ U$ determines a {\sl principal sieve}
$(V_0)$ on $U$, consisting of all $V$ with $V⊆V_0$. It is not
difficult to see that a sieve $S$ on $U$ is principal iff the
subfunctor $S$ of $𝐛y(U)$ is a subsheaf (Exercise 1). A sieve $S$ on
$U$ is said to be a {\sl covering sieve} for $U$ when $U$ is the union
of all the open sets $V$ in $S$.

\end{quotation}

Let's see how to visualize this.

Definitions:

if $V∈\Opens(X)$ then $↓V = \setofst{W∈\Opens(X)}{W⊆V}$;

if $\calV⊆\Opens(X)$ then $↓\calV = \bigcup_{V∈\calV}(↓V)$.

%L house = ".1.|2.3|4.5"
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L local mpl = mpnew({zdef="bottlelr", scale="12pt", meta=""}, "12321L")
%L mpl:addlrs():output()
\pu

Let's use this topology from \cite[sections 12 and 13]{PH1}:

$X = H = \dagHouse$ (the ``house'' DAG), and
%
$$\Opens(X) \;\; = \;\; \zha{bottlelr} \;\; .
$$

\newpage

Writing 0 for $∅$,

%R local y22, mid, lc, dnlc, y21 =
%R 1/ 0   \, 1/ 0   \, 1/ 0   \, 1/ 0   \, 1/ 0   \
%R  |  1  |   |  0  |   |  0  |   |  0  |   |  0  |
%R  | 1 1 |   | 0 0 |   | 0 0 |   | 0 0 |   | 1 0 |
%R  |1 1 1|   |1 1 1|   |1 1 0|   |1 1 0|   |1 1 0|
%R  | 1 1 |   | 1 1 |   | 0 0 |   | 1 1 |   | 1 1 |
%R  \  1  /   \  1  /   \  0  /   \  1  /   \  1  /
%R -- y22 :tozmp({zdef="y22",  meta="s", size="6pt"}):addcells():output()
%R y22 :tozmp({zdef="y22",  scale="8pt"}):addcells():output()
%R mid :tozmp({zdef="mid",  scale="8pt"}):addcells():output()
%R lc  :tozmp({zdef="lc",   scale="8pt"}):addcells():output()
%R dnlc:tozmp({zdef="dnlc", scale="8pt"}):addcells():output()
%R y21 :tozmp({zdef="y21",  scale="8pt"}):addcells():output()
%R y21 :tozmp({zdef="bott", scale="5pt"}):addbullets():output()
\pu

$𝐛y(22) = \Hom(-,22) = \zha{y22} \;\; ,$

This is also a sieve on 22: $S = \zha{dnlc} \;\; .$

Let $\calV = \setofst{V_i⊂U}{i∈I} = \zha{lc}$;

then $\calV$ spans ${↓}\calV = \zha{dnlc}$.

Note that this ${↓}\calV$ is not a principal sieve.

We have $\bigcup ({↓}\calV) = 21 ≠ 22$, so ${↓}\calV$ is not a covering sieve on $U$.

\bsk

A subset $\calV⊆\Opens(X)$ is a sieve on $X$ if and only if $\calV = {↓}\calV$.

Let's use the letters $\calA, \calB, \calC, \ldots$ to denote sieves on $X$.

For every sieve $\calA$ on $X$ we have:

$\calA$ is a covering sieve on $\bigcup\calA$,

and ${↓}\bigcup\calA$ is a principal sieve (generated by $\bigcup\calA$).

\bsk

The operation $\calA \mapsto \calA^* := {↓}\bigcup\calA$ takes sieves to principal sieves.

This operation obeys $\calA ⊆ \calA^* = \calA^{**}$.

Fact (true but not obvious): $\calA^* ∩ \calB^* = (\calA ∩ \calB)^*$.

\bsk

Now reread \cite[sections 12 and 13]{PH1}.

Remember that $\Opens(H) = \Opens(\dagHouse) = \zha{bott}$.

In \cite[p.20]{DaveyPriestley} the operation `$\Opens$' is defined in
a different, but equivalent, way: if $X$ is an ordered set then
$\Opens(X)$ is the set of the down-sets of $X$, ordered by inclusion.

\newpage

% «O-Bottle»  (to ".O-Bottle")
% «OO-House»  (to ".OO-House")
% (find-LATEX "2020sheaves.tex" "OO-House")

With the definition in \cite{DaveyPriestley} it is easy to calculate
$\Opens(\Opens(H))$ as a set of down-sets, and then interpret it as a
topology. We have:

% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ 10  24)    "1.28 The ordered set O(P ) of down-sets")
% (find-daveypriestleytext (+ 10  24)    "1.28 The ordered set O(P ) of down-sets")

% (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
%
% Let B be the bottle ZHA.
% Label its nodes like this:
%
%    L
%     M
%    L R
%   L M R
%    L R
%     M
%
% I name the elements of O(B) by counting how many 1s
% they have on Ls, Ms, and Rs. The topology O(B) is:
%
%         433
%            \
%             333
%              |
%             323
%            /   \
%         322     223
%        /   \   /   \
%     321     222     123
%        \   / | \   /
%         221 212 122
%          | X   X |
%         211 121 112
%        /   \ | /   \
%     210     111     012
%        \   /   \   /
%         110     011
%            \   /
%             000
%
%
% (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
\def\Def#1#2{\expandafter\def\csname myDef#1\endcsname{#2}}
\def\Get  #1{\csname                 myDef#1\endcsname}
\def\Run  #1{\csname                 myDef#1\endcsname}
\def\Defupperargs   #1#2{\Def{21}{#1}\Def{12}{#2}}
\def\Defmiddleargs#1#2#3{\Def{20}{#1}\Def{11}{#2}\Def{02}{#3}}
\def\Deflowerargs   #1#2{\Def{10}{#1}\Def{01}{#2}}
\def\Defallargs#1.#2.#3.#4.#5.#6{
  \Def{32}{#1}
    \Def{22}{#2}
    \Defupperargs#3
    \Defmiddleargs#4
    \Deflowerargs#5
    \Def{00}{#6}
}
\def\Setbottle#1#2{\Def{#1}{\Defallargs#2}}

\Setbottle{433}{1.1.11.111.11.1}
\Setbottle{333}{0.1.11.111.11.1}
\Setbottle{323}{0.0.11.111.11.1}

\Setbottle{322}{0.0.10.111.11.1}
\Setbottle{223}{0.0.01.111.11.1}

\Setbottle{321}{0.0.10.110.11.1}
\Setbottle{222}{0.0.00.111.11.1}
\Setbottle{123}{0.0.01.011.11.1}

\Setbottle{221}{0.0.00.110.11.1}
\Setbottle{212}{0.0.00.101.11.1}
\Setbottle{122}{0.0.00.011.11.1}

\Setbottle{211}{0.0.00.100.11.1}
\Setbottle{121}{0.0.00.010.11.1}
\Setbottle{112}{0.0.00.001.11.1}

\Setbottle{210}{0.0.00.100.10.1}
\Setbottle{111}{0.0.00.000.11.1}
\Setbottle{012}{0.0.00.001.01.1}

\Setbottle{110}{0.0.00.000.10.1}
\Setbottle{011}{0.0.00.000.01.1}

\Setbottle{010}{0.0.00.000.00.1}

\Setbottle{000}{0.0.00.000.00.0}

%% A simple test using matrices:
%
% \def\pbottle{\psm{
%         \Get{32} \;\;\;      \\
%            \Get{22}          \\
%         \Get{21} \Get{12}    \\
%   \Get{20} \Get{11} \Get{02} \\
%         \Get{10} \Get{01}    \\
%            \Get{00}          \\
%   }}
% 
% \def\B#1#2#3{\Run{#1#2#3}\pbottle}
% 
% $\def\S{\phantom{mmm}}
%  \mat{  \B433 \phantom{mm} \\
%            \B333 \\
%            \B323 \\
%         \B322 \S \B223 \\
%      \B321 \S \B222 \S \B123 \\
%      \B221 \B212 \B122 \\
%      \B211 \B121 \B112 \\
%      \B210 \S \B111 \S \B012 \\
%         \B110 \S \B011 \\
%             \B000 \\
%  }
% $


\def\G  #1#2{\Get{#1#2}}
\def\B#1#2#3{\Run{#1#2#3}\zha{bottlesieve}}

%R local bottlesieve =
%R 4/    !G32            \
%R  |        !G22        |
%R  |    !G21    !G12    |
%R  |!G20    !G11    !G02|
%R  |    !G10    !G01    |
%R  \        !G00        /
%R bottlesieve:tozmp({zdef="bottlesieve", meta="s", scale="4.5pt"}):addcells():output()
%R local bottlesieves =
%R 5/     !B433               \
%R  |          !B333          |
%R  |          !B323          |
%R  |     !B322     !B223     |
%R  |!B321     !B222     !B123|
%R  |     !B221!B212!B122     |
%R  |     !B211!B121!B112     |
%R  |!B210     !B111     !B012|
%R  |     !B110     !B011     |
%R  \          !B000          |
%R
%R -- A bug fix:
%R -- (find-dn6 "zhas.lua" "MixedPicture")
%R -- (find-dn6 "zhas.lua" "MixedPicture" "addarrowsexcept =")
%R -- (find-dn6 "zhas.lua" "MixedPicture-cuts")
%R -- (find-dn6file "zhas.lua" "addxys =")
%R -- (find-dn6 "picture.lua" "V" " xy =")
%R
%R V.__index.xy = function (v) return pformat("(%s,%s)", v[1], v[2]) end
%R
%R MixedPicture.__index.
%R    arrows = function (mp, w) return (mp.ar or mp.zha):arrows(w) end
%R
%R bottlesieves:tozmp({zdef="bottlesieves", meta="s", scale="42pt"})
%R      :addcells()
%R      :addarrowsexcept("w", "(0,4)0")
%R      :output()

\pu

$$\Opens(\Opens(\dagHouse))
 \;\;=\;\;
 \Opens(\zha{bott})
 \;\;=\;\;
 \zha{bottlesieves}
$$

The elements of $\Opens(\Opens(H))$ are exactly the sieves on $H$.

The operation $\calA \mto \calA^*$ that takes sieves on $H$ to
principal sieves is a J-operator on $\Opens(\Opens(H))$ (see
\cite{PH2}).


\newpage


% «top-sheaves-in-my-notation»  (to ".top-sheaves-in-my-notation")
\section*{Topological sheaves in my notation}

\def\calVi{\calV_i}
\def\calVj{\calV_j}
\def\hij{h_i|_j}
\def\hji{h_j|_i}


%D diagram top-sheaves-my-notation-1
%D 2Dx     100 +20 +20 +20 +20 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D  100 A0      C0
%D 2D         \       \
%D 2D  +20     A1      C1      E1          G1          I1 
%D 2D        /  |    /  |    /    \      /    \      /    \
%D 2D  +20 A2   |  C2   |  E2      E3  G2      G3  I2      I3
%D 2D        \  |    \  |    \    /      \    /      \      |
%D 2D  +20     A3      C3      E4          G4          I4  I5
%D 2D  +15     B0'             F0'
%D 2D  +10     B0 ---> D0      F0 ------>  H0  
%D 2D
%D ren A0 A1 A2 A3 ==> X U V W
%D ren C0 C1 C2 C3 ==> F(X) F(U) F(V) F(W)
%D ren B0' B0 D0   ==> \Opens(X)\;\; \Opens(X)^\op \Set
%D ren F0' F0 H0   ==> \Opens(X)\;\; \Opens(X)^\op \Set
%D ren E1 E2 E3 E4 ==> \bigcup\calV \calVi \calVj \calVi∩\calVj
%D ren G1 G2 G3 G4 ==> F(\bigcup\calV) F(\calVi) F(\calVj) F(\calVi∩\calVj)
%D ren I1 I2 I3 I4 I5 ==> g h_i h_j \hij \hji
%D
%D (( A0 A1 <-
%D    A1 A2 <-
%D    A2 A3 <-
%D    A1 A3 <-
%D    C0 C1 ->
%D    C1 C2 ->
%D    C2 C3 ->
%D    C1 C3 ->
%D    B0' xy+= -10 0
%D    B0  xy+= -10 0
%D    D0  xy+= -10 0
%D    B0' place
%D    B0 D0 ->
%D
%D    E1 E2 <-
%D    E1 E3 <-
%D    E2 E4 <-
%D    E3 E4 <-
%D    G1 G2 ->
%D    G1 G3 ->
%D    G2 G4 ->
%D    G3 G4 ->
%D    F0' place
%D    F0 H0 ->
%D
%D    I4 xy+= -10 0  I5 xy+= -10 0
%D    I4 xy+=  4  0  I5 xy+=  -4 0
%D    I1 I2 |->
%D    I1 I3 |->
%D    I2 I4 |->
%D    I3 I5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{top-sheaves-my-notation-1}
$$

$$
  \begin{array}[t]{l}
  I : \text{a set} \\
  \calV : I → \Opens(X) \\
  \bigcup\calV := \bigcup_{i∈I} \calV_i \\
  g : F(\bigcup\calV) \\
  h : (i:I) \to F(\calV_i) \\
  i,j : I \\
  g|_\calV : F_e(\calV) \\
  g|_\calV := λi.F(ι:\calV_i→\bigcup\calV)(g) \\
  \end{array}
  %
  \!\!\!\!\!\!\!\!
  %
  \begin{array}[t]{l}
  \hij := F(ι:\calV_i∩\calV_j→\calV_i)(h_i) \\
  \hji := F(ι:\calV_j∩\calV_j→\calV_j)(h_j) \\
  F_0(\calV) := F(\bigcup\calV) \\
  F_1(\calV) :=   (i:I) \to F(\calV_i) \\
  F_e(\calV) := \setofst {h:(i:I)→F(\calV_i)} {∀(i,j:I).\hij=\hji} \\
  F_2(\calV) := (i,j:I) \to F(\calV_i∩\calV_j) \\
  \end{array}
$$

%D diagram top-sheaves-my-notation-2
%D 2Dx     100  +30  +30  +30  +30  +30
%D 2D  100 A0             B0
%D 2D      |  \           |  \             
%D 2D  +22 |   \          B1   B2
%D 2D   +8 Ae - A1 - A2   B3 - B4
%D 2D   +8                     B5 - B6
%D 2D   +8                     B7 - B8
%D 2D
%D ren A0 Ae A1 A2 ==> F_0(\calV) F_e(\calV) F_1(\calV) F_2(\calV)
%D ren B0 B1 B2 B3 B4 ==> g g|_\calV g|_\calV h h
%D ren B5 B6 ==> h λi,j.\hij
%D ren B7 B8 ==> h λi,j.\hji
%D
%D (( A0 Ae ->
%D    A0 A1 ->
%D    Ae A1 ->
%D    A1 A2 ->
%D
%D    B0 B1 |->
%D  # B0 B2 |->
%D    B3 B4 |->
%D       B5 B6 |->
%D       B7 B8 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{top-sheaves-my-notation-2}
$$

\newpage

% (find-maclanemoerdijkpage (+ 11 83) "5. Sheaves and cross-sections")
% (find-maclanemoerdijkpage (+ 11 87) "Corollary 4")

{\bf II.5. Sheaves and cross-sections}

(Page 87):

%D diagram ??
%D 2Dx     100  +40  +20
%D 2D  100 A0 - A1   C0
%D 2D      |     |    |
%D 2D  +20 A2 - A3   C1
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> ΓΛ_P P
%D ren A2 A3 ==> F F
%D ren B0 B1 ==> \Sh(X) \SetsOXop
%D ren C0 C1 ==> P ΓΛ_P
%D
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= l σ
%D    A1 A3 -> .plabel= r θ
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 |->
%D
%D    B0 B1 <- sl^ .plabel= a ΓΛ
%D    B0 B1 >-> sl_ .plabel= b \text{inc}
%D  # newnode: B1' at: @B1+v(45,0) .TeX= =\widehat{\Opens(X)}=\PSh(X)? place
%D    newnode: B1' at: @B1+v(30,0) .TeX= =\widehat{\Opens(X)} place
%D
%D    C0 C1 -> .plabel= r η
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

% (find-maclanemoerdijkpage (+ 11 88) "6. Sheaves as Étale Spaces")

(Page 88):

6. Sheaves as Étale Spaces

%D diagram ??
%D 2Dx     100   +25  +45  +20
%D 2D  100 L0    A0 - A1   R0
%D 2D      |     |     |    |
%D 2D  +20 L1    A2 - A3   R1
%D 2D
%D 2D  +15 B0' - B0 - B1
%D 2D
%D ren A0 A1 ==> ΛP P
%D ren A2 A3 ==> Y ΓY
%D ren B0 B1 ==> \Bund(X) \SetsOXop
%D ren L0 L1 ==> ΛΓY Y
%D ren R0 R1 ==> P ΓΛP
%D
%D (( A0 A1 <-|
%D    A0 A2 -> # .plabel= l σ
%D    A1 A3 -> # .plabel= r θ
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 |->
%D
%D    newnode: B0' at: @B0+v(-35,0) .TeX= \Top/X  B0' B0 =
%D    B0 B1 <- sl^ .plabel= a Λ
%D    B0 B1 -> sl_ .plabel= b Γ
%D  # newnode: B1' at: @B1+v(45,0) .TeX= =\widehat{\Opens(X)}=\PSh(X)? place
%D  # newnode: B1' at: @B1+v(30,0) .TeX= =\widehat{\Opens(X)} place
%D
%D    R0 R1 -> .plabel= r η_P
%D    L0 L1 -> .plabel= l ε_Y
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\newpage

% «sheaves-on-a-site»  (to ".sheaves-on-a-site")
% (mmop 13 "sheaves-on-a-site")
% (mmoa    "sheaves-on-a-site")

\subsubsection*{III.4. Sheaves on a Site}

(Page 121)

% (find-maclanemoerdijkpage (+ 11 121) "4. Sheaves on a Site")
% (find-maclanemoerdijkpage (+ 11 123) "Proposition 1")

Definition in page 122:
%
%D diagram ??
%D 2Dx     100 +20 +20  +20 +30 +30
%D 2D  100 A0  A1  B0 - B1  C0  D0
%D 2D           |  |  /     |   |
%D 2D  +20     A2  B2       C1  D1
%D 2D
%D ren A0 A1 A2 ==> C J(C) ∀S
%D ren B0 B1 B2 ==> 𝐛yC P S
%D ren C0 C1    ==> \Hom(𝐛yC,P) \Hom(S,P)
%D ren D0 D1    ==> g g∘i
%D
%D (( A0 place
%D    A1 A2 <- .plabel= r ∈
%D    B0 B1 -> .plabel= a ∃!g
%D    B0 B2 <- .plabel= l i
%D    B2 B1 -> .plabel= r ∀f
%D    C0 C1 -> .plabel= r \sm{(∘i)\\\text{iso}}
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



Archetypal case:
%
%D diagram ??
%D 2Dx     100 +20 +20  +20 +30 +30
%D 2D  100 A0  A1  B0 - B1  C0  D0
%D 2D           |  |  /     |   |
%D 2D  +20     A2  B2       C1  D1
%D 2D
%D ren A0 A1 A2 ==> U J(U) ∀\calU
%D ren B0 B1 B2 ==> {↓}U F \calU
%D ren C0 C1    ==> \Hom({↓U},F) \Hom(\calU,F)
%D ren D0 D1    ==> g g∘i
%D
%D (( A0 place
%D    A1 A2 <- .plabel= r ∈
%D    B0 B1 -> .plabel= a ∃!g
%D    B0 B2 <- .plabel= l i
%D    B2 B1 -> .plabel= r ∀f
%D    C0 C1 -> .plabel= r \sm{(∘i)\\\text{iso}}
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

Only the `$j$'s:
%
%D diagram ??
%D 2Dx     100 100 +20  +20 +30 +30
%D 2D  100 A0  A1  B0 - B1  C0  D0
%D 2D           |  |  /     |   |
%D 2D  +20     A2  B2       C1  D1
%D 2D
%D ren A0 A1 A2 ==> . P^* ∀P
%D ren B0 B1 B2 ==> P^* F P
%D ren C0 C1    ==> \Hom(P^*,F) \Hom(P,F)
%D ren D0 D1    ==> g g∘d
%D
%D (( A0 place
%D    A1 A2 <- .plabel= l \sm{d\\\text{dense}}
%D    B0 B1 -> .plabel= a ∃!g
%D    B0 B2 <- .plabel= l d
%D    B2 B1 -> .plabel= r ∀f
%D    C0 C1 -> .plabel= r \sm{(∘d)\\\text{iso}}
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

All dense truth values:
%
%D diagram ??
%D 2Dx     100 100 +20  +20 +30 +30
%D 2D  100 A0  A1  B0 - B1  C0  D0
%D 2D           |  |  /     |   |
%D 2D  +20     A2  B2       C1  D1
%D 2D
%D ren A0 A1 A2 ==> . ∀Q ∀P
%D ren B0 B1 B2 ==> Q F P
%D ren C0 C1    ==> \Hom(Q,F) \Hom(P,F)
%D ren D0 D1    ==> g g∘d
%D
%D (( A0 place
%D    A1 A2 <- .plabel= l \sm{d\\\text{dense}}
%D    B0 B1 -> .plabel= a ∃!g
%D    B0 B2 <- .plabel= l d
%D    B2 B1 -> .plabel= r ∀f
%D    C0 C1 -> .plabel= r \sm{(∘d)\\\text{iso}}
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

All dense maps (see Bell p.174):
%
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 174)    "(mu-)sheaf")
%
%D diagram ??
%D 2Dx     100 100 +20  +20 +30 +30
%D 2D  100 A0  A1  B0 - B1  C0  D0
%D 2D           |  |  /     |   |
%D 2D  +20     A2  B2       C1  D1
%D 2D
%D ren A0 A1 A2 ==> . ∀B ∀A
%D ren B0 B1 B2 ==> B F A
%D ren C0 C1    ==> \Hom(B,F) \Hom(A,F)
%D ren D0 D1    ==> g g∘d
%D
%D (( A0 place
%D    A1 A2 <- .plabel= l \sm{d\\\text{dense}}
%D    B0 B1 -> .plabel= a ∃!g
%D    B0 B2 <- .plabel= l d
%D    B2 B1 -> .plabel= r ∀f
%D    C0 C1 -> .plabel= r \sm{(∘d)\\\text{iso}}
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage

\subsubsection*{III.5. The associated sheaf functor}

(Page 128):

% (find-maclanemoerdijkpage (+   11 128) "5. The associated sheaf functor" "P^+")

%D diagram ??
%D 2Dx     100  +40  +20
%D 2D  100 A0 - A1   C0
%D 2D      |     |    |
%D 2D  +20 A2 - A3   C1
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> 𝐛a{P} P
%D ren A2 A3 ==> F F
%D ren B0 B1 ==> \Sh(\catC,J) \SetsCop
%D ren C0 C1 ==> P i𝐛aP
%D
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= l ?
%D    A1 A3 -> .plabel= r ?
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 |->
%D
%D    B0 B1 <- sl^ .plabel= a 𝐛a
%D    B0 B1 >-> sl_ .plabel= b i
%D    newnode: A0' at: @A0+v(-25,0) .TeX= (P^+)^+= place
%D    newnode: B1' at: @B1+v(30,0) .TeX= =\widehat{\Opens(X)} place
%D
%D    C0 C1 -> .plabel= r η
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\newpage

% «LT-subsumes-groth»  (to ".LT-subsumes-groth")
% (mmop 12 "LT-subsumes-groth")
% (mmoa    "LT-subsumes-groth")

% (find-maclanemoerdijkpage (+   11 233) "V.4 Lawvere-Tierney Subsumes Grothendieck")

\section*{V.4 Lawvere-Tierney Subsumes Grothendieck}


%  _                    _ _        _                    _ 
% | |    ___   ___ __ _| (_) ___  | |_ ___  _ __   ___ (_)
% | |   / _ \ / __/ _` | | |/ __| | __/ _ \| '_ \ / _ \| |
% | |__| (_) | (_| (_| | | | (__  | || (_) | |_) | (_) | |
% |_____\___/ \___\__,_|_|_|\___|  \__\___/| .__/ \___/|_|
%                                          |_|            
%
% «localic-topoi»  (to ".localic-topoi")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11 470) "IX. Localic Topoi")
% (find-maclanemoerdijkpage (+   11 480)   "4. Embeddings and Surjections of Locales")
% (find-maclanemoerdijkpage (+   11 483)     "nucleus")
% (find-maclanemoerdijkpage (+   11 487)   "5. Localic Topoi")

\section*{IX. Localic Topoi}

% (find-maclanemoerdijkpage (+   11 471) "Lemma 1")

(Page 471)

Lemma IX.1.1:

%D diagram ??
%D 2Dx     100  +25
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +20 A2 - A3
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> Φ(V) V
%D ren A2 A3 ==> U Ψ(U)
%D ren B0 B1 ==> A B
%D
%D (( A0 A1 <-|
%D    A0 A2 ->
%D    A1 A3 ->
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 |->
%D    B0 B1 <- sl^ .plabel= a Φ
%D    B0 B1 -> sl_ .plabel= b Ψ
%D
%D    newnode: A3' at: @A3+v(50,0) .TeX= =\bigvee\setofst{V∈B}{Φ(V)≤U} place
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

%D diagram ??
%D 2Dx     100  +30
%D 2D  100 A0 - A1
%D 2D      |     |
%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^{-1}(V) V
%D ren A2 A3 ==> U f_*(U)
%D ren B0 B1 ==> \Opens(S) \Opens(T)
%D ren C0 C1 ==> S T
%D
%D (( A0 A1 <-|
%D    A0 A2 ->
%D    A1 A3 ->
%D    A0 A3 harrownodes nil 20 nil <->
%D    A2 A3 |->
%D    B0 B1 <- sl^ .plabel= a f^{-1}
%D    B0 B1 -> sl_ .plabel= b f_*
%D    C0 C1 -> .plabel= a f
%D
%D    newnode: A3' at: @A3+v(60,0) .TeX= =\bigcup\setofst{V∈\Opens(T)}{f^{-1}V⊆U} place
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


% (find-maclanemoerdijkpage (+ 11 472) "(Locales)")

(Page 472):
%
%D diagram ??
%D 2Dx     100 +65  +30 +30  +40
%D 2D  100 A0  B0 - B1  C0 - C1
%D 2D      |   |     |  |     |
%D 2D  +25 A1  B2 - B3  C2 - C3
%D 2D      |   |     |  |     |
%D 2D  +25 A2  B4 - B5  C4 - C5
%D 2D
%D ren A0 A1 A2 ==> (\Locales) (\Frames)^\op (\Spaces)
%D ren B0 B1 C0 C1 ==>        S         T  (\Opens(S),⊆) (\Opens(T),⊆)
%D ren B2 B3 C2 C3 ==> \Opens(S) \Opens(T) (\Opens(S),⊆) (\Opens(T),⊆)
%D ren B4 B5 C4 C5 ==>        S         T  (S,\Opens(S)) (T,\Opens(T))
%D
%D
%D (( A0 A1 <->
%D    A1 A2 <-
%D
%D    B0 B1 -> .plabel= a f
%D    B0 B2 <->
%D    B1 B3 <->
%D    B0 B3 varrownodes nil 17 nil <->
%D    B2 B3 <- .plabel= a f^{-1}
%D    B2 B4 <->
%D    B3 B5 <->
%D    B2 B5 varrownodes nil 17 nil <-|
%D    B4 B5  -> .plabel= a f
%D
%D    C0 C1 <-
%D    C0 C2 <->
%D    C1 C3 <->
%D    C0 C3 varrownodes nil 17 nil <->
%D    C2 C3 <-
%D    C2 C4 <->
%D    C3 C5 <->
%D    C2 C5 varrownodes nil 17 nil <-|
%D    C4 C5  ->
%D
%D    newnode: A1' at: @A1+v(35,0) .TeX= (\Frames) place
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage

% (find-maclanemoerdijkpage (+ 11 472) "(Locales)")

(Page 474):
%
Lemma 1, archetypal case:
%
%D diagram ??
%D 2Dx     100 +100 +30
%D 2D  100     B0 - B1
%D 2D
%D 2D  +15 A0  B2 - B3
%D 2D      |
%D 2D  +20 A1  B4 - B5
%D 2D
%D ren A0 A1 ==> (\Frames) (\Spaces)^\op
%D ren B0 B1 ==> p^{-1}U U
%D ren B2 B3 ==> \{0,1\} \Opens(X)
%D ren B4 B5 ==> 1 X
%D
%D (( A0 A1 <-
%D    newnode: A1' at: @A1+v(35,0) .TeX= (\Spaces) place
%D
%D    B0 B1 <-|
%D    B2 B3 <-  .plabel= a p^{-1}
%D    B4 B5  -> .plabel= a p
%D
%D    newnode: B0' at: @B0+v(-45,0) .TeX= \setofst{*∈1}{p(*)\not∈U}= place
%D    newnode: B2' at: @B2+v(-30,0) .TeX= \{∅,\{*\}\}= place
%D    newnode: B4' at: @B4+v(-22,0) .TeX= \{*\}= place
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

For each $p:1→X$ we define $K$ and $P$ as:
%
$$\begin{array}{rcl}
  \Opens(X) \;\; ⊇ \;\;
  K &:=& \Ker p^{-1} \\
     &=& \setofst{U∈\Opens(X)}{p^{-1}U=0} \\
     &=& \setofst{U∈\Opens(X)}{p^{-1}U=∅} \\
     &=& \setofst{U∈\Opens(X)}{*\not∈p^{-1}U} \\
     &=& \setofst{U∈\Opens(X)}{p(*)\not∈U} \\
  \Opens(X) \;\; \ni \;\;
  P &:=& \bigcup K \\
     &=& \bigcup\setofst{U∈\Opens(X)}{p(*)\not∈U} \\
     &=& \Int(X-\{p(*)\}) \\
  \end{array}
$$

This $K$ is a {\sl kernel} on $\Opens(X)$. The definition is: a kernel
on $\Opens(X)$ is a subset $K⊆\Opens(X)$ that is closed downwards,
closed by taking arbitrary unions, and it obeys $1\not∈K$ and, for all
$U,V∈\Opens(X)$:
%
$$U∧V∈K \text{ implies } U∈K \text{ or } V∈K.$$

This $P$ is a {\sl proper prime element} of $\Opens(X)$. The
definition is: a $P∈\Opens(X)$ is a proper prime element iff $1≠P$,
and, for all $U,V∈\Opens(X)$:
%
$$U∩V⊆P \text{ implies } U⊆P \text{ or } V⊆P.$$

\newpage

%  _                       _         _   
% | |    ___   ___        | |  _ __ | |_ 
% | |   / _ \ / __|  _____| | | '_ \| __|
% | |__| (_) | (__  |_____| | | |_) | |_ 
% |_____\___/ \___|       | | | .__/ \__|
%                         |_| |_|        
%
% «spaces-from-locales»  (to ".spaces-from-locales")
% (mmop 14 "spaces-from-locales")
% (mmoa    "spaces-from-locales")

% (find-maclanemoerdijkpage (+ 11 473) "There is an obvious functor Loc")

(Page 473):

There is an obvious functor $\Loc$ from spaces to locales:

%D diagram ??
%D 2Dx     100  +45 +40  +40
%D 2D  100 A0 - A1  C0 - C1
%D 2D      |     |  |     |
%D 2D  +20 A2 - A3  C2 - C3
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> S \Loc(S)
%D ren A2 A3 ==> T \Loc(T)
%D ren B0 B1 ==> (\Spaces)   (\Locales)
%D ren C0 C1 ==> (S,\Opens(S)) (\Opens(S),⊆)
%D ren C2 C3 ==> (T,\Opens(S)) (\Opens(T),⊆)
%D
%D (( A0 A1 |->
%D    A0 A2 -> .plabel= l f
%D    A1 A3 -> .plabel= r \Loc(f)
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    B0 B1 -> .plabel= a \Loc
%D    
%D    C0 C1 |->
%D    C0 C2 -> .plabel= l f
%D    C1 C3 <- .plabel= r f^{-1}
%D    C0 C3 harrownodes nil 20 nil |->
%D    C2 C3 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\bsk

(Page 475):

IX.3: Spaces from locales

% (find-maclanemoerdijkpage (+ 11 475) "3. Spaces from Locales")
% (find-maclanemoerdijkpage (+ 11 477) "Proposition 2")

On locales that come from a topological spaces we define the functor
$\Pt: (\Locales)→(\Spaces)$ as this. The functor takes each locale
$X≡(\Opens(X),⊆)$ to a topological space $\Pt(X) ≡
(\Pt(X),\Opens(\Pt(X))$, where:
%
$$\begin{array}{rcl}
  \Pt(X) &:=& \setofst{p}{p:1→X} \\
  \text{for $U∈\Opens(X)$, } \;\;\;
  \Pt(U) &:=& \setofst{p:1→X}{p(*)∈U} \\
          &=& \setofst{p:1→X}{*∈p^{-1}(U)} \\
          &=& \setofst{p:1→X}{p^{-1}U = 1} \\
  \Opens(\Pt(X)) &:=& \setofst{\Pt(U)}{U∈\Opens(X)} \\
  \end{array}
$$

On locales $X≡(X,≤)$ we define the functor $\Pt: (\Locales)→(\Spaces)$
as this generalization of the idea above:
%
$$\begin{array}{rcl}
  \Pt(X) &:=& \setofst{p}{p:1→X} \\
  \text{for $U∈X$, } \;\;\;
  \Pt(U) &:=& \setofst{p:1→X}{p^{-1}U = 1} \\
  \Opens(\Pt(X)) &:=& \setofst{\Pt(U)}{U∈X} \\
  \end{array}
$$

We draw that functor as:
%
%D diagram ??
%D 2Dx     100  +40  +30  +45 +40
%D 2D  100 A0 - A1   C0 - C1  D0
%D 2D      |     |   |     |   |
%D 2D  +20 A2 - A3   C2 - C3  D1
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> X \Pt(X) Y \Pt(Y)
%D ren B0 B1    ==> (\Locales) (\Spaces)
%D ren C0 C1    ==> (X,≤) (\Pt(X),\Opens(\Pt(X))
%D ren C2 C3    ==> (Y,≤) (\Pt(Y),\Opens(\Pt(Y))
%D ren D0 D1    ==> p f∘p
%D
%D (( A0 A1 |->
%D    A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r \Pt(f)
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    B0 B1  -> .plabel= a \Pt
%D    
%D    C0 C1 |->
%D    C0 C2 <-
%D    C1 C3  ->
%D    C0 C3 harrownodes nil 20 nil |->
%D    C2 C3 |->
%D
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\newpage

(Page 476):

Theorem 1: The functor $\Pt: (\Locales) → (\Spaces)$ is right adjoint
to the functor $\Loc: (\Spaces) → (\Locales)$.

% (find-maclanemoerdijkpage (+ 11 476) "Theorem 1. Loc -| pt")

%D diagram ??
%D 2Dx     100 +20  +40 +30  +50
%D 2D  100 A0  B0 - B1  C0 - C1
%D 2D      |   |     |  |     |
%D 2D  +20 A1  B2 - B3  C2 - C3
%D 2D
%D 2D  +15     D0 - D1
%D 2D
%D ren D0 D1 ==> (\Locales) (\Spaces)
%D ren B0 B1 B2 B3 ==> \Loc(S) S X \Pt(X)
%D ren C0 C1 C2 C3 ==> (\Opens(S),⊆) (S,\Opens(S)) (X,≤) (\Pt(X),\Opens(\Pt(X))
%D
%D (( D0 D1 <- sl^ .plabel= a \Loc
%D    D0 D1 -> sl_ .plabel= b \Pt
%D    
%D    B0 B1 <-|
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r g
%D    B0 B3 harrownodes nil 20 nil <->
%D    B2 B3 |->
%D    
%D    C0 C1 <-|
%D    C0 C2 <- .plabel= l f^{-1}
%D    C1 C3  -> .plabel= r g
%D    C0 C3 harrownodes nil 20 nil <->
%D    C2 C3 |->
%D    
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

% (find-maclanemoerdijkpage (+ 11 477) "Proof")

Proof:
%
$$\begin{array}{rcl}
  f^{-1} &:=& \\
  \end{array}
$$



%  ____     _                    _ _        _                    _ 
% | ___|   | |    ___   ___ __ _| (_) ___  | |_ ___  _ __   ___ (_)
% |___ \   | |   / _ \ / __/ _` | | |/ __| | __/ _ \| '_ \ / _ \| |
%  ___) |  | |__| (_) | (_| (_| | | | (__  | || (_) | |_) | (_) | |
% |____(_) |_____\___/ \___\__,_|_|_|\___|  \__\___/| .__/ \___/|_|
%                                                   |_|            
%
% «5._localic_topoi»  (to ".5._localic_topoi")
% (find-maclanemoerdijkpage (+ 11 487) "Proof")
% (find-maclanemoerdijkpage (+ 11 488) "Theorem 1")

\subsubsection*{IX.5. Localic topoi}

(Page 487):

(Page 488):

Theorem 1: For a Grothendieck topos the following are equivalent:

(i) $\calE$ is localic,

(ii) there exists a site for $\calE$ with a poset as underlying category,

(iii) $\calE$ is generated by the subobjects of its terminal object 1.

Proof. Since a frame is a poset, (i) trivially implies (ii).

(ii) $⇒$ (iii) Suppose that $\calE = \Sh(\catP,J)$, where $J$ is a
Grothendieck topology on a poset $\catP$, and write $𝐛a𝐛y: \catP →
\calE$ for the process of sheafification $𝐛a$ followed by the Yoneda
embedding. Now for each $p∈\catP$ the map is necessarily monic in
presheaves, while sheafification $𝐛a$ is left exact, hence preserves
monics. Thus every map $𝐛a𝐛y(p)→1$ is monic, hence gives a subobject
of 1. But III.6(17) showed that the images of the $𝐛a𝐛y$ generate the
topos $\calE$.

%D diagram ??
%D 2Dx     100  +30  +35  +25
%D 2D  100 A0 - A1 - A2
%D 2D
%D 2D  +20      A4 - A5
%D 2D
%D 2D  +15 B0 - B1 - B2 = B3
%D 2D
%D ren A0 A1 A2 ==> p 𝐛yp 𝐛a𝐛yp
%D ren    A4 A5 ==>    1    1
%D ren B0 B1 B2 B3 ==> \catP \Sets^{\catP^\op} \Sh(\catP,J) \calE
%D
%D (( A0 A1 |->
%D    A1 A2 |->
%D    A1 A4 >->
%D    A2 A5 >->
%D    A4 A5 |->
%D    B0 B1 -> .plabel= a 𝐛y
%D    B1 B2 -> .plabel= a 𝐛a
%D    B2 B3 =
%D  # newnode: B2' at: @B2+v(20,0) .TeX= =\calE place
%D    B0 B3 -> .slide= -10pt .plabel= b 𝐛a𝐛y
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


% (find-maclanemoerdijkpage (+ 11 487) "5. Localic Topoi")
% (find-maclanemoerdijkpage (+ 11 488) "Theorem 1. For a Grothendieck topos")
% (find-maclanemoerdijkpage (+ 11 488) "canonical")
% (find-maclanemoerdijkpage (+ 11 488) "following the Yoneda embedding")

\newpage

$\acz
  \psm{
       & ·  &    &    &    \\
       &    & ·  &    &    \\
       & ·  &    & ·  &    \\
    20 &    & ·  &    & 02 \\
       & 10 &    & 01 &    \\
       &    & 00 &    &    \\
  }
$
is a covering sieve for 22


% (find-books "__cats/__cats.el" "godement")

% (find-books "__cats/__cats.el" "grothendieck-tohoku")
% (find-grothtohokutpage (+ 9 36) "3 Cohomology with coefficients in a sheaf")

\printbibliography


\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020maclane-moerdijk veryclean
make -f 2019.mk STEM=2020maclane-moerdijk pdf

% Local Variables:
% coding: utf-8-unix
% ee-tla: "mmo"
% End: