|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019ebl-five-appls.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019ebl-five-appls.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019ebl-five-appls.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019ebl-five-appls.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019ebl-five-appls; makeindex 2019ebl-five-appls"))
% (defun e () (interactive) (find-LATEX "2019ebl-five-appls.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019ebl-five-appls"))
% (find-xpdfpage "~/LATEX/2019ebl-five-appls.pdf")
% (find-sh0 "cp -v ~/LATEX/2019ebl-five-appls.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019ebl-five-appls.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019ebl-five-appls.pdf
% file:///tmp/2019ebl-five-appls.pdf
% file:///tmp/pen/2019ebl-five-appls.pdf
% http://angg.twu.net/LATEX/2019ebl-five-appls.pdf
%
% Upload to:
% «.colors» (to "colors")
% «.defs» (to "defs")
% «.title-page» (to "title-page")
% «.category-theory» (to "category-theory")
% «.children» (to "children")
% «.five-applications» (to "five-applications")
% «.finite-topologies» (to "finite-topologies")
% «.finite-topologies-2» (to "finite-topologies-2")
% «.finite-topologies-3» (to "finite-topologies-3")
% «.finite-topologies-4» (to "finite-topologies-4")
% «.famous-J-operator» (to "famous-J-operator")
% «.strange-J-operator» (to "strange-J-operator")
% «.logic-in-a-ZHA» (to "logic-in-a-ZHA")
% «.logic-in-a-ZHA-2» (to "logic-in-a-ZHA-2")
% «.logic-in-a-ZHA-3» (to "logic-in-a-ZHA-3")
% «.J-operators» (to "J-operators")
% «.famous-J-operator-2» (to "famous-J-operator-2")
% «.strange-J-operator-2» (to "strange-J-operator-2")
% «.question-marks» (to "question-marks")
% «.question-marks-2» (to "question-marks-2")
% «.geometric-morphisms» (to "geometric-morphisms")
% «.geometric-morphisms-2» (to "geometric-morphisms-2")
% «.geometric-morphisms-3» (to "geometric-morphisms-3")
% «.a-factorization» (to "a-factorization")
% «.a-factorization-2» (to "a-factorization-2")
% «.a-factorization-3» (to "a-factorization-3")
% «.a-factorization-4» (to "a-factorization-4")
% «.shape-and-movement» (to "shape-and-movement")
\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorBrown #1{{\color{Brown}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}
\long\def\ColorBook #1{{\color{brown}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
% «defs» (to ".defs")
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\smile{\ensuremath{{=})}}
\def\frown{\ensuremath{{=}(}}
\def\smirk{\ensuremath{{=}/}}
\def\BPM{𝐬{BPM}}
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}
\def\uCH#1{\und{#1}{context / hypotheses}}
\def\uvt#1{\und{#1}{v:T}}
\def\uterm#1{\und{#1}{term}}
\def\utype#1{\und{#1}{type}}
\def\uconc#1{\und{#1}{conclusion}}
\def\Sets{\mathsf{Sets}}
\def\TALA{\mathsf{TA}_λ^→}
\def\app {\mathsf{app}}
\def\pair{\mathsf{pair}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\myvcenter#1{\begin{matrix}#1\end{matrix}}
\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}
\setlength{\parindent}{0em}
\def\O{\mathcal{O}}
\def\T{\mathbf{T}}
\def\F{\mathbf{F}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (ntyp 1 "title-page")
% (nty "title-page")
% (find-es "tex" "huge")
% (find-LATEXfile "2019ebl-abs.tex" "Five applications")
\begin{center}
\Large
{\bf
Five applications of the
``Logic for Children''
project to Category Theory
\large
\ssk
% \ColorGray{and to the ``Logic for Children'' project}
}
%\bsk
%
\normalsize
%
%(a part of the ``Logic for Children'' project)
\msk
Eduardo Ochs (UFF, Brazil)
\footnotesize
\url{http://angg.twu.net/math-b.html\#ebl-2019}
\end{center}
\newpage
\noedrxfooter
% ____ _____
% / ___|_ _|
% | | | |
% | |___ | |
% \____| |_|
%
% «category-theory» (to ".category-theory")
{\bf Category Theory...}
...\ColorRed{seems} to be a very elegant area with ``the right
abstractions'' and lots of diagrams, but the diagrams are usually
omitted from the texts as if they were ``obvious exercises'', and the
motivating examples are mentioned briefly, if at all --- so the
comparisons between these ``abstractions'' and the examples are also
left as exercises.
\msk
Topos Theory is a very important sub-area of CT.
When I tried to read Johnstone's ``Topos Theory'' (1977)
I understood very little, even though I tried \ColorRed{very} hard.
\ColorRed{``I need a version for children of this!!!''}
(I.e., with the \ColorRed{missing} diagrams and the examples.)
\newpage
% ____ _ _ _ _
% / ___| |__ (_) | __| |_ __ ___ _ __
% | | | '_ \| | |/ _` | '__/ _ \ '_ \
% | |___| | | | | | (_| | | | __/ | | |
% \____|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «children» (to ".children")
{\bf My current favorite definition of ``children'':}
They prefer to start from particular cases
and then generalize ---
They like diagrams and finite objects
drawn very explicitly ---
They become familiar with mathematical ideas
by calculating / checking several cases
(rather than by proving theorems)
\msk
% http://puzzler.sourceforge.net/docs/pentominoes.html
% http://puzzler.sourceforge.net/docs/images/ominoes/pentominoes-8x8.png
$\hskip-5.5pt
%
\begin{tabular}[b]{l}
Example: pentominos. \\
Let ``children'' \ColorRed{play} \\
with pentominos for a while \\
\ColorRed{before} showing to them \\
theorems and game trees! \\
\end{tabular}
%
\qquad
\quad
%
\includegraphics[height=52pt]{pentominoes-8x8.png}
$
\newpage
% _____ _ _
% | ___(_)_ _____ __ _ _ __ _ __ | |___
% | |_ | \ \ / / _ \ / _` | '_ \| '_ \| / __|
% | _| | |\ V / __/ | (_| | |_) | |_) | \__ \
% |_| |_| \_/ \___| \__,_| .__/| .__/|_|___/
% |_| |_|
%
% «five-applications» (to ".five-applications")
{\bf Five applications}
{%\footnotesize
\begin{enumerate}
\item A way to develop visual intuition about Intuitionistic
Propositional Logic. Models for IPL are Heyting Algebras; topologies
are HAs. Look for finite topologies! Use order topologies. Bonus:
use \ColorRed{planar} topologies (``\ColorRed{ZHA}s'').
\item A way to build a topos with a given logic (when that logic is a
ZHA). Solution: $\Set^{(P,A)}$.
\item Sheaves are related to J-operators ($←$ old terminology) on HAs.
So: a way to visualize J-operators on ZHAs (``slashings'').
\end{enumerate}
\newpage
\begin{enumerate}
\item The sheaf associated to a J-operator. Solution:
\ColorRed{question marks}; erasing followed by reconstruction yields
the sheafification functor.
\item A version ``for children'' for parts of The Elephant --- in
which the ``missing diagrams'' are no longer missing and we can
remember theorems and constructions by \ColorRed{shape} and
\ColorRed{movement}. Also: motivating examples ``for children'', in
which everything is finite and can be drawn explicitly. ``Children''
develop familiarity with mathematical structures by
\ColorRed{calculating} rather than by \ColorRed{proving theorems}.
\end{enumerate}
}
\newpage
% _____ _ _ _ _
% | ___(_)_ __ (_) |_ ___ | |_ ___ _ __ ___
% | |_ | | '_ \| | __/ _ \ | __/ _ \| '_ \/ __|
% | _| | | | | | | || __/ | || (_) | |_) \__ \
% |_| |_|_| |_|_|\__\___| \__\___/| .__/|___/
% |_|
%
% «finite-topologies» (to ".finite-topologies")
% (eb5p 6 "finite-topologies")
% (eb5 "finite-topologies")
% (ph1p 24 "topologies-as-partial-orders")
% (ph1 "topologies-as-partial-orders")
{\bf Finite topologies}
%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 house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt", meta="s"}):addcells():output()
%R house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R house:tomp({def="zdagHouse", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse", scale="12pt", meta="s"}):addlrs():addarrows("w"):output()
%
%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 guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R guill:tomp({def="zdagGuill", scale="7pt", meta="t"}):addbullets():addarrows():output()
%R guill:tomp({def="zdagGuill", scale="20pt", meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill", scale="28pt", meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill", scale="12pt", meta="s"}):addlrs():addarrows():output()
%
%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({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW", scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({def="zdagOW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%
\pu
$\resizebox{!}{80pt}{$
(\Opens\left(\zdagHouse\right), ⊂_1)
=
\def\h{\zfHouse}\zdagOHouse
$}
$
\newpage
% «finite-topologies-2» (to ".finite-topologies-2")
% (eb5p 7 "finite-topologies-2")
% (eb5 "finite-topologies-2")
{\bf Finite topologies (2)}
$\resizebox{!}{80pt}{$
(\Opens\left(\zdagGuill\right), ⊂_1)
=
\def\g{\zfGuill}\zdagOGuill
$}
$
\newpage
% «finite-topologies-3» (to ".finite-topologies-3")
% (eb5p 8 "finite-topologies-3")
% (eb5 "finite-topologies-3")
{\bf Finite topologies (3)}
$\resizebox{!}{70pt}{$
(\Opens\left(\zdagW\right), ⊂_1)
=
\def\w{\zfW}\zdagOW
$}
$
Non-planar! Why?
Answer: because the W has \ColorRed{three independent points!}
\newpage
% «finite-topologies-4» (to ".finite-topologies-4")
% (eb5p 9 "finite-topologies-4")
% (eb5 "finite-topologies-4")
{\bf Finite topologies (4): 2CGs and ZHAs}
A \ColorRed{2-column graph} never has three independent points.
Trick: $\pile(25) = \{2▁,1▁,\;\;▁1,▁2,▁3,▁4,▁5\}$.
% (oxap 8 "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
\bsk
$\resizebox{!}{60pt}{$
(\Opens\tcg{(P,A)}, ⊂_1)
\;\;=\;\;
\zha{O_A(P)}
$}
$
\newpage
% «famous-J-operator» (to ".famous-J-operator")
% (eb5p 10 "famous-J-operator")
% (eb5 "famous-J-operator")
{\bf A famous J-operator: $(13∨)$}
\bsk
$\resizebox{!}{60pt}{$
\tcg{closed-op} \squigbij \zha{closed-op} \\
$}
$
\newpage
% «strange-J-operator» (to ".strange-J-operator")
% (eb5p 11 "strange-J-operator")
% (eb5 "strange-J-operator")
{\bf A strange J-operator}
\bsk
$\resizebox{!}{60pt}{$
\tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
$}
$
\newpage
% _ _ _ ______ _ _
% | | ___ __ _(_) ___ (_)_ __ __ _ |__ / | | | / \
% | | / _ \ / _` | |/ __| | | '_ \ / _` | / /| |_| | / _ \
% | |__| (_) | (_| | | (__ | | | | | | (_| | / /_| _ |/ ___ \
% |_____\___/ \__, |_|\___| |_|_| |_| \__,_| /____|_| |_/_/ \_\
% |___/
%
% «logic-in-a-ZHA» (to ".logic-in-a-ZHA")
% (eb5p 12 "logic-in-a-ZHA")
% (eb5 "logic-in-a-ZHA")
% (lodp 27 "ipl-on-a-topology-2")
% (lod "ipl-on-a-topology-2")
{\bf Logic in a ZHA (visually!!!)}
Notation: a 2-column graph is \ColorRed{$(P,A)$} --- (points, arrows) ---
its order topology is \ColorRed{$\Opens_A(P)$},
and a Planar Heyting Algebra (a ZHA) is $\ColorRed{H}⊂\Z^2$.
The correspondence is written as \ColorRed{$(P,A) \squigbij H$}
and formally it means $\Opens_A(P) ≅ H$.
There are two ways to define $⊤,⊥∈H$ and $∧,∨,→∈⊤$...
\msk
1) Via topology, in $\Opens_A(P)$:
$⊤:=P$,
$⊥:=∅$,
$Q∧R:=Q∩R$,
$Q∨R:=Q∪R$,
$R→S := \ColorRed{𝐬{Int}}((T∖R)∪S)$
\newpage
% «logic-in-a-ZHA-2» (to ".logic-in-a-ZHA-2")
% (eb5p 13 "logic-in-a-ZHA-2")
% (eb5 "logic-in-a-ZHA-2")
{\bf Logic in a ZHA (visually!!!) (2)}
2) Via order. For example:
$\begin{array}{rcl}
(Q→(R→S)) &↔& ((Q∧R)→S) \\
(Q≤(R→S)) &↔& ((Q∧R)≤S) \\
\setofst{Q∈H}{Q≤(R→S)} &=& \setofst{Q∈H}{(Q∧R)≤S} \\
(R→S) &=& \sup \; \setofst{Q∈H}{(Q∧R)≤S} \\
&=& ⋃ \; \setofst{Q∈H}{(Q∧R)≤S} \\
\end{array}
$
\newpage
% «logic-in-a-ZHA-3» (to ".logic-in-a-ZHA-3")
% (eb5p 14 "logic-in-a-ZHA-3")
% (eb5 "logic-in-a-ZHA-3")
{\bf Logic in a ZHA (visually!!!) (3)}
\bsk
\bsk
% (ph1p 11 "HAs")
% (ph1 "HAs")
%R local QoRai, PoQai, PnnP =
%R 1/ T \, 1/ T \, 1/ T \
%R | . . | | . . | | . |
%R | . . . | | . . . | | . . |
%R | . o . i | | . o . . | |d . n|
%R |. Q . . .| |. P . . .| | P . |
%R | . . R . | | . . Q . | \ F /
%R | . a . | | . . . |
%R | . . | | . . |
%R \ F / \ F /
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R T="·", F="·", T="⊤", F="⊥", }
%R PoQai:tozmp({def="PoQai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
\pu
$$% \lozfive \qquad
\QoRai
%\qquad \PoQai
$$
\newpage
% «J-operators» (to ".J-operators")
% (eb5p 15 "J-operators")
% (eb5 "J-operators")
{\bf J-operators}
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^*$.
Some famous J-operators: $(¬¬)$, $(A∨)$, $(A→)$ (for $A∈H$).
\msk
A J-operator induces an equivalence relation:
$P ∼_J Q$ iff $P^*=Q^*$.
For many years I didn't have \ColorRed{ANY} visual intuition on
what J-operators were, or could be.
When we play with J-operators on ZHAs we discover that:
Each equivalence class $[P]^J$ has a top element, a bottom
element, and all element in between; and $P^*$ is always the
top element of $[P]^J$...
So we only need to \ColorRed{draw} the equivalence classes!
\newpage
% «famous-J-operator-2» (to ".famous-J-operator-2")
% (eb5p 16 "famous-J-operator-2")
% (eb5 "famous-J-operator-2")
{\bf A famous J-operator: $(13∨)$}
\bsk
$\resizebox{!}{60pt}{$
\tcg{closed-op} \squigbij \zha{closed-op} \\
$}
$
\newpage
% «strange-J-operator-2» (to ".strange-J-operator-2")
% (eb5p 17 "strange-J-operator-2")
% (eb5 "strange-J-operator-2")
{\bf A strange J-operator}
\bsk
$\resizebox{!}{60pt}{$
\tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
$}
$
\newpage
% «question-marks» (to ".question-marks")
% (eb5p 18 "question-marks")
% (eb5 "question-marks")
{\bf Question marks}
Every set of question marks $Q⊆P$ in $(P,A)$ induces an equivalence
relation on $H≅\Opens_A(P)$. Two subsets $S,S'⊆P$ are
𝐢{$Q$-equivalent} when $S$ and $S'$ only differ in points of $Q$,
i.e.: $S∖Q = S'∖Q$. Here $Q=\{4▁,3▁,2▁,$ \; $▁1,▁2,▁3,▁5,\}$, and:
$\pile(22) ∼_Q \pile(23) \not∼_Q \pile(24)$,
$12^* = 23$, \;\; $22 ∼_J \pile23 \not∼_J 24$.
$\resizebox{!}{45pt}{$
\tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
$}
$
\newpage
% «question-marks-2» (to ".question-marks-2")
% (eb5p 19 "question-marks-2")
% (eb5 "question-marks-2")
$\pile(22) ∼_Q \pile(23) \not∼_Q \pile(24)$,
$12^* = 23$, \;\; $22 ∼_J \pile23 \not∼_J 24$.
$\resizebox{!}{70pt}{$
\tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
$}
$
\newpage
% «geometric-morphisms» (to ".geometric-morphisms")
% (eb5p 20 "geometric-morphisms")
% (eb5 "geometric-morphisms")
{\bf Toposes, geometric morphisms, internal diagrams}
Internal diagrams are a tool to \ColorRed{lower the lever of abstraction}.
This is a \ColorRed{geometric morphism} between toposes.
%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
\pu
\msk
$\resizebox{!}{70pt}{$
\diag{internal-gm}
$}
$
\newpage
% «geometric-morphisms-2» (to ".geometric-morphisms-2")
% (eb5p 21 "geometric-morphisms-2")
% (eb5 "geometric-morphisms-2")
{\bf Toposes, geometric morphisms, internal diagrams (2)}
Let $\catA$ and $\catB$ be 2CGs regarded as categories.
Then a functor $f:\catA→\catB$ induces a geometric morphism...
\msk
$\resizebox{!}{60pt}{$
\diag{internal-zgm}
$}
$
\msk
And if we draw the internal views of $\catA$, $\catB$, $C$, $D$...
\newpage
% «geometric-morphisms-3» (to ".geometric-morphisms-3")
% (eb5p 22 "geometric-morphisms-3")
% (eb5 "geometric-morphisms-3")
%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}
\pu
$\resizebox{!}{100pt}{$
\diag{internal-zgm-particular-case}
$}
$
\newpage
% «a-factorization» (to ".a-factorization")
% (eb5p 23 "a-factorization")
% (eb5 "a-factorization")
{\bf A factorization}
The Elephant presents in its sections A4.2 and A4.5 two factorizations
of geometric morphisms that can be combined in a single diagram (next
slide). 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$.
\newpage
% «a-factorization-2» (to ".a-factorization-2")
% (eb5p 24 "a-factorization-2")
% (eb5 "a-factorization-2")
{\bf A factorization (2)}
\bsk
%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
\def\vtext#1#2{#1\text{ (#2)}}
\def\anygm{any g.m.}
$
\diag{factorization-1}
$
\newpage
% «a-factorization-3» (to ".a-factorization-3")
% (eb5p 25 "a-factorization-3")
% (eb5 "a-factorization-3")
{\bf A factorization (3)}
\bsk
$
\diag{factorization-2}
$
\newpage
% «a-factorization-4» (to ".a-factorization-4")
% (eb5p 26 "a-factorization-4")
% (eb5 "a-factorization-4")
{\bf A factorization (4)}
\msk
\resizebox{1.0\textwidth}{!}{$%
\diag{fact-characterization}
$}
\msk
These factorizations are almost completely opaque to people who know
just the basics of toposes... how can we?...
\newpage
% produce a version ``for
% children'' of them in the sense of section \ref{cats-for-children}?
%
% \newpage
% ____ _ _
% / ___|| |__ __ _ _ __ ___ __ _ _ __ __| | _ __ ___ _____ __
% \___ \| '_ \ / _` | '_ \ / _ \ / _` | '_ \ / _` | | '_ ` _ \ / _ \ \ / /
% ___) | | | | (_| | |_) | __/ | (_| | | | | (_| | | | | | | | (_) \ V /
% |____/|_| |_|\__,_| .__/ \___| \__,_|_| |_|\__,_| |_| |_| |_|\___/ \_/
% |_|
%
% «shape-and-movement» (to ".shape-and-movement")
% (eb5p 27 "shape-and-movement")
% (eb5 "shape-and-movement")
{\bf Shape and movement}
This is how I remember the Frobenius Property:
%
%D diagram Frob-std
%D 2Dx 100 +45 +35 +10 +30
%D 2D 100 B0 ================> B1
%D 2D ^ ^ ^
%D 2D | / |
%D 2D - \ -
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D - / -
%D 2D | \ |
%D 2D v v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |---------------> b1
%D 2D
%D (( B0 .tex= P B1 .tex= Σ_fP
%D B2 .tex= P∧f^*Q B3 .tex= Σ_f(P∧f^*Q) B3' .tex= (Σ_fP)∧Q
%D B4 .tex= f^*Q B5 .tex= Q
%D b0 .tex= A b1 .tex= B
%D ))
%D ((
%D B0 B1 |-> B2 B0 -> B3 B1 -> B3' B1 ->
%D B4 B5 <-| B2 B4 -> B3 B5 -> B3' B5 ->
%D B2 B3 |-> B3 B3' -> sl^ .plabel= a \nat B3 B3' <- sl_ .plabel= b 𝐬{Frob}
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B2 B4 midpoint B3 B5 midpoint harrownodes nil 20 nil |->
%D ))
%D (( b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
% (idap 1 "mental-space")
% (ida "mental-space")
% (ida "mental-space" "frob-sketch.eps")
% (idap 19 "pres-frob-bcc")
% (ida "pres-frob-bcc")
\bsk
\bsk
$\pu
\def∧{{\land}}
%
\resizebox{!}{40pt}{$\diag{Frob-std}$}
\quad
\myvcenter{
\includegraphics[scale=0.8]{frob-sketch.eps}
}
$
\bsk
\bsk
\ColorBrown{(From ``Internal Diagrams and Archetypal Reasoning
in
Category Theory'' (Ochs 2013))}
\newpage
% _____ _
% |_ _| _ _ __ ___ ___ _ _ ___| |_ ___ _ __ ___ ___
% | || | | | '_ \ / _ \ / __| | | / __| __/ _ \ '_ ` _ \/ __|
% | || |_| | |_) | __/ \__ \ |_| \__ \ || __/ | | | | \__ \
% |_| \__, | .__/ \___| |___/\__, |___/\__\___|_| |_| |_|___/
% |___/|_| |___/
%
{\bf Formalizing diagrams in type systems}
...so I got lots of diagrams for things in CT --- for example, the
construction that uses a comonad in the
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "eb5"
% End: