|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2018vichy-video.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018vichy-video.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018vichy-video.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2018vichy-video; makeindex 2018vichy-video"))
% (defun e () (interactive) (find-LATEX "2018vichy-video.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018vichy-video"))
% (find-xpdfpage "~/LATEX/2018vichy-video.pdf")
% (find-sh0 "cp -v ~/LATEX/2018vichy-video.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2018vichy-video.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2018vichy-video.pdf
% file:///tmp/2018vichy-video.pdf
% file:///tmp/pen/2018vichy-video.pdf
% http://angg.twu.net/LATEX/2018vichy-video.pdf
%
% (find-es "ffmpeg" "vichy-video")
% «.colors» (to "colors")
% «.myoval» (to "myoval")
% «.title-page» (to "title-page")
% «.why» (to "why")
% «.why-2» (to "why-2")
% «.why-3» (to "why-3")
% «.bigger-project» (to "bigger-project")
% «.adults» (to "adults")
% «.children» (to "children")
% «.children-2» (to "children-2")
% «.toolbox» (to "toolbox")
% «.publish» (to "publish")
% «.publish-2» (to "publish-2")
% «.rest-adults» (to "rest-adults")
% «.VGM» (to "VGM")
% «.VGM-2» (to "VGM-2")
% «.VGM-3» (to "VGM-3")
% «.VGM-4» (to "VGM-4")
% «.VGM-5» (to "VGM-5")
% «.VGM-6» (to "VGM-6")
% «.internal-views» (to "internal-views")
% «.internal-views-functors» (to "internal-views-functors")
% «.internal-views-functors-2» (to "internal-views-functors-2")
% «.internal-views-gm» (to "internal-views-gm")
% «.internal-views-gm-2» (to "internal-views-gm-2")
\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\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-angg "LATEX/edrx15.sty")
\input edrxaccents.tex % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[paperwidth=11cm, paperheight=8.5cm,
%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")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
% «colors» (to ".colors")
% (find-LATEX "2017ebl-slides.tex" "colors")
% (find-LATEX "2017ebl-slides.tex" "colors" "\\def\\ColorGreen")
\long\def\ColorRed #1{{\color{Red}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
% «myoval» (to ".myoval")
% (find-LATEXfile "2018pict2e.tex" "\\def\\myoval")
\def\myvcenter#1{\ensuremath{\vcenter{\hbox{#1}}}}%
\def\myoval(#1,#2)(#3,#4)[#5]{%
\myvcenter{%
\begin{picture}(#1,#2)(-#3,-#4)
\put(0,0){\oval[#5](#1,#2)}
\end{picture}%
}}
\def\calU{{\mathcal{U}}}
\def\calI{{\mathcal{I}}}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title-page» (to ".title-page")
% (vivp 1 "title-page")
% (viv "title-page")
{\Huge {\bf Logic for Children}}
(i.e., for people without mathematical maturity ---
a workshop at UniLog 2018)
%
$$
\begin{tabular}[b]{c}
% (xz "~/LATEX/2018vichy-video-edrx.jpg")
\includegraphics[width=2cm]{2018vichy-video-edrx.jpg} \\
Eduardo \\ Ochs \\
\end{tabular}
\quad
\begin{tabular}[b]{c}
% (xz "~/LATEX/2018vichy-video-lucatelli.jpg")
\includegraphics[width=2cm]{2018vichy-video-lucatelli.jpg} \\
Fernando \\ Lucatelli \\
\end{tabular}
\quad
\begin{tabular}[b]{c}
% (xz "~/LATEX/2018vichy-video-selana.jpg")
\includegraphics[width=2cm]{2018vichy-video-selana.jpg} \\
Selana \\ Ochs \\
\end{tabular}
$$
\newpage
\noedrxfooter
% __ ___ ___
% \ \ / / |__ _ |__ \
% \ \ /\ / /| '_ \| | | |/ /
% \ V V / | | | | |_| |_|
% \_/\_/ |_| |_|\__, (_)
% |___/
%
% «why» (to ".why")
% (vivp 2)
{\bf Why?}
\ssk
\par Many years ago...
\par Non-Standard Analysis
\par $→$ Ultrapowers
\par $→$ Filter-powers
\par $→$ Toposes
\par $→$ Johnstone's ``Topos Theory''
\newpage
% __ ___ ___ ____
% \ \ / / |__ _ |__ \ |___ \
% \ \ /\ / /| '_ \| | | |/ / __) |
% \ V V / | | | | |_| |_| / __/
% \_/\_/ |_| |_|\__, (_) |_____|
% |___/
%
% «why-2» (to ".why-2")
% (vivp 3)
{\bf Why?}
\ssk
\par Many years ago...
\par Non-Standard Analysis
\par $→$ Ultrapowers
\par $→$ Filter-powers
\par $→$ Toposes
\par $→$ Johnstone's ``Topos Theory''
\par $→$ FAR too abstract for me
\newpage
% __ ___ ___ _____
% \ \ / / |__ _ |__ \ |___ /
% \ \ /\ / /| '_ \| | | |/ / |_ \
% \ V V / | | | | |_| |_| ___) |
% \_/\_/ |_| |_|\__, (_) |____/
% |___/
%
% «why-3» (to ".why-3")
% (vivp 4)
{\bf Why?}
\ssk
\par Many years ago...
\par Non-Standard Analysis
\par $→$ Ultrapowers
\par $→$ Filter-powers
\par $→$ Toposes
\par $→$ Johnstone's ``Topos Theory''
\par $→$ FAR too abstract for me
\par $→$ {\bf I NEED A VERSION FOR CHILDREN OF THIS}
\newpage
% __ ___ ___ _____
% \ \ / / |__ _ |__ \ |___ /
% \ \ /\ / /| '_ \| | | |/ / |_ \
% \ V V / | | | | |_| |_| ___) |
% \_/\_/ |_| |_|\__, (_) |____/
% |___/
%
% «why-3» (to ".why-3")
% (vivp 5)
{\bf Why?}
\ssk
\par Many years ago...
\par Non-Standard Analysis
\par $→$ Ultrapowers
\par $→$ Filter-powers
\par $→$ Toposes
\par $→$ Johnstone's ``Topos Theory''
\par $→$ FAR too abstract for me
\par $→$ {\bf I NEED A VERSION \ColorRed{FOR CHILDREN} OF THIS}
\newpage
% ____ _ _
% | _ \ _ __ ___ (_) ___ ___| |_
% | |_) | '__/ _ \| |/ _ \/ __| __|
% | __/| | | (_) | | __/ (__| |_
% |_| |_| \___// |\___|\___|\__|
% |__/
%
% «bigger-project» (to ".bigger-project")
% (vivp 6)
With time this became
\ssk
{\Large {\bf A MUCH BIGGER}}
project...
\msk
Some subtasks:
{\def\Sub#1{}
1. Find the right definition of ``children''
\Sub{(inspired by how I function)}
2. Develop a basic toolbox
\Sub{(and name its tools)}
3. Make these things publishable
\Sub{(make them look formal and non-trivial)}
}
\newpage
% (vivp 7 "bigger-project")
% (viv "bigger-project")
With time this became
\ssk
{\Large {\bf A MUCH BIGGER}}
project...
\msk
Some subtasks:
{\def\Sub#1{\quad\ColorGray{#1}}
1. Find the right definition of ``children''
\Sub{(inspired by how I function)}
2. Develop a basic toolbox
\Sub{(and name its tools)}
3. Make these things publishable
\Sub{(make them look formal and non-trivial)}
}
\newpage
% _ _ _ _
% / \ __| |_ _| | |_ ___
% / _ \ / _` | | | | | __/ __|
% / ___ \ (_| | |_| | | |_\__ \
% /_/ \_\__,_|\__,_|_|\__|___/
%
% «adults» (to ".adults")
% (vivp 8)
{\bf The opposite of ``children''}
The opposite of ``children'' is
``\ColorRed{adults}'', or ``\ColorRed{mathematicians}''.
% An ``adult'' feels that everything
A ``mathematician'' feels that everything
should be done as generally and as abstractly
as possible --- and doing otherwise is {\sl bad style}.
\newpage
% (vivp 9)
{\bf The opposite of ``children''}
The opposite of ``children'' is
``\ColorRed{adults}'', or ``\ColorRed{mathematicians}''.
% An ``adult'' feels that everything
A ``mathematician'' feels that everything
should be done as generally and as abstractly
as possible --- and doing otherwise is {\sl bad style}.
\msk
Example: finding a right adjoint by
guesswork / trial and error...
\msk
One expression that I love is: ``{\sl this step
(or argument) offends adults}''.
\newpage
% ____ _ _ _ _
% / ___| |__ (_) | __| |_ __ ___ _ __
% | | | '_ \| | |/ _` | '__/ _ \ '_ \
% | |___| | | | | | (_| | | | __/ | | |
% \____|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «children» (to ".children")
% (vivp 10 "children")
% (viv "children")
{\bf Task 1: The right 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)
\newpage
% «children-2» (to ".children-2")
% (vivp 11 "children-2")
% (viv "children-2")
{\bf Task 1: The right 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
% _____ _ _
% |_ _|__ ___ | | |__ _____ __
% | |/ _ \ / _ \| | '_ \ / _ \ \/ /
% | | (_) | (_) | | |_) | (_) > <
% |_|\___/ \___/|_|_.__/ \___/_/\_\
%
% «toolbox» (to ".toolbox")
% (vivp 12)
{\bf Task 2: Develop a basic toolbox}
I'm starting with ``Category Theory for children''
because I am a categorist, and
because CT uses diagrams and generalizations {\sl a lot}...
\msk
Basic tools:
Use \ColorRed{parallel diagrams},
\ColorRed{positional notations},
\ColorRed{internal views},
\ColorGray{archetypal cases}...
\msk
\ColorGreen{(I'll show some diagrams soon)}
\newpage
% ____ _ _ _ _
% | _ \ _ _| |__ | (_)___| |__
% | |_) | | | | '_ \| | / __| '_ \
% | __/| |_| | |_) | | \__ \ | | |
% |_| \__,_|_.__/|_|_|___/_| |_|
%
% «publish» (to ".publish")
% (vivp 13)
{\bf Task 3: Find ways to publish this}
CT books treat examples very briefly,
as if they were trivial exercises... ${=}($
Ideas: do things ``for children'' and ``for adults''
in parallel, find ways to {\sl transfer knowledge}
between the two approaches...
\msk
\ColorGreen{(Non-standard Analysis has transfer theorems
between the standard universe, $\Set$, and $\Set^\calU/\calI$)}
\newpage
% ____ _ _ _ _ ____
% | _ \ _ _| |__ | (_)___| |__ |___ \
% | |_) | | | | '_ \| | / __| '_ \ __) |
% | __/| |_| | |_) | | \__ \ | | | / __/
% |_| \__,_|_.__/|_|_|___/_| |_| |_____|
%
% «publish-2» (to ".publish-2")
% (vivp 14)
{\bf Task 3: Find ways to publish this}
CT books treat examples very briefly,
as if they were trivial exercises... ${=}($
Ideas: do things ``for children'' and ``for adults''
in \ColorRed{parallel}, find ways to \ColorRed{\sl transfer knowledge}
between the two approaches...
%
\def\tm #1#2{ \begin{tabular}{#1}#2\end{tabular}}
\def\ptm#1#2{\left (\begin{tabular}{#1}#2\end{tabular}\right )}
\def\smm#1#2{\sm{\text{#1}\\\text{#2}}}
%
$$\ptm{c}{particular \\ case \\ ``for children''}
\two/<-`->/<500>^{\smm{particularize}{(easy)}}_{\smm{generalize}{(hard)}}
\ptm{c}{general \\ case \\ ``for adults''}
$$
The diagrams for the general case and for a particular case
{\sl have the same shape!!!}
\newpage
% _ __ _ _ _
% _ __ ___ ___| |_ / / __ _ __| |_ _| | |_ ___
% | '__/ _ \/ __| __| / / / _` |/ _` | | | | | __/ __|
% | | | __/\__ \ |_ / / | (_| | (_| | |_| | | |_\__ \
% |_| \___||___/\__| /_/ \__,_|\__,_|\__,_|_|\__|___/
%
% «rest-adults» (to ".rest-adults")
% (vivp 15)
{\bf In the rest of these slides...}
...we will show an example:
\ColorRed{Geometric Morphisms} for children!
($↑$ a thing from Topos Theory)
\newpage
% __ ______ __ __
% \ \ / / ___| \/ |
% \ \ / / | _| |\/| |
% \ V /| |_| | | | |
% \_/ \____|_| |_|
%
% «VGM» (to ".VGM")
% (vivp 16)
{\bf Visualizing Geometric Morphisms}
An application:
\ColorRed{Sheaves} and \ColorRed{Geometric Morphisms}
$↑$ two parts of Topos Theory that look
{\sl incredibly abstract} at first
% \msk
\ColorGray{
(Btw, I'll give a talk at the ``Logic and Categories''
workshop about that)
}
\msk
Trick:
Start with presheaves {\sl that are easy to visualize;}
Start with a very small, planar category like this...
\newpage
% __ ______ __ __ ____
% \ \ / / ___| \/ | |___ \
% \ \ / / | _| |\/| | __) |
% \ V /| |_| | | | | / __/
% \_/ \____|_| |_| |_____|
%
% «VGM-2» (to ".VGM-2")
% (vivp 17)
% (find-angg "LUA/texinfo.lua" "preproc")
{\bf Visualizing Geometric Morphisms}
\ColorRed{Trick: positional notations}
Start with presheaves {\sl that are easy to visualize;}
Start with a very small, planar category like this,
%
%L sesw = {[" w"]="↙", [" e"]="↘"}
%
%R local B, BF = 3/ 1 \, 3/ F_1 \
%R | w e | | w e |
%R | 2 3 | |F_2 F_3 |
%R | e w e | | e w e |
%R | 4 5 | | F_4 F_5|
%R | e w | | e w |
%R \ 6 / \ F_6 /
%R
%R B:tozmp({def="Bbig", scale="10pt", meta="p"}):addcells(sesw):output()
$$\pu \catB = \Bbig
$$
{\color{GrayLight}
Technicalities:
$\catB$ is a preorder
}
\newpage
% __ ______ __ __ _____
% \ \ / / ___| \/ | |___ /
% \ \ / / | _| |\/| | |_ \
% \ V /| |_| | | | | ___) |
% \_/ \____|_| |_| |____/
%
% «VGM-3» (to ".VGM-3")
% (vivp 18)
{\bf Visualizing Geometric Morphisms}
...and now a presheaf $F$ on $\catB$
can be drawn like this...
%
%R local B, BF = 3/ 1 \, 3/ F_1 \
%R | w e | | w e |
%R | 2 3 | |F_2 F_3 |
%R | e w e | | e w e |
%R | 4 5 | | F_4 F_5|
%R | e w | | e w |
%R \ 6 / \ F_6 /
%R
%R B :tozmp({def="Bmed", scale="7pt", meta="s p"}):addcells(sesw):output()
%R BF:tozmp({def="BF", scale="7pt", meta="s p"}):addcells(sesw):output()
$$\pu \catB = \Bmed \qquad F = \BF
$$
\newpage
% __ ______ __ __ _ _
% \ \ / / ___| \/ | | || |
% \ \ / / | _| |\/| | | || |_
% \ V /| |_| | | | | |__ _|
% \_/ \____|_| |_| |_|
%
% «VGM-4» (to ".VGM-4")
% (vivp 19)
{\bf Visualizing Geometric Morphisms}
...and now a presheaf $F$ on $\catB$
can be drawn like this...
%
%R local B, BF = 3/ 1 \, 3/ F_1 \
%R | w e | | w e |
%R | 2 3 | |F_2 F_3 |
%R | e w e | | e w e |
%R | 4 5 | | F_4 F_5|
%R | e w | | e w |
%R \ 6 / \ F_6 /
%R
%R B :tozmp({def="Bmed", scale="7pt", meta="s p"}):addcells(sesw):output()
%R BF:tozmp({def="BF", scale="7pt", meta="s p"}):addcells(sesw):output()
$$\pu \catB = \Bmed \qquad F = \BF
$$
{\color{GrayLight}
Technicalities:
$F_1, F_2, \ldots, F_6$ are sets,
the `$F_i→F_j$'s are functions,
$F:\catB→\Set$, i.e., $F∈\Set^{\catB}$,
And there may be an `$\op$' omitted somewhere
}
% \newpage
%
% {\bf Visualizing Geometric Morphisms}
%
% ...and now a presheaf $F$ on $\catB$
%
% can be drawn like this...
% %
% %R local B, BF = 3/ 1 \, 3/ F_1 \
% %R | w e | | w e |
% %R | 2 3 | |F_2 F_3 |
% %R | e w e | | e w e |
% %R | 4 5 | | F_4 F_5|
% %R | e w | | e w |
% %R \ 6 / \ F_6 /
% %R
% %R B :tozmp({def="Bmed", scale="7pt", meta="s p"}):addcells(sesw):output()
% %R BF:tozmp({def="BF", scale="7pt", meta="s p"}):addcells(sesw):output()
% $$\pu \catB = \Bmed \qquad F = \BF
% $$
\newpage
% __ ______ __ __ ____
% \ \ / / ___| \/ | | ___|
% \ \ / / | _| |\/| | |___ \
% \ V /| |_| | | | | ___) |
% \_/ \____|_| |_| |____/
%
% «VGM-5» (to ".VGM-5")
% (vivp 20)
{\bf Visualizing Geometric Morphisms}
...choose a subcategory $\catA$ of $\catB$, e.g., the one below.
Then a presheaf $G$ on $\catA$ can be drawn as:
%
%R local B, BF, BG = 3/ 1 \, 3/ F_1 \, 3/ !Gt \
%R | w e | | w e | | w e |
%R | 2 3 | |F_2 F_3 | |G_2 G_3 |
%R | e w e | | e w e | | e w e |
%R | 4 5 | | F_4 F_5| | G_4 G_5|
%R | e w | | e w | | e w |
%R \ 6 / \ F_6 / \ 1 /
%R
%R local A, AG, AF = 3/ 2 3 \, 3/G_2 G_3 \, 3/F_2 F_3 \
%R | e w e | | e w e | | e w e |
%R \ 4 5 / \ G_4 G_5/ \ F_4 F_5/
%R
%R
%R B :tozmp({def="Bmed", scale="7pt", meta="s p"}):addcells(sesw):output()
%R BF:tozmp({def="BF", scale="7pt", meta="s p"}):addcells(sesw):output()
%R BG:tozmp({def="BG", scale="7pt", meta="s p"}):addcells(sesw):output()
%R A :tozmp({def="Amed", scale="7pt", meta="s p"}):addcells(sesw):output()
%R AG:tozmp({def="AG", scale="7pt", meta="s p"}):addcells(sesw):output()
%R AF:tozmp({def="AF", scale="7pt", meta="s p"}):addcells(sesw):output()
\def\Gt{G_2 {×_{G_4}} G_3}
\pu
$$\catB = \Bmed \qquad F = \BF
$$
$$\catA = \Amed \qquad G = \AG
$$
{\color{GrayLight}
Technicalities: too many ${=}($
}
\newpage
% __ ______ __ __ __
% \ \ / / ___| \/ | / /_
% \ \ / / | _| |\/| | | '_ \
% \ V /| |_| | | | | | (_) |
% \_/ \____|_| |_| \___/
%
% «VGM-6» (to ".VGM-6")
% (vivp 21)
{\bf Visualizing Geometric Morphisms}
...and the inclusion $f:\catA→\catB$
induces a geometric morphism $f:\Set^\catA→\Set^\catB$,
that ``is'' an adjunction $f^*⊣f_*$:
%
$$\Set^\catA
\two/<-`->/<200>^{f^*}_{f_*}
\Set^\catB
$$
...where $f^*$ is ``obvious'' \ColorGray{(for some value of ``obvious'')}
and $f_*$ can be obtained by \ColorRed{trial and error} if we don't
understand Kan Extensions...
Kan Extensions: \ColorRed{for adults}
Trial and error: \ColorRed{for children}
\newpage
% ___ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| |
% | || '_ \| __/ _ \ '__| '_ \ / _` | |
% | || | | | || __/ | | | | | (_| | |
% |___|_| |_|\__\___|_| |_| |_|\__,_|_|
%
% «internal-views» (to ".internal-views")
% (vivp 22 "internal-views")
% (viv "internal-views")
{\bf Interlude: internal views}
The best way to explain the adjunction of the
previous slide to children is through \ColorRed{\sl internal views}.
The internal view of the \ColorRed{function} $√{}:\N→\R$ is:
%
\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
$$\pu
\resizebox{2.2cm}{!}{$\diag{second-blob-function}$}
$$
(`$↦$'s take elements of a blob-set to another blob-set)
% Internal views of \ColorRed{functors} have blob-{\sl categories}.
\newpage
% «internal-views-functors» (to ".internal-views-functors")
% (vivp 23)
{\bf Interlude: internal views}
Internal views of \ColorRed{functors} have blob-\ColorRed{categories}
instead of blob-\ColorRed{sets}, like this:
\unitlength=10pt
%D diagram ??
%D 2Dx 100 +40
%D 2D 100 A FA
%D 2D
%D 2D +30 B FB
%D 2D
%D 2D +20 \catC \catD
%D 2D
%D
%D (( A FA |->
%D B FB |->
%D A FB harrownodes nil 18 nil |->
%D A B -> .plabel= l g
%D FA FB -> .plabel= r Fg
%D \catC \catD -> .plabel= a F
%D A B midpoint .TeX= \myoval(3.4,7)(1.7,3.5)[1] place
%D FA FB midpoint .TeX= \myoval(3.4,7)(1.7,3.5)[1] place
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\newpage
% «internal-views-functors-2» (to ".internal-views-functors-2")
% (vivp 24)
{\bf Interlude: internal views}
We draw the internal view of $F:\catC → \catD$ as this,
%D diagram ??
%D 2Dx 100 +25
%D 2D 100 A FA
%D 2D
%D 2D +20 B FB
%D 2D
%D 2D +15 \catC \catD
%D 2D
%D
%D (( A FA |->
%D B FB |->
%D # A FB harrownodes nil 18 nil |->
%D A B -> .plabel= l g
%D FA FB -> .plabel= r Fg
%D \catC \catD -> .plabel= a F
%D # A B midpoint .TeX= \myoval(3.4,7)(1.7,3.5)[1] place
%D # FA FB midpoint .TeX= \myoval(3.4,7)(1.7,3.5)[1] place
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\msk
we omit the blobs (the ``{\unitlength=5pt\myoval(1,2)(0.5,1)[0.3]}''s), and we draw
the internal view --- objects and maps in $\catC$ and $\catD$ ---
above the external view ($F:\catC→\catD$).
\newpage
% «internal-views-gm» (to ".internal-views-gm")
% (vivp 25 "internal-views-gm")
% (viv "internal-views-gm")
{\bf Internal views}
Here is the internal view of the
geometric morphism $f:\Set^\catA→\Set^\catB$...
remember that $f$ is an adjunction $f^*⊣f_*$.
%D diagram GM-particular
%D 2Dx 100 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D ren A0 A1 ==> f^*F F
%D ren A2 A3 ==> G f_*G
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D
%D (( A0 A1 <-
%D A2 A3 ->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D
%D ))
%D enddiagram
%D
%D diagram GM-general
%D 2Dx 100 +35
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D ren A0 A1 ==> f^*F F
%D ren A2 A3 ==> G f_*G
%D ren A4 A5 ==> \calF \calE
%D
%D (( A0 A1 <-
%D A2 A3 ->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D
%D ))
%D enddiagram
%D
\pu
$$%\pu
\resizebox{!}{50pt}{$
\begin{array}{ccc}
\diag{GM-particular}&
\quad&
\ColorGray{
\diag{GM-general}
}
\\
\\
\ColorGray{\text{(particular case)}}&&
\ColorGray{\text{(general case)}}\\
\end{array}
$}
$$
\newpage
% «internal-views-gm-2» (to ".internal-views-gm-2")
% (vivp 26 "internal-views-gm-2")
% (viv "internal-views-gm-2")
{\bf A geometric morphism (for children)}
%D diagram GM-children-big
%D 2Dx 100 +55
%D 2D 100 A0 A1
%D 2D
%D 2D +45 A2 A3
%D 2D
%D 2D +25 A4 A5
%D 2D
%D ren A0 A1 ==> \AF \BF
%D ren A2 A3 ==> \AG \BG
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D
%D (( A0 A1 <-|
%D A2 A3 |->
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D
%D ))
%D enddiagram
%D
$$\pu
\resizebox{!}{70pt}{$
\begin{array}{ccc}
\diag{GM-children-big}&
\qquad
\qquad&
\diag{GM-general}\\
\\
\text{(for children)}&&
\text{(for adults)}\\
\end{array}
$}
$$
\newpage
% (vivp 27)
{\bf Resources about the workshop}
Here:
\url{http://angg.twu.net/logic-for-children-2018.html}
Cheers! $=)$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "viv"
% End: