|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019elephant-poster-z.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019elephant-poster-z.tex" :end))
% (defun b () (interactive) (find-sh "biber 2019elephant-poster-z.tex"))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019elephant-poster-z.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019elephant-poster-z.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019elephant-poster-z; makeindex 2019elephant-poster-z"))
% (defun e () (interactive) (find-LATEX "2019elephant-poster-z.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019elephant-poster-z"))
% (defun g () (interactive) (ee-pdftools-revert-all))
% (setq revert-without-query '("pdf$"))
% (find-xpdfpage "~/LATEX/2019elephant-poster-z.pdf")
% (find-sh0 "cp -v ~/LATEX/2019elephant-poster-z.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019elephant-poster-z.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019elephant-poster-z.pdf
% file:///tmp/2019elephant-poster-z.pdf
% file:///tmp/pen/2019elephant-poster-z.pdf
% http://angg.twu.net/LATEX/2019elephant-poster-z.pdf
% «.is-associated-to» (to "is-associated-to")
% «.parallel-diagrams» (to "parallel-diagrams")
% «.projections-and-liftings» (to "projections-and-liftings")
% «.drawing-topologies» (to "drawing-topologies")
% «.2CGs» (to "2CGs")
% «.ZHAs» (to "ZHAs")
% «.logic-in-a-ZHA» (to "logic-in-a-ZHA")
% «.J-operators» (to "J-operators")
% «.question-marks» (to "question-marks")
% «.toposes-for-children» (to "toposes-for-children")
% «.classifier» (to "classifier")
% «.local-operators» (to "local-operators")
% «.the-factorization» (to "the-factorization")
% «.references» (to "references")
%
% «.write-poster-body» (to "write-poster-body")
\documentclass[oneside,12pt]{extarticle}
%\usepackage[colorlinks,urlcolor=violet]{hyperref} % (find-es "tex" "hyperref")
\usepackage[colorlinks,citecolor=violet,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage[varg]{txfonts}
\usepackage{pict2e}
%\usepackage{indentfirst}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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 edrx17defs.tex % (find-LATEX "edrx17defs.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")
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% (find-es "tex" "newlength")
\newlength{\colwidth}
\setlength{\colwidth}{\textwidth}
% FROM HERE
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}
\def\catX{{\mathbf{X}}}
\def\catY{{\mathbf{Y}}}
\def\resizediag#1#2#3{\resizebox{#1}{#2}{$\diag{#3}$}}
\def\eqQ{\sim_Q}
% (find-2a nil '(d))
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
%L deletecomments = function (str)
%L return (str:gsub("%%[^\n]*\n[ \t]*", ""))
%L end
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\co#1{{%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
% (find-LATEX "2017planar-has-defs.tex" "squigbijtest")
% (find-LATEX "2017planar-has-defs.tex" "squigbijtest" "values")
\def\squigbijy{-2.5} % for 12pt
% Title
% (find-LATEXfile "2019elephant-poster.tex" "\\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
The abstract of the extended abstract that I submitted to the
conference was just this:
% (find-es "tex" "abstract")
\begin{quotation}
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{quotation}
Its focus was the factorization in the last paragraph --- let me call
it simply ``the factorization'' from here on; it is explained in the
section \ref{the-factorization} of the poster.
In this poster I will try to do something different: I will try to
give a broad view of the whole project, and show that the
factorization is just a cherry on top of the sundae --- a cherry that
is there to please the mathematicians who believe that constructions
and techniques only relevant when they {\sl prove new theorems}.
% The ``whole project''' --- we need a short name for it... the
% ``sundae''?
The references in boldface in this poster are to papers, slides and
notes that can accessed from the section titled ``On some missing
diagrams in the Elephant'' in my webpage:
%
$$\begin{tabular}{l}
\url{http://angg.twu.net/math-b.html} \\
\url{http://angg.twu.net/math-b.html\#missing-diagrams-elephant} \\
\end{tabular}
$$
% (find-es "tex" "biber")
% (find-books "__cats/__cats.el" "mclarty-risingsea")
They are:
%
$$\begin{tabular}{ll}
\cite{IDARCT}: & {\bf Internal Diagrams and Archetypal Reasoning} \\
& {\bf in Category Theory} \\
& (Logica Universalis, 2013) \\
\cite{PH1}: & {\bf Planar Heyting Algebras for Children} \\
& (Accepted @ South Americal Journal of Logic) \\
\cite{MDE} & {\bf On Some Missing Diagrams in the Elephant} \\
& (My extended abstract to the ACT2019 --- it's not \\
& in the conference website because poster session people \\
& are second-class people, duh) \\
\cite{NYo}: & {\bf Notes on the Yoneda Lemma} \\
& (In which each node and arrow can be \\
& interpreted precisely as a ``term'', \\
& and most of the interpretations are \\
&``obvious''; plus dictionaries!!!) \\
& (slides, 2019) \\
\end{tabular}
$$
% «is-associated-to» (to ".is-associated-to")
\section{``Is associated to''}
The symbol `$\squigbijbody$' will be pronounced ``is associated to'',
but the {\sl formal} meaning of `$A \squigbij B$' will depend on the
types of $A$ and $B$. For example,
%
$$(P,A) \squigbij H$$
%
will mean that the 2-column graph $(P,A)$ is associated to the Planar
Heyting Algebra (a ``ZHA'') $H$ through the standard bijection between
2CGs and ZHAs;
%
$$((P,A),Q) \squigbij (H,J)$$
%
will mean that besides $(P,A) \squigbij J$ the equivalence relation
induced by set of question marks $Q$ is ``the same'' as the one
induced by J-operator $J$; and
%
$$J \squigbij j$$
%
means that in the topos that we are talking about the J-operator $J$
(J-operators are a concept that fell out of fashion) is associated to
the local operator $j:Ω→Ω$ --- something is everyone (?!?) knows that
induces a notion of ``sheaf'' on the topos we're in.
% \section{Outsiders}
% This is ``Category Theory for outsiders'' in several senses... I teach
% in a small countryside campus of a Federal
% (ph1p 2 "introduction")
% (ph1 "introduction")
% (ph1p 2 "introduction" "everything felt far too abstract")
% (ph1 "introduction" "everything felt far too abstract")
% ____ _ _ _ _ _
% | _ \ __ _ _ __ __ _| | | ___| | __| (_) __ _ __ _ ___
% | |_) / _` | '__/ _` | | |/ _ \ | / _` | |/ _` |/ _` / __|
% | __/ (_| | | | (_| | | | __/ | | (_| | | (_| | (_| \__ \
% |_| \__,_|_| \__,_|_|_|\___|_| \__,_|_|\__,_|\__, |___/
% |___/
%
% «parallel-diagrams» (to ".parallel-diagrams")
\section{Parallel diagrams (of several kinds)}
\label{parallel-diagrams}
% (ph1p 4 "internal-external")
% (ph1 "internal-external")
Look at the diagram below. Let's call its three subdiagrams $\sm{A \;
B \\ C}$. Each of the subdiagrams $A$, $B$, $C$ have an ``external
diagram'', or an ``external view'', below, and an ``internal diagram''
or ``internal view'' above.
\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 generic-adjunction
%D 2Dx 100 +30 +35 +25
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +30 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +30 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +30 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> LA' A'
%D ren LB B ==> LA A
%D ren C RC ==> B RB
%D ren D RD ==> B' RB'
%D ren E F ==> \catB \catA
%D ren G H ==> LRB B
%D ren I J ==> A RLA
%D
%D (( LA A <-| .plabel= a L_0
%D LB B <-| .plabel= a L_0
%D C RC |-> .plabel= b R_0
%D D RD |-> .plabel= b R_0
%D
%D LA B harrownodes nil 20 nil <-| sl^ .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> sl^ .plabel= b R_1
%D
%D LA LB -> .plabel= l Lα
%D A B -> .plabel= r α
%D LB C -> .plabel= l \sm{g^♭\\f}
%D B RC -> .plabel= r \sm{g\\f^♯}
%D C D -> .plabel= l β
%D RC RD -> .plabel= r Rβ
%D E F <- sl^ .plabel= a L
%D E F -> sl_ .plabel= b R
%D G H -> .plabel= l εB
%D I J -> .plabel= r ηA
%D ))
%D enddiagram
%D
%D diagram (xB)-|(B->)
%D 2Dx 100 +45 +35 +40
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +30 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +30 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +30 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> A{×}C A
%D ren LB B ==> B{×}C B
%D ren C RC ==> D (C{→}D)
%D ren D RD ==> E (C{→}E)
%D ren E F ==> \Set \Set
%D ren G H ==> (C{→}D){×C} D
%D ren I J ==> B (C→B{×}C)
%D ren I J ==> B (C{→}(B{×}C))
%D
%D (( LA A <-| # .plabel= a ({×}B)_0
%D LB B <-| # .plabel= a ({×}B)_0
%D C RC |-> # .plabel= b (B{→})_0
%D D RD |-> # .plabel= b (B{→})_0
%D
%D LA B harrownodes nil 20 nil <-| sl^ # .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> sl^ # .plabel= b R_1
%D
%D LA LB -> .plabel= l λp.(f(πp),π'p)
%D A B -> .plabel= r f
%D LB C -> .plabel= l \sm{λp.g(πp)(π'p)\\\phantom{mmmmmm}h}
%D B RC -> .plabel= r \sm{g\phantom{mmmmm}\\λb.λc.h(b,c)}
%D C D -> .plabel= l k
%D RC RD -> .plabel= r λf.λc.k(fc)
%D E F <- sl^ .plabel= a ({×}C)
%D E F -> sl_ .plabel= b (C{→})
%D G H -> .plabel= l λp.(πp)(π'p)
%D I J -> .plabel= r λb.λc.(b,c)
%D ))
%D enddiagram
%D
\pu
$$\begin{array}{c}
\resizediag{!}{!}{second-blob-function}
\qquad
\resizediag{!}{!}{generic-adjunction}
\\
\\
\resizediag{!}{!}{(xB)-|(B->)}
\end{array}
$$
\def\sqrtph{\sqrt{\phantom{a}}}
Our notions of ``external'' and ``internal'' are the same as in
\cite{LawvereSchanuel} or \cite{LawvereRosebrugh}, but our use of
arrows is much more precise. Note that in diagram $A$
\begin{itemize}
\item we distinguish `$→$' and `$↦$' in the usual way --- $\N
\ton{\sqrtph} \R$ is a {\sl typing},
\item one of the `$↦$' arrows above $\N \ton{\sqrtph} \R$ is
``generic'': $n ↦ \sqrt{n}$ shows how to produce the image of a
generic element $n∈\N$ --- i.e., as an untyped $λ$-calculus term,
$\sqrtph = λn.\sqrt{n}$,
\def\U#1{\underline{#1}}
\item \U{all the other} `$↦$' arrows \U{above} $\N \ton{\sqrtph} \R$
are \U{substituition instances} of $n ↦ \sqrt{n}$, \U{maybe after
some term reductions}.
``$3 ↦ \sqrt{3}$'' is just a substituion instance of ``$n ↦
\sqrt{n}$'', but ``$4 ↦ 2$'' is a substitution instance of ``$n ↦
\sqrt{n}$'' followed by the reduction that transforms ``$√4$'' into
``2''.
\end{itemize}
The notion of ``above'' in these diagrams is very important. The blob
above $\N$ shows some elements of $\N$; same for $\R$, and the `$↦$'
arrows above the `$→$' are internal views of the `$→$'.
The subfigure $B$ shows the external view and the internal view of a
(generic) adjunction. Things are much more complex now --- we don't
draw the blobs; above $\catB$ we have six objects and four morphisms
from the category $\catB$, and the same for $\catA$; the arrows marked
`$L_0$' above $L$ are the action of $L$ on objects and the arrow
`$L_1$' is the action of $L$ on morphisms, and the same for $R$; we
draw the transpositions $♭$ and $♯$; we draw the unit and the counit.
The subfigure $C$ is a particular case of the subfigure $B$ --- among
other things it has exactly the same shape as $B$, and we can extract
from it the definitions of $L_0$, $L_1$, etc in this particular case.
The ``general case'' $B$ and the ``particular case'' $C$ are evidently
parallel diagrams, but in each of $A$, $B$, $C$ we have a internal
diagram parallel to an external diagram --- but the internal diagrams
are much bigger.
\msk
Note: these diagrams can be interpreted in proof assistants! See
\cite{NYo} for a reasonably big example worked out in all detail!
(A curiosity: many years ago I spent a lot of time studying
\cite{Jacobs} and trying to create a bridge between his
fibration-based categorical models for type theory and what I thought
that were the ``archetypal cases'' motivating them. Some of my
conventions for ``above'', ``below'', etc, comes from conventions for
fibrations.)
% \msk
% \msk
% \msk
%
%
%
% The second way to explain the goals of PH123 is by taking {\sl
% Diagrammatic Reasoning} as the main theme. Let me start with an
% anecdote (90\% true). Many, many years ago, when I tried to learn
% Topos Theory for the first time, mainly from \cite{Johnstone} and
% \cite{Goldblatt}, everything felt far too abstract: most of the
% diagrams were omitted, and the motivating examples were mentioned very
% briefly, if at all. The intended audience for those books surely knew
% how to supply by themselves the missing diagrams, examples,
% calculations, and details --- but I didn't. My slogan became: ``I need
% a version for children of this!''.
%
% At first this expression, ``for children'', was informal, and I used
% it as a half-joke. Very gradually it started to acquire a precise
% sense: clearly, CT done in a purely algebraic way is ``for adults'',
% and diagrams, particular cases, and finite examples are ``for
% children''. Writing ``for adults'' only and keeping the mentions to
% the ``for children'' part very brief is considered good style because
% ``adults'' have the technical machinery for producing more or less
% automatically the ``for children'' part when they need it, and people
% who are not yet ``adults'' can become ``adults'' by struggling with
% the texts ``for adults'' long enough and learning by themselves how to
% handle the new level of abstraction.
%
% A clear frontier between ``for adults'' and ``for children'' appears
% when we realize that we can draw a diagram for the general case (``for
% adults'') of a categorical concept and the diagram for a particular
% case of it (``for children'') side by side. The two diagrams will have
% roughly the same shape, and we can transport knowledge between them in
% both ways: from the general to the particular, {\sl and back}. Look at
% Figure \ref{fig:internal-external}; let's name its subdiagrams as $A$,
% $B$, and $C$, like this: $\sm{A \; B \\ C}$. Each one of $A$, $B$, $C$
% has an {\sl internal view} above and an {\sl external view} below.
% ____ _ _ _ _ __ _
% | _ \ _ __ ___ (_)___ __ _ _ __ __| | | (_)/ _| |_ ___
% | |_) | '__/ _ \| / __| / _` | '_ \ / _` | | | | |_| __/ __|
% | __/| | | (_) | \__ \ | (_| | | | | (_| | | | | _| |_\__ \
% |_| |_| \___// |___/ \__,_|_| |_|\__,_| |_|_|_| \__|___/
% |__/
%
% «projections-and-liftings» (to ".projections-and-liftings")
% (find-angg ".emacs" "idarct-preprint")
% (idap 1 "projs-and-lifts")
% (ida "projs-and-lifts")
\section{Projections and liftings}
One of the first ideas presented in \cite{IDARCT} is that we can treat
operations that discard information, like {\sl particularization}, as
{\sl projections}, and we can treat {\sl generalization} as {\sl
lifting}... and the paper shows how to represent visually several
operations that {\sl erase} and that {\sl reconstruct} information.
Suppose that we learned adjunctions from \cite{CWM}. His presentation
is not very visual, so we worked a bit (or a lot) and found the
diagrams for adjunctions in sec.\ref{parallel-diagrams}; we are now in
a situation where we know the ``algebraic'' definition of an
adjunction plus a diagrammatic way to represent it. We work a bit more
and we get a diagram for a particular case -- the adjunction
$({×}B)⊣(B{→})$.
There are some advantages in knowing the ``algebraic version'', plus
having a diagram for the general case, that lets us play with some
sequences operations as if they were shape and movement, plus having
particular cases that let us test conjectures quickly... in recent
texts about the Philosophy of Mathematics, like \cite{Kromer},
\cite{Mancosu}, \cite{Corfield} we can even find {\sl names} for each
kind of reasoning, and each kind of intuition, that becomes accessible
to us after we get another view of, say, adjunctions...
The diagram below let us visualize these ``states of knowledge'':
%
%L forths["-"] = function () pusharrow("-") end
%
%D diagram ??
%D 2Dx 100 +40 +40 +40 +40
%D 2D 100 \EVT
%D 2D
%D 2D +40 \GAD \GPD
%D 2D
%D 2D +40 \GA \GD \PD
%D 2D
%D 2D +40 \SHAPE
%D 2D
%D
%D (( \EVT \GAD - \EVT \GPD -
%D \GAD \GA - \GAD \GD - \GPD \GD - \GPD \PD -
%D \GD \SHAPE - \PD \SHAPE -
%D ))
%D enddiagram
%D
%
% generic parallel
% case, diagrams
% alg+diag
%
% generic general particular
% case, case, case,
% algebraic diagram diagram
%
% shape
%
$$\pu
\def\ta#1{\begin{tabular}{c}#1\end{tabular}}
\def\EVT{\ta{(everything)}}
\def\GAD{\ta{generic \\ case, \\ alg $+$ diag }}
\def\GPD{\ta{generic and \\ particular \\ in parallel }}
\def\GA {\ta{generic \\ case, \\ algebraic }}
\def\GD {\ta{generic \\ case, \\ diagram }}
\def\PD {\ta{particular \\ case, \\ diagram}}
\def\SHAPE{\ta{(shape)}}
\diag{??}
$$
There are some processes that I discuss in \cite{IDARCT} that are only
mentioned very, very briefly in the three references above --- namely,
forgetting details and then reconstructing them, and ``omitting
diagrams'' for publication followed by ``reconstructing the diagrams
that the author had in mind'' as explained in the abstract in the
beginning of the poster.
Also, there is an idea in \cite{IDARCT} that I haven't seen anywhere
else and that became a long-term project for me, that is that we can
``project out'' all the terms in a categorical construction or proof
that mention equalities of morphisms --- I call this ``dropping the
boring part and keeping only the fun part'' of the categorical
constructions and arguments ---, then we do our constructions there,
and {\sl after we're finished with this part} we reconstruct the
``boring'' part in a way that matches the rest.
% ____ _ _
% | _ \ _ __ __ ___ _(_)_ __ __ _ | |_ ___ _ __ ___
% | | | | '__/ _` \ \ /\ / / | '_ \ / _` | | __/ _ \| '_ \/ __|
% | |_| | | | (_| |\ V V /| | | | | (_| | | || (_) | |_) \__ \
% |____/|_| \__,_| \_/\_/ |_|_| |_|\__, | \__\___/| .__/|___/
% |___/ |_|
%
% «drawing-topologies» (to ".drawing-topologies")
\section{Drawing topologies}
%L kite = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite", meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW", meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex", meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu
We can draw subsets of a set $\dagKite•••••$ by their characteristic
functions: $\dagKite10110$, $\dagKite00111$, and so on. The {\sl order
topology} on a set $\dagKite•••••$ is defined by:
%
$$\begin{tabular}{l}
a subset of $\dagKite•••••$ is {\sl open} \\
when its characteristic function \\
{\sl doesn't have} a `1' above a `0'. \\
\end{tabular}
$$
We can draw topologies as directed graphs. Let ``$A ⊂_1 B$'' stand
for: ``$A⊂B$, and the difference $B∖A$ has exactly one element''. We
will draw the topology $(X,\Opens(X))$ as the DAG $(\Opens(X), ⊂_1)$,
meaning that there will be an arrow $V→U$ when $V⊂_1U$. We have:
%
% (ph1p 25 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders")
%
%R local house, ohouse = 2/ #1 \, 7/ !h11111 \
%R |#2 #3| | !h01111 |
%R \#4 #5/ | !h01011 !h00111 |
%R |!h01010 !h00011 !h00101|
%R | !h00010 !h00001 |
%R \ !h00000 /
%R
%R house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({zdef="House" , scale="20pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({zdef="OHouse", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R
%R local guill, oguill = 2/ #1 #2\, 8/ !g111111 \
%R |#3 #4 | | !g101111 !g011111 |
%R \ #5 #6/ | !g001111 !g010111|
%R | !g001011 !g000111 |
%R |!g001010 !g000011 |
%R | !g000010 !g000001 |
%R \ !g000000 /
%R
%R guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R guill:tomp({zdef="Guill", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({zdef="OGuill", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R
%R local w, womit, W =
%R 2/#1 #2 #3\, 2/ a \, 7/ !w11111 \
%R \ #4 #5 / | b c d | | !w11011!w10111!w01111 |
%R | e f g | | !w10011!w01011!w00111 |
%R |h i j | |!w10010 !w00011 !w00101|
%R | k l | | !w00010 !w00001 |
%R \ m / \ !w00000 /
%R w:tomp({def="zfW#1#2#3#4#5", scale="3.5pt", meta="s"}):addcells():output()
%R w:tomp({zdef="W", scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({zdef="OW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
\pu
%
$$(\Opens(\dagHouse•••••), ⊂_1) = \def\h{\zfHouse}\zha{OHouse}$$
$$(\Opens(\dagGuill••••••), ⊂_1) = \def\g{\zfGuill}\zha{OGuill}$$
$$(\Opens(\dagW•••••), ⊂_1) = \def\w{\zfW}\zha{OW}$$
The DAGs $(\Opens(\dagHouse•••••), ⊂_1)$ and
$(\Opens(\dagGuill••••••), ⊂_1)$ are planar (neat!), and \\
$(\Opens(\dagW•••••), ⊂_1)$ is non-planar (clumsy!). The nonplanarity
comes from $\dagW•••••$ having three independent points; the subDAG
generated by the open sets of the form $\dagW???11$ is a cube.
% ____ ____ ____
% |___ \ / ___/ ___|___
% __) | | | | _/ __|
% / __/| |__| |_| \__ \
% |_____|\____\____|___/
%
% «2CGs» (to ".2CGs")
\subsection{2-Column Graphs (``2CGs'')}
One way to make sure that our topologies will be neat (i.e., planar)
is to forbid having three independent points, and one way to do this
is to declare that we are only interested in topologies in {\sl
2-columns graphs} (2CGs).
This is an example of a 2CG, and its topology:
%
% (oxap 7 "fig:2CGs-ZHA")
% (oxa "fig:2CGs-ZHA")
% (oxa "fig:2CGs-ZHA" "\\tcg{(P,A)}")
%
%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
%
$$\Opens\tcg{(P,A)} \quad = \quad \zha{O_A(P)}$$
%
but we are drawing the open sets using a two-digit notation...
% (oxap 6 "2CGs-and-ZHAs" "{specification} for a 2CG")
% (oxa "2CGs-and-ZHAs" "{specification} for a 2CG")
%
We write $\pile(ab)$ for the set $\{a▁,\dots,1▁, \;\; ▁1,\ldots,▁b\}$;
the characteristic function of $\pile(a,b)$ is a pile of $a$ `1's in
the left column and $b$ `1's in the right column.
We sometimes omit the `$\pile$'s; for example, the 25 above means
%
$$25 ≡ \pile(2,5) = \{2▁,1▁, \;\; ▁1,▁2,▁3,▁4,▁5\},$$
%
an open set. Note the $\pile(2,1)$ is not an open set --- its
characteristic functions has a `1' (in the position $2▁$) pointing to
a `0' (in the position $▁2$).
A {\sl specification} of 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 above is generated by this specification:
%
$$(4,6,\csm{\ltor45, \\ \ltor34, \\ \ltor22, \\ \ltor11,},
\csm{\lotr25})
$$
In the library that I wrote to calculate with these objects that
specification is represented as a string: \co{"46; 11 22 34 45, 25"}.
% ______ _ _
% |__ / | | | / \ ___
% / /| |_| | / _ \ / __|
% / /_| _ |/ ___ \\__ \
% /____|_| |_/_/ \_\___/
%
% «ZHAs» (to ".ZHAs")
\subsection{Planar Heyting Algebras (``ZHAs'')}
We can treat the topology above as a subset of $\Z^2$. Here's how.
\msk
$(x,y)$ means: start at $(0,0)$, walk $x$ steps east and $y$ steps north.
$〈a,b〉$ means: start at $(0,0)$, walk $a$ steps northwest and
$b$ steps northeast --- i.e., $〈a,b〉 = (0,0) + a\VEC{-1,1} + b\VEC{1,1}$.
$\LR$ is $\setofst{〈a,b〉}{a,b∈\N}$ --- like $\N^2$ tilted $45°$
counterclockwise.
$ab$ is an abbreviation for $〈a,b〉$.
\msk
Look at the topology above again. It is generated by a 2CG whose
specification in \co{"46; 11 22 34 45, 25"}. The 46 is the top element
of the topology, and the \co{"11 22 34 45"} and the \co{"25"} are the
points where the left wall and the right wall have ``bumps''.
\cite{PH1} defines ZHAs in sec.4 as a finite subset of $\LR$ ``between
a left wall and a right wall'' (long story --- see the paper), and it
shows a correspondence that we write as:
%
$$(P,A) \squigbij H$$
%
we pronounce that as: ``every 2CG $(P,A)$ is associated to a ZHA $H$
and vice-versa''.
Topologies are Heyting Algebras, so the order topology
$(P,\Opens_A(P))$ of a 2CG is a Heyting Algebra --- and we can
interpret intuitionistic propositional logic on it.
\bsk
Here is a particular case of $(P,A) \squigbij H$:
%
$$\tcg{(P,A)} \;\; \squigbij \;\;\; \zha{O_A(P)}$$
% _ _ _ ______ _ _
% | | ___ __ _(_) ___ (_)_ __ __ _ |__ / | | | / \
% | | / _ \ / _` | |/ __| | | '_ \ / _` | / /| |_| | / _ \
% | |__| (_) | (_| | | (__ | | | | | | (_| | / /_| _ |/ ___ \
% |_____\___/ \__, |_|\___| |_|_| |_| \__,_| /____|_| |_/_/ \_\
% |___/
%
% «logic-in-a-ZHA» (to ".logic-in-a-ZHA")
% (ph1p 11 "prop-calc-ZHA")
% (ph1 "prop-calc-ZHA")
% (ph1p 12 "prop-calc-ZHA" "valuations")
% (ph1 "prop-calc-ZHA" "valuations")
% (ph1p 12 "HAs")
% (ph1 "HAs")
% (ph1p 13 "HAs" "helpful for visualizing")
% (ph1 "HAs" "helpful for visualizing")
% (ph1p 18 "logic-in-HAs")
% (ph1 "logic-in-HAs")
\subsection{Logic in a ZHA}
The standard way of interpreting logic on a topology $(X,\Opens(X))$
is: the truth values are the open sets $P,Q,R,\ldots∈\Opens(X)$;
$⊤=X$; $⊥=∅$; $P∧Q=P∩Q$; $P∨Q=P∪Q$; $P→Q = \Int((X∖P)∪Q)$. On a ZHA
the operations $⊤,⊥,∧,∨$ are very easy to visualize...
%
%R local PQaoi =
%R 1/ T \
%R | . . |
%R | . . . |
%R | . o . i |
%R |. P . . .|
%R | . . Q . |
%R | . a . |
%R | . . |
%R \ F /
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R T="·", F="·", T="⊤", F="⊥", }
%R PQaoi:tozmp({zdef="PQaoi", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PQaoi:tozmp({zdef="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
$$
\pu
\zha{lozfive} \qquad \zha{PQaoi}
$$
There is a way to calculate $P→Q$ {\sl visually}, but the formula has
four subcases. For example, if $P$ is ``left of'' $Q$ then $P→Q$ is
$𝐬{ne}(Q)$, i.e.: start from $Q$ and walk northeast as many steps as
possible. The diagram above shows that $31→12=14$ --- you can check
that by calculating $\Int((\pile(44)∖\pile(31))∪\pile(12))$.
By the way, this is one of the first things that I present to students
in a hands-on seminar course called ``$λ$-Calculus, Logics, and
Translations''... they learn how the interpret the definitions for
$⊤,⊥,∧,∨,→,¬$ in a ZHA, then they see that in these logics some
classical tautologies sometimes give results different from $⊤$,
%
%R local znotnotP =
%R 1/ T \
%R | . |
%R | . c |
%R |b . a|
%R | P . |
%R \ F /
%R local T = {F="⊥", T="⊤", a="P'", b="P''", c="→"}
%R znotnotP:tozmp({def="znotnotP", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R local zdemorgan =
%R 1/ T \
%R | o |
%R | . . |
%R |q . p|
%R | P Q |
%R \ a /
%R local T = {F="⊥", T="⊤", p="P'", q="Q'", a="∧", o="∨"}
%R zdemorgan:tozmp({def="zdemorgan", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse", scale="12pt", meta=nil}):addlrs():output()
%
%UB (¬ ¬ P) → P
%UB -- --
%UB 10 10
%UB ---
%UB 02
%UB -----
%UB 20
%UB -----------
%UB 12
%L
%L defub "notnotP"
%
%UB ¬(P ∧ Q) → (¬ P ∨ ¬ Q)
%UB -- -- -- --
%UB 10 01 10 01
%UB ----- --- ---
%UB 00 02 20
%UB ------- ---------
%UB 32 22
%UB ----------------------
%UB 22
%L
%L defub "demorgan"
%
$$\pu
\begin{array}{ccccl}
\ohouse && \znotnotP && \mat{\ub{notnotP}} \\ \\
&& \zdemorgan && \mat{\ub{demorgan}} \\
\end{array}
$$
%
and only then they learn what is a Heyting Algebra, and they check
that ZHAs with these operations are Heyting Algebras, they learn
topologies, etc, etc... the ordering of topics is very unusual ---
from particular to general --- but it works!
% _ _
% | | ___ _ __ ___ _ __ __ _| |_ ___ _ __ ___
% _ | |_____ / _ \| '_ \ / _ \ '__/ _` | __/ _ \| '__/ __|
% | |_| |_____| (_) | |_) | __/ | | (_| | || (_) | | \__ \
% \___/ \___/| .__/ \___|_| \__,_|\__\___/|_| |___/
% |_|
%
% «J-operators» (to ".J-operators")
\subsection{J-operators on ZHAs}
% (p2lp 1 "J-operators")
% (p2l "J-operators")
\catcode`¹=13 \def¹{^{*}}
\catcode`²=13 \def²{^{**}}
\catcode`³=13 \def³{^{***}}
A {\sl J-operator} on a Heyting Algebra $H$ is a function $J:H→H$ that
obeys the axioms $\J1$, $\J2$, $\J3$ below; we usually write $J$ as
$·^*:Ω→Ω$, and write the axioms as rules.
%
%L addabbrevs(".\\eqJ.", " \\eqJ ")
%L -- addabbrevs("&", "\\&", "vv", "∨", "->", "→")
%L -- addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
% (fooi "!!" "²" "!" "¹" "^*" "¹" "<=" "≤" "->" "→" "&" "∧" "vv" "∨")
%:
%: -----\J1 ------\J2 ------------\J3
%: P≤P¹ P¹=P² (P∧Q)¹=P¹∧Q¹
%:
%: ^J1 ^J2 ^J3
%:
\pu
$$\ded{J1} \qquad \ded{J2} \qquad \ded{J3}$$
\par $\J1$ says that the operation $·^*$ is non-decreasing.
\par $\J2$ says that the operation $·^*$ is idempotent.
\par $\J3$ is a bit mysterious but has amazing consequences.
\msk
A J-operator induces an equivalence relation: $P∼Q$ iff $P¹=Q¹$. Let's
write $[P]^J$ for the equivalence class of $P$.
It is possible to prove that every equivalence class $[P]^J$ has a
maximal element, a minimal element, and contains all the elements of
$H$ between the minimal and the maximal element, and nothing else.
Also, for all elements $Q∈[P]^J$ we have that $Q^*$ is the maximal
element of $[P]^J$. So we can represent a J-operator graphically by
the fences between its equivalence classes; if we interpret this as a
J-operator,
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234567654321")
%L mp:addlrs():addcuts("c 10w-14n 11n-61n 42w-46n 44n-04e"):output()
$$\pu
\foo
$$
%
then $32¹=44¹=44$, $30¹=61¹=61$, etc...
...but this has ``cuts stopping midway'', and a --- very non-trivial
--- consequence of $\J1$, $\J2$, $\J3$ is that we can't have ``cuts
stopping midway''!
{\bf Definition} (informal): a {\sl slashing} on a ZHA $H$ is any
drawing obtained by cutting $H$ by diagonals cuts without ``cuts
stopping midway''. This is an example of a ZHA with a slashing:
%
% (ph2p 4 "piccs-and-slashings")
% (ph2 "piccs-and-slashings")
%
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
$$\pu
\ZQuotients
$$
I said that every J-operator ``is'' a slashing. The converse is also
true: every slashing ``is'' a J-operator.
% ___ _ _
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ ___
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \/ __|
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | \__ \
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|___/
%
% «question-marks» (to ".question-marks")
\subsection{Question marks}
\label{question-marks}
Take a 2CG $(P,A)$, and choose a subset $Q⊆P$. This $Q$ will be the
{\sl set of question marks}, and we will represent it by drawing `?'s
at the side of its points. A structure $((P,A),Q)$ will be called a
{\sl 2CG with question marks}.
Suppose that $(P,A) \squigbij H$. A set of question marks $Q⊆P$
induces an equivalence relation $\eqQ$ on $H$: $ab \eqQ cd$ if and
only if $\pile(ab)$ and $\pile(cd)$ differ only on points of $Q$ ---
or, more formally, $\pile(ab)∖Q = \pile(cd)∖Q$.
It is easy to convert a set of question marks to a slashing and
vice-versa --- and slashings correspond to J-operators and vice-versa.
Our favourite way of writing these bijection is as:
%
$$((P,A),Q) \squigbij (H,J),$$
%
and here is a particular case of it:
%
$$\tcg{(P,A),Q} \squigbij \zha{O_A(P),J}$$
Note that if we erase the question marks and the cuts above we get a
particular case of $(P,A) \squigbij H.$
% (oxap 7 "fig:2CGs-ZHA")\
% (oxa "fig:2CGs-ZHA")
% (oxap 7 "fig:2CGs-ZHA")
% (oxa "fig:2CGs-ZHA")
% (oxap 7 "fig:2CGs-ZHA" "$Q$-equivalent")
% (oxa "fig:2CGs-ZHA" "$Q$-equivalent")
% _____ _
% | ___|_ _ _ __ ___ ___ _ _ ___ | | ___ _ __ ___
% | |_ / _` | '_ ` _ \ / _ \| | | / __| _ | |_____ / _ \| '_ \/ __|
% | _| (_| | | | | | | (_) | |_| \__ \ | |_| |_____| (_) | |_) \__ \
% |_| \__,_|_| |_| |_|\___/ \__,_|___/ \___/ \___/| .__/|___/
% |_|
%
%\subsection{Some famous J-operators}
% (ph2p 29 "polynomial-J-ops")
% (ph2 "polynomial-J-ops")
% (ph2 "polynomial-J-ops" "open quotient")
% _____ __ _
% |_ _|__ _ __ ___ ___ ___ ___ / _| ___ _ __ ___| |__
% | |/ _ \| '_ \ / _ \/ __|/ _ \/ __| | |_ / _ \| '__| / __| '_ \
% | | (_) | |_) | (_) \__ \ __/\__ \ | _| (_) | | | (__| | | |
% |_|\___/| .__/ \___/|___/\___||___/ |_| \___/|_| \___|_| |_|
% |_|
%
% «toposes-for-children» (to ".toposes-for-children")
\section{Toposes for children}
My favourite very short {\sl explanation} for what a topos is is:
\begin{enumerate}
\item a Cartesian Closed Category (CCC) is a category with a terminal,
binary products, and exponentials,
\item CCCs are exactly the categories in which we can interpret the
simply-typed $λ$-calculus (``$λ1$''),
\item the archetypal CCC is $\Set$ (see \cite{IDARCT}),
\item every Heyting Algebra is a CCC,
\item a topos is a CCC with pullbacks and a classifier object.
\item toposes are exactly the categories in which we can interpret a
certain form of intuitionistic, typed Set Theory,
\item the archetypal topos is $\Set$,
\item the subcategory $\Sub(1)⊂\calE$ of a topos $\calE$ is a Heyting
Algebra --- the ``logic'' of $\calE$,
\item for every small category $\catA$ the category $\Set^\catA$ is a
topos,
\item for every 2CG $(P,A) \squigbij H$ the category $\Set^{(P,A)}$ is
a topos whose ``logic'' is $H$.
\end{enumerate}
% ____ _ _ __ _
% / ___| | __ _ ___ ___(_)/ _(_) ___ _ __
% | | | |/ _` / __/ __| | |_| |/ _ \ '__|
% | |___| | (_| \__ \__ \ | _| | __/ |
% \____|_|\__,_|___/___/_|_| |_|\___|_|
%
% «classifier» (to ".classifier")
% (elzp 14 "classifier")
% (elz "classifier")
\subsection{The classifier}
% From:
% (find-LATEX "2017planar-has-3.tex" "classifier")
%L tcg_big = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2}
%L tcg_med = {scale= "8pt", meta="p s", dv=1, dh=2, ev=0.32, eh=0.25}
%L tcgnew = function (opts, def, str)
%L return TCG.new(opts, def, unpack(split(str, "[ %d]+")))
%L end
%L tcgbig = function (def, spec) return tcgnew(tcg_big, def, spec or tcg_spec) end
%L tcgmed = function (def, spec) return tcgnew(tcg_med, def, spec or tcg_spec) end
%L
%L tcg_bigq = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2, dq=1.4}
%L tcg_medq = {scale= "8pt", meta="p s", dv=1, dh=2, ev=0.32, eh=0.25, dq=1.4}
%L tcg_Medq = {scale="10pt", meta="p", dv=1, dh=3, ev=0.32, eh=0.25, dq=1.4}
%L
%L tcgbigq = function (def, spec) return tcgnew(tcg_bigq, def, spec or tcg_spec) end
%L tcgmedq = function (def, spec) return tcgnew(tcg_medq, def, spec or tcg_spec) end
%L tcgMedq = function (def, spec) return tcgnew(tcg_Medq, def, spec or tcg_spec) end
%L -- (find-dn6 "zhas.lua" "TCG")
%L -- (find-dn6 "zhas.lua" "TCG" "lrs =")
%L
%L TCG.__index.QL = function (tcg, y) return v(0 -tcg.lp.dq, tcg.dv*y) end
%L TCG.__index.QR = function (tcg, y) return v(tcg.dh+tcg.lp.dq, tcg.dv*y) end
%L TCG.__index.putql = function (tcg, y, str) tcg.lp:put(tcg:QL(y), str) end
%L TCG.__index.putqr = function (tcg, y, str) tcg.lp:put(tcg:QR(y), str) end
%L TCG.__index.qmarks = function (tcg, lstr, rstr)
%L for y=1,tcg.l do tcg:putql(y, lstr:sub(y, y)) end
%L for y=1,tcg.r do tcg:putqr(y, rstr:sub(y, y)) end
%L return tcg
%L end
%L mytcgspec = "3, 3; 32, 13"
%L myspec = "1232RL1"
%L mycuts = "c 32/10 012|3"
%L mytop = v"35"
%L myf = "lr -> lr:below(mytop) and lr:lr() or '..'"
%L
%L foo = function (top, opts)
%L mytop = v(top)
%L mpnew(opts, myspec):addcutssub(mytop, mycuts):zhalrf0(myf):print():output()
%L end
%L foo("33", {zdef="(H,J)"})
%L
%L foo("32", {zdef="3_"})
%L foo("20", {zdef="2_"})
%L foo("10", {zdef="1_"})
%L foo("13", {zdef="_3"})
%L foo("02", {zdef="_2"})
%L foo("01", {zdef="_1"})
%L claOpts = {scale="90pt", meta="p", dv=1.2, dh=1.4, ev=0.45, eh=0.28}
%L claT = tcgnew(claOpts, "fooT", mytcgspec)
%L claT:strs("\\zha{1_} \\zha{2_} \\zha{3_}", "\\zha{_1} \\zha{_2} \\zha{_3}"):hs():vs():output()
%L local tcg = tcgbigq("footcg", mytcgspec)
%L tcg:lrs():hs():vs()
%L tcg:qmarks("? ?", "?? ")
%L tcg:output()
Choose a 2CG $(P,A)$. Let $\calE$ be the topos $\Set^{(P,A)}$. There
is an easy way to draw the classifier $Ω_\calE$, but the result is
big. Let's see an example. Suppose that $(P,A) \squigbij H$ is:
%
\pu
$$\footcg
\quad
\squigbij
\quad
\zha{(H,J)}
$$
Ignore the question marks and the slashing for the moment. Then
$Ω_\calE$ is (ignoring the slashings):
%
$$\fooT$$
Now stop ignoring the question marks and the slashing above. We get an
2CG with question marks $((P,A),Q)$ and its associated ZHA with
J-operator $(H,J)$...
% $$(H,J) = \zha{(H,J)}
% \quad
% \squigbij
% \quad
% ((P,A),Q) = \footcg
% $$
%
% $$\calE = \Set^{(P,A)} = \Set^{\footcg}$$
% _ _
% | | ___ ___ __ _| | ___ _ __ ___
% | | / _ \ / __/ _` | | / _ \| '_ \/ __|
% | |__| (_) | (_| (_| | | | (_) | |_) \__ \
% |_____\___/ \___\__,_|_| \___/| .__/|___/
% |_|
% «local-operators» (to ".local-operators")
%\subsection{Local operators}
%\section{Geometric morphisms}
% (oxap 5 "fig:internal-gms")
% (oxa "fig:internal-gms")
% (oxap 8 "two-factorizations-gms")
% (oxa "two-factorizations-gms")
% (find-LATEXfile "2019oxford-abs.tex" "Conditions on the functors")
% _____ _ _ _ _
% | ___|_ _ ___| |_ ___ _ __(_)______ _| |_(_) ___ _ __
% | |_ / _` |/ __| __/ _ \| '__| |_ / _` | __| |/ _ \| '_ \
% | _| (_| | (__| || (_) | | | |/ / (_| | |_| | (_) | | | |
% |_| \__,_|\___|\__\___/|_| |_/___\__,_|\__|_|\___/|_| |_|
%
% «the-factorization» (to ".the-factorization")
\section{The factorization}
\label{the-factorization}
% (oxap 9 "fig:factorizations")
% (oxa "fig:factorizations")
% _____ _ _ _ _
% | ___|_ _ ___| |_ ___ _ __(_)______ _| |_(_) ___ _ __
% | |_ / _` |/ __| __/ _ \| '__| |_ / _` | __| |/ _ \| '_ \
% | _| (_| | (__| || (_) | | | |/ / (_| | |_| | (_) | | | |
% |_| \__,_|\___|\__\___/|_| |_/___\__,_|\__|_|\___/|_| |_|
%
% «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\colwidth}{!}{$%
\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}
{\bf Theorem.}
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}
% (ph1p 8 "ZHAs")
% (ph1 "ZHAs")
% ____ __
% | _ \ ___ / _| ___ _ __ ___ _ __ ___ ___ ___
% | |_) / _ \ |_ / _ \ '__/ _ \ '_ \ / __/ _ \/ __|
% | _ < __/ _| __/ | | __/ | | | (_| __/\__ \
% |_| \_\___|_| \___|_| \___|_| |_|\___\___||___/
%
% «references» (to ".references")
% (find-LATEX "2019oxford-abs.tex" "references")
% (find-es "tex" "bibtex-2017")
% (find-kopkadaly4page (+ 12 217) "9.3.1 Bibliography by hand")
% (find-kopkadaly4text (+ 12 217) "9.3.1 Bibliography by hand")
% (find-kopkadaly4page (+ 12 310) "\\bibliographystyle{style}")
% (find-kopkadaly4text (+ 12 310) "\\bibliographystyle{style}")
% \bibliographystyle{plain}
% \begin{thebibliography}{9}
%
% \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).}
%
% \end{thebibliography}
% TO HERE
\printbibliography
\end{document}
% «write-poster-body» (to ".write-poster-body")
% (find-LATEX "2019elephant-poster.tex" "input-poster-body")
% (find-LATEX "2019elephant-poster-body.tex")
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
fname1 = "2019elephant-poster-z.tex" -- input
fname2 = "2019elephant-poster-body.tex" -- output
bigstr = ee_readfile(fname1)
smallerstr = bigstr:match("%% FROM HERE.-%% TO HERE\n")
head = "\\directlua{tf_push(\""..fname2.."\")}\n"
tail = "\\directlua{tf_pop()}\n"
= head
= tail
newbody = head..smallerstr..tail
ee_writefile(fname2, newbody)
-- (find-fline "2019elephant-poster-body.tex")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2017planar-has-1.mk")
make -f 2017planar-has-1.mk STEM=2019elephant-poster-z veryclean
make -f 2017planar-has-1.mk STEM=2019elephant-poster-z pdf
make -f 2017planar-has-1.mk STEM=2019elephant-poster veryclean
make -f 2017planar-has-1.mk STEM=2019elephant-poster pdf
# (elzp)
# (elpp)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
mount
sudo umount /dev/sdb1
mkdir /tmp/pen/
sudo mount -o uid=$UID /dev/sdb1 /tmp/pen/
sudo mount -o uid=$UID /dev/sdc1 /tmp/pen/
sudo mount -o uid=$UID /dev/sdb /tmp/pen/
sudo mount -o uid=$UID /dev/sdc /tmp/pen/
# (find-fline "/tmp/pen/")
cp -v ~/LATEX/2019elephant-poster.pdf /tmp/pen/
# (find-pdf-page "/tmp/pen/2019elephant-poster.pdf")
sudo umount /tmp/pen
sync
% Local Variables:
% coding: utf-8-unix
% ee-tla: "elz"
% End: