|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019oxford-abs.tex")
% (defun c () (interactive) (find-LATEXsh "pdflatex -record 2019oxford-abs.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019oxford-abs.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019oxford-abs.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019oxford-abs; makeindex 2019oxford-abs"))
% (defun e () (interactive) (find-LATEX "2019oxford-abs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019oxford-abs"))
% (defun de () (interactive) (find-LATEX "2019oxford-abs.dnt"))
% (defun dp () (interactive) (find-LATEXsh "./dednat6load.lua -4 2019oxford-abs.tex" :end))
% (find-xpdfpage "~/LATEX/2019oxford-abs.pdf")
% (find-sh0 "cp -v ~/LATEX/2019oxford-abs.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019oxford-abs.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019oxford-abs.pdf
% file:///tmp/2019oxford-abs.pdf
% file:///tmp/pen/2019oxford-abs.pdf
% http://angg.twu.net/LATEX/2019oxford-abs.pdf
% «.defs» (to "defs")
% «.title» (to "title")
% «.cats-for-children» (to "cats-for-children")
% «.ZCategories» (to "ZCategories")
% «.defpictdots» (to "defpictdots")
% «.internal-diagrams» (to "internal-diagrams")
% «.fig:internal-1» (to "fig:internal-1")
% «.geometric-morphisms» (to "geometric-morphisms")
% «.fig:internal-gms» (to "fig:internal-gms")
% «.2CGs-and-ZHAs» (to "2CGs-and-ZHAs")
% «.fig:2CGs-ZHA» (to "fig:2CGs-ZHA")
% «.sheaves» (to "sheaves")
% «.two-factorizations-gms» (to "two-factorizations-gms")
% «.two-factorizations-zgms» (to "two-factorizations-zgms")
% «.fig:factorizations» (to "fig:factorizations")
% «.references» (to "references")
\documentclass[a4paper,superscriptaddress,11pt,accepted=2018-07-22,issuemonth=July,
issueyear=2018, shorttitle=template]{compositionalityarticle}
\pdfoutput=1
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{hyperref}
\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 2019oxford-chars.tex % (find-LATEX "2019oxford-chars.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")
\input 2019oxford-abs.dnt % (find-LATEX "2019oxford-abs.dnt")
\usepackage{tikz}
\usepackage{lipsum}
\newtheorem{theorem}{Theorem}
\newtheorem{conjecture}{Conjecture}
\begin{document}
% (find-angg "LATEX/2019oxford-diags.tex")
% ____ __
% | _ \ ___ / _|___
% | | | |/ _ \ |_/ __|
% | |_| | __/ _\__ \
% |____/ \___|_| |___/
%
% «defs» (to ".defs")
\def\termdef#1{{\sl #1}}
%\def\catA{\mathbf{A}}
%\def\catB{\mathbf{B}}
\def\catX{\mathbf{X}}
\def\catY{\mathbf{Y}}
\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}
\def\pu{}
%L -- output(preamble1)
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
%L -- io.stdout:setvbuf("no")
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (oxap 1 "title")
% (oxa "title")
\title{On some missing diagrams in the Elephant}
\date{2019-05-10}
\author{Eduardo Ochs}
\email{eduardoochs@gmail.com}
\homepage{http://angg.twu.net/math-b.html}
% \orcid{0000-0003-0290-4698}
\affiliation{Universidade Federal Fluminense, Rio das Ostras, RJ, Brazil}
\maketitle
\begin{abstract}
Imagine two category theorists, Aleks and Bob, who both think very
visually and who have exactly the same background. One day Aleks
discovers a theorem, $T_1$, and sends an e-mail, $E_1$, to Bob,
stating and proving $T_1$ in a purely algebraic way; then Bob is
able to reconstruct by himself Aleks's diagrams for $T_1$ exactly as
Aleks has thought them. We say that Bob has reconstructed the
𝐢{missing diagrams} in Aleks's e-mail.
Now suppose that Carol has published a paper, $P_2$, with a theorem
$T_2$. Aleks and Bob both read her paper independently, and both
pretend that she thinks diagrammatically in the same way as them.
They both ``reconstruct the missing diagrams'' in $P_2$ in the same
way, even though Carol has never used those diagrams herself.
Here we will reconstruct, in the sense above, some of the ``missing
diagrams'' in two factorizations of geometric morphisms in section
A4 of Johnstone's ``Sketches of an Elephant'', and also some
``missing examples''. Our criteria for determining what is
``missing'' and how to fill out the holes are essentially the ones
presented in the ``Logic for Children'' workshop at the UniLog 2018;
they are derived from a certain 𝐢{definition} of ``children'' that
turned out to be especially fruitful.
\end{abstract}
One of the themes of the workshop \cite{OchsLucatelli} was a set of
techniques for drawing diagrams for general cases and for particular
cases in parallel, in a way that makes both diagrams have similar
shapes, and that lets us transfer knowledge from the general to the
particular 𝐢{and back}. The term ``for children'' in the title of the
workshop comes from some peoples' reactions to Category Theory: ``𝐢{I
need a version for children of that!}''. We 𝐢{defined} children in a
certain way in order to get guidelines for how to construct a version
``for children'' of a categorical text; namely, ``children'': 1)
prefer to start from particular cases and then generalize; 2) like
diagrams and like finite objects that can be drawn explicitly; 3)
become familiar with mathematical ideas by calculating and by checking
several cases (i.e., by ``playing''), rather than by proving theorems.
% In this work we apply these ideas to toposes and geometric morphisms,
% and show a way to develop visual intuition about them.
% --- and a conjecture.
% (vivp 10 "children")
% (viv "children")
% In this work we apply these ideas to toposes and geometric morphisms.
% We play with toposes of the form $\Set^\catA$, where $\catA$ is a
% finite category with a defined shape, and with toposes whose logics
% are finite, planar Heyting Algebras. We get a shape for representing
% the diagrams for geometric morphisms and the surjection-inclusion and
% the dense-closed factorizations, and from this minimal knowledge we
% get
% «cats-for-children» (to ".cats-for-children")
%\section{Categories for Children}
%\label{cats-for-children}
% _________ _
% |__ / ___|__ _| |_ ___
% / / | / _` | __/ __|
% / /| |__| (_| | |_\__ \
% /____\____\__,_|\__|___/
%
% «ZCategories» (to ".ZCategories")
% (find-LATEX "2017planar-has-1.tex" "positional")
% \section{Categories drawn in a canonical way}
\section{Categories with coordinates}
\label{ZCategories}
Let's see a way to define finite categories whose objects have
coordinates in $\N^2$ and whose arrows can be named by just their
sources and targets. We call these categories 𝐢{ZCategories}, and it's
easier to start with an example. The left half of
Figure~\ref{fig:zcat-zpresheaf} is a ZCategory $\catA$ whose objects
are $\catA_0 = \{1,2,3,4,5\}$, with coordinates $c(1)=(0,2)$,
$c(2)=(1,1)$, $c(3)=(2,1)$, $c(4)=(1,0)$, $c(5)=(2,0)$. The arrow
$2→4$ belongs to $\catA$, but it is not shown. The right half of
Figure~\ref{fig:zcat-zpresheaf} is a functor $F:\catA→\Set$ --- a
𝐢{ZPresheaf}.
%D diagram ZCatA
%D 2Dx 100 +20 +20
%D 2D 100 o1
%D 2D
%D 2D +20 o2 o3
%D 2D
%D 2D +20 o4 o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> 1 2 3 4 5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram
%
%D diagram ZToposF
%D 2Dx 100 +20 +20
%D 2D 100 o1
%D 2D
%D 2D +20 o2 o3
%D 2D
%D 2D +20 o4 o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> F_1 F_2 F_3 F_4 F_5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram
\begin{figure}[!htbp]
\centering
$\pu
\catA =
\left(
\diag{ZCatA}
\right)
\qquad
F =
\left(
\diag{ZToposF}
\right)
$
\caption{A ZCategory and a ZPresheaf.}
\label{fig:zcat-zpresheaf}
\end{figure}
A 𝐢{ZSet} is a finite set $P⊂\N^2$ that touches both the $x$-axis and
the $y$-axis. A 𝐢{ZDirectedGraph} is a pair $(P,A)$ where $P$ is a
ZSet and $A⊆P×P$ is a set of arrows. We write $(P,A^*)$ for the
transitive-reflexive closure of $(P,A)$.
The section 1 of \cite{PH1} defines positional notations for ZSets and
for functions with ZSets as their domains. They're like this:
% (ph1p 3 "positional")
% (ph1 "positional")
% (ph1 "positional" "(1,3)")
% «defpictdots» (to ".defpictdots")
% (oxap 2 "defpictdots")
% (oxa "defpictdots")
%
%L defpictdots("a", "Kaxes", 0,0,2,3,nil, " 1,3 0,2 2,2 1,1 1,0 ")
%L defpictdots(nil, "K", 0,0,2,3,nil, " 1,3 0,2 2,2 1,1 1,0 ")
\pu
$$\csm{ (1,3), \\
(0,2), \;\;\; (2,2), \\
(1,1), \\
(1,0) \\
}
= \;\pido{Kaxes}\;
= \;\pido{K}
%
\qquad
%
\csm{ ((1,3),4), \\
((0,2),5), \;\;\; ((2,2),6), \\
((1,1),7), \\
((1,0),8) \\
}
=
\sm{ & 4 & \\
5 & & 6 \\
& 7 & \\
& 8 & \\
}
$$
The condition ``𝐢{...that touches both the $x$-axis and the
$y$-axis}'' lets us draw ZSets as just bullets, omitting the axes.
A 𝐢{ZCategory} $\catB$ is a category plus a structure $((P,A),c)$,
called its 𝐢{drawing instructions}, obeying: 1) $(P,A)$ is a
ZDirectedGraph; 2) $c:\catB_0→P$ is a bijection between the objects of
$\catB$ and the ZSet $P$; 3) for any objects $D,E∈\catB$ the hom-set
$\Hom_\catB(D,E)$ is singleton when $(c(D),c(E))∈A^*$, and is empty
when $(c(D),c(E)) \not∈ A^*$. The conditions 1--3 imply that a
ZCategory is a finite preorder category; the coordinates say where
each object is to be drawn, and the set $A$ says which arrows are to
be drawn explicitly; the other arrows are said to be 𝐢{implicit}.
A 𝐢{ZTopos} is a functor category of the form $\Set^\catB$, where
$\catB$ is a ZCategory. Objects of a ZTopos $\Set^\catB$ inherit the
drawing instructions from $\catB$, as the $F$ in the example above.
We call the objects of a ZTopos 𝐢{ZPresheaves}. Note that a
𝐢{presheaf} $P$ on $\catB$ is an element of $\Set^{\catB^\op}$, which
means that for each arrow $D→E$ in $\catB$ the presheaf $P$ returns an
arrow $P(D→E):PE→PD$ in $\Set$; ZPresheaves don't have this reversal
of direction.
% ___ _ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __| (_) __ _ __ _ ___
% | || '_ \| __/ _ \ '__| '_ \ / _` | | / _` | |/ _` |/ _` / __|
% | || | | | || __/ | | | | | (_| | | | (_| | | (_| | (_| \__ \
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \__,_|_|\__,_|\__, |___/
% |___/
% «internal-diagrams» (to ".internal-diagrams")
% (oxap 3 "internal-diagrams")
% (oxa "internal-diagrams")
\section{Internal Diagrams}
\label{internal-diagrams}
% (find-LATEXgrep "grep --color -niH -e internal *.tex")
% (vivp 22 "internal-views")
% (viv "internal-views")
% (find-books "__cats/__cats.el" "lawvere-rosebrugh")
% (find-books "__cats/__cats.el" "riehl")
Internal diagrams are a tool that lets us 𝐢{lower the level of
abstraction}. They merge ideas from the standard notation for
declaring functions with the way we used to draw functions in school,
using arrows between the elements of blob-sets. Look at
Figure~\ref{fig:internal-1}, at the left. Compare its `$\N→\R$' in the
upper line (the external view), with the `$n↦\sqrt{n}$' in the lower
line (the internal view); the $n↦\sqrt{n}$ shows a (generic) element
and its image. The middle part of Figure~\ref{fig:internal-1} shows
the external view at the bottom and an internal view at the top; note
that all elements in the blobs for $\N$ and $\R$ are named, but only a
few of the elements are shown (compare with \cite{LawvereRosebrugh},
p.3); the arrows like $3↦\sqrt3$ and $4↦2$, that show elements and
their images, are substitution instances of the generic $n↦\sqrt{n}$,
maybe after some calculations (or ``reductions'' in $λ$-calculus
terminology). The right part of Figure~\ref{fig:internal-1} shows an
adjunction $L⊣R$ between categories $\catA$ and $\catB$, drawn in our
favourite ``shape'' (see \cite{OchsYoneda}, where all this is
explained in detail): with the functor $L$ going left and the functor
$R$ going right. We don't draw blobs to stress that $B,LA,LRB∈\catB$
and $A,RB,RLA∈\catA$, and we draw ``generic'' unit and counit maps.
% «fig:internal-1» (to ".fig:internal-1")
% (oxap 4 "fig:internal-1")
% (oxa "fig:internal-1")
%
\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx 100 +20 +20
%D 2D 100 a-1 |--> b-1
%D 2D +08 a0 |--> b0
%D 2D +08 a1 |--> b1
%D 2D +08 a2 |--> b2
%D 2D +08 a3 |--> b3
%D 2D +08 a4 |--> b4
%D 2D +14 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D (( a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D b-1 place
%D a0 b0 |->
%D a1 b1 |->
%D a2 b2 |->
%D a3 b3 |->
%D a4 b4 |->
%D a5 b5 |->
%D \N \R -> .plabel= a \sqrt{\phantom{a}}
%D a-1 relplace -7 -7 \phantom{foo}
%D b5 relplace 7 7 \phantom{bar}
%D ))
%D enddiagram
%D
%D diagram adjunction
%D 2Dx 100 +20 +30 +20
%D 2D 100 A1 B1 <-| B2 C1
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 A2 B3 |-> B4 C2
%D 2D
%D 2D +20 D1 <=> D2
%D 2D
%D ren A1 A2 ==> LRB B
%D ren B1 B2 B3 B4 ==> LA A B RB
%D ren C1 C2 ==> A RLA
%D ren D1 D2 ==> \catB \catA
%D
%D (( A1 A2 -> .plabel= l εB
%D C1 C2 -> .plabel= r ηA
%D
%D B1 B2 <-| .plabel= a L_0
%D B1 B3 -> .plabel= l f
%D B2 B4 -> .plabel= r g
%D B3 B4 |-> .plabel= b R_0
%D B1 B4 harrownodes nil 20 nil <-| sl^ .plabel= a ♭_{AB}
%D B1 B4 harrownodes nil 20 nil |-> sl_ .plabel= b ♯_{AB}
%D
%D D1 D2 <- sl^ .plabel= a L
%D D1 D2 -> sl_ .plabel= b R
%D
%D ))
%D enddiagram
%D
\begin{figure}[!htbp]
\centering
$\begin{array}{rrcl}
\sqrt{\;\;}: & \N &→& \R \\
& n &↦& \sqrt{n} \\
\end{array}
\qquad
\diag{second-blob-function}
\qquad
%\diag{functor}
\diag{adjunction}
$
\caption{The standard notation for defining a function; \\
An internal view and the external view of the function $\sqrt{\;\;}$; \\
An internal view and the external view of an adjunction $L⊣R$.
}
\label{fig:internal-1}
\end{figure}
%D diagram functor
%D 2Dx 100 +30
%D 2D 100 A |-> FA
%D 2D
%D 2D +30 B |-> FB
%D 2D
%D 2D +20 \catC -> \catD
%D
%D (( A FA |-> .plabel= a F_0
%D A B -> .plabel= l g
%D FA FB -> .plabel= r Fg
%D B FB |-> .plabel= b F_0
%D A FB harrownodes nil 20 nil |-> .plabel= a F_1
%D \catC \catD -> .plabel= a F
%D ))
%D enddiagram
%D diagram NT
%D 2Dx 100 +20 +30 +45 +40
%D 2D 100 A FA -> GA a b
%D 2D
%D 2D +22 d1
%D 2D +8 B FB -> GB c d2
%D 2D
%D 2D +20 F --> G
%D 2D
%D 2D +20 \catC \catD
%D ren a b d1 ==> x TA(x) Gh(TA(x))
%D ren a c d2 ==> x Fh(x) TB(Fh(x))
%D
%D (( A B -> .plabel= l h
%D FA GA -> .plabel= a TA
%D FA FB -> .plabel= l Fh
%D GA GB -> .plabel= r Gh
%D FB GB -> .plabel= a TB
%D F G -> .plabel= a T
%D # \catD x+= 15
%D # \catC \catD ->
%D
%D a b |-> b d1 |->
%D a c |-> c d2 |->
%D ))
%D enddiagram
%D
% (ntyp 54 "CCCs")
% (nty "CCCs")
% ____ __ __
% / ___| \/ |___
% | | _| |\/| / __|
% | |_| | | | \__ \
% \____|_| |_|___/
%
% «geometric-morphisms» (to ".geometric-morphisms")
% (oxap 3 "geometric-morphisms")
% (oxa "geometric-morphisms")
\section{Geometric morphisms (and how to draw them)}
\label{geometric-morphisms}
A geometric morphism $f:\calE→\calF$ is an adjunction $(f^*⊣f_*)$
between toposes $\calE$ and $\calF$ plus the assurance that $f^*$ is
exact; a 𝐢{ZGM} is a geometric morphism generated by a functor
$f:\catA→\catB$ between ZCategories (a 𝐢{ZFunctor}), in the following
sense. A functor $f:\catA→\catB$ induces a geometric morphism
$f:\Set^\catA→\Set^\catB$ between ZToposes; where $f^*$ is defined
``by composition''. The right adjoint $f_*$ can be calculated by the
Kan extension formula, but in small examples it is better to calculate
it directly by guess-and-test. Figure~\ref{fig:gm-and-zgm} shows how
we draw a geometric morphism and a ZGM;
Figure~\ref{fig:zgm-particular-case} shows why we are interested in
ZGMs: if we choose ZCategories $\catA$ and $\catB$ we can replace
several objects of our diagram for ZGMs by their internal views, and
this gives us a way to ``understand'' the adjunction and the unit and
counit maps.
% Note that we reuse the name `$f$'.
% (find-LATEX "2017elephant.tex" "elephant-A4.1.5")
% «fig:internal-gms» (to ".fig:internal-gms")
% (oxap 5 "fig:internal-gms")
% (oxa "fig:internal-gms")
% (vivp 26 "internal-views-gm-2")
% (viv "internal-views-gm-2")
%D diagram internal-gm
%D 2Dx 100 +20 +30 +20
%D 2D 100 A1 B1 <-| B2 C1
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 A2 B3 |-> B4 C2
%D 2D
%D 2D +20 D1 <=> D2
%D 2D
%D 2D +20 E1 --> E2
%D 2D
%D 2D +20 F1 F2
%D 2D
%D ren A1 A2 ==> f^*f_*D D
%D ren B1 B2 B3 B4 ==> f^*C C D f_*D
%D ren C1 C2 ==> C f_*f^*C
%D ren B3 B4 ==> D f_*D
%D ren D1 D2 ==> \calE \calF
%D ren E1 E2 ==> \calE \calF
%D ren F1 F2 ==> \phantom{\catA} \phantom{\catB}
%D
%D (( A1 A2 -> .plabel= l εD
%D C1 C2 -> .plabel= r ηC
%D
%D B1 B2 <-|
%D B1 B3 -> B2 B4 ->
%D B3 B4 |->
%D B1 B4 harrownodes nil 20 nil <->
%D
%D D1 D2 <- sl^ .plabel= a f^*
%D D1 D2 -> sl_ .plabel= b f_*
%D E1 E2 -> .plabel= a f
%D
%D F1 place F2 place
%D ))
%D enddiagram
%D
%D diagram internal-zgm
%D 2Dx 100 +20 +30 +20
%D 2D 100 A1 B1 <-| B2 C1
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +30 A2 B3 |-> B4 C2
%D 2D
%D 2D +20 D1 <=> D2
%D 2D
%D 2D +20 E1 --> E2
%D 2D
%D 2D +20 F1 F2
%D 2D
%D ren A1 A2 ==> f^*f_*D D
%D ren B1 B2 B3 B4 ==> f^*C C D f_*D
%D ren C1 C2 ==> C f_*f^*C
%D ren B3 B4 ==> D f_*D
%D ren D1 D2 ==> \Set^\catA \Set^\catB
%D ren E1 E2 ==> \Set^\catA \Set^\catB
%D ren F1 F2 ==> \catA \catB
%D
%D (( A1 A2 -> .plabel= l εD
%D C1 C2 -> .plabel= r ηC
%D
%D B1 B2 <-|
%D B1 B3 -> B2 B4 ->
%D B3 B4 |->
%D B1 B4 harrownodes nil 20 nil <->
%D
%D D1 D2 <- sl^ .plabel= a f^*
%D D1 D2 -> sl_ .plabel= b f_*
%D E1 E2 -> .plabel= a f
%D
%D F1 F2 -> .plabel= a f
%D ))
%D enddiagram
%D
%R sesw = {[" w"]="↙", [" e"]="↘"}
%R
%R local zcB, zpBC, zpBRD
%R = 3/ 1 \, 3/ C_1 \, 3/ !Dt \
%R | w e | | w e | | w e |
%R | 2 3 | |C_2 C_3 | |D_2 D_3 |
%R | e w e | | e w e | | e w e |
%R | 4 5 | | C_4 C_5| | D_4 D_5|
%R | e w | | e w | | e w |
%R \ 6 / \ C_6 / \ 1 /
%R
%R local zpBRLC
%R = 3/ !Ct \
%R | w e |
%R |C_2 C_3 |
%R | e w e |
%R | C_4 C_5|
%R | e w |
%R \ 1 /
%R
%R local zcA, zpALC, zpAD
%R = 3/ 2 3 \, 3/C_2 C_3 \, 3/D_2 D_3 \
%R | e w e | | e w e | | e w e |
%R \ 4 5 / \ C_4 C_5/ \ D_4 D_5/
%R
%R zcB :tozmp({def="zcB", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBC :tozmp({def="zpBC", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRD :tozmp({def="zpBRD" , scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRLC:tozmp({def="zpBRLC", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zcA :tozmp({def="zcA", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpALC :tozmp({def="zpALC", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpAD :tozmp({def="zpAD", scale="7pt", meta="s p"}):addcells(sesw):output()
%D diagram internal-zgm-particular-case
%D 2Dx 100 +50 +55 +50
%D 2D 100 A1 B1 <-| B2 C1
%D 2D | | | |
%D 2D | | <-> | |
%D 2D v v v v
%D 2D +50 A2 B3 |-> B4 C2
%D 2D
%D 2D +30 D1 <=> D2
%D 2D
%D 2D +20 E1 --> E2
%D 2D
%D 2D +30 F1 F2
%D 2D
%D ren A1 B1 B2 C1 ==> \zpALC \zpALC \zpBC \zpBC
%D ren A2 B3 B4 C2 ==> \zpAD \zpAD \zpBRD \zpBRLC
%D ren D1 D2 ==> \Set^\catA \Set^\catB
%D ren E1 E2 ==> \Set^\catA \Set^\catB
%D ren F1 F2 ==> \catA \catB
%D ren F1 F2 ==> \zcA \zcB
%D
%D (( A1 A2 -> .plabel= l εD
%D C1 C2 -> .plabel= r ηC
%D
%D B1 B2 <-|
%D B1 B3 -> B2 B4 ->
%D B3 B4 |->
%D B1 B4 harrownodes nil 20 nil <->
%D
%D D1 D2 <- sl^ .plabel= a f^*
%D D1 D2 -> sl_ .plabel= b f_*
%D E1 E2 -> .plabel= a f
%D
%D F1 F2 -> .plabel= a f
%D ))
%D enddiagram
%D
\def\Ct{C_2 {×_{C_4}} C_3}
\def\Dt{D_2 {×_{D_4}} D_3}
\begin{figure}[!htbp]
\centering
$\diag{internal-gm}
\qquad
\diag{internal-zgm}
$
\caption{A geometric morphism and a ZGM.}
\label{fig:gm-and-zgm}
%
\bsk
\bsk
%
\centering
$\diag{internal-zgm-particular-case}$
\caption{A ZGM in a particular case.}
\label{fig:zgm-particular-case}
\end{figure}
% ____ _ ____ ____ ____
% / ___|| |__ ___ __ ___ _____ ___ ___ _ __ |___ \ / ___/ ___|___
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __| / _ \| '_ \ __) | | | | _/ __|
% ___) | | | | __/ (_| |\ V / __/\__ \ | (_) | | | | / __/| |__| |_| \__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/ \___/|_| |_| |_____|\____\____|___/
%
% «2CGs-and-ZHAs» (to ".2CGs-and-ZHAs")
% (oxap 4 "2CGs-and-ZHAs")
% (oxa "2CGs-and-ZHAs")
\section{Planar Heyting Algebras and 2-Column Graphs}
\label{sheaves-on-2CGs}
\label{2CGs-and-ZHAs}
The preprints \cite{PH1} and \cite{PH2} explain how to use 𝐢{2-column
graphs} (``{\sl 2CGs}'') to develop visual intuition about
intuitionistic logic (the first one) and sheaves (the second one).
The central construction in \cite{PH1} can be stated as: every 2CG is
associated to a Planar Heyting Algebra (a ``ZHA'', defined in section
4 of \cite{PH1}) and vice-versa, and the central construction in
\cite{PH2} is: every 2CG with question marks is associated to a ZHA
with a J-operator and vice-versa. This can be represented as:
%
$$\begin{array}{rcl}
(P,A) & \squigbijbody & H \\
% \\
((P,A),Q) & \squigbijbody & (H,J) \\
\end{array}
$$
%
where the `$\squigbijbody$' is pronounced ``is associated to''.
Formally, $(P,A) \squigbij H$ when $H$ is isomorphic to the order
topology $\Opens_A(P)$, and $((P,A),Q) \squigbij (H,J)$ when $(P,A)
\squigbij H$ and besides that the equivalence relation that $Q$
induces on $\Opens_A(P)$ is the same as the equivalence that the
J-operator $J$ induces on $H$.
Here's why this is relevant to us. We can regard a 2CG $(P,A)$ as a
ZCategory. The logic of the ZTopos $\Set^{(P,A)}$ --- i.e., its
$\Sub(1)$ --- is exactly $\Opens_A(P)$. Also, each sheaf
$\sh_j(\Set^{(P,A)})$ on $\Set^{(P,A)}$ corresponds to a set of
question marks $Q⊆P$ and vice-versa.
These constructions are easy to understand if we have a concrete
example, so look at Figure~\ref{fig:2CG-ZHA-example}.
% «fig:2CGs-ZHA» (to ".fig:2CGs-ZHA")
% (oxap 7 "fig:2CGs-ZHA")
% (oxa "fig:2CGs-ZHA")
%
\linethickness{0.3pt}
%
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7} -- with v arrows
%L tspec_PA = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L tspec_PA :mp ({zdef="O_A(P)"}) :addlrs():print() :output()
%L tspec_PAQ:mp ({zdef="O_A(P),J"}):addlrs():print() :output()
%L tspec_PA :tcgq({tdef="(P,A)", meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L tspec_PAC = TCGSpec.new("46; 11 22 34 45, 25", "?...", "???...")
%L tspec_PAC:mp ({zdef="closed-op"}) :addlrs():print() :output()
%L tspec_PAC:tcgq({tdef="closed-op", meta="1pt p"}, "lr q h v ap") :output()
%L
\pu
\begin{figure}[!htbp]
\centering
$\begin{array}{rcl}
(P,A) & \squigbijbody & H \\
% \\
((P,A),Q) & \squigbijbody & (H,J) \\
\end{array}
$
\caption{The correspondence between 2CGs and ZHAs: the general case.}
\label{fig:2CG-ZHA-general}
\bsk
\bsk
\bsk
$\begin{array}{ccl}
\tcg{(P,A)} & \squigbij & \zha{O_A(P)} \\
\\
\tcg{(P,A),Q} & \squigbij & \zha{O_A(P),J} \\
\end{array}
$
\caption{The correspondence between 2CGs and ZHAs: an example.}
\label{fig:2CG-ZHA-example}
\bsk
\bsk
\bsk
$\begin{array}{ccl}
\tcg{closed-op} & \squigbij & \zha{closed-op} \\
\end{array}
$
\caption{The closed operator $(13∨)$ (right) and its associated question marks (left).}
\label{fig:2CG-ZHA-closed-operator}
\end{figure}
The 𝐢{representation} of the characteristic function of a subset
$S⊆P$, $χ_S$, is the diagram that we obtain from $(P,A)$ by replacing
each point of $P$ by 1 when it belongs to $S$ and by 0 when not. We
say that $S$ 𝐢{obeys the condition} of an arrow $(α→β)∈A$ when
$χ_S(α)≤χ_S(β)$, and that $S$ 𝐢{violates the condition} of an
$(α→β)∈A$ when $χ_S(α)=1$ and $χ_S(β)=0$. A subset $S⊆P$ is
𝐢{$A$-open} when it obeys the conditions of all arrows in $A$.
$\Opens_A(P)$ is the set of all $A$-open subsets of $P$.
A 𝐢{specification} for a 2CG is a 4-uple $(l,r,R,L)$; it generates a
2CG $(P,A)$ with $P:=\pile(lr)$, and with sets of intercolumn arrows
$R$ (going right) and $L$ (going left). The set $A$ of arrows of
$(P,A)$ is $R∪L$ plus all the intracolumn arrows that point one step
down. The 2CG $(P,A)$ in Figure~\ref{fig:2CG-ZHA-general} is generated
by this specification:
%
$$(4,6,\csm{\ltor45, \\ \ltor34, \\ \ltor22, \\ \ltor11,},
\csm{\lotr25})
$$
We write $\pile(ab)$ for the set $\{a▁,\dots,1▁, \;\; ▁1,\ldots,▁b\}$;
$χ_{\pile(a,b)}$ is a pile of $a$ `1's in the left column and $b$ `1's
in the right column. A $\pile(ab)$ automatically obeys the conditions
of the vertical arrows in $A$ (as they all point one step down), and
it is possible to translate the intercolumn arrows into conditions in
the `$ab$'s (sec.15 of \cite{PH1}). The specification above becomes
this:
%
$$\Opens_A(P) = \setofst {\pile(ab)}
{a∈\{0,\ldots,4\},
b∈\{0,\ldots,6\},
\psm {a≥4 \;→\; b≥5 \; ∧ \\
a≥3 \;→\; b≥4 \; ∧ \\
a≥2 \;→\; b≥2 \; ∧ \\
a≥1 \;→\; b≥1 \;\;\; \\
} ∧
\psm {a≥2 \;←\; b≥5 \\
}
}
$$
%
that lets us draw the ZHA $H≅\Opens_A(P)$ very quickly --- and lets us
check the `$\squigbijbody$' in the top of
Figure~\ref{fig:2CG-ZHA-example}.
In the lower half of Figure~\ref{fig:2CG-ZHA-example} the set of
question marks is $Q=\{4▁,3▁,2▁,$ \; $▁1,▁2,▁3,▁5,\}$. The subsets
$S,S'⊆P$ are 𝐢{$Q$-equivalent} when $S$ and $S'$ only differ in points
of $Q$, i.e., $S∖Q = S'∖Q$. In the example, $\pile(22) ∼_Q \pile(23)
\not∼_Q \pile(24)$.
A J-operator on a Heyting Algebra $H$ is an operation $J:H→H$,
abbreviated as `$·^*$', obeying $P≤P^*=P^{**}$ and $(P∧Q)^*=P^*∧Q^*$.
The ``slashing'' in the ZHA of the lower half of
Figure~\ref{fig:2CG-ZHA-example} induces a J-operator that takes each
element of $H$ to the top element of its equivalence class:
$J(12)=23$. We say that $A,B∈H$ are $J$-equivalent when $A^*=B^*$. In
the example, $22 ∼_J 23 \not∼_J 24$. It is not hard to see that in
this case $(∼_Q) = (∼_P)$.
Figure \ref{fig:2CG-ZHA-closed-operator} shows the ``closed''
J-operator $(13∨)$, that takes each $A∈H$ to $13∨A$; it would be
called $J_{13}(p) = 13∨p$ in the notation of \cite{Fourman}, page 329,
2.18.(i).
% ____ _
% / ___|| |__ ___ __ ___ _____ ___
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __|
% ___) | | | | __/ (_| |\ V / __/\__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/
%
% «sheaves» (to ".sheaves")
% (oxap 7 "sheaves")
% (oxa "sheaves")
% (elep 15 "elephant-A4.5.3")
% (ele "elephant-A4.5.3")
% (find-elephanttext (+ 17 205))
% (find-elephantpage (+ 17 206) "Proposition 4.5.3")
\section{Question marks and sheaves}
\label{question-marks-and-sheaves}
\label{restrictions}
A J-operator $J$ in a $((P,A),Q) \squigbij (H,J)$ can be interpreted
in the topos $\Set^{(P,A)}$ as an operation $J:\Sub(1)→\Sub(1)$ on its
truth-values. This $J$ can be 𝐢{extended} to a 𝐢{local operator} (see
[EA4.4]) $j:Ω→Ω$ in the topos $\Set^{(P,A)}$. The Elephant uses local
operators instead of J-operators practically everywhere; our $(13∨)$
corresponds to a ``closed local operator'' $c(\pile(13))$ in it ---
see [EA p.206].
Each set of question marks $Q⊆P$ induces an operation that erases the
information on objects associated to the points of $Q$ and an
operation that ``reconstructs'' this information on those objects in a
``natural'' way. Figure~\ref{fig:zgm-particular-case} shows a case of
this erasing and reconstruction, with $Q=\{1,6\}$.
It is possible to show that in Figure~\ref{fig:zgm-particular-case}
and in all similar cases the image of $f_*$ is a sheaf and $η$ is a
sheafification functor. By ``all similar cases'' we mean: the points
of $\catA$ are a subset of the points of $\catB$, and the partial
order on $\catA$ is the restriction to those points
of the partial order on $\catB$. We will need a notation for that. If
$\catB$ is drawn as the directed graph $(P,A)$ and $S⊆P$, then we draw
$\catB$ as $(S,A|_S)$, where $A|_S⊆S×S$ is a set of arrows on $S$ that
obeys $(A|_S)^* = (S×S)∩A^*$. We refer to that as a 𝐢{restriction of
$\catA$ to $S$}, or as a 𝐢{restriction of $\catA$ with question
marks $Q$}, where $Q=P∖S$.
% (find-LATEX "2017elephant.tex" "elephant-A4.4")
% (find-slnm0753page (+ 14 329) "2.18 Elementary J-operators")
% (find-slnm0753page (+ 14 330) "The forcing quotient")
% (find-slnm0753page (+ 14 331) "(i) J_a v J_b = J_avb")
% (vivp 26 "internal-views-gm-2")
% (viv "internal-views-gm-2")
% _____ _ _ _ _
% | ___|_ _ ___| |_ ___ _ __(_)______ _| |_(_) ___ _ __
% | |_ / _` |/ __| __/ _ \| '__| |_ / _` | __| |/ _ \| '_ \
% | _| (_| | (__| || (_) | | | |/ / (_| | |_| | (_) | | | |
% |_| \__,_|\___|\__\___/|_| |_/___\__,_|\__|_|\___/|_| |_|
%
% «two-factorizations-gms» (to ".two-factorizations-gms")
% (oxap 8 "two-factorizations-gms")
% (oxa "two-factorizations-gms")
\section{Two factorizations of geometric morphisms}
\label{two-factorizations-gms}
The Elephant presents in its sections A4.2 and A4.5 two factorizations
of geometric morphisms that can be combined in a single diagram ---
see Figure~\ref{fig:factorization-1}. An arbitrary geometry morphism
$g:\calA→\calD$ can be factored in an essentially unique way as a
surjection followed by an inclusion ([EA4.2.10]), and an inclusion
$i:\calB→\calD$ can be factored in an essentially unique way as a
dense g.m.\ followed by a closed g.m.\ ([EA4.5.20]). A canonical way
to build these factorizations is by taking $\calB := \calA_\bbG$,
where $\bbG$ is a certain comonad on $\calA$ ([EA4.2.8]), and taking
$\calC := \sh_j(\calD)$, where $j$ is a certain local operator on
$\calD$.
% (elep 10 "elephant-fact-p.182")
% (ele "elephant-fact-p.182")
% (elep 10 "elephant-A4.2.10" "surjection followed by an inclusion")
% (ele "elephant-A4.2.10" "surjection followed by an inclusion")
% (find-elephantpage (+ 17 183) "Theorem 4.2.10")
% (elep 16 "elephant-A4.5.20" "factorization" "dense" "closed")
% (ele "elephant-A4.5.20" "factorization" "dense" "closed")
% (vgmp 15 "a-factorization")
% (vgm "a-factorization")
% «fig:factorizations» (to ".fig:factorizations")
% (oxap 9 "fig:factorizations")
% (oxa "fig:factorizations")
%
%D diagram factorization-1
%D 2Dx 100 +50 +40 +40
%D 2D 100 A0 A3
%D 2D
%D 2D +12 B0 B1 B3
%D 2D
%D 2D +12 C1 C2 C3
%D 2D
%D 2D +12 D1 D2
%D 2D
%D ren A0 A3 ==> \calA \calD
%D ren B0 B1 B3 ==> \calA \calB \calD
%D ren C1 C2 C3 ==> \calB \calC \calD
%D ren D1 D2 ==> \calA_\bbG \sh_j(\calD)
%D
%D (( A0 A3 -> .plabel= a \vtext{g}{\anygm}
%D B0 B1 -> .plabel= a \vtext{s}{surjection}
%D B1 B3 -> .plabel= a \vtext{i}{inclusion}
%D C1 C2 -> .plabel= a \vtext{d}{dense}
%D C2 C3 -> .plabel= a \vtext{c}{closed}
%D D1 place
%D D2 place
%D ))
%D enddiagram
%D
%D diagram factorization-2
%D 2Dx 100 +55 +45 +45
%D 2D 100 A0 A3
%D 2D
%D 2D +12 B0 B1 B3
%D 2D
%D 2D +12 C1 C2 C3
%D 2D
%D 2D +12 D1 D2
%D 2D
%D 2D +20 a0 a3
%D 2D
%D 2D +12 b0 b1 b3
%D 2D
%D 2D +12 c1 c2 c3
%D 2D
%D ren A0 A3 ==> \Set^\catA \Set^\catD
%D ren B0 B1 B3 ==> \Set^\catA \Set^\catB \Set^\catD
%D ren C1 C2 C3 ==> \Set^\catB \Set^\catC \Set^\catD
%D ren D1 D2 ==> (\Set^\catA)_\bbG \sh_j(\Set^\catD)
%D
%D ren a0 a3 ==> \catA \catD
%D ren b0 b1 b3 ==> \catA \catB \catD
%D ren c1 c2 c3 ==> \catB \catC \catD
%D
%D (( A0 A3 -> .plabel= a \vtext{g}{\anygm}
%D B0 B1 -> .plabel= a \vtext{s}{surjection}
%D B1 B3 -> .plabel= a \vtext{i}{inclusion}
%D C1 C2 -> .plabel= a \vtext{d}{dense}
%D C2 C3 -> .plabel= a \vtext{c}{closed}
%D D1 place
%D D2 place
%D a0 a3 -> .plabel= a g
%D b0 b1 -> .plabel= a s
%D b1 b3 -> .plabel= a i
%D c1 c2 -> .plabel= a d
%D c2 c3 -> .plabel= a c
%D ))
%D enddiagram
%D
%D diagram fact-characterization
%D 2Dx 100 +20 +30 +20 +45 +20 +30 +20 +35 +20 +30 +20 +20 +20 +30 +20
%D 2D 100 A0 A1 A2 A3 B0 B1 B2 B3
%D 2D
%D 2D +20 A4 A5 A6 A7 B4 B5 B6 B7
%D 2D
%D 2D +20 A8 A9 B8 B9
%D 2D
%D 2D +20 a8 a9 b8 b9
%D 2D
%D 2D +20 C0 C1 C2 C3 D0 D1 D2 D3
%D 2D
%D 2D +20 C4 C5 C6 C7 D4 D5 D6 D7
%D 2D
%D 2D +20 C8 C9 D8 D9
%D 2D
%D 2D +20 c8 c9 d8 d9
%D 2D
%D ren A4 A5 A6 A0 ==> A A s_*A s^*s_*A
%D ren A3 A2 A1 A7 ==> B B s^*B s_*s^*B
%D ren A8 A9 a8 a9 ==> \Set^\catA \Set^\catB \catA \catB
%D
%D ren B4 B5 B6 B0 ==> B B i_*B i^*i_*B
%D ren B3 B2 B1 B7 ==> D D i^*D i_*i^*D
%D ren B8 B9 b8 b9 ==> \Set^\catB \Set^\catD \catB \catD
%D
%D ren C4 C5 C6 C0 ==> B B d_*B d^*d_*B
%D ren C3 C2 C1 C7 ==> kC C d^*C d_*d^*kC
%D ren C8 C9 c8 c9 ==> \Set^\catB \Set^\catC \catB \catC
%D
%D ren D4 D5 D6 D0 ==> C C c_*C c^*c_*C
%D ren D3 D2 D1 D7 ==> D D c^*D c_*c^*D
%D ren D8 D9 d8 d9 ==> \Set^\catC \Set^\catD \catC \catD
%D
%D (( A0 A4 -> .plabel= l {}
%D A3 A7 -> .plabel= r \text{(monic)}
%D A1 A2 <-| A1 A5 -> A2 A6 -> A5 A6 |->
%D A1 A6 harrownodes nil 20 nil <->
%D A8 A9 <- sl^ .plabel= a s^*
%D A8 A9 -> sl_ .plabel= b s_*
%D a8 a9 -> .plabel= a s
%D ))
%D
%D (( B0 B4 -> .plabel= l \text{(iso)}
%D B3 B7 -> .plabel= r {}
%D B1 B2 <-| B1 B5 -> B2 B6 -> B5 B6 |->
%D B1 B6 harrownodes nil 20 nil <->
%D B8 B9 <- sl^ .plabel= a i^*
%D B8 B9 -> sl_ .plabel= b i_*
%D b8 b9 -> .plabel= a i
%D ))
%D
%D (( C0 C4 -> .plabel= l {}
%D C3 C7 -> .plabel= r \sm{\text{(monic}\\\text{on\;c.p.s)}}
%D C1 C2 <-| C1 C5 -> C2 C6 -> C5 C6 |->
%D C1 C6 harrownodes nil 20 nil <->
%D C8 C9 <- sl^ .plabel= a d^*
%D C8 C9 -> sl_ .plabel= b d_*
%D c8 c9 -> .plabel= a d
%D ))
%D
%D (( D0 D4 -> .plabel= l {}
%D D3 D7 -> .plabel= r {}
%D D1 D2 <-| D1 D5 -> D2 D6 -> D5 D6 |->
%D D1 D6 harrownodes nil 20 nil <->
%D D8 D9 <- sl^ .plabel= a c^*
%D D8 D9 -> sl_ .plabel= b c_*
%D d8 d9 -> .plabel= a c
%D ))
%D
%D enddiagram
%D
\pu
\begin{figure}[!htbp]
\centering
$
\def\vtext#1#2{#1\text{ (#2)}}
\def\anygm{any g.m.}
\diag{factorization-1}
$
\caption{Two factorizations of geometric morphisms.}
\label{fig:factorization-1}
\bsk
\bsk
\bsk
$
\def\vtext#1#2{#1\text{ (#2)}}
\def\anygm{any g.m.}
\diag{factorization-2}
$
\caption{The same factorizations, but on ZGMs.}
\label{fig:factorization-2}
\bsk
\bsk
\bsk
\resizebox{0.8\textwidth}{!}{$%
\diag{fact-characterization}
$}
\caption{Conditions on the functors $\catA \ton{s} \catB \ton{i}
\catD$ and $\catB \ton{d} \catC$.}
\label{fig:factorization-3}
\end{figure}
These factorizations are almost completely opaque to people who know
just the basics of toposes. How can we produce a version ``for
children'' of them in the sense of the introduction?
The trick is to start with geometric morphisms whose internal views
can be drawn explicity --- the ZGMs of section
\ref{internal-diagrams}. Actually we start with the lower level of
Figure 2, and with the 𝐢{belief} that all factorizations can be
performed within ZGMs.
% _____ _ _________ __ __
% | ___|_ _ ___| |_ ___ _ __ |__ / ___| \/ |___
% | |_ / _` |/ __| __/ _ \| '__| / / | _| |\/| / __|
% | _| (_| | (__| || (_) | | / /| |_| | | | \__ \
% |_| \__,_|\___|\__\___/|_| /____\____|_| |_|___/
%
% «two-factorizations-zgms» (to ".two-factorizations-zgms")
% (oxap 10 "two-factorizations-zgms")
% (oxa "two-factorizations-zgms")
\section{Two factorizations of ZGMs}
\label{two-factorizations-gms}
The Elephant defines surjections by a list of equivalent conditions,
and the same for inclusions and dense and closed geometric morphisms.
Some of these conditions --- the ones drawn in
Figure~\ref{fig:factorization-3} --- are very easy to test on ZGMs.
% (elep 8 "elephant-A4.2.6" "surjection")
% (elep 9 "elephant-A4.2.6" "surjection" "(iv)")
% (ele "elephant-A4.2.6" "surjection")
% [EA] 4.2.6 (iv)
%
1. $\Set^\catA \ton{s} \Set^\catB$ is a 𝐢{surjection} when for every
object $B∈\Set^\catB$ the unit map $ηB$ is monic ([EA4.2.6 (iv)]);
% (elep 9 "elephant-A4.2.9" "inclusion")
% (ele "elephant-A4.2.9" "inclusion")
% [EA], 4.2.8-4.2.9
%
2. $\Set^\catB \ton{i} \Set^\catD$ is an 𝐢{inclusion} when for every
object $B∈\Set^\catB$ the counit map $εB$ is an iso ([EA4.2.8]);
% (elep 5 "dense-closed")
% (ele "dense-closed")
% (elep 16 "elephant-A4.5.20" "factorization" "dense" "closed")
% (ele "elephant-A4.5.20" "factorization" "dense" "closed")
%
3. $\Set^\catB \ton{d} \Set^\catC$ is an 𝐢{dense} when for every
constant presheaf $kC$ the unit map $εkC$ is a monic 𝐢{[I can't find a
reference for this now]}.
\msk
We also have two conditions for ``dense'' and ``close'' that are easy
to state on ``restrictions'' in the sense of section
\ref{restrictions} --- but it's not trivial to derive them from the
material in the Elephant. Let's state them anyway:
4. A restriction $\Set^\catB \ton{d} \Set^\catC$ is 𝐢{dense} when all
its question marks ``have non-question marks ahead of them'', i.e.:
for every $α$ in $\catC$ such that $α∈Q$ there is an arrow $α→β$ in
$\catC$ with $β \not∈ Q$;
5. A restriction $\Set^\catC \ton{d} \Set^\catD$ is 𝐢{closed} when all
its question marks ``are at the end'', i.e.: there are no arrows $α→β$
in $\catD$ with $α∈Q$ and $β \not∈ Q$.
\msk
We will say that a ZFunctor $\catA \ton{s} \catB$ 𝐢{induces a
surjection} when the ZGM $\Set^\catA \ton{s} \Set^\catB$ induced by
it is a surjection; and the same for inclusion, dense, and closed.
How can we factor a ZFunctor $\catA \ton{g} \catD$ into ZFunctors
$\catA \ton{s} \catB \ton{i} \catD$ that induce a surjection and an
inclusion, and how do we factor this $\catB \ton{i} \catD$ into $\catB
\ton{d} \catC \ton{c} \catD$? Here is a way to get a good part of a
possible answer.
We can think that a ZFunctor $f:\catX→\catY$ does several 𝐢{actions}.
If we think that $\catX$ is ``before'' and $\catY$ is ``after'', then
$f$ can, for example: create isolated objects, collapse isolated
objects, collapse two ordered objects, create an arrow, create objects
at the beginning of a connected set, create objects at the middle of a
connected set, create objects at the end of a connected set... here
are some examples that only do one of these actions each:
%
$$\def\-{\hbox{$→$}}
\def\.{\phantom{\hbox{$→$}}}
\begin{array}{rcl}
% surjective actions:
%
(1 \- 1') &→& (1) \\
(1 \. 1') &→& (1) \\
(1 \. 2) &→& (1 \- 2) \\
%
% dense actions:
(2) &→& (1 \- 2) \\
(1 \- 3) &→& (1 \- 2 \- 3) \\
%
% closed actions:
(1) &→& (1 \. 2) \\
(1) &→& (1 \- 2) \\
\end{array}
$$
When we take $\catA \ton{g} \catD$ as each one of the seven ZFunctors
and we try to factor that $g$ as $\catA \ton{s} \catB \ton{d} \catC
\ton{c} \catD$ we see that the first three functors factor as $(s=g,
d=\id, c=\id)$, the next two as $(s=\id, d=g, c=\id)$, and the last
two as $(s=\id, d=\id, c=g)$. The leads to a:
% (find-es "tex" "newtheorem")
\begin{conjecture}
Take a ZFunctor $\catA \ton{g} \catD$. Factor it into $\catA \ton{s}
\catB \ton{d} \catC \ton{c} \catD$ in the following way: $s$ collapses
objects and creates arrows; $c$ creates objects at the middle and at
the beginnings of connected sets; $d$ creates objects at the ends of
connected sets. Then this factorization of ZFunctors induces a
surjective-dense-closed factorization of ZGMs.
\end{conjecture}
% \bsk
% \bsk
%
% When we factor the seven ZFunctors above we see that they induce either surjections
%
%
% An identity ZFunctor does none of these actions, and it's easy to
% construct a ZFunctor that does several or all of them. It is
% reasonable to guess, by the names ``surjection'' and ``inclusion'',
% that that if $\catA \ton{g} \catD$ is $(1\;\;1') \ton{g} (1\;\;2)$,
% that takes both 1 and $1'$ to the same object, then it factors as
% $(1\;\;1') \ton{s} (1) \ton{i} (1\;\;2)$. It is easy to 𝐢{test}
% guesses like this; we find, for example, that only surjections can
% create arrows, that our first two guesses are both right, that only
% closed ZGMs can create objects at the end of connected sets, and that
% only dense ZGMs can create objects at the beginning and at the middle
% of connected sets.
%
% {\bf Conjecture:} take any ZFunctor $\catA \ton{g} \catD$ and factor
% it into $\catA \ton{s} \catB \ton{d} \catC \ton{c} \catD$ in the
% following way: the step $s$ only collapses objects and creates arrows;
% the step
% _____ _ _
% | ____|_ __ (_) | ___ __ _ _ _ ___
% | _| | '_ \| | |/ _ \ / _` | | | |/ _ \
% | |___| |_) | | | (_) | (_| | |_| | __/
% |_____| .__/|_|_|\___/ \__, |\__,_|\___|
% |_| |___/
%
\section{Epilogue: timber}
Sections 1, 10, 11, 12, and 16 of \cite{OchsIDARCT} discuss how to
reconstruct theorems from incomplete versions that take very little
mental space, or very little space on paper; we do something similar
here.
% https://twitter.com/_theek_/status/1117895531563372544
One idea that was widely circulated after the fire in the Notre Dame
cathedral was that it would be impossible to reconstruct its roof,
because that would require an entire forest full of old oak trees, and
that thing doesn't exist anymore... but I saw a thread on
Tweeter\footnote{https://twitter.com/\_theek\_/status/1117895531563372544}
that contained these tweets: ``The steeple and the beams supporting it
are 160 years old, and oaks for new beams awaits at Versailles, the
grown replacements for oaks cut to rebuild after the revolution.''
``Do you have a source on that protocol? Would love to hear more -
feel free to DM.'' ``It was a lecture I attended at Versailles on
disaster recovery and long term planning. Once per century events have
to be planned for in a city where structures are a thousand years
old.'' ``It was a lecture from a decade ago. I'm sorry that I don't
have more details but there must be better sources than me out there.
It's similar to the oaks at Oxford grown to replace the ones that rot
out every 500 years, on schedule.''
Sometimes we have to deal with a Topos Theory whose timber is made
from Algebric Geometry oaks. Sometimes, for one reason or another, we
want to be prepared to replace them by oaks from Computer Science, or
with oaks coming from finite examples. The structure of the cathedral
modulo these timbers can be described in several forms; some more
algebraic, some more diagramatic, like the idea of ``shape'' in our
Figures~\ref{fig:gm-and-zgm} and~\ref{fig:factorization-3} and in
\cite{OchsYoneda}.
% (ph2p 29 "polynomial-J-ops" "closed quotient")
% (ph2 "polynomial-J-ops" "closed quotient")
% (ph2p 31 "polynomial-J-ops" "Using this new notation")
% (ph2 "polynomial-J-ops" "Using this new notation")
%
% $f$ is {\sl closed} when all the `?'s are below `!'
% ____ __
% | _ \ ___ / _| ___ _ __ ___ _ __ ___ ___ ___
% | |_) / _ \ |_ / _ \ '__/ _ \ '_ \ / __/ _ \/ __|
% | _ < __/ _| __/ | | __/ | | | (_| __/\__ \
% |_| \_\___|_| \___|_| \___|_| |_|\___\___||___/
%
% «references» (to ".references")
% (find-LATEX "catsem-u.bib" "bib-Johnstone")
% (find-es "tex" "compositionality")
% (find-es "tex" "compositionality" "thebibliography")
% (find-comptfile "compositionality-template.tex" "\\begin{thebibliography}")
\bibliographystyle{plain}
\begin{thebibliography}{9}
% % (find-LATEX "catsem-u.bib" "bib-Goldblatt")
% \bibitem{Goldblatt}
% R.~Goldblatt,
% \href{https://doi.org/10.22331/ idonotexist}{Topoi: The Categorial
% Analysis of Logic, North Holland, 1984.}
% (find-LATEX "catsem-u.bib" "bib-Johnstone")
\bibitem{Johnstone}
Peter T.~Johnstone,
\href{https://doi.org/10.22331/ idonotexist}{Topos Theory, Academic
Press, 1977.}
% (find-LATEX "catsem-u.bib" "bib-Johnstone" "Elephant1")
\bibitem{Elephant1}
Peter T.~Johnstone,
\href{https://doi.org/10.22331/ idonotexist}{Sketches of an
Elephant: A Topos Theory Compendium, vol.~1, Oxford University
Press, 2002}.
% (find-LATEX "catsem.bib" "bib-Fourman")
\bibitem{Fourman}
M.P.~Fourman and D.S.~Scott,
\href{https://doi.org/10.22331/ idonotexist}{Sheaves and Logic,
pages 302--401 in: M.P. Fourman and D.J. Mulvey and D.S. Scott,
eds.: Applications of Sheaves: Proceedings of the Research
Symposium on Applications of Sheaf Theory to Logic, Algebra and
Analysis - Durham, july 9-21, 1977 (1979) (SLNM0753)}.
% (find-LATEX "catsem-u.bib" "bib-LawvereRosebrugh")
\bibitem{LawvereRosebrugh}
W.~Lawvere and R.~Rosebrugh,
\href{https://doi.org/10.22331/ idonotexist}{Sets for Mathematics,
Cambridge, 2003}.
\bibitem{OchsLucatelli}
F.~Lucatelli and E.~Ochs,
\href{http://angg.twu.net/logic-for-children-2018.html}{Logic for
Children - Workshop at UniLog 2018 (Vichy) - unofficial homepage.}
% % (find-LATEX "catsem-u.bib" "bib-Mancosu")
% \bibitem{Mancosu}
% Paolo Mancosu,
% \href{https://doi.org/10.1093/acprof:oso/9780199296453.001.0001}{The
% Philosophy of Mathematical Practice, Oxford, 2008.}
% (find-LATEX "catsem-u.bib" "bib-Ochs")
\bibitem{OchsIDARCT}
E.~Ochs,
\href{https://doi.org/10.1007/s11787-013-0083-z}{Internal Diagrams
and Archetypal Reasoning in Category Theory, Logica Universalis,
vol.~7, no.~3, september 2013, pp.~291--321.}
% (find-TH "math-b" "zhas-for-children-2")
\bibitem{PH1}
E.~Ochs,
\href{http://angg.twu.net/math-b.html\#zhas-for-children-2}{Planar
Heyting Algebras for Children (2017).}
\bibitem{PH2}
E.~Ochs,
\href{http://angg.twu.net/math-b.html\#zhas-for-children-2}{Planar
Heyting Algebras for Children 2: Closure Operators (2018).}
\bibitem{OchsYoneda}
E.~Ochs,
\href{http://angg.twu.net/LATEX/2019notes-yoneda.pdf}{Notes on the
Yoneda Lemma (2018).}
% % (find-LATEX "catsem-u.bib" "bib-Ochs")
% \bibitem{Riehl}
% Emily Riehl,
% \href{http://www.math.jhu.edu/~eriehl/context/}{Category Theory in
% Context, Dover (2016).}
% \bibitem{examplecitation}
% Name Surname,
% \href{https://doi.org/10.22331/
% idonotexist}{Compositionality
% \textbf{123}, 123456 (1916).}
%
% \bibitem{biblatexsubmittingtothearxiv}
% StackExchange discussion on
% \href{http://tex.stackexchange.com/questions/26990/biblatex-submitting-to-the-arxiv}{``Biblatex:
% submitting to the arXiv'' (2017-01-10)}
%
% \bibitem{arxivpdfoutput}
% Help article published by the arXiv on
% \href{https://arxiv.org/help/submit_tex}{``Considerations for TeX
% Submissions'' (2017-01-10)}
%
% \bibitem{howtogetdoilinksinbibliography}
% StackExchange discussion on
% \href{http://tex.stackexchange.com/questions/3802/how-to-get-doi-links-in-bibliography}{``How
% to get DOI links in bibliography'' (2016-11-18)}
%
% \bibitem{automaticallyaddingdoifieldstoahandmadebibliography}
% StackExchange discussion on
% \href{http://tex.stackexchange.com/questions/6810/automatically-adding-doi-fields-to-a-hand-made-bibliography}{``Automatically
% adding DOI fields to a hand-made bibliography'' (2016-11-18)}
\end{thebibliography}
%L -- write_dnt_file()
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "oxa"
% End: