|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2021sgl.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021sgl.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2021sgl.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021sgl.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021sgl.pdf"))
% (defun e () (interactive) (find-LATEX "2021sgl.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021sgl"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2021sgl.pdf"))
% (code-eec-LATEX "2021sgl")
% (find-pdf-page "~/LATEX/2021sgl.pdf")
% (find-xournalpp "~/LATEX/2021sgl.pdf")
% (find-sh0 "cp -v ~/LATEX/2021sgl.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021sgl.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021sgl.pdf
% file:///tmp/2021sgl.pdf
% file:///tmp/pen/2021sgl.pdf
% http://angg.twu.net/LATEX/2021sgl.pdf
% http://angg.twu.net/LATEX/2021sgl.tex.html
% (find-LATEX "2019.mk")
% (find-lualatex-links "2021sgl")
% «.defs» (to "defs")
% «.monics-in-Set^2» (to "monics-in-Set^2")
% «.page-26-yoneda» (to "page-26-yoneda")
% «.page-32-true-terminal» (to "page-32-true-terminal")
% «.pages-35-36-Set^2» (to "pages-35-36-Set^2")
% «.page-57-theorem-1» (to "page-57-theorem-1")
% «.page-58-theorem-2» (to "page-58-theorem-2")
% «.pages-58-59-theorem-2» (to "pages-58-59-theorem-2")
% «.page-63-exercise-8» (to "page-63-exercise-8")
% «.page-63-exercise-10» (to "page-63-exercise-10")
\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{edrx21} % (find-LATEX "edrx21.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")
%\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
%top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
top=1.5cm, bottom=.25cm, left=0.5cm, right=0.5cm, includefoot
]{geometry}
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
% «defs» (to ".defs")
\def\drafturl{http://angg.twu.net/LATEX/2021sgl.pdf}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
\def\Nat {\text{Nat}}
\def\phop {{}^{\phantom{\op}}}
\def\Cop {{\catC^\op}}
\def\SetsCop {\Sets^{\catC^\op}}
\def\hatC {{\widehat\catC}}
\def\OXop {\Opens(X)^\op}
\def\SetsOXop{\Sets^{\Opens(X)^\op}}
\def\univ {\mathsf{univ}}
\def\Spaces {\mathbf{Spaces}}
\def\Locales {\mathbf{Locales}}
\def\Frames {\mathbf{Frames}}
\def\Top {\mathbf{Top}}
\def\Bund {\mathbf{Bund}}
\def\Loc {\mathrm{Loc}}
\def\Ker {\operatorname{Ker}}
\def\Pt {\operatorname{pt}}
\def\Sh {\operatorname{Sh}}
\def\PSh {\operatorname{PSh}}
\def\acz {\setlength{\arraycolsep}{0pt}}
\def\y {\mathbf{y}}
\def\HomC {\Hom_\catC}
\def\True {\mathbf{T}}
\def\False {\mathbf{F}}
\def\goneism{\text{$g_1$ is monic}}
\def\gtwoism{\text{$g_2$ is monic}}
\def\gonetwoism{\text{$(g_1,g_2)$ is monic}}
\def\incgr#1#2{\myvcenter{\includegraphics[#1]{#2}}}
\def\scale#1#2{\scalebox{#1}{$#2$}}
% (find-LATEX "2020clops-and-tops.tex" "defs")
\def\Incs {\mathsf{Incs}}
% «monics-in-Set^2» (to ".monics-in-Set^2")
\def\und#1#2{\underbrace{#1}_{\textstyle#2}}
\def\nound#1#2{#1}
Proposition: a morphism $g=(g_1,g_2)$ in $\Set^2$ is a monic
if and only if its two components, $g_1$ and $g_2$, are monics in $\Set$.
\msk
With the right abbreviations, this becomes:
$(\gonetwoism) ↔ (\goneism) ∧ (\gtwoism)$
\msk
We will use the diagrams below.
%D diagram ??
%D 2Dx 100 +30 +25 +50 +40 +30 +15 +30
%D 2D 100 A0 = A1 B0 = B1 C0 = C1 D0 = D1
%D 2D \ | \ | \ | \ |
%D 2D +30 A2 B2 C2 D2
%D 2D
%D ren A0 A1 A2 ==> ∀A B C
%D ren B0 B1 B2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren C0 C1 C2 ==> ∀A_1 B_1 C_1
%D ren D0 D1 D2 ==> ∀A_2 B_2 C_2
%D
%D (( A0 A1 -> sl^ .plabel= a ∀f
%D A0 A1 -> sl_ .plabel= b ∀f'
%D A0 A2 -> sl^
%D A0 A2 -> sl_
%D A1 A2 -> .plabel= r g
%D ))
%D (( B0 B1 -> sl^ .plabel= a ∀(f_1,f_2)
%D B0 B1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D B0 B2 -> sl^
%D B0 B2 -> sl_
%D B1 B2 -> .plabel= r (g_1,g_2)
%D ))
%D (( C0 C1 -> sl^ .plabel= a ∀f_1
%D C0 C1 -> sl_ .plabel= b ∀f'_1
%D C0 C2 -> sl^
%D C0 C2 -> sl_
%D C1 C2 -> .plabel= r g_1
%D ))
%D (( D0 D1 -> sl^ .plabel= a ∀f_2
%D D0 D1 -> sl_ .plabel= b ∀f'_2
%D D0 D2 -> sl^
%D D0 D2 -> sl_
%D D1 D2 -> .plabel= r g_2
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{??}
$}
$$
\scalebox{0.58}{
\begin{tabular}{l}
%
[5pt]
%
Def: $B_1 \xton{g_1} C_1$ is a monic in $\Set$ \\
means $\und{ ∀A_1.\, ∀f_1,f'_1.\,
(\und{g_1∘f_1=g_1∘f'_1}{α_1} → \und{f_1=f'_1}{β_1})
}{\text{``$g_1$ is monic''}}
$ \\
%
[55pt]
%
Def: $B_2 \xton{g_2} C_2$ is a monic in $\Set$ \\
means $\und{ ∀A_2.\, ∀f_2,f'_2.\,
(\und{g_2∘f_2=g_2∘f'_2}{α_2} → \und{f_2=f'_2}{β_2})
}{\text{``$g_2$ is monic''}}
$ \\
%
[55pt]
%
Def: $B \xton{g} C$ is a monic in $\Set^2$, \\
i.e, $(B_1,B_2) \xton{(g_1,g_2)} (C_1,C_2)$ is a monic in $\Set^2$, \\
means $∀A.\, ∀f,f'.\, (\und{g∘f=g∘f'}{α} → \und{f=f'}{β})$, \\
i.e., $∀(A_1,A_2).\, ∀(f_1,f_2),(f'_1,f'_2).\,
(\und{(g_1,g_2)∘(f_1,f_2)=(g_1,g_2)∘(f'_1,f'_2)}{α_{12}=α}
→ \und{(f_1,f_2)=(f'_1,f'_2)}{β_{12}=β})$,
\\
[10pt]
%
i.e., $∀(A_1,A_2).\, ∀(f_1,f_2),(f'_1,f'_2).\,
(\nound{(g_1∘f_1,g_2∘f_2)=(g_1∘f'_1,g_2∘f'_2)}{α_{12}=α}
→ \nound{(f_1,f_2)=(f'_1,f'_2)}{β_{12}=β})$,
\\
[5pt]
%
i.e., $\und{ ∀A_1,A_2.\, ∀f_1,f_2, f'_1,f'_2.\,
((\und{g_1∘f_1=g_1∘f'_1}{α_1}) ∧
(\und{g_2∘f_2=g_2∘f'_2}{α_2}) →
(\und{f_1=f'_1}{β_1}) ∧
(\und{f_2=f'_2}{β_2}))
}{\text{``$(g_1,g_2)$ is monic''}}
$.
\\
[55pt]
%
We want to prove this: $(\gonetwoism) ↔ (\goneism) ∧ (\gtwoism)$
\end{tabular}
}
\newpage
Trick 1: make $f_1$ and $f'_1$ identities. We will need $A_1:=B_1$.
Trick 2: make $f_2$ and $f'_2$ identities. We will need $A_2:=B_2$.
\bsk
%D diagram tricks-1-and-2
%D 2Dx 100 +50 +70 +50
%D 2D 100 A0 = A1 B0 = B1
%D 2D \ | => \ |
%D 2D +30 A2 B2
%D 2D
%D 2D +20 C0 = C1 D0 = D1
%D 2D \ | => \ |
%D 2D +30 C2 D2
%D 2D
%D ren A0 A1 A2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren B0 B1 B2 ==> (B_1,∀A_2) (B_1,B_2) (C_1,C_2)
%D ren C0 C1 C2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren D0 D1 D2 ==> (∀A_1,B_2) (B_1,B_2) (C_1,C_2)
%D
%D (( A0 A1 -> sl^ .plabel= a ∀(f_1,f_2)
%D A0 A1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D A0 A2 -> sl^
%D A0 A2 -> sl_
%D A1 A2 -> .plabel= r (g_1,g_2)
%D ))
%D (( B0 B1 -> sl^ .plabel= a (\id,∀f_2)
%D B0 B1 -> sl_ .plabel= b (\id,∀f'_2)
%D B0 B2 -> sl^
%D B0 B2 -> sl_
%D B1 B2 -> .plabel= r (g_1,g_2)
%D ))
%D (( A0 B2 harrownodes nil 25 nil =>
%D .plabel= a \sm{A_1:=B_1\;\;\\f_1:=\id_{B_1}\\f'_1:=\id_{B_1}}
%D ))
%D (( C0 C1 -> sl^ .plabel= a ∀(f_1,f_2)
%D C0 C1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D C0 C2 -> sl^
%D C0 C2 -> sl_
%D C1 C2 -> .plabel= r (g_1,g_2)
%D ))
%D (( D0 D1 -> sl^ .plabel= a (∀f_1,\id)
%D D0 D1 -> sl_ .plabel= b (∀f'_1,\id)
%D D0 D2 -> sl^
%D D0 D2 -> sl_
%D D1 D2 -> .plabel= r (g_1,g_2)
%D ))
%D (( C0 D2 harrownodes nil 25 nil =>
%D .plabel= a \sm{A_2:=B_2\;\;\\f_2:=\id_{B_2}\\f'_2:=\id_{B_2}}
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{tricks-1-and-2}
$}
$$
\newpage
If we specialize ``$\gonetwoism$''
by doing $A_1:=B_1$, $f_1:=\id$, $f'_1:=\id$,
we get this:
%
%UB ∀A_1,A_2.\, ∀f_1,f_2, f'_1,f'_2.\, (g_1∘f_1=g_1∘f'_1)∧(g_2∘f_2=g_2∘f'_2)→(f_1=f'_1)∧(f_2=f'_2)
%UB --- --- ---- --- ---- ---------------- --- ---- --------
%UB B_1 \id \id \id \id α_2 \id \id β_2
%UB ------- -------- --------
%UB g_1 g_1 \True
%UB ---------------- --------------------
%UB \True β_2
%UB ------------------------------------
%UB α_2
%UB ----------------------------------------------------------------------------------------------
%UB ∀A_2.\, ∀f_2,f'_2.\, α_2→β_2
%UB ----------------------------------------------------------------------------------------------
%UB \gtwoism
%L
%L defub "trick 1"
%L
$$\pu
\scale{0.7}{
\ub{trick 1}
}
$$
so $(\gonetwoism) → (\gtwoism)$.
The proof of $(\gonetwoism) → (\goneism)$ is similar,
but with $A_2:=B_2$, $f_2:=\id$, $f'_2:=\id$.
So: $(\gonetwoism) → (\goneism) ∧ (\gtwoism)$.
\newpage
This is a proof of
$(\gonetwoism) ← (\goneism) ∧ (\gtwoism)$
in Natural Deduction:
%:
%: [α_1∧α_2]^1 [A_1,f_1,f'_1]^2 \goneism [α_1∧α_2]^1 [A_2,f_2,f'_2]^2 \gtwoism
%: ----------- --------------------------- ----------- --------------------------
%: α_1 α_1→β_1 α_1 α_2→β_2
%: ------------ ------------------
%: β_1 β_2
%: ---------------------------------------
%: β_1∧β_2
%: ---------------1
%: α_1∧α_2→β_1∧β_2
%: ----------------------------------------------2
%: ∀A_1,A_2,f_1,f_2,f'_1,f'_2.\,(α_1∧α_2→β_1∧β_2)
%: ----------------------------------------------
%: \gonetwoism
%:
%: ^foo
%:
\pu
$$\scale{0.9}{
\ded{foo}
}
$$
\newpage
% ____ ____ __
% | _ \ __ _ __ _ ___ |___ \ / /_
% | |_) / _` |/ _` |/ _ \ __) | '_ \
% | __/ (_| | (_| | __/ / __/| (_) |
% |_| \__,_|\__, |\___| |_____|\___/
% |___/
%
% «page-26-yoneda» (to ".page-26-yoneda")
% (sglp 6 "page-26-yoneda")
% (sgla "page-26-yoneda")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijk-links (+ 11 26) "This makes y into a functor")
% (find-fline "~/LATEX/2021sgl/" "p026-y")
%D diagram p26-b
%D 2Dx 100 +30 +35 +35 +40 +30 +15 +20
%D 2D 100 A0 - A1 C0 D0 - D1 F0 G0 - G1
%D 2D | | | | | | | /
%D 2D +20 A2 - A3 C1 D2 - D3 F1 G2
%D 2D
%D 2D +12 B0 E0
%D 2D +8 B1 - B2 E1 - E2
%D 2D
%D ren A0 A1 A2 A3 ==> D \y(C)(D) D' \y(C)(D')
%D ren B0 B1 B2 ==> \catC \phop\catC^\op \Set
%D ren C0 C1 ==> u \y(C)(α)(u)
%D
%D ren D0 D1 D2 D3 ==> D \HomC(D,C) D' \HomC(D',C)
%D ren E0 E1 E2 ==> \catC \phop\catC^\op \Set
%D ren F0 F1 ==> u u∘α
%D ren G0 G1 G2 ==> D C D'
%D
%D (( A0 A1 |->
%D A0 A2 <- .plabel= l α
%D A1 A3 -> .plabel= r \y(C)(α)
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 place
%D B1 B2 -> .plabel= a \y(C)
%D C0 C1 |->
%D ))
%D (( D0 D1 |->
%D D0 D2 <- .plabel= l α
%D D1 D3 -> .plabel= r (∘α)
%D D2 D3 |->
%D D0 D3 harrownodes nil 20 nil |->
%D E0 place
%D E1 E2 -> .plabel= a \HomC(-,C)
%D F0 F1 |->
%D G0 G1 -> .plabel= a u
%D G0 G2 <- .plabel= l α
%D G2 G1 -> .plabel= r u∘α
%D ))
%D enddiagram
%D
%D diagram p26-yoneda
%D 2Dx 100 +45 +50 +30 +30
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 - A3 E0 F0 G0
%D 2D | | | | |
%D 2D +20 A4 - A5 | | |
%D 2D | | |
%D 2D +20 B0 - B1 | | |
%D 2D | | |
%D 2D +15 C0 - C1 | | |
%D 2D \ | | | |
%D 2D +20 C2 | | |
%D 2D | | |
%D 2D +15 D0 - D1 E1 F1 G1
%D 2D \ |
%D 2D +20 D2
%D 2D
%D 2D +20
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 C PC D PD
%D ren B0 B1 ==> \phop\catC^\op \Set
%D ren C0 C1 C2 ==> \Hom_\catC(D,C) \Hom(1,PD) PD
%D ren D0 D1 D2 ==> \Hom_\catC(-,C) \Hom(1,P-) P
%D ren E0 E1 ==> PC \Hom_\hatC(\y(C),P)
%D ren F0 F1 ==> α_C(1_C) α
%D ren G0 G1 ==> e λD.λu.Pu∘\nameof{e}
%D
%D (( A1 A3 -> .plabel= r \nameof{e} # \sm{\nameof{θ(α)}=\\\nameof{α_C(1_C)}}
%D A2 A3 |->
%D A2 A4 <- .plabel= l u
%D A3 A5 -> .plabel= r Pu
%D A1 A5 -> .slide= 20pt .plabel= r \sm{Pu∘\nameof{e}=\\\nameof{(Pu)(e)}}
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D B0 relplace 0 -8 \catC
%D B0 B1 -> .plabel= a P
%D C0 C1 ->
%D C1 C2 <->
%D C0 C2 -> .plabel= b λu.(Pu)(e)\;\;
%D C0 relplace -38 0 \y(C)(D)=
%D D0 D1 ->
%D D1 D2 <->
%D D0 D2 -> .plabel= b α
%D D0 relplace -35 0 \y(C)=
%D E0 E1 <-| sl_ .plabel= l θ
%D E0 E1 |-> sl^ .plabel= r θ^{-1}
%D F0 F1 <-|
%D G0 G1 |->
%D ))
%D enddiagram
%D
\pu
% (favp 35 "yoneda-lemma")
% (fava "yoneda-lemma")
\ColorBrown{\tiny Page 26:}
\msk
$
% (find-maclanemoerdijk-links (+ 11 26) "This makes y into a functor")
% (find-pdf-page "~/LATEX/2021sgl/p026-y.pdf")
\incgr {height=5.5cm} {2021sgl/p026-y.pdf}
\quad
\scalebox{0.45}{$
\begin{array}{l}
\diag{p26-b} \\[50pt]
\diag{p26-yoneda} \\
\end{array}
$}
$
\newpage
% ____ _________
% | _ \ __ _ __ _ ___ |___ /___ \
% | |_) / _` |/ _` |/ _ \ |_ \ __) |
% | __/ (_| | (_| | __/ ___) / __/
% |_| \__,_|\__, |\___| |____/_____|
% |___/
%
% «page-32-true-terminal» (to ".page-32-true-terminal")
% (sglp 7 "page-32-true-terminal")
% (sgla "page-32-true-terminal")
\ColorBrown{\tiny Page 32:}
%
\def\rito{\rotatebox[origin=c]{270}{$\ito$}} % \ito rotated right
\def\rmon{\rotatebox[origin=c]{270}{$\monicto$}} % \monic rotated right
\def\aninc#1#2#3#4{\pmat{#1 \\ #2 \rito #3 \\ #4}} % an inclusion
\def\amon #1#2#3#4{\pmat{#1 \\ #2 \rmon #3 \\ #4}} % a monic
\def\inctrue{{\aninc {1\ph{mm}} {}{\,\text{true}} {Ω\ph{mm} }}} % true: 1 \ito Ω
\def\montrue{{\amon {1\ph{mm,}} {}{\,\text{true}} {Ω\ph{mm,}}}} % true: 1 \ito Ω
\def\incSX {{\aninc {S} {}{} {X}}} % S \ito X
\def\monSX {{\amon {S} {}{} {X}}} % S \monicto X
\def\incSY {{\aninc {S'} {}{} {Y}}} % S' \ito Y
\def\monSY {{\amon {S'} {}{} {Y}}} % S' \monicto Y
%
%$\inctrue
% \montrue
% \incSX
% \monSX
% \incSY
% \monSY
%$
%
%D diagram p32-1-monics
%D 2Dx 100 +45
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +25 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> ∀S 1 ∀X Ω
%D ren B0 B1 ==> ∀\monSX \montrue
%D
%D (( A0 A1 -> .plabel= a ϕ'=!
%D A0 A2 >-> .plabel= l ∀
%D A1 A3 >-> .plabel= r \text{true}
%D A2 A3 -> .plabel= a ϕ
%D A0 relplace 7 7 \pbsymbol{7}
%D B0 B1 -> .plabel= a ∃!\psm{ϕ'\\ϕ}
%D ))
%D enddiagram
%D
%D diagram p32-1-inclusions
%D 2Dx 100 +45
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +25 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> ∀S 1 ∀X Ω
%D ren B0 B1 ==> ∀\incSX \inctrue
%D
%D (( A0 A1 -> .plabel= a ϕ'=!
%D A0 A2 `-> .plabel= l ∀
%D A1 A3 `-> .plabel= r \text{true}
%D A2 A3 -> .plabel= a ϕ
%D A0 relplace 7 7 \pbsymbol{7}
%D B0 B1 -> .plabel= a ∃!\psm{ϕ'\\ϕ}
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-1-monics}
% \quad
% \diag{p32-1-inclusions}
%$$
%
%D diagram p32-2-monics
%D 2Dx 100 +50 +25
%D 2D 100 A0 - A1 - A2
%D 2D | | |
%D 2D +20 A3 - A4 - A5
%D 2D
%D 2D +20 B0 - B1
%D 2D
%D 2D +20 C0 - C1
%D 2D | |
%D 2D +20 C2 - C3
%D 2D
%D ren A0 A1 A2 ==> S' S 1
%D ren A3 A4 A5 ==> Y X Ω
%D ren B0 B1 ==> \monSY \monSX
%D ren C0 C1 C2 C3 ==> \Sub_\catC(Y) \Sub_\catC(X) Y X
%D
%D (( A0 A1 -> A1 A2 ->
%D A0 A3 -> .plabel= l m'
%D A1 A4 -> .plabel= l m
%D A2 A5 -> .plabel= r \text{true}
%D A3 A4 -> .plabel= a f
%D A4 A5 ->
%D A0 relplace 7 7 \pbsymbol{7}
%D A1 relplace 7 7 \pbsymbol{7}
%D B0 B1 <-|
%D C0 C1 <- .plabel= a \Sub_\catC(f)
%D C0 C2 <-|
%D C1 C3 <-|
%D C2 C3 -> .plabel= b f
%D C0 C3 varrownodes nil 15 nil <-|
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-2-monics}
%$$
%
%D diagram p32-3-monics
%D 2Dx 100 +30 +30
%D 2D 100 A0 - A1 C0
%D 2D | | |
%D 2D +30 A2 - A3 C1
%D 2D
%D 2D +20 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> X \Sub_\catC(X) Y \Sub_\catC(Y)
%D ren B0 B1 ==> \catC^\op \Set
%D ren C0 C1 ==> \scale{0.7}{\monSX} \scale{0.7}{\monSY}
%D
%D (( A0 A1 |->
%D A0 A2 <- .plabel= l f
%D A1 A3 -> .plabel= r \Sub_\catC(f)
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a \Sub_\catC
%D newnode: B0' at: @B0+v(-2.5,-7) .TeX= \catC place
%D C0 C1 |->
%D
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-3-monics}
%$$
% (find-maclanemoerdijk-links (+ 11 32) "Definition... subobject classifier" "-sc")
$% (find-pdf-page "~/LATEX/2021sgl/p032-sc.pdf")
\incgr{height=6cm}{2021sgl/p032-sc.pdf}
\quad
\scale{0.45}{
\begin{array}{l}
\begin{tabular}{l}
In the category of \\
monic and pullbacks, \\
\end{tabular}
\\
\diag{p32-1-monics} \\
\\
\begin{tabular}{l}
and $ϕ'=!$, so $∃!ϕ$. \\
$\scale{0.5}{\monSX}$ is an element of $\Sub_\catC(X)$. \\
$\scale{0.5}{\monSX}$ is an equivalence class, \\
and may not be a set. \\
\end{tabular}
\\
\\
\diag{p32-2-monics} \quad
\diag{p32-3-monics} \\
\end{array}
}
$
\newpage
% ____ _________ _______ __
% | _ \ __ _ __ _ ___ ___ |___ / ___| / /___ / / /_
% | |_) / _` |/ _` |/ _ \/ __| |_ \___ \ / / |_ \| '_ \
% | __/ (_| | (_| | __/\__ \ ___) |__) / / ___) | (_) |
% |_| \__,_|\__, |\___||___/ |____/____/_/ |____/ \___/
% |___/
%
% «pages-35-36-Set^2» (to ".pages-35-36-Set^2")
% (sglp 8 "pages-35-36-Set^2")
% (sgla "pages-35-36-Set^2")
\ColorBrown{\tiny Pages 35 and 36:}
\msk
\def\monSSXX{{\amon {\ph{mi}(S,S')}
{(⊂,⊂)}{\ph{mi}}
{\ph{mi}(X,X')}}}
\def\montt {{\amon {(1,1)\ph{m}}
{\ph{m}}{\,\text{true}}
{(1,2)\ph{m}}}}
% $\monSSXX \montt$
%D diagram p35-SxS
%D 2Dx 100 +10 +30 +35 +40 +40 +55
%D 2D 100 A0 A1 B0 C0 - C1
%D 2D +10 | | | | | D0 - D1
%D 2D +10 A2 A3 B1 C2 - C3
%D 2D
%D 2D +20 A4 A5 B2
%D 2D
%D ren A0 A1 A2 A3 ==> Y Y' X X'
%D ren B0 B1 B2 ==> (Y,Y') (X,Y') \Sets×\Sets
%D ren C0 C1 C2 C3 ==> ∀(S,S') (1,1) ∀(X,X') (2,2)
%D ren D0 D1 ==> ∀\monSSXX \montt
%D
%D (( A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r f'
%D A4 A5 midpoint .TeX= \Sets place
%D B0 B1 -> .plabel= r (f,f')
%D B2 place
%D C0 C1 -> .plabel= a !
%D C0 C2 >-> .plabel= l ∀(⊂,⊂)
%D C1 C3 >-> .plabel= r \text{true}
%D C2 C3 -> .plabel= b (ϕ_S,ϕ_{S'})
%D C0 relplace 12 7 \pbsymbol{7}
%D D0 D1 -> .plabel= a ∃!
%D ))
%D enddiagram
%D
\pu
%
\def\rS {(S_0 \ton{σ} S_1)}
\def\rX {(X_0 \ton{σ} X_1)}
\def\rone{(\{0\} \ton{σ} \{0\})}
\def\rOm {(\{0,1,2\} \xton{σ = \csm{0↦0 \\ 1↦0 \\ 2↦1}} \{0,1\})}
\def\rmyone{(\{11\} \ton{σ} \{·1\})}
\def\rmyOm {(\{11,01,00\} \xton{σ = \csm{11↦·1 \\ 01↦·1 \\ 00↦·0}} \{·1,·0\})}
%
%D diagram p35-2
%D 2Dx 100 +80
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +40 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> \rS \rone \rX \rOm
%D
%D (( A0 A1 -> .plabel= a !
%D A0 A2 >-> .plabel= l (⊂,⊂)
%D A1 A3 >-> .plabel= r (⊂,⊂)
%D A2 A3 -> .plabel= b (ϕ_0,ϕ_1)
%D A0 relplace 15 8 \pbsymbol{7}
%D newnode: A0' at: @A0+v(-25,0) .TeX= S= place
%D ))
%D enddiagram
%D
%D diagram p35-2-my
%D 2Dx 100 +80
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +40 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> \rS \rmyone \rX \rmyOm
%D
%D (( A0 A1 -> .plabel= a !
%D A0 A2 >-> .plabel= l (⊂,⊂)
%D A1 A3 >-> .plabel= r (⊂,⊂)
%D A2 A3 -> .plabel= b (ψ_0,ψ_1)
%D A0 relplace 15 8 \pbsymbol{7}
%D newnode: A0' at: @A0+v(-25,0) .TeX= S= place
%D ))
%D enddiagram
%D
\pu
$ % (find-maclanemoerdijk-links (+ 11 35) "For the arrow category 2 and Sets^2" "-SxS")
% (find-maclanemoerdijk-links (+ 11 35) "For the arrow category 2 and Sets^2" "-S2")
% (find-maclanemoerdijk-links (+ 11 36) "For the arrow category 2 and Sets^2" "-S2")
% (find-pdf-page "~/LATEX/2021sgl/p035-SxS.pdf")
% (find-pdf-page "~/LATEX/2021sgl/p035-S2.pdf")
% (find-pdf-page "~/LATEX/2021sgl/p036-S2.pdf")
\begin{array}{c}
\incgr{width=6cm}{2021sgl/p035-SxS.pdf} \\
\incgr{width=6cm}{2021sgl/p035-S2.pdf} \\
\incgr{width=6cm}{2021sgl/p036-S2.pdf} \\
\end{array}
\quad
\begin{array}{l}
\scale{0.4}{\diag{p35-SxS}} \\ \\
\scale{0.4}{\diag{p35-2}} \\[20pt]
\scale{0.4}{\diag{p35-2-my}} \\[20pt]
\scale{0.4}{
\begin{array}{cccccc}
x∈S_0 & σx∈S_1 & ϕ_0x & ϕ_1(σx) & ψ_0x & ψ_1(σx) \\ \hline
\True & \True & 0 & 0 & 11 & ·1 \\
\False & \True & 1 & 0 & 01 & ·1 \\
\False & \False & 2 & 1 & 00 & ·0 \\
\end{array}
}
\end{array}
$
\msk
{\tiny
\ColorBrown{See:}
%
% (cltp 29 "SetD-chi")
% (clta "SetD-chi")
% http://angg.twu.net/LATEX/2020clops-and-tops.pdf#page=29
\url{http://angg.twu.net/LATEX/2020clops-and-tops.pdf#page=29}
}
\newpage
% ____ ____ _____ _ _ _
% | _ \ __ _ __ _ ___ | ___|___ | | |_| |__ _ __ ___ / |
% | |_) / _` |/ _` |/ _ \ |___ \ / / | __| '_ \| '_ ` _ \ | |
% | __/ (_| | (_| | __/ ___) |/ / | |_| | | | | | | | | | |
% |_| \__,_|\__, |\___| |____//_/ \__|_| |_|_| |_| |_| |_|
% |___/
%
% «page-57-theorem-1» (to ".page-57-theorem-1")
% (find-maclanemoerdijkpage (+ 11 57) "9. Quantifiers as Adjoints")
% (find-maclanemoerdijk-links (+ 11 57) "9. Quantifiers as Adjoints" "-thm-1")
% (hypp 18 "quants-for-children")
% (hyp "quants-for-children")
\ColorBrown{\tiny Page 57, theorem 1:}
$% (find-pdf-page "~/LATEX/2021sgl/p057-thm-1.pdf")
\incgr{width=5cm}{2021sgl/p057-thm-1.pdf}
$
% ____ ____ ___ _ _ ____
% | _ \ __ _ __ _ ___ | ___| ( _ ) | |_| |__ _ __ ___ |___ \
% | |_) / _` |/ _` |/ _ \ |___ \ / _ \ | __| '_ \| '_ ` _ \ __) |
% | __/ (_| | (_| | __/ ___) | (_) | | |_| | | | | | | | | / __/
% |_| \__,_|\__, |\___| |____/ \___/ \__|_| |_|_| |_| |_| |_____|
% |___/
%
% «page-58-theorem-2» (to ".page-58-theorem-2")
% (find-maclanemoerdijkpage (+ 11 58) "9. Quantifiers as Adjoints" "-thm-2")
% «pages-58-59-theorem-2» (to ".pages-58-59-theorem-2")
% (find-maclanemoerdijkpage (+ 11 58) "9. Quantifiers as Adjoints" "-thm-3")
\newpage
% ____ __ ___ ___
% | _ \ __ _ __ _ ___ / /_ ( _ ) _____ __ ( _ )
% | |_) / _` |/ _` |/ _ \ | '_ \ / _ \ / _ \ \/ / / _ \
% | __/ (_| | (_| | __/ | (_) | (_) | | __/> < | (_) |
% |_| \__,_|\__, |\___| \___/ \___/ \___/_/\_\ \___/
% |___/
% «page-63-exercise-8» (to ".page-63-exercise-8")
% (sglp 9 "page-63-exercise-8")
% (sgla "page-63-exercise-8")
% (find-maclanemoerdijk-links (+ 11 63) "Exercise 8" "-exercise-8")
% https://categorytheory.zulipchat.com/#narrow/stream/300905-SGL-Reading.20Group/topic/stream.20events/near/257669027
% https://ncatlab.org/nlab/show/category+of+presheaves
% (code-pdf-page "swarajch1ex8" "~/SGL/sgl-swaraj-ch1ex8.pdf")
% (find-swarajch1ex8page)
\ColorBrown{\tiny Page 63, exercise 8:}
\msk
$% (find-pdf-page "~/LATEX/2021sgl/p063-exercise-8.pdf")
\incgr{width=5.5cm}{2021sgl/p063-exercise-8.pdf}
$
\msk
% ____ __ _____ _ ___
% | _ \ __ _ __ _ ___ / /_|___ / _____ __ / |/ _ \
% | |_) / _` |/ _` |/ _ \ | '_ \ |_ \ / _ \ \/ / | | | | |
% | __/ (_| | (_| | __/ | (_) |__) | | __/> < | | |_| |
% |_| \__,_|\__, |\___| \___/____/ \___/_/\_\ |_|\___/
% |___/
%
% «page-63-exercise-10» (to ".page-63-exercise-10")
% (sglp 9 "page-63-exercise-10")
% (sgla "page-63-exercise-10")
% (find-maclanemoerdijk-links (+ 11 63) "Exercise 10" "-exercise-10")
\ColorBrown{\tiny Page 63, exercise 10:}
\msk
$% (find-pdf-page "~/LATEX/2021sgl/p063-exercise-10.pdf")
\incgr{width=6cm}{2021sgl/p063-exercise-10.pdf}
$
%\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021sgl veryclean
make -f 2019.mk STEM=2021sgl pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "sgl"
% End: