|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017adjunctions.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017adjunctions.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017adjunctions.pdf"))
% (defun e () (interactive) (find-LATEX "2017adjunctions.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017adjunctions"))
% (find-xpdfpage "~/LATEX/2017adjunctions.pdf")
% (find-sh0 "cp -v ~/LATEX/2017adjunctions.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017adjunctions.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017adjunctions.pdf
% file:///tmp/2017adjunctions.pdf
% file:///tmp/pen/2017adjunctions.pdf
% http://angg.twu.net/LATEX/2017adjunctions.pdf
\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")
%
\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
%:*->*\to *
\newpage
\def\Sets{\mathsf{Sets}}
$π$ and $π'$ are natural transformations
$(×):\Set×\Set→\Set$
$(→):\Set^\op×\Set→\Set$
\msk
$(×):\Set×\Set→\Set$
$A,B,A',B':\Objs(\Set)$
$(A,B),(A',B'):\Objs(\Set×\Set)$
$(α,β):(A,B)→(A',B')$
$(α,β):\Hom_{\Set×\Set}((A,B),(A',B'))$
%D diagram foo
%D 2Dx 100 +45 +55 +45
%D 2D 100 A1 |--> A2 B1 |--> B2
%D 2D | | | |
%D 2D | |--> | | |--> |
%D 2D v v v v
%D 2D +30 A3 |--> A4 B3 |--> B4
%D 2D
%D ren A1 A2 ==> (A,B) (×)_0(A,B)
%D ren A3 A4 ==> (A',B') (×)_0(A',B')
%D ren B1 B2 ==> (A,B) A×B
%D ren B3 B4 ==> (A',B') A'×B'
%D (( A1 A2 |-> .plabel= a (×)_0
%D A1 A3 -> .plabel= l (α,β)
%D A2 A4 -> .plabel= r (×)_1(α,β)
%D A3 A4 |-> .plabel= b (×)_0
%D A1 A4 harrownodes nil 20 nil |-> .plabel= a (×)_1
%D B1 B2 |-> .plabel= a (×)_0
%D B1 B3 -> .plabel= l (α,β)
%D B2 B4 -> .plabel= r \color{red}{α×β}
%D B3 B4 |-> .plabel= b (×)_0
%D B1 B4 harrownodes nil 20 nil |-> .plabel= a (×)_1
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
%D diagram bar
%D 2Dx 100 +45 +55 +45
%D 2D 100 A1 |--> A2 B1 |--> B2
%D 2D | | | |
%D 2D | |--> | | |--> |
%D 2D v v v v
%D 2D +30 A3 |--> A4 B3 |--> B4
%D 2D
%D ren A1 A2 ==> (A^\op,B) (→)_0(A^\op,B)
%D ren A3 A4 ==> ({A'}^\op,B') (→)_0({A'}^\op,B')
%D ren B1 B2 ==> (A^\op,B) A{→}B
%D ren B3 B4 ==> ({A'}^\op,B') A'{→}B'
%D (( A1 A2 |-> .plabel= a (→)_0
%D A1 A3 -> .plabel= l (α^\op,β)
%D A2 A4 -> .plabel= r (→)_1(α^\op,β)
%D A3 A4 |-> .plabel= b (→)_0
%D A1 A4 harrownodes nil 20 nil |-> .plabel= a (→)_1
%D B1 B2 |-> .plabel= a (→)_0
%D B1 B3 -> .plabel= l (α^\op,β)
%D B2 B4 -> .plabel= r \color{red}{α→β}
%D B3 B4 |-> .plabel= b (→)_0
%D B1 B4 harrownodes nil 20 nil |-> .plabel= a (→)_1
%D ))
%D enddiagram
%D
$$\pu
\diag{bar}
$$
%:
%: α:A->A' β:B->B'
%: ----------------
%: α×β:A×B->A'×B'
%:
%: ^dp1
%:
%: A B A B
%: ------π -----π'
%: :A×B->A α:A->A' :A×B->B β:B->B'
%: -----------------; -----------------;
%: :A×B->A' :A×B->B'
%: ---------------------------\ang{,}
%: :A×B->A'×B'
%:
%: ^dp2
%:
\pu
$$\ded{dp1}$$
$$\ded{dp2}$$
$$α×β \;\;:=\;\; \ang{(π;α),(π';β)}$$
$$(×)_1(α,β) \;\;:=\;\; α×β$$
$$(×)_1(γ) \;\;:=\;\; (πγ)×(π'γ)$$
%:
%: α^\op:A^\op->{A'}^\op
%: ---------------------
%: α:A'->A β:B->B'
%: -------------------------------
%: α{→}β:(A{→}B)->(A'→B')
%:
%: ^di1
%:
%: α:A'->A [f:A→B]^1 β:B->B'
%: ---------------------------------;;
%: α;f;β:A'→B'
%: ---------------------------------------λ
%: λf{:}A{→}B.(α;f;β):(A{→}B)→(A'{→}B')
%:
%: ^di2
%:
\pu
$$\ded{di1}$$
$$\ded{di2}$$
$$α{→}β \;\;:=\;\; λf{:}A{→}B.(α;f;β)$$
$$(→)_1(α^\op,β) \;\;:=\;\; α{→}β$$
$$(×)_1(δ) \;\;:=\;\; (πδ)^\op{}→(π'δ)$$
%:
%: A:\Objs(\catA) B:\Objs(\catB)
%: -------------------------------(×)_0
%: (A,B):\Objs(\catA×\catB)
%:
%: ^da
%:
%: A:\Objs(\Set) B:\Objs(\Set)
%: -------------------------------(×)_0
%: (A,B):\Objs(\Set×\Set)
%:
%: ^db
%:
%: A:\Sets B:\Sets
%: -----------------×
%: A×B:\Sets
%:
%: ^dc
\pu
$$\ded{da}$$
$$\ded{db}$$
$$\ded{dc}$$
\newpage
%:
%: A'\ton{α}A A\ton{f}RB A'\ton{α}A A\ton{f}RB
%: -----------------------; ----------L_1 ----------♭
%: A'->RB LA'->LA LA->B
%: ------♭ = ---------------------;
%: LA'->B LA'->B
%:
%: ^nat-fl-1 ^nat-fl-2
%:
%: LA\ton{g}B B\ton{β}B' LA\ton{g}B B\ton{β}B'
%: -----------------------; ----------♭ ----------R_1
%: LA->B' A->RB RB->RB'
%: ------♯ = -------------------♯
%: A->RB' A->RB'
%:
%: ^nat-sh-1 ^nat-sh-2
%:
Naturalities:
%
$$\pu
\begin{array}{lcrcl}
(α;f)^♭ = Lα;f^♭ && \ded{nat-fl-1} &=& \ded{nat-fl-2} \\\\
(g;β)^♯ = g^♯;Rβ && \ded{nat-sh-1} &=& \ded{nat-sh-2} \\\\
\end{array}
$$
\bsk
%: Interdefinabilities:
%:
%: A
%: --L_0
%: LA
%: ------\id
%: A LA->LA
%: ------η = ------♯
%: A->RLA A->RLA η_A = (\id_{LA})^♯
%:
%: ^idef-eta-1 ^idef-eta-2
%:
%: B
%: --R_0
%: RB
%: ------\id
%: B RB->RB
%: ------ε = ------♭ ε_B = (\id_{RB})^♭
%: LRB->B LRB->B
%:
%: ^idef-eps-1 ^idef-eps-2
%:
%: A
%: ------η
%: A'\ton{α}A A->RLA
%: -------------------;
%: A'\ton{α}A A'->RLA
%: ----------L_1 = -------♭
%: LA'->LA LA'->LA
%:
%: ^idef-L1-1 ^idef-L1-2 Lα = (α;η_A)^♭
%:
%: B
%: ------ε
%: LRB->B B\ton{β}B'
%: -------------------;
%: B\ton{β}B' LRB->B'
%: ----------R_1 = -------♭
%: RB->RB' RB->RB' Rβ = (η_B;β)^♯
%:
%: ^idef-R1-1 ^idef-R1-2
%:
%:
%: A\ton{g}RB B
%: ----------L_1 ------ε
%: A\ton{g}RB LA->LRB LRB->B
%: ----------♭ = --------------------;
%: LA->B LA->B g^♭ = Lg;ε_B
%:
%: ^idef-fl-1 ^idef-fl-2
%:
%: A LA\ton{f}B
%: ------η ----------R_1
%: LA\ton{f}B A->RLA RLA->RB
%: ----------♯ = -------------------;
%: A->RB A->RB f^♯ = η_A;Rf
%:
%: ^idef-sh-1 ^idef-sh-2
%:
Interdefinabilities:
%
$$\pu
\begin{array}{lcrcl}
η_A = (\id_{LA})^♯ && \ded{idef-eta-1} &=& \ded{idef-eta-2} \\\\
Lα = (α;η_A)^♭ && \ded{idef-L1-1} &=& \ded{idef-L1-2} \\\\
g^♭ = Lg;ε_B && \ded{idef-fl-1} &=& \ded{idef-fl-2} \\\\
f^♯ = η_A;Rf && \ded{idef-sh-1} &=& \ded{idef-sh-2} \\
Rβ = (η_B;β)^♯ && \ded{idef-R1-1} &=& \ded{idef-R1-2} \\\\
ε_B = (\id_{RB})^♭ && \ded{idef-eps-1} &=& \ded{idef-eps-2} \\\\
\end{array}
$$
\newpage
\def\p{\phantom}
Expensive adjunction: $(\catA, \catB, L, R, ♭, ♯, η, ε)$
Cheap adjunction 1: $\;\;\;(\catA, \catB, L, R, \, ♭, ♯ \p{, η, ε})$
Cheap adjunction 2: $\;\;\;(\catA, \catB, L, R, \p{♭, ♯,} η, ε)$
Cheap adjunction 3: $\;\;\;(\catA, \catB, L, R_0, \p{β,} ♯, η \p{,ε}\!)$
Cheap adjunction 4: $\;\;\;(\catA, \catB, L_0, R, ♭, \p{♯, η,} ε)$
\bsk
Bijection:
$f = (f^♯)^♭ = L(η_A;Rf);ε_B = Lη_A;LRf;ε_B$
$g = (g^♭)^♯ = η_A;R(Lg;ε_B) = η_A;RLg;Rε_B$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: