% (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:
