% (find-angg "LATEX/2018vichy-vgms-slides.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018vichy-vgms-slides.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018vichy-vgms-slides.pdf"))
% (defun e () (interactive) (find-LATEX "2018vichy-vgms-slides.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018vichy-vgms-slides"))
% (find-xpdfpage   "~/LATEX/2018vichy-vgms-slides.pdf")
% (find-sh0 "cp -v  ~/LATEX/2018vichy-vgms-slides.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2018vichy-vgms-slides.pdf /tmp/pen/")
% (find-sh0 "cp -v  ~/LATEX/2018vichy-vgms-slides.pdf /tmp/pen/ochs-talk-cats.pdf")
%   file:///home/edrx/LATEX/2018vichy-vgms-slides.pdf
%               file:///tmp/2018vichy-vgms-slides.pdf
%           file:///tmp/pen/2018vichy-vgms-slides.pdf
% http://angg.twu.net/LATEX/2018vichy-vgms-slides.pdf
% (find-fline "~/.emacs" "\"vgm\"")

% «.colors»			(to "colors")
% «.myoval»			(to "myoval")
% «.title-page»			(to "title-page")
%
% «.LCT-for-children»		(to "LCT-for-children")
% «.PHAfC»			(to "PHAfC")
% «.PHAfC-2»			(to "PHAfC-2")
% «.local-operators»		(to "local-operators")
% «.ZCategories»		(to "ZCategories")
% «.ZPresheaves»		(to "ZPresheaves")
% «.internal-views»		(to "internal-views")
% «.internal-views-2»		(to "internal-views-2")
% «.internal-views-3»		(to "internal-views-3")
% «.internal-views-4»		(to "internal-views-4")
% «.parallel»			(to "parallel")
% «.first-gm»			(to "first-gm")
% «.a-factorization»		(to "a-factorization")
% «.factorization-2»		(to "factorization-2")
% «.factorization-3»		(to "factorization-3")
% «.factorization-4»		(to "factorization-4")
% «.surjection-inclusion»	(to "surjection-inclusion")
% «.dense-closed»		(to "dense-closed")

% «.cats-for-children»		(to "cats-for-children")
% «.on-children»		(to "on-children")
% «.tools»			(to "tools")

\documentclass[oneside]{book}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
\usepackage{svgcolor}             % (find-es "tex" "svgcolor")
\usepackage[colorlinks,urlcolor=brown]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
%\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")
\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=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{dednat6dir = "dednat6/"}
% \directlua{dofile(dednat6dir.."dednat6.lua")}
% \directlua{texfile(tex.jobname)}
% \directlua{verbose()}
% \directlua{output(preamble1)}
% \def\expr#1{\directlua{output(tostring(#1))}}
% \def\eval#1{\directlua{#1}}
% \def\pu{\directlua{pu()}}
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

\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}%
  }}

\catcode`•=13 \def•{\ensuremath{\bullet}}

\def\calA{\mathcal{A}}
\def\calB{\mathcal{B}}
\def\calC{\mathcal{C}}
\def\calD{\mathcal{D}}
\def\bbG{\mathbb{G}}
\def\antitabular{\hskip-5.5pt}

\setlength{\parindent}{0em}


%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page» (to ".title-page")
% (find-es "tex" "huge")

\begin{center}

{\Large {\bf Visualizing Geometric Morphisms}}

% {\large {\bf (An application of ``Logic for Children'')}}

{\large
 An application of the ``Logic for Children''

 project to Category Theory
}

\msk

\ColorGray{(talk @ ``Logic and Categories'' workshop, UniLog 2018)}

\bsk


%$$
  \text{By:}
  \quad
  \begin{tabular}{c}
    % (xz              "~/LATEX/2018vichy-video-edrx.jpg")
    \includegraphics[height=50pt]{2018vichy-video-edrx.jpg} \\
    Eduardo \\ Ochs \\ (UFF, Brazil)
  \end{tabular}
  \quad
  \begin{tabular}{c}
    % (xz              "~/LATEX/2018vichy-video-selana.jpg")
    \includegraphics[height=50pt]{2018vichy-video-selana.jpg} \\
    Selana \\ 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}
%$$

\end{center}



\newpage

%  _____                 _     _ _     _                
% |  ___|__  _ __    ___| |__ (_) | __| |_ __ ___ _ __  
% | |_ / _ \| '__|  / __| '_ \| | |/ _` | '__/ _ \ '_ \ 
% |  _| (_) | |    | (__| | | | | | (_| | | |  __/ | | |
% |_|  \___/|_|     \___|_| |_|_|_|\__,_|_|  \___|_| |_|
%                                                       
% «LCT-for-children» (to ".LCT-for-children")
% (vgsp 2 "LCT-for-children")
% (vgs    "LCT-for-children")

\noedrxfooter

{\bf Logic / categories / toposes for children}

({\sl Very} short version; for the long version see

the resources for the ``Logic for Children'' workshop)

\msk

\par Many years ago...
\par Non-Standard Analysis
% \par $→$ Toposes
\par $→$ Johnstone's ``Topos Theory''
\par $→$ FAR too abstract for me
\par $→$ {\bf I NEED A VERSION \ColorRed{FOR CHILDREN} OF THIS}

\msk

\ColorRed{For Children:} using ``internal views'' and

examples with finite objects that are easy to draw

Heyting Algebras that are subset of $\Z^2$ \ColorGray{(paper)}

Presheaves that can be drawn on a subset of $\Z^2$ \ColorGray{(new)}




\newpage

%  ______   _    _        
% |__  / | | |  / \   ___ 
%   / /| |_| | / _ \ / __|
%  / /_|  _  |/ ___ \\__ \
% /____|_| |_/_/   \_\___/
%                         
% «PHAfC» (to ".PHAfC")

{\bf Planar Heyting Algebras for Children}

($↑$ paper submitted in 2017 ---

\url{http://angg.twu.net/math-b.html})

\msk

\unitlength=8pt
\def\closeddot{\circle*{0.7}}

$
  \antitabular
  \begin{tabular}[c]{l}
    Main definition:                                 \\
    A ZHA is a finite subset of $\Z^2$               \\
    made of all even points ($x+y=2k$)               \\
    between $(0,0)$ and $⊤$                          \\
    between a ``left'' and a ``right wall''.         \\
    (The ``Z'' in \ColorRed{Z}HA means ``$⊂\Z^2$'')  \\[5pt]
    Main theorems:                                   \\
    every ZHA is a Heyting Algebra                   \\
    every ZHA is a topology in disguise              \\
  \end{tabular}
  \qquad
  \begin{tabular}{c}
    $\picturedotsa(-3,0)(3,7){
              0,6
          -1,5   1,5
              0,4   2,4
          -1,3   1,3
      -2,2    0,2   2,2
          -1,1   1,1
              0,0
     }
    $ \\[32pt]
    $↑$ a ZHA
  \end{tabular}
$

\newpage

%  ______   _    _          ____  
% |__  / | | |  / \   ___  |___ \ 
%   / /| |_| | / _ \ / __|   __) |
%  / /_|  _  |/ ___ \\__ \  / __/ 
% /____|_| |_/_/   \_\___/ |_____|
%                                 
% «PHAfC-2» (to ".PHAfC-2")

{\bf Planar Heyting Algebras for Children}

($↑$ Very good paper! No prerequisites!

Lots of fun! Go read it!)

\msk

%R local PQaoi =
%R     1/    T    \, 1/    T    \, 1/ T   \
%R      |   . .   |   |   . .   |   |  .  | 
%R      |  . . .  |   |  . . .  |   | . . | 
%R      | . o . i |   | . o . . |   |d . n| 
%R      |. P . . .|   |. P . . .|   | P . | 
%R      | . . Q . |   | . . Q . |   \  F  / 
%R      |  . a .  |   |  . . .  |           
%R      |   . .   |   |   . .   |           
%R      \    F    /   \    F    /           
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R            T="·", F="·", T="⊤", F="⊥", }
%R PQaoi:tozmp({def="PQaoi", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PQaoi:tozmp({def="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
\pu

$
  \antitabular
  \begin{tabular}[c]{l}
    Most toposes have more           \\
    than two truth-values and        \\
    an intuitionistic logic.         \\[5pt]
    The paper PHAfC shows how        \\
    to visualize this (on ZHAs).     \\
    It uses LR-coordinates and       \\
    shows how the `$→$' on ZHAs      \\
    can be calculated quickly        \\
    using a formula with four cases. \\
    % It doesn't mention categories.   \\
  \end{tabular}
  % \quad
  \resizebox{!}{2.2cm}{$
    \begin{array}{c}
      \lozfive
      \qquad\qquad
      \qquad\qquad
      \\[-10pt]
      \qquad\qquad
      \qquad\qquad
      \PQaoi
    \end{array}
  $}
$

\newpage

%  ____  _   _    _     __  ____   ____  
% |  _ \| | | |  / \   / _|/ ___| |___ \ 
% | |_) | |_| | / _ \ | |_| |       __) |
% |  __/|  _  |/ ___ \|  _| |___   / __/ 
% |_|   |_| |_/_/   \_\_|  \____| |_____|
%                                        
% «local-operators» (to ".local-operators")

{\bf Planar Heyting Algebras for Children 2:}

{\bf Local Operators}

%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()

$
  \pu
  \antitabular
  \begin{tabular}[c]{l}
    The second paper in the series.      \\[5pt]
    Sheaves {\sl correspond} to local    \\
    operators on HAs.                    \\[5pt]
    A local operator on a ZHA            \\
    corresponds to slashing the ZHA      \\
    by diagonal cuts and blurring        \\
    the distinction between              \\
    the truth-values in each region.     \\[5pt]
    PHAfC doesn't mention categories.    \\
    PHAfC2 doesn't mention categories \ColorRed{yet}. \\
  \end{tabular}
  % \quad
  \resizebox{!}{2.2cm}{$
    \begin{array}{c}
      \ZQuotients
    \end{array}
  $}
$

\newpage

%  _________      _       
% |__  / ___|__ _| |_ ___ 
%   / / |   / _` | __/ __|
%  / /| |__| (_| | |_\__ \
% /____\____\__,_|\__|___/
%                         
% «ZCategories» (to ".ZCategories")
% (vgmp 6 "ZCategories")
% (vgm    "ZCategories")

{\bf ZCategories}

%D diagram ZCatPB
%D 2Dx     100 +20 +20
%D 2D  100 o1
%D 2D
%D 2D  +20     o2  o3
%D 2D
%D 2D  +20     o4  o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> 1 2 3 4 5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D    o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram

%D diagram ZPresheaf
%D 2Dx     100 +20 +20
%D 2D  100 o1
%D 2D
%D 2D  +20     o2  o3
%D 2D
%D 2D  +20     o4  o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> F_1 F_2 F_3 F_4 F_5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D    o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram

\pu

$
  \antitabular
  \begin{tabular}[c]{l}
    Choose a finite subset of $\Z^2$.    \\
    (Optional step: rename its points.)  \\
    Use this set as the set of objects   \\
    of a category.                       \\
    Add a finite set of arrows.          \\
    This is a \ColorRed{ZCategory}.      \\
    The $\Z^2$-coordinates tell          \\
    how to draw it.                      \\
  \end{tabular}
  \quad
  \diag{ZCatPB}
$

\newpage

%  _________                _                               
% |__  /  _ \ _ __ ___  ___| |__   ___  __ ___   _____  ___ 
%   / /| |_) | '__/ _ \/ __| '_ \ / _ \/ _` \ \ / / _ \/ __|
%  / /_|  __/| | |  __/\__ \ | | |  __/ (_| |\ V /  __/\__ \
% /____|_|   |_|  \___||___/_| |_|\___|\__,_| \_/ \___||___/
%                                                           
% «ZPresheaves» (to ".ZPresheaves")
% (vgmp 7 "ZPresheaves")
% (vgm    "ZPresheaves")

{\bf ZPresheaves and ZToposes}

A ZPresheaf is a functor $F:\catA → \Set$,

where $\catA$ is a ZCategory.

(Obs: not $F:\catA^{\ColorRed\op} → \Set$!)

A ZPresheaf $F$ inherits its drawing instructions from $\catA$.

\ColorGray{(``Positional notations'')}
%
$$
  \resizebox{!}{35pt}{$
    \catA =
    \left(
    \diag{ZCatPB}
    \right)
    \quad
    F =
    \left(
    \diag{ZPresheaf}
    \right)
  $}
$$

A ZTopos is a category $\Set^\catA$ where $\catA$ is a ZCategory.

\newpage

%  ___       _                        _ 
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| |
%  | || '_ \| __/ _ \ '__| '_ \ / _` | |
%  | || | | | ||  __/ |  | | | | (_| | |
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_|
%                                       
% «internal-views» (to ".internal-views")
% (find-LATEX "2018vichy-video.tex" "internal-views")
% (find-LATEX "2018vichy-video.tex" "internal-views-2")

{\bf Internal views}

(Part 1: functions)

\unitlength=10pt

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     a0 a5 midpoint .TeX= \myoval(3.4,10)(1.7,5)[1.5] place
%D    b-1 b5 midpoint .TeX= \myoval(3.4,11)(1.7,5.5)[1.5] 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
$$\scalebox{0.7}{$\diag{second-blob-function}$}
$$

(`$↦$'s take elements of a blob-set to another blob-set)



\newpage

%  ___       _                        _   ____  
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| | |___ \ 
%  | || '_ \| __/ _ \ '__| '_ \ / _` | |   __) |
%  | || | | | ||  __/ |  | | | | (_| | |  / __/ 
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_| |_____|
%                                               
% «internal-views-2» (to ".internal-views-2")
% (vgmp 9 "internal-views-2")
% (vgm    "internal-views-2")

{\bf Internal views}

(Part 2: functors)

Internal views of \ColorRed{functors} have blob-\ColorRed{categories}

instead of blob-\ColorRed{sets}. Compare:

%D diagram internal-view-F
%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
%D diagram internal-view-F-noblobs
%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
$$\scalebox{0.7}{$\diag{second-blob-function}$}
  \qquad
  \qquad
  \scalebox{0.7}{$\diag{internal-view-F}$}
$$


\newpage

%  ___       _                        _   _____ 
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| | |___ / 
%  | || '_ \| __/ _ \ '__| '_ \ / _` | |   |_ \ 
%  | || | | | ||  __/ |  | | | | (_| | |  ___) |
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_| |____/ 
%                                               
% «internal-views-3» (to ".internal-views-2")

{\bf Internal views}

(Part 3: omitting the blobs)

$$\scalebox{0.9}{$\diag{internal-view-F}$}
  \qquad
  \quad
  \scalebox{0.9}{$\diag{internal-view-F-noblobs}$}
$$

\newpage

%  ___       _                        _   _  _   
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| | | || |  
%  | || '_ \| __/ _ \ '__| '_ \ / _` | | | || |_ 
%  | || | | | ||  __/ |  | | | | (_| | | |__   _|
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_|    |_|  
%                                                
% «internal-views-4» (to ".internal-views-4")
% (vgsp 11 "internal-views-4")
% (vgs     "internal-views-4")

{\bf Internal views}

(Part 4: adjunctions)

Left: generic adjunction $L⊣R$

Middle: generic geometric morphism $f^*⊣f_*$

Right: g.m. between toposes $\Set^\catA$ and $\Set^\catB$
%
%D diagram adjunctions
%D 2Dx     100 +25     +30 +25     +30 +30     
%D 2D  100 A0  A1      B0  B1      C0  C1      
%D 2D                                          
%D 2D  +20 A2  A3      B2  B3      C2  C3      
%D 2D                                          
%D 2D  +15 A4  A5      B4  B5      C4  C5      
%D 2D
%D 2D  +20                         C6  C7
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> LC C D RD \catD \catC
%D ren B0 B1 B2 B3 B4 B5 ==> f^*F F G f_*G \mathcal{E} \mathcal{F}
%D ren C0 C1 C2 C3 C4 C5 ==> f^*F F G f_*G \Set^\catA  \Set^\catB
%D ren C6 C7 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D    A0 A2 ->  A1 A3 ->
%D    A2 A3 |->
%D    A4 A5 <- sl^ .plabel= a L
%D    A4 A5 -> sl_ .plabel= b R
%D    A0 A3 harrownodes nil 20 nil <->
%D
%D    B0 B1 <-|
%D    B0 B2 ->  B1 B3 ->
%D    B2 B3 |->
%D    B4 B5 <- sl^ .plabel= a f^*
%D    B4 B5 -> sl_ .plabel= b f_*
%D    B0 B3 harrownodes nil 20 nil <->
%D
%D    C0 C1 <-|
%D    C0 C2 ->  C1 C3 ->
%D    C2 C3 |->
%D    C4 C5 <- sl^ .plabel= a f^*
%D    C4 C5 -> sl_ .plabel= b f_*
%D    C0 C3 harrownodes nil 20 nil <->
%D    C6 C7 -> .plabel= a f
%D    
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{adjunctions}
$$


\newpage

%  ____                 _ _      _ 
% |  _ \ __ _ _ __ __ _| | | ___| |
% | |_) / _` | '__/ _` | | |/ _ \ |
% |  __/ (_| | | | (_| | | |  __/ |
% |_|   \__,_|_|  \__,_|_|_|\___|_|
%                                          
% «parallel» (to ".parallel")
% (vgmp 12 "parallel")
% (vgm     "parallel")
% (vivp 10 "children")
% (viv     "children")

{\bf Working in two languages in parallel}

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

{\bf Working in two universes in parallel}

In Non-Standard Analysis we have {\sl transfer theorems}

$$\ptm{c}{Standard \\ universe}
  \two/<-`->/<500>
  \ptm{c}{Non-Standard \\ universe \\ (ultrapower)}
$$

\newpage


%  _     _      ____ __  __ 
% / |___| |_   / ___|  \/  |
% | / __| __| | |  _| |\/| |
% | \__ \ |_  | |_| | |  | |
% |_|___/\__|  \____|_|  |_|
%                           
% «first-gm» (to ".first-gm")
% (vgsp 14 "first-gm")
% (vgs     "first-gm")

{\bf Our first geometric morphism}
%
%L sesw = {[" w"]="↙",  [" e"]="↘"}
%
%R local B, F, RG = 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, G, LF = 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 B :tozmp({def="pB",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R F :tozmp({def="pF",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R RG:tozmp({def="pRG", scale="7pt", meta="s p"}):addcells(sesw):output()
%R A :tozmp({def="pA",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R G :tozmp({def="pG",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R LF:tozmp({def="pLF", scale="7pt", meta="s p"}):addcells(sesw):output()
\def\Gt{G_2 {×_{G_4}} G_3}
\pu
%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 2D  +25 A6    A7
%D 2D
%D ren A0 A1 ==> \pLF \pF
%D ren A2 A3 ==> \pG \pRG
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D ren A6 A7 ==> \pA \pB
%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    A6 A7 -> sl^ .plabel= a 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
  \resizebox{!}{70pt}{$
     \begin{array}{ccc}
       \diag{GM-children-big}&
       \qquad
       \qquad&
       \diag{GM-general}\\
       \\
       \text{(for children; inclusion, sheaf)}&&
       \text{(for adults)}\\
     \end{array}
  $}
$$



\newpage

%     _       __            _             _          _   _             
%    / \     / _| __ _  ___| |_ ___  _ __(_)______ _| |_(_) ___  _ __  
%   / _ \   | |_ / _` |/ __| __/ _ \| '__| |_  / _` | __| |/ _ \| '_ \ 
%  / ___ \  |  _| (_| | (__| || (_) | |  | |/ / (_| | |_| | (_) | | | |
% /_/   \_\ |_|  \__,_|\___|\__\___/|_|  |_/___\__,_|\__|_|\___/|_| |_|
%                                                                      
% «a-factorization» (to ".a-factorization")
% (vgmp 15 "a-factorization")
% (vgm     "a-factorization")

{\bf A factorization}

Elephant $=$ Bible

Section A4: Geometric Morphisms

Each `$\diagxyto/->/<200>$' below is a g.m. (an adjunction)

Any g.m. factors as a surjection followed by an inclusion.

Any inclusion factors as a dense g.m.

followed by a closed g.m.\,.
%
%D diagram ??
%D 2Dx     100 +30 +30 +30
%D 2D  100 A0          A3
%D 2D
%D 2D  +12 B0  B1      B3
%D 2D
%D 2D  +12     C1  C2  C3
%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
%D (( A0 A3 -> .plabel= a \text{any}
%D    B0 B1 -> .plabel= a \text{surjection}
%D    B1 B3 -> .plabel= a \text{inclusion}
%D    C1 C2 -> .plabel= a \text{dense}
%D    C2 C3 -> .plabel= a \text{close}
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

The Elephant {\sl constructs} the toposes $\calB$, $\calC$ and the maps.

\newpage

%  _____          _             _          _   _               ____  
% |  ___|_ _  ___| |_ ___  _ __(_)______ _| |_(_) ___  _ __   |___ \ 
% | |_ / _` |/ __| __/ _ \| '__| |_  / _` | __| |/ _ \| '_ \    __) |
% |  _| (_| | (__| || (_) | |  | |/ / (_| | |_| | (_) | | | |  / __/ 
% |_|  \__,_|\___|\__\___/|_|  |_/___\__,_|\__|_|\___/|_| |_| |_____|
%                                                                    
% «factorization-2» (to ".factorization-2")
% (vgmp 16 "factorization-2")
% (vgm     "factorization-2")

{\bf A factorization: version using ZPresheaves}

This would be a nicer theorem --- that if we start

with ZToposes $\Set^\catA$ and $\Set^\catD$ the factorization can be

through ZToposes...

\def\ftext#1#2{\text{$#1$ (#2)}}
\def\ftext#1#2{\text{#2}}

%L forths["=="] = function () pusharrow("==") end
%
%D diagram ??
%D 2Dx     100 +35 +35 +35
%D 2D  100 A0          A3
%D 2D
%D 2D  +20 B0  B1      B3
%D 2D
%D 2D  +20     C1  C2  C3
%D 2D
%D 2D  +20         D2
%D 2D
%D ren A0    A3 ==> \Set^\catA                  \Set^\catD
%D ren B0 B1 B3 ==> \Set^\catA \calB            \Set^\catD
%D ren C1 C2 C3 ==>            \Set^\catB \calC \Set^\catD
%D ren    D2    ==>                       \Set^\catC
%D
%D (( A0 A3 -> .plabel= a \ftext{a}{any}
%D    B0 B1 -> .plabel= a \ftext{s}{surjection}
%D    B1 B3 -> .plabel= a \ftext{i}{inclusion}
%D    C1 C2 -> .plabel= a \ftext{d}{dense}
%D    C2 C3 -> .plabel= a \ftext{c}{closed}
%D    A0 B0 =  A3 B3 =   B1 C1 ==   B3 C3 = C2 D2 ==
%D ))
%D enddiagram
%D
$$\pu
  \resizebox{!}{50pt}{$
  \diag{??}
  $}
$$

\newpage

%  _____          _             _          _   _               _____ 
% |  ___|_ _  ___| |_ ___  _ __(_)______ _| |_(_) ___  _ __   |___ / 
% | |_ / _` |/ __| __/ _ \| '__| |_  / _` | __| |/ _ \| '_ \    |_ \ 
% |  _| (_| | (__| || (_) | |  | |/ / (_| | |_| | (_) | | | |  ___) |
% |_|  \__,_|\___|\__\___/|_|  |_/___\__,_|\__|_|\___/|_| |_| |____/ 
%                                                                    
% «factorization-3» (to ".factorization-3")
% (visp 15)

%  _____          _             _          _   _               _  _   
% |  ___|_ _  ___| |_ ___  _ __(_)______ _| |_(_) ___  _ __   | || |  
% | |_ / _` |/ __| __/ _ \| '__| |_  / _` | __| |/ _ \| '_ \  | || |_ 
% |  _| (_| | (__| || (_) | |  | |/ / (_| | |_| | (_) | | | | |__   _|
% |_|  \__,_|\___|\__\___/|_|  |_/___\__,_|\__|_|\___/|_| |_|    |_|  
%                                                                     

% «factorization-4» (to ".factorization-4")
% (visp 16)

{\bf That factorization, for children}

We start with a particular case, with a factorization

that only has ZToposes, and we use it to understand

how the Elephant defines sujection, inclusion, etc...

($s$ is not an inclusion, $i$ is not a surjection, and so on)
%
\def\ftext#1#2{\text{#2}}
\def\ftext#1#2{\text{$#1$ (#2)}}
%
%D diagram fact-children
%D 2Dx     100 +55 +45 +45
%D 2D  100 F   G   H   I
%D 2D
%D 2D  +15 A0          A3
%D 2D
%D 2D  +20 B0  B1      B3
%D 2D
%D 2D  +20     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
%D (( F place G place H place I place
%D    A0 A3 -> .plabel= a \ftext{g}{any}
%D    B0 B1 -> .plabel= a \ftext{s}{surjection}
%D    B1 B3 -> .plabel= a \ftext{i}{inclusion}
%D    C1 C2 -> .plabel= a \ftext{d}{dense}
%D    C2 C3 -> .plabel= a \ftext{c}{closed}
%D    A0 B0 =  A3 B3 =   B1 C1 =   B3 C3 =
%D ))
%D enddiagram
%
\pu
$$
  \resizebox{!}{50pt}{$
  \diag{fact-children}
  $}
$$

\newpage

%  ____             _      __  _            _ 
% / ___| _   _ _ __(_)    / / (_)_ __   ___| |
% \___ \| | | | '__| |   / /  | | '_ \ / __| |
%  ___) | |_| | |  | |  / /   | | | | | (__| |
% |____/ \__,_|_| _/ | /_/    |_|_| |_|\___|_|
%                |__/                         
%
% «surjection-inclusion» (to ".surjection-inclusion")
% (ele "elephant-A4.2.6")
% (vgmp 18 "surjection-inclusion")
% (vgm     "surjection-inclusion")

{\bf The surjection-inclusion factorization for children}
%
%D diagram dense-closed
%D 2Dx     100 +55 +20    +40 +20 +120
%D 2D  100 AD0 <----------------| AD1
%D 2D                        
%D 2D  +25 AD2 |----------------> AD3
%D 2D                        
%D 2D  +15 AD4 -----------------> AD5
%D 2D
%D 2D  +20 AB0 AB1 ABa    BDa BD0 BD1
%D 2D
%D 2D  +20 AB2 AB3 ABb    BDb BD2 BD3
%D 2D
%D 2D  +15 AB4 AB5            BD4 BD5
%D 2D
%D ren AD0 AD1 ==> g^*I I
%D ren AD2 AD3 ==> F g_*F
%D ren AD4 AD5 ==> \Set^\catA \Set^\catD
%D 
%D ren AB0 AB1 ==> s^*G G
%D ren AB2 AB3 ==> F s_*F
%D ren AB4 AB5 ==> \Set^\catA \Set^\catB
%D ren ABa ABb ==> G s_*s^*G
%D
%D ren BD0 BD1 ==> i^*I I
%D ren BD2 BD3 ==> G i_*G
%D ren BD4 BD5 ==> \Set^\catB \Set^\catD
%D ren BDa BDb ==> i^*i_*G G
%D
%D (( AD0 AD1 <-|
%D    AD0 AD2 ->
%D    AD1 AD3 ->
%D    AD2 AD3 |->
%D    AD0 AD3 harrownodes nil 20 nil <->
%D    AD4 AD5 -> .plabel= a \ftext{g}{any}
%D
%D    AB0 AB1 <-|
%D    ABa ABb -> .plabel= r \sm{ηG\\\text{(monic)}}
%D    AB0 AB2 ->
%D    AB1 AB3 ->
%D    AB2 AB3 |->
%D    AB0 AB3 harrownodes nil 20 nil <->
%D    AB4 AB5 -> .plabel= a \ftext{s}{surjection}
%D
%D    BDa BDb -> .plabel= l \sm{εG\\\text{(iso)}}
%D    BD0 BD1 <-|
%D    BD0 BD2 ->
%D    BD1 BD3 ->
%D    BD2 BD3 |->
%D    BD0 BD3 harrownodes nil 20 nil <->
%D    BD4 BD5 -> .plabel= a \ftext{i}{inclusion}
%D
%D ))
%D enddiagram
\pu
$$
  % \resizebox{!}{60pt}{$
  \resizebox{220pt}{!}{$
  \diag{dense-closed}
  $}
$$

    

\newpage

%  ____                           __       _                    _ 
% |  _ \  ___ _ __  ___  ___     / /   ___| | ___  ___  ___  __| |
% | | | |/ _ \ '_ \/ __|/ _ \   / /   / __| |/ _ \/ __|/ _ \/ _` |
% | |_| |  __/ | | \__ \  __/  / /   | (__| | (_) \__ \  __/ (_| |
% |____/ \___|_| |_|___/\___| /_/     \___|_|\___/|___/\___|\__,_|
%                                                                 
% «dense-closed» (to ".dense-closed")
% (vgmp 19 "dense-closed")
% (vgm     "dense-closed")
% (visp 16)
% (vis    )

{\bf The dense-closed factorization for children}
%
%D diagram dense-closed
%D 2Dx     100 +20 +45 +20        +40 +45
%D 2D  100 BDa BD0 <----------------| BD1
%D 2D                            
%D 2D  +25 BDb BD2 |----------------> BD3
%D 2D                            
%D 2D  +15     BD4 -----------------> BD5
%D 2D
%D 2D  +20     BC0 BC1 BCa        CD0 CD1
%D 2D
%D 2D  +20     BC2 BC3 BCb        CD2 CD3
%D 2D
%D 2D  +20     BC4 BC5            CD4 CD5
%D 2D
%D 2D  +20 
%D 2D
%D ren BDa BDb ==> i^*i_*G G
%D ren BD0 BD1 ==> i^*I I
%D ren BD2 BD3 ==> G i_*G
%D ren BD4 BD5 ==> \Set^\catB \Set^\catD
%D
%D ren BCa BCb ==> K d_*d^*K
%D ren BC0 BC1 ==> d^*H H
%D ren BC2 BC3 ==> G d_*G
%D ren BC4 BC5 ==> \Set^\catB \Set^\catC
%D
%D ren CD0 CD1 ==> c^*I I
%D ren CD2 CD3 ==> H c_*H
%D ren CD4 CD5 ==> \Set^\catC \Set^\catD
%D
%D (( BDa BDb -> .plabel= l \sm{εG\\\text{(iso)}}
%D    BD0 BD1 <-|
%D    BD0 BD2 ->
%D    BD1 BD3 ->
%D    BD2 BD3 |->
%D    BD0 BD3 harrownodes nil 20 nil <->
%D    BD4 BD5 -> .plabel= a \ftext{i}{inclusion}
%D
%D    BCa BCb -> .plabel= r \sm{ηK\\\text{(monic)}}
%D    BC0 BC1 <-|
%D    BC0 BC2 ->
%D    BC1 BC3 ->
%D    BC2 BC3 |->
%D    BC0 BC3 harrownodes nil 20 nil <->
%D    BC4 BC5 -> .plabel= a \ftext{d}{dense}
%D
%D    CD0 CD1 <-|
%D    CD0 CD2 ->
%D    CD1 CD3 ->
%D    CD2 CD3 |->
%D    CD0 CD3 harrownodes nil 20 nil <->
%D    CD4 CD5 -> .plabel= a \ftext{c}{closed}
%D
%D ))
%D enddiagram
%
\pu
$$
  \resizebox{!}{60pt}{$
  \diag{dense-closed}
  $}
$$

\ColorGray{($K$ is a constant ZPresheaf in $\Set^\catC$)}


\newpage

{\bf Acoording to the Elephant...}

%D diagram mysterious-B-and-C
%D 2Dx     100 +45 +45 +40
%D 2D  100 A0          A3
%D 2D
%D 2D  +20 B0  B1      B3
%D 2D
%D 2D  +20     c1
%D 2D
%D 2D  +20     C1  C2  C3
%D 2D
%D 2D  +20         d2
%D 2D
%D 2D  +20         D2
%D 2D
%D ren A0    A3 ==> \Set^\catA                  \Set^\catD
%D ren B0 B1 B3 ==> \Set^\catA \calB            \Set^\catD
%D ren C1 C2 C3 ==>            \Set^\catB \calC \Set^\catD
%D ren    D2    ==>                       \Set^\catC
%D
%D ren c1 ==> (\Set^\catB)_\bbG
%D ren d2 ==> \mathsf{sh}_{¬¬}(\Set^\catD)\oque
%D
%D (( A0 A3 -> .plabel= a \ftext{a}{any}
%D    B0 B1 -> .plabel= a \ftext{s}{surjection}
%D    B1 B3 -> .plabel= a \ftext{i}{inclusion}
%D    C1 C2 -> .plabel= a \ftext{d}{dense}
%D    C2 C3 -> .plabel= a \ftext{c}{closed}
%D    A0 B0 =  A3 B3 =   B1 c1 == c1 C1 ==   B3 C3 = C2 d2 == d2 D2 ==
%D ))
%D enddiagram
%D
\pu
\def\oque{\;\;\;(???)}
\antitabular
\begin{tabular}{l}
  A4.2.7, 4.2.10: \\
  to build $\calB$ we need \\
  comonads and \\
  coalgebras \\
  \\
  A4.5.9, A4.5.20: \\
  $\calC = \mathsf{sh}_{¬¬}(\Set^\catD)$ \\
  \ColorRed{(can't be!)} \\
\end{tabular}
\quad
$\resizebox{!}{60pt}{$
   \diag{mysterious-B-and-C}
   $}
$

\newpage

{\bf Another strategy}

Start with a functor $g:\catA → \catD$.

It induces a geometric morphism $g^*⊣g_*$.

$g^*$ is trivial to build.

$g_*$ can be found by guess-and-test.

\ColorGray{(or by Kan extensions)}

\msk

The functor $g$ can:

collapse objects,    $(1 \;\;\; 2) → (1)$

create objects,      $(\,) → (3)$

collapse arrows,     $(4 \two/->`->/ 5) → (4 → 5)$

create arrows,       $(6 \;\;\; 7) → (6 → 7)$

\msk

Try to factor it. Example: if $g$ just collapses objects...

\newpage

{\bf Another strategy}

The functor $g$ can do several \ColorRed{things}:

collapse objects,    $(1 \;\;\; 2) → (1)$

create objects,      $(\,) → (3)$

collapse arrows,     $(4 \two/->`->/ 5) → (4 → 5)$

create arrows,       $(6 \;\;\; 7) → (6 → 7)$

refine the order,    $(2 → 4) → (1 → 2 → 3 → 4 → 5)$...

\msk

Try to factor it.

Example: if $g$ just \ColorRed{collapses} objects,

then it factor as $s=g$ (surj. part), $i=\id$ (inclusion part)...

The factorization filters the {\sl things} that the functor can do,

\ColorRed{collapsing objects} go to the surjective part.


\newpage

{\bf Another strategy}

\antitabular
\begin{tabular}{l}
  Choose a functor                    \\
  $f:\catA→\catB$                     \\
  that does all \ColorRed{things}.    \\
  Factorize it.                       \\
  $\calB$ and $\calC$ will            \\
  be non-trivial.                     \\
  They tell us how                    \\
  $\calB$ and $\calC$ will be         \\
  \ColorRed{modulo}                   \\
  \ColorRed{isomorphism}.             \\
\end{tabular}
\;\;
$\resizebox{!}{60pt}{$
   \diag{mysterious-B-and-C}
   $}
$


\newpage

For more information:

\url{http://angg.twu.net/logic-for-children-2018.html}

\url{http://angg.twu.net/math-b.html}


% (ph2     "algebra-of-J-ops")
% (ph2p 32 "algebra-of-J-ops")
% (ph2p 34 "algebra-of-J-ops" "algebra")



\end{document}




% Local Variables:
% coding: utf-8-unix
% ee-tla: "vgs"
% End:
