|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2016-2-LA-cats.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-2-LA-cats.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-2-LA-cats.pdf"))
% (defun e () (interactive) (find-LATEX "2016-2-LA-cats.tex"))
% (defun u () (interactive) (find-latex-upload-links "2016-2-LA-cats"))
% (find-xpdfpage "~/LATEX/2016-2-LA-cats.pdf")
% (find-sh0 "cp -v ~/LATEX/2016-2-LA-cats.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2016-2-LA-cats.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2016-2-LA-cats.pdf
% file:///tmp/2016-2-LA-cats.pdf
% file:///tmp/pen/2016-2-LA-cats.pdf
% http://angg.twu.net/LATEX/2016-2-LA-cats.pdf
%
% «.composition» (to "composition")
% «.lateral-inverses» (to "lateral-inverses")
% «.multiple-inverses» (to "multiple-inverses")
% «.no-inverses» (to "no-inverses")
% «.products» (to "products")
% «.exponentials» (to "exponentials")
\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage{tikz}
%
\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")
%
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\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 "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}
\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\app{\operatorname{app}}
\def\ren{\operatorname{ren}}
\def∧{\&}
\def\namedfunction#1#2#3#4#5{
\begin{array}{rrcl}
#1: & #2 & → & #3 \\
& #4 & ↦ & #5 \\
\end{array}
}
% _ _ _
% ___ ___ _ __ ___ _ __ ___ ___(_) |_(_) ___ _ __
% / __/ _ \| '_ ` _ \| '_ \ / _ \/ __| | __| |/ _ \| '_ \
% | (_| (_) | | | | | | |_) | (_) \__ \ | |_| | (_) | | | |
% \___\___/|_| |_| |_| .__/ \___/|___/_|\__|_|\___/|_| |_|
% |_|
%
% «composition» (to ".composition")
% (lac162p 1 "composition")
Composition
(is associative)
%L mapstos_1 = function (str)
%L local n, latex = 0, ""
%L for d in str:gmatch("%d") do
%L latex = latex .. format("%d \\mapsto %d \\\\\n", n, d)
%L n = n + 1
%L end
%L return latex
%L end
%L
%L mapstos_2 = function (str)
%L local latex = ""
%L for a,b in str:gmatch("(%d)(%d)") do
%L latex = latex .. format("%d \\mapsto %d \\\\\n", a, b)
%L end
%L return latex
%L end
\pu
\def\mapsb #1{\sm{\expr{mapstos_1("#1")}}}
\def\mapsab#1{\sm{\expr{mapstos_2("#1")}}}
% \bsk
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren a b ==> \{1,2\} \{3,4\}
%D ren c d ==> \{5,6\} \{7,8\}
%D (( A B -> .plabel= a f
%D B C -> .plabel= m g
%D C D -> .plabel= b h
%D A C -> .plabel= l (g∘f=)\;\;f;g
%D B D -> .plabel= r g;h\;\;(=h∘g)
%D
%D a b -> .plabel= a \mapsab{13,24}
%D b c -> .plabel= m \mapsab{36,45}
%D c d -> .plabel= b \mapsab{57,67}
%D a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
%D diagram composition-1
%D 2Dx 100 +30 +30 +30
%D 2D 100 D <-- C <-- B <-- A
%D 2D
%D (( D A <- .plabel= a (h∘g)∘f .slide= 22pt
%D D B <- .plabel= a h∘g .slide= 10pt
%D D C <- .plabel= m h C B <- .plabel= m g B A <- .plabel= m f
%D C A <- .plabel= b g∘f .slide= -10pt
%D D A <- .plabel= b h∘(g∘f) .slide= -22pt
%D ))
%D enddiagram
%D
%
$$\begin{array}{rcl}
((h∘g)∘f)(a) &=& (h∘g)(f(a)) \\
&=& h(g(f(a))) \\
&=& h((g∘f)(a)) \\
&=& (h∘(g∘f))(a) \\[5pt]
((h∘g)∘f)(a) &=& (h∘(g∘f))(a) \\[5pt]
(h∘g)∘f &=& h∘(g∘f) \\
\end{array}
\qquad
\Diag{composition-1}
$$
\bsk
\bsk
Identities:
If $f:A→B$ then $\id_A;f = f = f;\id_B$
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren A B ==> A A
%D ren C D ==> B B
%D ren a b ==> \{1,2\} \{1,2\}
%D ren c d ==> \{3,4\} \{3,4\}
%D (( A B -> .plabel= a \id_A
%D B C -> .plabel= m f
%D C D -> .plabel= b \id_B
%D A C -> .plabel= l f\;=\;\id_A;f
%D B D -> .plabel= r f;\id_B\;=\;f
%D
%D a b -> .plabel= a \mapsab{11,22}
%D b c -> .plabel= m \mapsab{13,24}
%D c d -> .plabel= b \mapsab{33,44}
%D a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
% «lateral-inverses» (to ".lateral-inverses")
A theorem about lateral inverses:
If $f;g = \id$ and $g;h=\id$ then $f=h$
%D diagram ??
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 A --> B a --> b
%D 2D | |
%D 2D v v
%D 2D +35 C --> D c --> d
%D 2D
%D ren A B ==> B A
%D ren C D ==> B A
%D ren a b ==> \{1,2\} \{1,2\}
%D ren c d ==> \{3,4\} \{3,4\}
%D (( A B -> .plabel= a f
%D B C -> .plabel= m g
%D C D -> .plabel= b h
%D A C -> .plabel= l \id_B\;=\;f;g
%D B D -> .plabel= r \id_A\;=\;g;h
%D
%D # a b -> .plabel= a \mapsab{11,22}
%D # b c -> .plabel= m \mapsab{13,24}
%D # c d -> .plabel= b \mapsab{33,44}
%D # a c -> b d ->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
\qquad
\begin{array}{rcl}
\multicolumn {3}{c} {(f;g);h = \id_B;h = h} \\
\multicolumn {3}{c} {f;(g;h) = f;\id_A = f} \\[5pt]
f &=& f;\id_A \\
&=& f;(g;h) \\
&=& (f;g);h \\
&=& \id_B;h \\
&=& h
\end{array}
$$
\newpage
% «multiple-inverses» (to ".multiple-inverses")
% (lac162p 2 "multiple-inverses")
Multiple inverses
%L forths["->>"] = function () pusharrow("->>") end
%D diagram ??
%D 2Dx 100 +35 +35 +35
%D 2D 100 A --> B D
%D 2D | |
%D 2D v v
%D 2D +35 C E --> F
%D 2D
%D ren A B D ==> \{1,2\} \{3,4,5\} \{5,6\}
%D ren C E F ==> \{1,2\} \{7,8,9\} \{5,6\}
%D (( A B >-> sl^ .plabel= a ? A B >-> sl_ .plabel= b ?
%D B C ->> .plabel= r \mapsab{31,42,52}
%D A C -> .plabel= l \id
%D
%D D E ->> .plabel= l \mapsab{57,68}
%D E F >-> sl^ .plabel= a ? E F >-> sl_ .plabel= b ?
%D D F -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
\def\frown{=(}
% «no-inverses» (to ".no-inverses")
No inverses
%D diagram ??
%D 2Dx 100 +35 +35 +10 +35 +35
%D 2D 100 A --> B E --> F
%D 2D | |
%D 2D v v
%D 2D +35 C --> D G --> H
%D 2D
%D ren A B E F ==> \{3,4,5\} \{1,2\} \{8,9\} \{5,6,7\}
%D ren C D G H ==> \{3,4,5\} \{1,2\} \{8,9\} \{5,6,7\}
%D (( A B -> .plabel= a \frown
%D B C >-> .plabel= m \mapsab{13,24}
%D A C -> .plabel= l \id
%D C D ->> sl^ C D ->> sl_
%D B D -> .plabel= r \id
%D
%D E G -> .plabel= l \id
%D E F >-> sl^ E F >-> sl_
%D F G ->> .plabel= m \mapsab{58,69,79}
%D G H -> .plabel= b \frown
%D F H -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%D diagram ??
%D 2Dx 100 +35 +35
%D 2D 100 A --> B
%D 2D |
%D 2D v
%D 2D +35 C --> D
%D 2D
%D ren A B ==> \{4,5,6\} \{1,2,3\}
%D ren C D ==> \{4,5,6\} \{1,2,3\}
%D (( A B -> .plabel= a \frown
%D B C -> .plabel= m \mapsab{14,25,35}
%D C D -> .plabel= r \frown
%D A C -> .plabel= l \id
%D B D -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
\bsk
\bsk
\bsk
% «products» (to ".products")
% (lac162p 2 "products")
{\bf Products}
Property: $∀f,g.∃!h.(f=h;π\;∧\;g=h;π')$
Solution: $h=λa:A.(f(a),g(a))$
Bijection: $(f,g)↔h$
$(→)$: $λ(f,g).(λa:A.(f(a),g(a)))$
$(←)$: $λh.((h;π),(h;π'))$
\bsk
%D diagram product-ABC
%D 2Dx 100 +45 +45
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +45 B <-- BxC --> C
%D 2D
%D ren A ==> A
%D ren B BxC C ==> B B×C C
%D
%D (( A B -> .plabel= l f
%D A BxC -> .plabel= m h
%D A C -> .plabel= r g
%D B BxC <- .plabel= b π\mathstrut
%D BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
%D diagram product-explicit
%D 2Dx 100 +45 +45
%D 2D 100 A
%D 2D |
%D 2D v
%D 2D +45 B <-- BxC --> C
%D 2D
%D ren A ==> \{1,2\}
%D ren B BxC C ==> \{3,4\} \csm{(3,5),(3,6),\\(4,5),(4,6)} \{5,6\}
%D
%D (( A B -> .plabel= l \mapsab{13,24}
%D A BxC -> .plabel= m \midmap
%D A C -> .plabel= r \mapsab{15,26}
%D B BxC <- .plabel= b π\mathstrut
%D BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
$$\pu
\def\midmap{\sm{1↦(3,5)\\2↦(4,6)}}
%
\diag{product-ABC}
\qquad
\diag{product-explicit}
$$
\newpage
% «exponentials» (to ".exponentials")
% (lac162p 3 "exponentials")
{\bf Exponentials}
Bijection: $f↔g$
$(→)$ (``currying''): $g := \cur f := λa:A.λb:B.f(a,b)$
$(←)$ (``uncurrying''): $f := \uncur g := λ(a,b):A×B.((g(a))(b))$
\bsk
%D diagram exponentials-ABC
%D 2Dx 100 +45
%D 2D 100 AxB <--| A
%D 2D | |
%D 2D | <-> |
%D 2D v v
%D 2D +50 C |--> B->C
%D 2D
%D ren AxB A ==> A×B A
%D ren C B->C ==> C B{→}C
%D (( AxB A <-| .plabel= a λA.(A×B)
%D C B->C |-> .plabel= b λC.(B{→}C)
%D AxB C -> .plabel= l f
%D A B->C -> .plabel= r g
%D A C harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram exponentials-explicit
%D 2Dx 100 +60
%D 2D 100 AxB <--| A
%D 2D | |
%D 2D | <-> |
%D 2D v v
%D 2D +50 C |--> B->C
%D 2D
%D ren AxB A ==> \csm{(1,3),(1,4)\\(2,3),(2,4)} \{1,2\}
%D ren C B->C ==> \{5,6\} \csm{\fu55,\fu56,\\\fu65,\fu66}
%D (( AxB A <-|
%D C B->C |->
%D AxB C -> .plabel= l \sm{(1,3)↦5\\(1,4)↦6\\(2,3)↦6\\(2,4)↦5}
%D A B->C -> .plabel= r \sm{1↦\fu56\\2↦\fu65}
%D A C harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\def\fu#1#2{\csm{(3,#1),\\(4,#2)}}
\diag{exponentials-ABC}
\diag{exponentials-explicit}
$$
\bsk
\bsk
Properties: $\cur \uncur f = f$, \; $\uncur \cur g = g$
where: $f×f' := \ang{π;f,\,π';f'}$, \; $\uncur g := (g×\id);\ev$
solving type equations:
\bsk
%:*"* *
%:
%:
%: π f π' f' π:A×?→A f:A→B π':?×A'→A' f':A'→B'
%: ----- ------ ------ ------------ ---------------------
%: π;f π';f' π;f:A×?→B π';f':?×A'→B'
%: ---------------- ----------------------------------------
%: \ang{π;f,\,π';f'} \ang{π;f,\,π';f'}:A×A'→B×B'
%: ------------------\ren ----------------------------\ren
%: f×f' f×f':A×A'→B×B'
%:
%: ^fxf'_1 ^fxf'_2
%:
%:
%: g \id g:A→(B{→}C) \id:?→?
%: ------ ----------------------
%: g×\id \ev g×\id:A×?→(B{→}C)×? \ev:(B{→}C)×B→C
%: ----------- -----------------------------------------
%: (g×\id);\ev (g×\id);\ev:A×?→C
%: -----------\ren ------------------
%: \uncur"g \uncur"g:A×?→C
%:
%: ^uncur_g_1 ^uncur_g_2
%:
\pu
$$\ded{fxf'_1} \qquad \ded{fxf'_2}$$
$$\ded{uncur_g_1} \qquad \ded{uncur_g_2}$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: