% (find-LATEX "2020awodey.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020awodey.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020awodey.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020awodey.pdf"))
% (defun e () (interactive) (find-LATEX "2020awodey.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020awodey"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020awodey.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020awodey.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020awodey.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020awodey.pdf
%               file:///tmp/2020awodey.pdf
%           file:///tmp/pen/2020awodey.pdf
% http://angg.twu.net/LATEX/2020awodey.pdf
% (find-LATEX "2019.mk")

% «.8.2._yoneda-embedding»	(to "8.2._yoneda-embedding")
% «.8.3._yoneda-lemma»		(to "8.3._yoneda-lemma")
% «.9._adjoints»		(to "9._adjoints")
% «.10._monads_and_algebras»	(to "10._monads_and_algebras")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\def\nameof#1{\ulcorner#1\urcorner}
\def\Sets{\mathbf{Sets}}
\def\HomC{\Hom_\catC}
\def\HomS{\Hom_\Sets}



{\setlength{\parindent}{0em}
\footnotesize

Notes on Steve Awodey's ``Category Theory'':

\url{https://www.andrew.cmu.edu/user/awodey/}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020awodey.pdf}

\url{http://angg.twu.net/math-b.html\#notes-on-notation-2020}

}


% __   __                   _                        _     
% \ \ / /__  _ __   ___  __| | __ _    ___ _ __ ___ | |__  
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |  / _ \ '_ ` _ \| '_ \ 
%   | | (_) | | | |  __/ (_| | (_| | |  __/ | | | | | |_) |
%   |_|\___/|_| |_|\___|\__,_|\__,_|  \___|_| |_| |_|_.__/ 
%                                                          
% «8.2._yoneda-embedding»  (to ".8.2._yoneda-embedding")
% (awop 1 "8.2._yoneda-embedding")
% (awo    "8.2._yoneda-embedding")

\section*{8.2 The Yoneda Embedding}

% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 160) "8.2 The Yoneda embedding")
% (find-awodeyctpage (+ 10 161) "Definition 8.1. The Yoneda embedding")
% (find-awodeycttext (+ 10 161) "Definition 8.1. The Yoneda embedding")

Page 161:

Definition 8.1. The Yoneda embedding is the functor $y : \catC \to
\Sets^{\catC^\op}$ taking $C \in \catC$ to the contravariant
representable functor, $yC = \HomC(-, C) : \catC^\op \to \Sets$ and
taking $f : C \to D$ to the natural transformation, $yf = \HomC(-,f) :
\HomC(-,C) \to \HomC(-, D)$.
%
%D diagram yoneda-embedding-awodey
%D 2Dx     100 +40 +30
%D 2D  100         C0
%D 2D               |
%D 2D               v
%D 2D  +25 C1 |--> C2
%D 2D                
%D 2D  +15 C3 ---> C4
%D 2D                
%D 2D  +20 D0 ---> D1
%D 2D               |
%D 2D               v
%D 2D  +25         D2
%D 2D                
%D 2D  +15     D3    
%D 2D
%D ren C0 C1 C2 C3 C4 ==> 1 C \HomC(C,D) \catC^\op \Sets
%D ren D0 D1 D2 D3    ==> \HomC(-,C) \HomS(1,\HomC(-,D)) \HomC(-,D) \Sets^{\catC^\op}
%D
%D (( C0 C2  -> .plabel= r \nameof{f}
%D    C1 C2 |->
%D    C3 C4  -> .plabel= a \HomC(-,D)
%D    
%D    D0 D1 -> D1 D2 <-> .plabel= r ≅
%D    D0 D2 -> .plabel= l yf           # \;=\;\vartheta
%D    D0 D0 midpoint xy+= -31 0 .TeX= yC\;= place
%D    D2 D2 midpoint xy+=  31 0 .TeX= =\;yD place
%D    D3 place
%D    
%D    
%D ))
%D enddiagram
%
$$\pu
  \diag{yoneda-embedding-awodey}
$$


% __   __                   _         _     
% \ \ / /__  _ __   ___  __| | __ _  | |    
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |    
%   | | (_) | | | |  __/ (_| | (_| | | |___ 
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_____|
%                                           
% «8.3._yoneda-lemma»  (to ".8.3._yoneda-lemma")
% (awop 1 "8.3._yoneda-lemma")
% (awo    "8.3._yoneda-lemma")

\section*{8.3 The Yoneda Lemma}

% (find-awodeyctpage (+ 10 162) "8.3 The Yoneda Lemma")
% (find-awodeyctpage (+ 10 162) "Lemma 8.2.(Yoneda).")
% (find-awodeycttext (+ 10 162) "Lemma 8.2.(Yoneda).")

Page 162:

Lemma 8.2 (Yoneda). Let $\catC$ be locally small. For any object $C
\in \catC$ and functor $F \in \Sets^{\catC^\op}$ there is an
isomorphism $\Hom(yC, F) ≅ FC$ which, moreover, is natural in both $F$
and $C$.


%D diagram yoneda-lemma-awodey
%D 2Dx     100 +20 +40
%D 2D  100         A0 
%D 2D               | 
%D 2D               v 
%D 2D  +25 A1 |--> A2 
%D 2D                 
%D 2D  +15 A3 ---> A4 
%D 2D                 
%D 2D  +20 B0 ---> B1 
%D 2D               | 
%D 2D               v 
%D 2D  +25         B2 
%D 2D                 
%D 2D  +15     B3     
%D 2D
%D ren A0 A1 A2 A3 A4 ==> 1 C FC \catC^\op \Sets
%D ren B0 B1 B2 B3    ==> \HomC(-,C) \HomS(1,F-) F \Sets^{\catC^\op}
%D
%D (( A0 A2  -> .plabel= r \nameof{a}
%D    A1 A2 |->
%D    A3 A4  -> .plabel= a F
%D    
%D    B0 B1  ->
%D    B1 B2 <-> .plabel= r ≅
%D    B0 B2  -> .plabel= l \vartheta
%D    B0 B0 midpoint xy+= -31 0 .TeX= yC\;= place
%D    B3 place
%D ))
%D enddiagram
%
$$\pu
  \diag{yoneda-lemma-awodey}
$$



% (find-awodeyctpage (+ 10 167) "8.5 Limits in categories of diagrams")
% (find-awodeyctpage (+ 10 168) "8.6 Colimits in categories of diagrams")
% (find-awodeyctpage (+ 10 171)   "free cocompletion")
% (find-awodeyctpage (+ 10 172) "8.7 Exponentials in categories of diagrams")
% (find-awodeyctpage (+ 10 176) "8.9 Exercises")




%     _       _  _       _       _       
%    / \   __| |(_) ___ (_)_ __ | |_ ___ 
%   / _ \ / _` || |/ _ \| | '_ \| __/ __|
%  / ___ \ (_| || | (_) | | | | | |_\__ \
% /_/   \_\__,_|/ |\___/|_|_| |_|\__|___/
%             |__/                       
%
% «9._adjoints»  (to ".9._adjoints")
% (find-awodeyctpage (+ 10 179) "9 Adjoints")
% (find-awodeyctpage (+ 10 179) "9.1 Preliminary definition")
% (find-awodeyctpage (+ 10 180)   "eta")
% (find-awodeyctpage (+ 10 180) "Definition 9.1 (preliminary)")
% (find-awodeycttext (+ 10 180) "Definition 9.1 (preliminary)")
% (find-awodeyctpage (+ 10 183) "9.2 Hom-set definition")
% (find-awodeyctpage (+ 10 187) "9.3 Examples of adjoints")

\newpage

\section*{9. Adjoints}

(Page 180):

Definition 9.1 (preliminary). An adjunction between categories $\catC$ and $\catD$
consists of functors
%
$$F : \catC \two/<-`->/<250> \catD : U$$
%
and a natural transformation $η:1_C → U∘F$ with the UMP
$∀C.∀D.∀f.∃!g.▁$ below.

(Page 183):

% (find-awodeyctpage (+ 10 183) "9.2 Hom-set definition")
% (find-awodeycttext (+ 10 183) "9.2 Hom-set definition")

9.2 Hom-set definition

Proposition 9.4. Given categories and functors $\catC$, $\catD$, $F$,
$U$, the following conditions are equivalent:

\begin{enumerate}

\item $F$ is left adjoint to $U$; that is, there is a natural
transformation $η: 1_C → U∘F$ with the UMP $∀C.∀D.∀f.∃!g.▁$ below;

\item For any $C∈\catC$ and $D∈\catD$ there is an isomorphism
%
$$φ: \Hom_\catD(F C, D) → \Hom_\catC(C, U D)$$
%
that is natural in both $C$ and $D$.

\end{enumerate}
%
%D diagram adjoints
%D 2Dx     100 +25 +20 +20 +20 +20 +20 +20 +20 +25
%D 2D  100                                     R1
%D 2D
%D 2D  +20 L0  L1  A0  B0  C0  C1  E0  F0  R2  R3
%D 2D
%D 2D  +20 L2  L3  A1  B1  C2  C3  E1  F1  R4  R5
%D 2D
%D 2D  +20 L4              D0  D1
%D 2D
%D 2D  +20
%D 2D
%D ren A0 A1       ==> F{∘}U 1_\catD
%D ren B0 B1       ==> FUD D
%D ren C0 C1 C2 C3 ==> FC C D UD
%D ren D0 D1       ==> \catD \catC
%D ren E0 E1       ==> C UFC
%D ren E0 E1       ==> C UFC
%D ren F0 F1       ==> 1_\catC U{∘}F
%D ren R1 R2 R3 R4 R5 ==> ∀C FC UFC ∀D UD
%D ren L0 L1 L2 L3 L4 ==> FC ∀C FUD UD ∀D
%D
%D (( A0 A1 ->      .plabel= l ε
%D    B0 B1 ->      .plabel= l ε_D
%D    C0 C1 <-|
%D    C0 C2  ->     .plabel= l g
%D    C1 C3  ->     .plabel= r f
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil <-| sl^ .plabel= a ψ
%D    C0 C3 harrownodes nil 20 nil |-> sl_ .plabel= b ϕ
%D    D0 D1  <- sl^ .plabel= a F
%D    D0 D1  -> sl_ .plabel= b U
%D    E0 E1  ->     .plabel= r η_C
%D    F0 F1  ->     .plabel= r η
%D    R1 R3  ->     .plabel= r η_C
%D    R2 R3 |->
%D    R2 R4  ->     .plabel= l ∃!g
%D    R3 R5  ->     .plabel= r Ug
%D    R4 R5 |->
%D    R1 R5  -> .slide= 20pt .plabel= r ∀f
%D    R2 R5 harrownodes nil 20 nil |-> .plabel= b ϕ
%D    L0 L1 <-|
%D    L0 L2  ->     .plabel= l Ff
%D    L1 L3  ->     .plabel= r ∃!f
%D    L2 L3 <-|
%D    L2 L4  ->     .plabel= l ε_D
%D    L0 L4  -> .slide= -20pt .plabel= l ∀g
%D    L0 L3 harrownodes nil 20 nil <-| .plabel= a ψ
%D
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{adjoints}
$$

% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 187) "9.3 Examples of adjoints")


\newpage

%  __  __                       _     
% |  \/  | ___  _ __   __ _  __| |___ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|
% | |  | | (_) | | | | (_| | (_| \__ \
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/
%                                     
% «10._monads_and_algebras»  (to ".10._monads_and_algebras")
% (awop 3 "10._monads_and_algebras")
% (awo    "10._monads_and_algebras")

\section*{10. Monads and algebras}

% (find-awodeyctpage (+ 10 223) "10 Monads and algebras")
% (find-awodeycttext (+ 10 223) "10 Monads and algebras")
% (find-awodeyctpage (+ 10 223) "10.1 The triangle identities")
% (find-awodeyctpage (+ 10 225) "10.2 Monads and adjoints")

% (find-awodeyctpage (+ 10 228) "Example 10.4. Let P be a poset.")
% (find-awodeycttext (+ 10 228) "Example 10.4. Let P be a poset.")

Example 10.4 (p.228): Let $P$ be a poset.

%D diagram example-10.4
%D 2Dx     100 +20 +20
%D 2D  100 A0  A1  B0
%D 2D
%D 2D  +20 A2  A3  B1
%D 2D
%D 2D  +20 A4  A5  B2
%D 2D
%D ren A0 A1 A2 A3 ==> tp p k ik
%D ren A4 A5       ==> k p
%D ren B0 B1 B2    ==> 1 T T^2
%D
%D (( A0 A1 <-|
%D    A0 A2 -> A1 A3 ->
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    A0 A3 harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D
%D    A4 A5 <- sl^ .plabel= a t
%D    A4 A5 -> sl_ .plabel= b i
%D
%D    B0 B1 -> .plabel= r η
%D    B1 B2 -> .plabel= r μ=\id
%D ))
%D enddiagram
%D
$$\pu
  \diag{example-10.4}
$$

Example 10.5: $(\Pts,\{-\},\bigcup)$ on $\Sets$

% (find-awodeyctpage (+ 10 228) "Example 10.5" "singleton operation")
% (find-awodeycttext (+ 10 228) "Example 10.5" "singleton operation")

Proposition 10.6: Eilenberg-Moore

%D diagram 10.6-EM-1
%D 2Dx     100 +30 +30 +20 +20
%D 2D  100 L0  A0  A1  R0  M0
%D 2D
%D 2D  +20 L1  A2  A3  R1  M1
%D 2D
%D 2D  +20     A4  A5      M2
%D 2D
%D ren L0 L1       ==> (TA,μA) (A,α)
%D ren A0 A1 A2 A3 ==> (TC,μC) C (A,α) A
%D ren A4 A5       ==> \catC^T \catC
%D ren R0 R1       ==> C TC
%D ren M0 M1 M2    ==> 1 T T^2
%D
%D (( L0 L1 -> .plabel= l α
%D
%D    A0 A1 <-|
%D    A0 A2 -> .plabel= l \sm{Tg;α\\f}
%D    A1 A3 -> .plabel= r \sm{g;ηC;f}
%D    A2 A3 |->
%D    A4 A5 <- sl^ .plabel= a F
%D    A4 A5 -> sl_ .plabel= b U
%D
%D    R0 R1 -> .plabel= r ηC
%D    M0 M1 -> .plabel= r η
%D    M1 M2 <- .plabel= r μ
%D ))
%D enddiagram
%D
$$\pu
  \diag{10.6-EM-1}
$$



%D diagram 10.6-EM-2
%D 2Dx     100 +30 +30
%D 2D  100 D       C
%D 2D
%D 2D  +30     CT
%D 2D
%D ren D C CT ==> \catD \catC \catC^T
%D
%D (( D C <- sl^ .plabel= a F
%D    D C -> sl_ .plabel= b U
%D    
%D    CT C <- sl^ .plabel= a F^T
%D    CT C -> sl_ .plabel= b U^T
%D    
%D    D CT -> .plabel= l \Phi
%D ))
%D enddiagram
%D
$$\pu
  \diag{10.6-EM-2}
$$




%D diagram 10.6-EM-3
%D 2Dx     100 +35  +5  +35  +40
%D 2D  100     A0            A1
%D 2D  +8  L0  A2            A3
%D 2D  +8                    B1
%D 2D  +8                    B3
%D 2D
%D 2D  +20              B0
%D 2D  +8           L1  B2
%D 2D
%D ren A0 A1 A2 A3 ==> FC C D UD
%D ren B0 B1 B2 B3 ==> (UFC,μC) C (A,α) A
%D ren L0 L1       ==> D (UD,UεD)
%D
%D (( A0 place A1 place A2 place A3 place
%D    B0 place B1 place B2 place B3 place
%D    
%D    A0 A1 harrownodes nil 30 nil <-|
%D    A2 A3 harrownodes nil 30 nil |->
%D
%D    B0 B1 dharrownodes 10 15 nil <-|
%D    B2 B3 dharrownodes 10 15 nil |->
%D
%D    L0 L1 |->
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{10.6-EM-3}
$$







% (find-awodeyctpage (+ 10 229) "10.3 Algebras for a monad")
% (find-awodeyctpage (+ 10 234) "10.4 Comonads and coalgebras")
% (find-awodeyctpage (+ 10 236) "10.5 Algebras for endofunctors")
% (find-awodeyctpage (+ 10 244) "10.6 Exercises")




\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020awodey veryclean
make -f 2019.mk STEM=2020awodey pdf

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

