|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2019J-ops-arxiv.tex")
% Based on: (find-LATEX "2019J-ops.tex")
% (find-es "arxiv" "pdflatex")
\pdfoutput=1
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-arxiv.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-arxiv.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-arxiv.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-arxiv"))
% (find-pdf-page "~/LATEX/2019J-ops-arxiv.pdf")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-arxiv.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-arxiv.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019J-ops-arxiv.pdf
% file:///tmp/2019J-ops-arxiv.pdf
% file:///tmp/pen/2019J-ops-arxiv.pdf
% http://angg.twu.net/LATEX/2019J-ops-arxiv.pdf
% (find-LATEX "2019.mk")
\documentclass[oneside]{article}
%\usepackage[colorlinks,urlcolor=DarkRed,citecolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{hyperref} % (find-es "tex" "hyperref")
%
% (find-LATEXfile "2019notes-yoneda.tex" "ifluatex")
% (find-dednat6file "demo-write-dnt.tex")
%\usepackage{ifluatex}
%
% «chars» (to ".chars")
%\ifluatex
% \input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
% \input edrxchars.tex % (find-LATEX "edrxchars.tex")
% \catcode`¹=13 \def¹{^{*}}
% \catcode`²=13 \def²{^{**}}
% \catcode`³=13 \def³{^{***}}
%\else
\usepackage[utf8]{inputenc}
\input 2019oxford-chars.tex % (find-LATEX "2019oxford-chars.tex")
\DeclareUnicodeCharacter{00B9}{^{*}} % ¹
\DeclareUnicodeCharacter{00B2}{^{**}} % ²
\DeclareUnicodeCharacter{00B3}{^{***}} % ³
%\fi
%
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\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")
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib} % (find-LATEX "catsem-u.bib")
%
% (find-es "tex" "geometry")
\usepackage[a4paper]{geometry} % (find-es "tex" "geometry")
\begin{document}
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
\input 2019J-ops-defs.tex % (find-LATEX "2019J-ops-defs.tex")
%\ifluatex
% \catcode`\^^J=10
% \directlua{dofile "dednat6load.lua"}
%\else
\input\jobname.dnt
\def\pu{}
\def\directlua#1{}
%\fi
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
\def\ovl{\overline}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
% (jopp 1 "title")
% (jop "title")
\title{Planar Heyting Algebras for Children 2: Local Operators, J-Operators, and Slashings}
\author{Eduardo Ochs}
\maketitle
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% (jopp 1 "abstract")
% (jop "abstract")
\begin{abstract}
Choose a topos $\calE$. There are several different ``notions of
sheafness'' on $\calE$. How do we visualize them?
Let's refer to the classifier object of $\calE$ as $Ω$, and to its
Heyting Algebra of truth-values, $\Sub(1_\calE)$, as $H$; we will
sometimes call $H$ the ``logic'' of the topos. There is a well-known
way of representing notions of sheafness as morphisms $j:Ω→Ω$, but
these `$j$'s yield big diagrams when we draw them explicitly; here we
will see a way to represent these `$j$'s as maps $J:H→H$ in a way that
is much more manageable.
In the previous paper of this series --- called \cite{OchsPH1} from
here on --- we showed how certain toy models of Heyting Algebras,
called ``ZHAs'', can be used to develop visual intuition for how
Heyting Algebras and Intuitionistic Propositional Logic work; here we
will extend that to sheaves. The full idea is this: {\sl notions of
sheafness} correspond to {\sl local operators} and vice-versa; {\sl
local operators} correspond to {\sl J-operators} and vice-versa; if
our Heyting Algebra $H$ is a ZHA then {\sl J-operators} correspond to
{\sl slashings} on $H$, and vice-versa; {\sl slashings} on $H$
correspond to {\sl ``sets of question marks''} and vice-versa, and
each set of question marks induces a notion of {\sl erasing and
reconstructing}, which induces a sheaf. Also, every ZHA $H$
corresponds to an {(acyclic) 2-column graph}, and vice-versa, and for
any two-column graph $(P,A)$ the logic of the topos $\Set^{(P,A)}$ is
exactly the ZHA $H$ associated to $(P,A)$.
The introduction of \cite{OchsPH1} discusses two different senses in
which a mathematical text can be ``for children''. The first sense
involves some precise metamathetical tools for transfering knowledge
back and forth between a general case ``for adults'' and a toy model
``for children''; the second sense is simply that the text's
presentation has few prerequisites and never becomes too abstract.
Here we will use the second sense: everything here, except for the
last section, should be accessible to students who have taken a course
on Discrete Mathematics and read \cite{OchsPH1}. This means that
categories, toposes, sheaves and the maps $j:Ω→Ω$ only appear in the
last section, and before that we deal only with the J-operators
$J:H→H$, how they correspond to slashings and sets of question marks,
and how they form an algebra.
\end{abstract}
% (find-books "__cats/__cats.el" "bell")
% (find-belltpage (+ 14 163) "modality")
% (find-belltpage (+ 14 164) "universal closure operation")
%
% (find-books "__cats/__cats.el" "johnstone-elephant")
% (find-elephantpage (+ 17 195) "A4.4 Local Operators")
%
% (find-books "__cats/__cats.el" "fourman-scott")
% (find-slnm0753page (+ 16 324) "J-operators")
% TODO: add this (and an abstract):
% (ph2p 4 "piccs-and-slashings")
% (ph2 "piccs-and-slashings")
% \end{document}
% ____ _
% | _ \ __ _ _ __| |_ ___
% | |_) / _` | '__| __/ __|
% | __/ (_| | | | |_\__ \
% |_| \__,_|_| \__|___/
%
% «parts» (to ".parts")
\newpage
\input 2019J-ops-slashings.tex % (find-LATEX "2019J-ops-slashings.tex")
\newpage
\input 2019J-ops-logic.tex % (find-LATEX "2019J-ops-logic.tex")
\newpage
\input 2019J-ops-midway.tex % (find-LATEX "2019J-ops-midway.tex")
\newpage
\input 2019J-ops-cubes.tex % (find-LATEX "2019J-ops-cubes.tex")
\newpage
\input 2019J-ops-valuations.tex % (find-LATEX "2019J-ops-valuations.tex")
\newpage
\input 2019J-ops-algebra.tex % (find-LATEX "2019J-ops-algebra.tex")
\newpage
\input 2019J-ops-categories.tex % (find-LATEX "2019J-ops-categories.tex")
\newpage
\input 2019J-ops-classifier.tex % (find-LATEX "2019J-ops-classifier.tex")
\newpage
\input 2019J-ops-kan.tex % (find-LATEX "2019J-ops-kan.tex")
%L write_dnt_file()
\pu
% (find-LATEX "2019ilha-grande-poster-a4.tex" "references")
\newpage
\printbibliography
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
% (find-LATEX "2019ilha-grande-poster-a4.tex")
% (find-LATEX "2019ilha-grande-poster-a4.tex" "write-poster-body")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# Test the .zip.
# The e-script below downloads, unpacks and compiles the .zip in /tmp/edrx-latex/
#
rm -rfv /tmp/2019J-ops.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
# wget http://angg.twu.net/LATEX/2019J-ops.zip
cp -v ~/LATEX/2019J-ops.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2019J-ops.zip
cd /tmp/edrx-latex/
cp -v ~/LATEX/2019J-ops-arxiv.tex 2019J-ops.tex
rm -v /tmp/2019J-ops-arxiv.zip
zip /tmp/2019J-ops-arxiv.zip *
pdflatex 2019J-ops.tex
pdflatex 2019J-ops.tex
# (find-xpdfpage "/tmp/edrx-latex/2019J-ops.pdf")
# (find-fline "/tmp/2019J-ops-arxiv.zip")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2017planar-has-1.mk")
make -f 2017planar-has-1.mk STEM=2019J-ops-arxiv veryclean
make -f 2017planar-has-1.mk STEM=2019J-ops-arxiv pdf
# (jopp)
# (jopp 25)
% Local Variables:
% coding: utf-8-unix
% ee-tla: "NONE"
% End: