|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008monads.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008monads.tex && latex 2008monads.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008monads.tex && pdflatex 2008monads.tex"))
% (eev "cd ~/LATEX/ && Scp 2008monads.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008monads.dvi")
% (find-pspage "~/LATEX/2008monads.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008monads.ps 2008monads.dvi")
% (find-pspage "~/LATEX/2008monads.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008monads.pdf" (ee-twupfile "LATEX/2008monads.pdf") 'over)
% (ee-cp "~/LATEX/2008monads.pdf" (ee-twusfile "LATEX/2008monads.pdf") 'over)
% «.monads» (to "monads")
% «.coherence» (to "coherence")
% «.monads-manes» (to "monads-manes")
% «.monads-kleisli-cat» (to "monads-kleisli-cat")
% «.monads-kleisli-respids» (to "monads-kleisli-respids")
% «.monads-kleisli-assoc» (to "monads-kleisli-assoc")
% «.monads-em-cat» (to "monads-em-cat")
% «.monads-resolutions-cat» (to "monads-resolutions-cat")
% «.seely-mail-1» (to "seely-mail-1")
% «.seely-mail-2» (to "seely-mail-2")
% «.seely-mail-3» (to "seely-mail-3")
% «.ragsdiff-diags-1» (to "ragsdiff-diags-1")
% «.ragsdiff-diags-2» (to "ragsdiff-diags-2")
% «.ragsdiff-diags-3» (to "ragsdiff-diags-3")
% «.vector-spaces» (to "vector-spaces")
% «.differential-box» (to "differential-box")
% «.differential-combinator» (to "differential-combinator")
% «.comonad-structure» (to "comonad-structure")
% «.coalgebra-modality» (to "coalgebra-modality")
% «.term-calculus» (to "term-calculus")
% «.term-calculus-long» (to "term-calculus-long")
% «.d-combinator» (to "d-combinator")
% «.universals» (to "universals")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008monads.dnt
%*
% (eedn4-51-bounded)
% (eev-math-glyph-names "Delta" 916 "eta" 951 "mu" 956 "nu" 957)
% (eev-math-glyphs-set 'eev-glyph-face-math "nabla " "na" "¿")
% (eev-math-glyphs-set 'eev-glyph-face-greek "theta nu" "te nu" " Û")
% (eev-math-glyphs-set 'eev-glyph-face-math "Delta" "DD" "¿")
% (eev-math-glyphs-set 'eev-glyph-face-greek "eta mu" "et mu" " Û")
\def\myttchars{%
\ttchars%
\def¿{\ttchar{$\Delta$}}%
\def{\ttchar{$\eta$}}%
\defÛ{\ttchar{$\mu$}}%
}
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Monads} {2}
\tocline {Where our notation fails} {3}
\tocline {A presentation of monads due to Manes} {4}
\tocline {The Kleisli category of a monad} {5}
\tocline {The Eilenberg-Moore category of a monad} {6}
\tocline {The category of resolutions for a monad} {7}
\tocline {E-mail to Seely (1)} {8}
\tocline {E-mail to Seely (2)} {9}
\tocline {E-mail to Seely (3)} {10}
\tocline {Diagrams (1)} {11}
\tocline {Diagrams (2)} {12}
\tocline {Diagrams (3)} {13}
\tocline {Vector spaces} {14}
\tocline {The differential box} {15}
\tocline {The differential combinator} {16}
\tocline {Comonad structure} {17}
\tocline {Coalgebra modalities} {18}
\tocline {The term calculus} {19}
\tocline {The term calculus: long version} {20}
\tocline {The D combinator} {21}
\tocline {Universal and couniversal arrows} {22}
\setlength{\parindent}{0em}
\newpage
% --------------------
% «monads» (to ".monads")
% (s "Monads" "monads")
\myslide {Monads} {monads}
{\myttchars
\footnotesize
\begin{verbatim}
Fix a monoid M.
Notation: elements of M will be called a,b,c,...
Our archetypal monad is based on the functor (×M):Set->Set.
A monad over a functor T (T=(×M) for us) is triple (T,,Û)
where and Û are natural transformations:
Û .
X -----> TX <----- TTX x |---> x,1
x,ab <---| x,a,b
and Û have to obey certain equations:
(T;Û)=(T;Û)=id and
(ÛT;Û)=(TÛ;Û).
If we downcase those equations using x=>x,a as the archetype
they become exactly ýa.a1=1a=a and ýa,b,c.a(bc)=(ab)c.
TX --T--> TTX --Û--> TX x,a |---> x,a,1 |----> x,a1
TX --T--> TTX --Û--> TX x,a |---> x,1,a |----> x,1a
TX ---------id------> TX x,a |----------------> x,a
TTTX --ÛT--> TTX --Û--> TX x,a,b,c |---> x,a,bc |---> x,a(bc)
TTTX --TÛ--> TTX --Û--> TX x,a,b,c |---> x,ab,c |---> x,(ab)c
Here are square conditions for the two natural transformations.
For any objects X and Y and any morphism x|->y,
X
X -----> TX x |---> x,1
| | - -
| f | Tf | |
v v v v
Y -----> TY y |---> y,1
Y
ÛX
TX <---- TTX x,ab <---| x,a,b
| | - -
| Tf | TTf | |
v v v v
TY <---- TTY y,ab <---| y,a,b
ÛY
\end{verbatim}
}
\newpage
% --------------------
% «coherence» (to ".coherence")
% (s "Where our notation fails" "coherence")
\myslide {Where our notation fails} {coherence}
{\myttchars
\footnotesize
\begin{verbatim}
Our notation based on (×M) is not totally faithful -
sometimes it suggests that two morphisms are the same
when they may be different...
The square below does not need to commute.
TTTX x,a,b,cd
/ ^ \ ^
TÛX / \ ÛTTX / \
v \ v /
TTX TTTTX x,ab,cd x,a,b,c,d
^ / ^ \
ÛTX \ / TTÛX \ /
\ v / v
TTTX x,ab,c,d
But all canonical morphisms from T^nX to TX are equal -
\end{verbatim}
}
\newpage
% --------------------
% «monads-manes» (to ".monads-manes")
% (s "A presentation of monads due to Manes" "monads-manes")
\myslide {A presentation of monads due to Manes} {monads-manes}
{\myttchars
\footnotesize
\begin{verbatim}
A monad can also be given by an object function S
and operations
f f#
(X ---> S(Y)) |-> (S(X) ----> S(Y) (x|->y,a) |-> (x,b|->y,ab)
X
X |--> (X ----> S(X)) x -.> (x|->x,1)
Subject to:
(X)^# = 1_S(X)
X;f^# = f
f^#;g^# = (f;g^#)^#
Let's expand these equations:
X x|->x,1
------ ----------
(X)^# = 1_S(X) x,a|->x,1a = x,a|->x,a
f x|->y,a
--- ----------
X f^# x|->x,1 x,b|->y,ab
-------- -------------------
X;f^# = f x|->y,a1 = x|->y,a
g y|->z,a
--- ----------
f g f g^# x|->y,c y|->z,a x|->y,c y,b|->z,ab
--- --- ------- ---------- ---------- -------------------
f^# g^# f;g^# x,d|->y,cd y,b|->z,ab x|->z,ac
--------- --------- ----------------------- -----------
f^#;g^# = (f;g^#)^# x,d|->z,acd = x,d|->z,acd
\end{verbatim}
}
\newpage
% --------------------
% «monads-kleisli-cat» (to ".monads-kleisli-cat")
% (s "The Kleisli category of a monad" "monads-kleisli-cat")
\myslide {The Kleisli category of a monad} {monads-kleisli-cat}
{\myttchars
\footnotesize
\begin{verbatim}
Notation:
x:xT x xT xTT
- - -
| | f \ f
| v v
f;TG;mu | y:yT y yT yTT
| - - -
| | g g \ \ Tg
v v v v
z:zT z zT <-| zTT
mu
The adjunction:
x':x'T <===== x'
- -
f;eta | <--| |
v v
x:xT <====== x'
- -
g | <--| | g
g | |--> | g
v v
y:yT ======> yT
- -
h | |--> | Th;mu
v v
y':y'T ====> y'T
\end{verbatim}
}
\newpage
% --------------------
% «monads-kleisli-assoc» (to ".monads-kleisli-assoc")
% (s "Kleisli composition is associative" "monads-kleisli-assoc")
\myslide {Kleisli composition is associative} {monads-kleisli-assoc}
\def\K{\,¯K\,}
%D diagram kleisli-comp-std
%D 2Dx 100 +35 +35 +35
%D 2D 100 X
%D 2D ->
%D 2D +25 Y TY
%D 2D ->
%D 2D +25 Z TZ <- TTZ
%D 2D -> ->
%D 2D +25 W TW <= TTW <= TTTW
%D 2D
%D (( X TY -> .plabel= r f
%D Y place
%D TY TTZ -> .plabel= r Tg
%D Z place TZ TTZ <- .plabel= a \mu
%D TZ TTW -> .plabel= a Th TTZ TTTW -> .plabel= r TTh
%D W place TW TTW <- sl^ .plabel= a \mu TTW TTTW <. sl^ .plabel= a \mu
%D TW TTW <- sl_ .plabel= b \mu TTW TTTW <- sl_ .plabel= b T\mu
%D Y TZ .> .plabel= r g
%D Z TW .> .plabel= r h
%D ))
%D enddiagram
%D
%D diagram kleisli-comp-dnc
%D 2Dx 100 +35 +35 +35
%D 2D 100 x
%D 2D |->
%D 2D +25 y y,a
%D 2D |->
%D 2D +25 z z,ba <-| z,b,a
%D 2D |-> |->
%D 2D +25 w w,cba <-| w,c,ba <.| w,c,b,a
%D 2D +07 <-| w,cb,a <-|
%D 2D
%D (( x y,a |->
%D y place
%D y,a z,b,a |->
%D z place z,ba z,b,a <-|
%D z,ba w,c,ba |-> z,b,a w,c,b,a |->
%D w place w,cba w,c,ba <-| w,c,ba w,c,b,a <.|
%D w,cba w,cb,a <-| w,cb,a w,c,b,a <-|
%D ))
%D enddiagram
%:
%: x|->y,a y|->z,b
%: ----------------------¯K
%: x|->y,a|->z,b,a|->z,ba z|->w,c
%: ---------------------------------------¯K
%: x|->y,a|->z,b,a|->z,ba|->w,c,ba|->w,cba
%:
%: ^kleislicomp-dnc-1
%:
%: y|->z,b z|->w,c
%: -----------------------¯K
%: x|->y,a y|->z,b|->w,c,b|->w,cb
%: ----------------------------------------------¯K
%: x|->y,a|->y|->z,b,a|->w,c,b,a|->w,cb,a|->w,cba
%:
%: ^kleislicomp-dnc-2
%:
%: f g g h
%: --------¯K ---------¯K
%: f;Tg;\mu h f g;Th;\mu
%: ---------------¯K -----------------¯K
%: f;Tg;\mu;Th;\mu f;Tg;TTh;T\mu;\mu
%:
%: ^kleislicomp-std-1 ^kleislicomp-std-2
%:
\widemtos
We need to check that
$(f \K g) \K h = f \K (g \K h)$:
\msk
$\begin{array}{l}
% (f \K g) \K h = f \K (g \K h): \\
% \\
\ded{kleislicomp-std-1} \quad = \quad \ded{kleislicomp-std-2} \\
\\
\ded{kleislicomp-dnc-1} \\
\\
= \quad \ded{kleislicomp-dnc-2} \\
\\
\\
\diag{kleisli-comp-std} \\
\\
\diag{kleisli-comp-dnc} \\
\end{array}
$
\newpage
% --------------------
% «monads-kleisli-respids» (to ".monads-kleisli-respids")
% (s "Kleisli composition respects identities" "monads-kleisli-respids")
\myslide {Kleisli composition respects identities} {monads-kleisli-respids}
\def\K{\,¯K\,}
Also, $f \K \eta = f$, and $\eta \K f = f$ ---
because $T\eta ; \mu = \id$ and $\eta; \mu = \id$.
%D diagram kleisli-ids
%D 2Dx 100 +30 +30 +25 +30 +30
%D 2D 100 X x
%D 2D --> |->
%D 2D +20 Y TY y y,a
%D 2D --> --> |-> |->
%D 2D +20 Y{} {}TY <-- TTY y{} y,e y,e,a
%D 2D +7 y,ea <-|
%D 2D
%D (( X TY -> .plabel= a f
%D Y {}TY -> .plabel= r \eta TY TTY -> .plabel= r T\eta
%D Y{} place {}TY TTY <- .plabel= b \mu
%D ))
%D (( x y,a |->
%D y y,e |-> y,a y,e,a |->
%D y{} place y,ea y,e,a <-|
%D ))
%L clearnamednodes()
%D 2D +20 X{} x{}
%D 2D --> |->
%D 2D +20 X --> TX x |-> x,e
%D 2D --> --> |-> |-->
%D 2D +20 Y TY >-> TTY y y,a |--> y,a,e
%D 2D +7 <-- y,ae <-|
%D 2D
%D (( X{} TX -> .plabel= a \eta
%D X TX -> .plabel= a \eta
%D X TY -> .plabel= a f TX TTY -> .plabel= a Tf
%D Y place TY TTY >-> sl^ .plabel= a \eta
%D TY TTY <- sl_ .plabel= b \mu
%D ))
%D (( x{} x,e |->
%D x x,e |->
%D x y,a |-> x,e y,a,e |->
%D y place y,a y,a,e |->
%D y,ae y,a,e <-|
%D
%D ))
%D enddiagram
%D
\msk
$\diag{kleisli-ids}$
\newpage
% --------------------
% «monads-em-cat» (to ".monads-em-cat")
% (s "The Eilenberg-Moore category of a monad" "monads-em-cat")
\myslide {The Eilenberg-Moore category of a monad} {monads-em-cat}
{\myttchars
\footnotesize
\begin{verbatim}
The adjunction:
(x'T <--| x'TT) <=== x'
- - -
f;eta | | <-| | f
v v v
(xT <---| xTT) <==== x
--| ---| -
Tg;\aa / / <--| | g
h / / |--> | eta;h
v \aa v v
(y <---| yT) <============== y
- - -
k | | |--> | k
v v v
(y' <--| y'T) <============= y'
\end{verbatim}
}
\newpage
% --------------------
% «monads-resolutions-cat» (to ".monads-resolutions-cat")
% (s "The category of resolutions for a monad" "monads-resolutions-cat")
\myslide {The category of resolutions for a monad} {monads-resolutions-cat}
{\myttchars
\footnotesize
\begin{verbatim}
The Kleisli category is the initial resolution,
the Eilenbeg-Moore category is the final one.
Notation: O[yL] is not necessarily an image by L -
in some arrows it just just an arbitrary object of
the "other category" in an adjunction diagram.
Also: O[yT] = O[yLR].
/=== x:xT <==\
// - \\
// | \\
// v \\
// /== y:yT ===\ \\
// // \\ \\
// // \\ \\
\/ // \\ \\
xL <========================== x
- \\// \\ //-
| /\\ \// |
v \/ \\ //v v
yL ===\\==================//=> yT
\\ \\ // /\
\\ \\ // //
\\ \/ \/ //
\\ (xT <-| xTT) //
\\ - - //
\\ | | //
\/ v v //
(yT <-| yTT)
The functor x:xT => xL acts on objects as L
and on morphisms as the transposition.
The functor yL => (yT <-| yTT) acts on objects as R
(plus the counit: O[yL] |-> (yL <-| yLRL) |-> (yLR <-| yLRLR))
and on morphisms as R.
\end{verbatim}
}
% (find-lsrcfile "base/fontdef.dtx" "\\DeclareMathSymbol{\\gg}")
% (find-gregsymbolspage 2)
\def\kot{\mathchar"321C}
\def\kto{\mathchar"321D}
%:*>>*\kto *
%:*<<*\kot *
%:*<-|*\leftarrow\mapsfromchar *
\def\red#1{{\color{red}#1}}
\def\ph{\red}
\def\ph{\phantom}
%L thereplusxy = function (dx, dy, tag)
%L ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L return ds[1]
%L end
%L forths["there+xy:"] = function ()
%L thereplusxy(getword(), getword(), getword())
%L end
%D diagram kleisli-and-em
%D 2Dx 100 +50 +50
%D 2D 100 / k1
%D 2D // - /\
%D 2D // | \\
%D 2D // v \\
%D 2D +20 // k2 \\
%D 2D // // \\ \\
%D 2D \/ // \\ \\
%D 2D +20 r1 <================= o1
%D 2D - \\// \\ //-
%D 2D | /\\ \// |
%D 2D v \/ \\ //v v
%D 2D +20 r2 ===\\=========//=> o2
%D 2D \\ \\ // /\
%D 2D \\ \/ \/ //
%D 2D +20 \\ em1 //
%D 2D \\ - //
%D 2D \\ | //
%D 2D \/ v //
%D 2D +20 em2
%D 2D
%D (( # k1 .tex= (a^T>>a^{TT}) k2 .tex= (b^T>>b^{TT}) k1 place k2 place
%D k1 .tex= (a>>a^T) k2 .tex= (b>>b^T) k1 place k2 place
%D em1 .tex= (a^T<-|a^{TT}) em2 .tex= (b^T<-|b^{TT}) em1 place em2 place
%D r1 .tex= a^L r2 .tex= b^L
%D o1 .tex= a o2 .tex= b^T
%D k1 there+xy: -9 0 k1L .tex= \ph{a}
%D k1 there+xy: +6 0 k1R .tex= \ph{a^T}
%D k2 there+xy: -9 0 k2L .tex= \ph{b}
%D k2 there+xy: +6 0 k2R .tex= \ph{b^T}
%D em1 there+xy: -11 0 em1L .tex= \ph{a^T}
%D em1 there+xy: +9 0 em1R .tex= \ph{a^{TT}}
%D em2 there+xy: -11 0 em2L .tex= \ph{b^T}
%D em2 there+xy: +9 0 em2R .tex= \ph{b^{TT}}
%D o1 o2 |->
%D r1 r2 |->
%D k1L k2R |->
%D em1L em2L |-> em1R em2R |->
%D k1R o1 <= k2R o2 =>
%D r1 o1 <= r2 o2 =>
%D em1R o1 <= em2R o2 =>
%D k1L r1 => k2L r2 =>
%D r1 em1L => r2 em2L =>
%D k1R k2R midpoint o1 o2 midpoint dharrownodes nil 20 nil <->
%D r1 r2 midpoint o1 o2 midpoint dharrownodes nil 25 nil <->
%D em1R em2R midpoint o1 o2 midpoint dharrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram cokleisli-and-coem
%D 2Dx 100 +50 +50
%D 2D 100 k1
%D 2D /\ - \\
%D 2D // | \\
%D 2D // v \\
%D 2D +20 // k2 \\
%D 2D // // \\ \\
%D 2D // // \\ \/
%D 2D +20 l1 <================= r1
%D 2D - /\// \\ //-
%D 2D | /\\ \// |
%D 2D v \/ \\ //V v
%D 2D +20 l2 ===\\=========//=> r2
%D 2D \\ \\ // //
%D 2D \\ \\ \/ //
%D 2D +20 \\ em1 //
%D 2D \\ - //
%D 2D \\ | //
%D 2D \/ v \/
%D 2D +20 em2
%D 2D
%D (( k1 .tex= (a<<a^C) k2 .tex= (b<<b^C) k1 place k2 place
%D em1 .tex= (a^C|->a^{CC}) em2 .tex= (b^C|->b^{CC}) em1 place em2 place
%D l1 .tex= a^C r1 .tex= a^R
%D l2 .tex= b r2 .tex= b^R
%D k1 there+xy: -9 0 k1L .tex= \ph{a}
%D k1 there+xy: +6 0 k1R .tex= \ph{a^C}
%D k2 there+xy: -9 0 k2L .tex= \ph{b}
%D k2 there+xy: +6 0 k2R .tex= \ph{b^C}
%D em1 there+xy: -11 0 em1L .tex= \ph{a^C}
%D em1 there+xy: +9 0 em1R .tex= \ph{a^{CC}}
%D em2 there+xy: -11 0 em2L .tex= \ph{b^C}
%D em2 there+xy: +9 0 em2R .tex= \ph{b^{CC}}
%D k1R k2L |->
%D k1L l1 => k2L l2 <= k1R r1 => k2R r2 =>
%D l1 r1 <= l1 l2 |-> r1 r2 |-> l2 r2 =>
%D l1 em1L <= l2 em2L =>
%D r1 em1R => r2 em2R =>
%D em1L em2L |-> em1R em2R |->
%D l1 l2 midpoint k1L k2L midpoint dharrownodes nil 20 nil <->
%D l1 l2 midpoint r1 r2 midpoint dharrownodes nil 25 nil <->
%D l1 l2 midpoint em1L em2L midpoint dharrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
\msk
$\diag{kleisli-and-em} \diag{cokleisli-and-coem}$
\newpage
% --------------------
% «seely-mail-1» (to ".seely-mail-1")
% (s "E-mail to Seely (1)" "seely-mail-1")
\myslide {E-mail to Seely (1)} {seely-mail-1}
{\myttchars
\footnotesize
\begin{verbatim}
First, consider a function "f:A->B":
f: A --> B
a |-> f(a)
Let's write it like this (we're putting our physicist's hats on):
b:=f(a)
a |-------> b
We're seeing it as relating the value of two variables - the output,
b, is a function of the input; the rule "b:=f(a)" tells us how to
calculate the output from the input.
Now let's think that A is a one-dimensional vector space, whose points
are the possible values of a, and B is another one-dimensional vector
space, whose points are the possible values for b. If our f is a
linear function A->B (I will not write the arrow as a lollipop), then
we can write b:=f(a) as
b:=ka
a |-----> b
where k is a constant.
Now let's make things worse. A becomes a two-dimensional vector space,
X×Y, and B becomes a three-dimensional vector space, Z×W×T, where X is
the space of the possible values for a variable x, and the same for
the other letters: Y, Z, W, T. Now the value of A is a point in a
two-dimensional space; we can think of it as being the pair of
(numeric) values (x,y) - and the same for b: b=(z,w,t).
A linear transformation f:A->B sets the value of b from the value of
a; or, in freshman's terms, it sets the value of (z,w,t) from the
value of (x,y). It can be, for example, that f is like this:
z:=1x+2y
w:=3x+4y
t:=5x+6y
(x,y) |--------> (z,w,t)
a |--------> b
Now let me pick the case where A and B are both one-dimensional again,
but I will look at a polynomial function, b := 3a^2 + 4a, and I will
represent it as a linear function from !A to B.
!A is an infinite-dimensional space; a point in !A is a certain
quantity of a^0, plus a certain quantity of a^1, plus a certain
quantity of a^2, etc - note that I'm sort of confusing variables and
the base elements of vector spaces, that is not some random macarronic
dialect of mathematics, it's the trick that makes everything work...
anyway, ahead; writing the tensor product as "@", the basis of A is
{a}, and the basis of !A is {a^0, a, a@a, a@a@a, a@a@a@a, ...}, where
a^0 is the 0-th @-power of a; in another notation, this basis is {1,
a, a^2, a^3, a^4, ...}.
\end{verbatim}
}
\newpage
% --------------------
% «seely-mail-2» (to ".seely-mail-2")
% (s "E-mail to Seely (2)" "seely-mail-2")
\myslide {E-mail to Seely (2)} {seely-mail-2}
{\myttchars
\footnotesize
\begin{verbatim}
The polynomial b := 3a^2 + 4a now becomes
b:=3a^2+4a
(1,a,a^2,...) |----------> b
!A -----------> B,
a linear function.
This is just the beginning, of course - but I've worked out all
diagrams until D.2 in page 8, and some diagrams and equations ahead of
that, and everything became very nice in this notation - only the
dotted lines seem to need some tricks that I don't have yet... Just
for curiosity, here are two diagrams (with no explanations here, but I
can provide them later):
\ / \ /
A \ / !A da \ / !a'
\ / \ /
================= =================
| | | | | |
| !A | | | !a | a^3 := 3a'^2da
| ___|___ | | ___|___ |
| | | | | | | |
| | f | | | | f | |
| |_______| | | |_______| |
| | | | | |
| B | | | b := a^3 |
|_______|_______| |_______|_______|
| |
B | b_{a}da := 3a'^2da
| |
The differential combinator:
\ / \ /
A \ / !A da \ / !a'
\ / \ /
=============== ===============
| |
!A | d!a | a^3 := 3a'^2da
_______|_______ _______|_______
| | | | | |
| !A | | | !a | |
| ___|___ | | ___|___ |
| | | | | | | |
| | f | | | | f | |
| |_______| | | |_______| |
| | | | | |
| B | | | b := a^3 |
|_______|_______| |_______|_______|
| |
B | db := 3a'^2da
| |
\end{verbatim}
}
\newpage
% --------------------
% «seely-mail-3» (to ".seely-mail-3")
% (s "E-mail to Seely (3)" "seely-mail-3")
\myslide {E-mail to Seely (3)} {seely-mail-3}
{\myttchars
\footnotesize
\begin{verbatim}
In these examples I'm always pretending that A and B are
one-dimensional - everything works when they are more-dimensional, but
then I use some dictionary tricks to "read" the downcased diagrams as
something some general; formally, the downcased names for the wires
become just abstract names for things that are more complex - but
there is some precise relation between these abstract names (they're
not totally abstract or arbitrary) and the "real things" behind
them...
\end{verbatim}
}
% (find-ragsdiffpage 1)
% (find-ragsdiffpage 5)
\newpage
% --------------------
% «ragsdiff-diags-1» (to ".ragsdiff-diags-1")
% (s "Diagrams (1)" "ragsdiff-diags-1")
\myslide {Diagrams (1)} {ragsdiff-diags-1}
{\myttchars
\scriptsize
\tiny
\begin{verbatim}
[D.1] Constant maps:
(here a^0 := 0 da ¤ a^0)
\ /
a \ / !a
\ /
=================
| | |
| (·0) | a^0 |
| ___|___ |
| | | |
| | e | |
| |_______| |
| | |
| | 1 |
|_______|_______|
|
| 1
|
\ / | | | |
a \ / a^7 | | a^7 | | a^7
\ / | __|__ a | __|__
============================= a | / \ | / \
| | | | | ¿ | \ | ¿ |
| (·8) | a^8 | | \_____/ \___ \_____/
| __|__ | | / \ \/ \
| / \ | \ / a^2 \ _____/\ \ a^4
| | ¿ | | \ / | / \ |
| \_____/ | =============== | a^5 a^3 / ===============
| / \ | | | | | / | | |
| a^3 / \ a^5 | | (·3) | a^3 | | / | (·5) | a^5 |
| _____/_ _\_____ | | ___|___ | ___|___ ___|___ | ___|___ |
| | | | | | | | | | | | | | | | | |
| | f | | g | | = | | f | | | g | + | f | | | g | |
| |_______| |_______| | | |_______| | |_______| |_______| | |_______| |
| \ / | | | | / | | / |
| b \ / c | | b \ | / \ | / c |
| _\___/_ | |________\____| / c b \ |___/_________|
| | | | \ / \ /
| | @ | | \ / \ /
| |_______| | _\___/_ _\___/_
| | | | | | |
| | b@c | | @ | | @ |
|_____________|_____________| |_______| |_______|
| | |
| b@c | b@c | b@c
| | |
\end{verbatim}
}
\newpage
% --------------------
% «ragsdiff-diags-2» (to ".ragsdiff-diags-2")
% (s "Diagrams (2)" "ragsdiff-diags-2")
\myslide {Diagrams (2)} {ragsdiff-diags-2}
{\myttchars
\footnotesize
\begin{verbatim}
[D.3] Linear maps:
\ /
a \ / a^0 | |
\ / | | a^0
================= | ___|___
| | | | | |
| (·1) | a^1 | a | | \ee |
| ___|___ | | |_______|
| | | | | :
| | \ee | | | : 1
| |_______| | | :
| | | | .....'
| | a | = O'
| ___|___ | |
| | | | | a
| | f | | ___|___
| |_______| | | |
| | | | f |
| | b | |_______|
|_______|_______| |
| | b
| b |
|
\end{verbatim}
}
\newpage
% --------------------
% «ragsdiff-diags-3» (to ".ragsdiff-diags-3")
% (s "Diagrams (3)" "ragsdiff-diags-3")
\myslide {Diagrams (3)} {ragsdiff-diags-3}
{\myttchars
\scriptsize
\begin{verbatim}
[D.4] Chain rule:
| |
| | a^11
| __|__
a | / \
\ / | | ¿ |
a \ / a^11 | \_____/
\ / | / \
======================= | a^3 / \ a^8
| | | \ / \
| (·12) | a^12 | ================= ___\___________
| _______|_______ | | | | | \ |
| | | | | | (·4) | a^4 | | \ a^4 |
| | | a^4 | | | ___|___ | | __\____ |
| | ___|___ | | | | | | | | | |
| | | | | | | | f | | | | f | |
| | | f | | | | |_______| | | |_______| |
| | |_______| | | | \ | | | |
| | | | | | b \ | | _|_ b |
| | _|_ b | | = |__________\____| |_____/___\_____|
| |_____/___\_____| | \ /
| | | b \ / b^2
| | b^3 | \ /
| ___|___ | =================
| | | | | | |
| | g | | | (·3) | b^3 |
| |_______| | | ___|___ |
| | | | | | |
| | c | | | g | |
|___________|___________| | |_______| |
| | | |
| | | c |
|_______|_______|
|
| c
|
\end{verbatim}
}
\newpage
% --------------------
% «vector-spaces» (to ".vector-spaces")
% (s "Vector spaces" "vector-spaces")
\myslide {Vector spaces} {vector-spaces}
{\myttchars
\footnotesize
\begin{verbatim}
Fix a base field for our vector spaces: R, C, Q,
an arbitrary field K - it doesn't matter.
Let's denote by FinVec the category of finite-dimensional
vector spaces over that base field; morphisms are linear
transformations.
Each morphism in FinVec has a "dual", or "transpose",
going in the opposite direction.
A good notation (?) for morphisms:
/1 2\
|3 4|
\5 6/
R^2 -------> R^3 c := 1a + 2b
/c\ d := 3a + 4b
/a\ | | e := 5a + 6b
| | |------> |d| a,b |--------------> c,d,e
\b/ | |
\e/
We should be able to do a lot using morphisms
that are not as general as these - matrices that
are all 0s, with just one entry being a 1.
An example:
d:=a
a,b |------> c,d,e
Then our previous morphism is:
1(c:=a) + 2(c:=b) +
3(d:=a) + 4(d:=b) +
5(e:=a) + 6(e:=b)
\end{verbatim}
}
\newpage
% --------------------
% «differential-box» (to ".differential-box")
% (s "The differential box" "differential-box")
\myslide {The differential box} {differential-box}
{\myttchars
\footnotesize
\begin{verbatim}
\ / \ /
A \ / !A da \ / !a'
\ / \ /
================= =================
| | | | | |
| !A | | | !a | a^3 := 3a'^2da
| ___|___ | | ___|___ |
| | | | | | | |
| | f | | | | f | |
| |_______| | | |_______| |
| | | | | |
| B | | | b := a^3 |
|_______|_______| |_______|_______|
| |
B | b_{a}da := 3a'^2da
| |
\end{verbatim}
}
\newpage
% --------------------
% «differential-combinator» (to ".differential-combinator")
% (s "The differential combinator" "differential-combinator")
\myslide {The differential combinator} {differential-combinator}
{\myttchars
\footnotesize
\begin{verbatim}
\ / \ /
A \ / !A da \ / !a'
\ / \ /
=============== ===============
| |
!A | d!a | a^3 := 3a'^2da
_______|_______ _______|_______
| | | | | |
| !A | | | !a | |
| ___|___ | | ___|___ |
| | | | | | | |
| | f | | | | f | |
| |_______| | | |_______| |
| | | | | |
| B | | | b := a^3 |
|_______|_______| |_______|_______|
| |
B | db := 3a'^2da
| |
\end{verbatim}
}
\newpage
% --------------------
% «comonad-structure» (to ".comonad-structure")
% (s "Comonad structure" "comonad-structure")
\myslide {Comonad structure} {comonad-structure}
{\myttchars
\footnotesize
\begin{verbatim}
Two natural transformations, and ,
X <----- !X -----> !!X
Obeying the duals of what would be this,
if I downcased my favourite monad:
(T;Û)=(T;Û)=id
(ÛT;Û)=(TÛ;Û)
TX --T--> TTX --Û--> TX x,a |---> x,a,1 |----> x,a1
TX --T--> TTX --Û--> TX x,a |---> x,1,a |----> x,1a
TX ---------id------> TX x,a |----------------> x,a
TTTX --ÛT--> TTX --Û--> TX x,a,b,c |---> x,a,bc |---> x,a(bc)
TTTX --TÛ--> TTX --Û--> TX x,a,b,c |---> x,ab,c |---> x,(ab)c
The duals are:
(;!)=(;!)=id
(;!)=(;!)
!X <--!-- !!X <---- !X
!X <--!-- !!X <---- !X
!X <---------id------ !X
!!!X <--!-- !!X <---- !X
!!!X <--!-- !!X <---- !X
\end{verbatim}
}
\newpage
% --------------------
% «coalgebra-modality» (to ".coalgebra-modality")
% (s "Coalgebra modalities" "coalgebra-modality")
\myslide {Coalgebra modalities} {coalgebra-modality}
{\myttchars
\footnotesize
\begin{verbatim}
The comonad (!,,) is a _coalgebra modality_
if we are given, for every object X, maps:
e
§ <----- !X -----> !X¤!X
Obeying:
-- !X -- !X --------> !X¤!X
id / | \ id | |
/ ¿ | \ ¿ | | ¿¤1
v v v v 1¤¿ v
!X <---- !!X ---> !X !X¤!X -----> !X¤!X¤!X
1¤e e¤1
And this (" is a morphism of comonoids"):
!X -----> !!X !X ----------> !!X
\ | | |
e \ | e ¿ | |
\ v v ¤ v
---> § !X¤!X ------> !!X¤!!X
\end{verbatim}
}
% (find-anggfile ".emacs.papers" "ragsdiff3")
% (find-ragsdiff3page 19)
\newpage
% --------------------
% «term-calculus» (to ".term-calculus")
% (s "The term calculus" "term-calculus")
\myslide {The term calculus} {term-calculus}
{\myttchars
\footnotesize
\begin{verbatim}
The new rule:
a;b|-c a|-b a|-db
(Dt) -------------------
a|-c_{b}db
or, in long form:
a:A,b:B|-c(a,b):C a:A|-b(a):B a:A|-db(a):B
----------------------------------------------
a:A|-c_b(a,b(a))db(a):C
The equations ([S07], slide 20): the usual ones (?), plus these:
(Dt.1) (c+c')_{b}db=c_{b}db+c'_{b}db
0_{b}db=0
(Dt.2) c_{b}(db+db')=c_{b}db+c_{b}db'
(Dt.3a) b_{b}db=db
(Dt.3b) c_{(b,b')}(db,0)=c_{b}db
c_{(b,b')}(0,db')=c_{b'}db'
(Dt.4) (c,c')_{b}db=(c_{b}db,c'_{b}db)
(Dt.5) e_{b}db=e_{c}c_{b}db
(Dt.6) (c_{b}db)_{db}db'=c_{b}db'
\end{verbatim}
}
\newpage
% --------------------
% «term-calculus-long» (to ".term-calculus-long")
% (s "The term calculus: long version" "term-calculus-long")
\myslide {The term calculus: long version} {term-calculus-long}
{\myttchars
\footnotesize
\begin{verbatim}
Longer version, showing all the hypotheses:
a,b|-c a,b|-c' a|-b a|-db
(Dt.1) --------------------------------
a|-(c+c')_{b}db=c_{b}db+c'_{b}db
[a,b|-0] a|-b a|-db
-----------------------
a|-0_{b}db=0
a,b|-c a|-b a|-db a|-db'
(Dt.2) ---------------------------------
a|-c_{b}(db+db')=c_{b}db+c_{b}db'
[a,b|-b] a|-b a|-db
(Dt.3a) -----------------------
a|-b_{b}db=db
a,b,b'|-c a|-b a|-b' a|-db
(Dt.3b) --------------------------------
a|-c_{(b,b')}(db,0)=c_{b}db
a,b,b'|-c a|-b a|-b' a|-db
--------------------------------
a|-c_{(b,b')}(0,db')=c_{b'}db'
a,b|-c a,b|-c' a|-b a|-db
(Dt.4) ----------------------------------
a|-(c,c')_{b}db=(c_{b}db,c'_{b}db)
a,b,c|-e a,b|-c a|-b a|-db
(Dt.5) ----------------------------------
a|-e_{b}db=e_{c}c_{b}db
a,b|-c a|-b a|-db a|-db'
(Dt.6) ------------------------------
a|-(c_{b}db)_{db}db'=c_{b}db'
\end{verbatim}
}
\newpage
% --------------------
% «d-combinator» (to ".d-combinator")
% (s "The D combinator" "d-combinator")
\myslide {The D combinator} {d-combinator}
{\myttchars
\footnotesize
\begin{verbatim}
In the categorical setting the D works like this:
dx,x x
- -
|D[f] |f
v v
dy y
(=y_{x}dx)
In the term calculus the derivative works on one of the variables, not
on all at once, so we need a trick to convert between the two:
a
-
|<<a|-db,0>,<a|-b,1>>
v
(db,0),(b,a) b,a
- -
|D[a,b|-c] |a,b|-c
v v
c_{(b,a)}(db,0) c
=c_{b}db
=dc
So:
a|-c_{b}db := <<a|-db,0>,<a|-b,1>> D [a,b|-c]
[Note: [S07] uses "b" before "a"...]
In the other direction,
D[x|-y] = dx,x|-y_{x}dx
(dx,x),x'|-y dx,x|-x dx,x|-dx
-----------------------------------
dx,x|-y_{x}dx
a,b|-c a|-b a|-db
(Dt) -------------------
a|-c_{b}db
And the other direction?
\end{verbatim}
}
\newpage
% --------------------
% «universals» (to ".universals")
% (s "Universal and couniversal arrows" "universals")
\myslide {Universal and couniversal arrows} {universals}
{\myttchars
\footnotesize
\begin{verbatim}
Units are universal:
/ a \
| - |
/ a \ | | |
| - | | | |
| | | |-> (b -.> | a^L | |)
| v | | - î | |
\ a^L ==> a^LR/ | | |-> | |
| v v |
\ b ===> b^R /
Counits are couniversal:
/ a^L <=== a \
| - - |
/b^RL <== b^R \ | | <-| | |
| - | | | î v |
| | | |-> (a^op -.> | | b^R |)
| v | | | |
\ b / | | |
| v |
\ b /
When a|->a^LR is a unit then the NT "b -.> diagram" is a
natural iso (i.e., for each B the arrow î is a bijection
between hom-sets; this is the definition of "a|->a^LR is
universal").
When b^RL|->b is a counit the NT "a^op -.> diagram" is a
natural iso.
\end{verbatim}
}
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: