|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2019classifier.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019classifier.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019classifier.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019classifier.pdf"))
% (defun e () (interactive) (find-LATEX "2019classifier.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019classifier"))
% (find-pdf-page "~/LATEX/2019classifier.pdf")
% (find-sh0 "cp -v ~/LATEX/2019classifier.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019classifier.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019classifier.pdf
% file:///tmp/2019classifier.pdf
% file:///tmp/pen/2019classifier.pdf
% http://angg.twu.net/LATEX/2019classifier.pdf
% (find-LATEX "2019.mk")
%
% (find-TH "math-b" "2020-classifier")
% «.title» (to "title")
% «.introduction» (to "introduction")
% «.make» (to "make")
\documentclass[oneside]{article}
\usepackage[colorlinks,urlcolor=DarkRed,citecolor=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")
\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib} % (find-LATEX "catsem-u.bib")
%
% (find-es "tex" "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
\def\dnto{{\downarrow}}
\def\ovl{\overline}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
\title{Notes about classifiers and local operators in a
$\Set^{(P,A)}$}
\author{Eduardo Ochs}
\maketitle
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% (cl9p 1 "abstract")
% (cl9 "abstract")
\begin{abstract}
The last section of the paper \cite{OchsPH2} shows, quite briefly, how
to translate slashings on Planar Heyting Algebras to local operators
on toposes, but it omits some details and calculations and says that
they are ``routine''. These notes are an attempt to fill those gaps.
\end{abstract}
% ___ _ _ _ _
% |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
% (cl9p 1 "introduction")
% (cl9 "introduction")
% (jopp 25 "the-right-classifier")
% (joe "the-right-classifier")
\bsk
\bsk
{\bf Warning:} this is currently 1) a mess 2) a work in progress!
\bsk
If $F$ and $G$ are functors from $\catA$ to $\Set$ and $T:F→G$ then we
can draw the two internal views of the square condition of $T$ as:
%
%D diagram sqcond-1
%D 2Dx 100 +30 +30 +30 +45
%D 2D 100 B FB -> GB x |--> rx
%D 2D | | | - -
%D 2D | | | | v
%D 2D +22 v v v v drx
%D 2D +8 C FC -> GC dx |-> rdx
%D 2D
%D 2D +20 F --> G
%D 2D
%D ren rx drx ==> (TB)(x) (Gv∘TB)(x)
%D ren dx rdx ==> (Fv)(x) (TC∘Fv)(x)
%D
%D (( B C -> .plabel= l v
%D F G -> .plabel= a T
%D
%D FB GB -> .plabel= a TB
%D FB FC -> .plabel= l Fv
%D GB GC -> .plabel= r Gv
%D FC GC -> .plabel= a TC
%D
%D x rx |-> rx drx |->
%D x dx |-> dx rdx |->
%D ))
%D enddiagram
%D
$$\pu
\diag{sqcond-1}
$$
Formally, this is: $∀(v:B→C). \, ∀x∈FB. \, (Gv∘TB)(x) = (TC∘Fv)(x)$.
\bsk
In Section 7 of \cite{OchsPH2} I used these two diagrams to discuss
$Ω$ and $j$,
%
%D diagram Omega-and-j
%D 2Dx 100 +30 +30
%D 2D 100 B --> 1
%D 2D | |
%D 2D v v
%D 2D +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1 -> .plabel= a !
%D B C >-> .plabel= l i
%D 1 Om1 >-> .plabel= r ⊤
%D C Om1 -> .plabel= a χ_B
%D Om1 Om2 -> .plabel= a j
%D B relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
%D diagram Omega-and-j-2
%D 2Dx 100 +30 +30
%D 2D 100 B ----------> 1
%D 2D | |
%D 2D v v
%D 2D +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 B ==> Ω Ω \ovl{B}
%D
%D (( B 1 -> .plabel= a !
%D B C >-> .plabel= l i
%D 1 Om2 >-> .plabel= r ⊤
%D C Om1 -> .plabel= a χ_B
%D Om1 Om2 -> .plabel= a j
%D B relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
\pu
$$\diag{Omega-and-j}
\qquad
\diag{Omega-and-j-2}
$$
%
and I defined the objects $1$ and $Ω$ by:
%
$$\begin{array}{rcl}
1(p) &=& \{*\} \\
1(p\ton!q) &=& λ*.* \\
Ω(p) &=& \Sub(↓p) \\
Ω(p\ton!q) &=& λR{:}\Sub(↓p).R∧↓q \\
\end{array}
$$
%
Let's suppose that $B \monicto C$ is a canonical subobject, i.e., we
have $∀p∈P.B(p)⊆C(p)$ and every map $B(p\ton!q)$ is a restriction of
the corresponding map $C(p\ton!q)$. This means that:
%
%D diagram B->C-inj
%D 2Dx 100 +30 +40 +35 +55
%D 2D 100 p Bp ---> Cp b |---> cb
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v rcb
%D 2D +8 q Bq ---> Cq rb |--> crb
%D 2D
%D 2D +20 B ----> C
%D 2D
%D ren Bp Bq Cp Cq ==> B(p) B(q) C(p) C(q)
%D ren b cb rcb rb crb ==> b b C(p\ton!q)(b) B(p\ton!q)(b) B(p\ton!q)(b)
%D
%D (( p q -> .plabel= l !
%D Bp Cp `-> .plabel= a ip
%D Bp Bq -> .plabel= l B(p\ton!q)
%D Cp Cq -> .plabel= r C(p\ton!q)
%D Bq Cq `-> .plabel= a iq
%D B C `-> .plabel= a i
%D
%D b cb |-> cb rcb |->
%D b rb |-> rb crb |->
%D ))
%D enddiagram
%
$$\pu
\diag{B->C-inj}
$$
$$\begin{array}{rcl}
\end{array}
$$
% (jopp 25 "the-right-classifier")
% (joe "the-right-classifier")
\newpage
% (nyop 12 "first-yoneda-bijection-4")
% (nyo "first-yoneda-bijection-4")
% (nyo "yoneda-bij")
%D diagram B->1
%D 2Dx 100 +30 +40 +35 +45
%D 2D 100 p Bp ---> 1p b |---> *p1
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v *p2
%D 2D +8 q Bq --> 1q rb |--> *p3
%D 2D
%D 2D +20 B ----> 1
%D 2D
%D ren Bp Bq 1p 1q ==> B_0(p) B_0(q) \{*\} \{*\}
%D ren b rb *p1 *p2 *p3 ==> b B_1(p\ton!q)(b) * * *
%D
%D (( p q -> .plabel= l !
%D Bp 1p -> .plabel= a !
%D Bp Bq -> .plabel= l B_1(p\ton!q)
%D 1p 1q -> .plabel= r !
%D Bq 1q -> .plabel= a !
%D B 1 ->
%D
%D b *p1 |-> *p1 *p2 |->
%D b rb |-> rb *p3 |->
%D ))
%D enddiagram
$\pu
\diag{B->1}
$
\bsk
\bsk
%D diagram B->C
%D 2Dx 100 +30 +40 +35 +55
%D 2D 100 p Bp ---> Cp b |---> cb
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v rcb
%D 2D +8 q Bq ---> Cq rb |--> crb
%D 2D
%D 2D +20 B ----> C
%D 2D
%D ren Bp Bq Cp Cq ==> B_0(p) B_0(q) C_0(p) C_0(q)
%D ren b cb rcb rb crb ==> b b C_1(p\ton!q)(b) B_1(p\ton!q)(b) B_1(p\ton!q)(b)
%D
%D (( p q -> .plabel= l !
%D Bp Cp `-> .plabel= a ip
%D Bp Bq -> .plabel= l B_1(p\ton!q)
%D Cp Cq -> .plabel= r C_1(p\ton!q)
%D Bq Cq `-> .plabel= a iq
%D B C `-> .plabel= a i
%D
%D b cb |-> cb rcb |->
%D b rb |-> rb crb |->
%D ))
%D enddiagram
$\pu
\diag{B->C}
$
\bsk
\bsk
%D diagram 1->Om
%D 2Dx 100 +30 +40 +35 +45
%D 2D 100 p 1p ---> Omp * |---> t*
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v rt*
%D 2D +8 q 1q --> Omq r* |--> tr*
%D 2D
%D 2D +20 1 ----> Om
%D 2D
%D ren 1p 1q Omp Omq ==> \{*\} \{*\} \Sub(↓p) \Sub(↓q)
%D ren * t* rt* r* tr* ==> * ↓p ↓p∧↓q * ↓q
%D ren Om ==> Ω
%D
%D (( p q -> .plabel= l !
%D 1p Omp -> .plabel= a ⊤p
%D 1p 1q -> .plabel= l !
%D Omp Omq -> .plabel= r !
%D 1q Omq -> .plabel= a ⊤q
%D 1 Om -> .plabel= a ⊤
%D
%D * t* |-> t* rt* |->
%D * r* |-> r* tr* |->
%D ))
%D enddiagram
$\pu
\diag{1->Om}
$
\bsk
\bsk
%D diagram C->Om
%D 2Dx 100 +30 +40 +45 +95
%D 2D 100 p Cp ---> Omp c |---> chic
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v rchic
%D 2D +8 q Cq ---> Omq rc |--> chirc
%D 2D
%D 2D +20 C ----> Om
%D 2D
%D ren Cp Omp ==> C(p) \Sub(↓p)
%D ren Cq Omq ==> C(q) \Sub(↓q)
%D ren C Om ==> C Ω
%D
%D ren c chic ==> c \setofst{r∈↓p}{C(p\ton!r)(c)∈B(r)}
%D ren rchic ==> \setofst{r∈↓p}{C(p\ton!r)(c)∈B(r)}∧↓q
%D ren rc chirc ==> C(p\ton!q)(c) \setofst{s∈↓q}{C(q\ton!s)(C(p\ton!q)(c))∈B(s)}
%D
%D (( p q -> .plabel= l !
%D Cp Omp -> .plabel= a χ_B(p)
%D Cp Cq -> .plabel= l C(p\ton!q)
%D Omp Omq -> .plabel= r Ω(p\ton!q)
%D Cq Omq -> .plabel= a χ_B(q)
%D C Om -> .plabel= a χ_B
%D
%D c chic |-> chic rchic |->
%D c rc |-> rc chirc |->
%D ))
%D enddiagram
$\pu
\diag{C->Om}
$
\bsk
\bsk
%D diagram classifier-j
%D 2Dx 100 +30 +40 +35 +45
%D 2D 100 p Sp1 --> Sp2 R |---> jR
%D 2D | | | - -
%D 2D | | | | |
%D 2D | | | | v
%D 2D +25 v v v v rjR
%D 2D +8 q Sq1 --> Sq2 rR |--> jrR
%D 2D
%D 2D +20 Om1 --> Om2
%D 2D
%D ren Sp1 Sp2 ==> \Sub(↓p) \Sub(↓p)
%D ren Sq1 Sq2 ==> \Sub(↓q) \Sub(↓q)
%D ren Om1 Om2 ==> Ω Ω
%D ren R jR rjR ==> R R^*∧↓p (R^*∧↓p)∧↓q
%D ren rR jrR ==> R∧↓q (R∧↓q)^*∧↓q
%D
%D (( p q -> .plabel= l !
%D Sp1 Sp2 -> .plabel= a j(p)
%D Sp1 Sq1 -> .plabel= l Ω(p\ton!q)
%D Sp2 Sq2 -> .plabel= r Ω(p\ton!q)
%D Sq1 Sq2 -> .plabel= a j(q)
%D Om1 Om2 -> .plabel= a j
%D
%D R jR |-> jR rjR |->
%D R rR |-> rR jrR |->
%D ))
%D enddiagram
$\pu
\diag{classifier-j}
$
\newpage
\section{Garbage?}
$Ω(p) = \Sub(↓p)$
$Ω(p\ton!q) = λR{:}\Sub(↓p).(R∧↓q)$
\bsk
We need to understand these five morphisms in $\Set^{(P,A)}$.
Each one of them is a natural transformation.
The object $1∈\Set^{(P,A)}$ is $1_0(p) = \{*\}$, $1_1(p\ton!q) = λ{*}.{*}$.
The object $Ω∈\Set^{(P,A)}$ is $Ω_0(p) = ↓p$, $Ω_1(p\ton!q) = λr{:}↓p.r∧↓q$.
\msk
$B\ton!1$ is trivial: $(B\ton!1)(p) = λb{:}B_0(p).*$.
\msk
$B \diagxyto/^{ (}->/^{i} C$ is an inclusion:
for every $p∈P$ we have $B_0(p)⊆C_0(p)$, and
for every $p\ton!q$ the map $(B \diagxyto/^{ (}->/^{i} C)(p\ton!q)$ is
a restriction of $C_1(p\ton!q)$.
\msk
$1 \diagxyto/{ >}->/^{⊤} Ω$ is $λp{:}P.λ{*}{:}1(p).↓p$.
\msk
$C \diagxyto/->/^{χ_B} Ω$ is $λp{:}P.λc{:}C(p).???$.
% (find-sh "locate calvin")
%D diagram Q
%D 2Dx 100 +30 +30
%D 2D 100 B --> 1
%D 2D | |
%D 2D v v
%D 2D +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1 -> .plabel= a !
%D B C `-> .plabel= l i
%D 1 Om1 >-> .plabel= r ⊤
%D C Om1 -> .plabel= a χ_B
%D Om1 Om2 -> .plabel= a j
%D ))
%D enddiagram
%D
$$\pu
\diag{Q}
$$
\printbibliography
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2017planar-has-1.mk")
make -f 2017planar-has-1.mk STEM=2019classifier veryclean
make -f 2017planar-has-1.mk STEM=2019classifier pdf
# (cl9p)
# (jopp 25)
% Local Variables:
% coding: utf-8-unix
% ee-tla: "cla"
% End: