|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020clops-and-tops-garbage.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020clops-and-tops-garbage.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2020clops-and-tops-garbage.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2020clops-and-tops-garbage.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020clops-and-tops-garbage.pdf"))
% (defun e () (interactive) (find-LATEX "2020clops-and-tops-garbage.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020clops-and-tops-garbage"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2020clops-and-tops-garbage.pdf"))
% (code-eec-LATEX "2020clops-and-tops-garbage")
% (find-pdf-page "~/LATEX/2020clops-and-tops-garbage.pdf")
% (find-sh0 "cp -v ~/LATEX/2020clops-and-tops-garbage.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020clops-and-tops-garbage.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020clops-and-tops-garbage.pdf
% file:///tmp/2020clops-and-tops-garbage.pdf
% file:///tmp/pen/2020clops-and-tops-garbage.pdf
% http://angg.twu.net/LATEX/2020clops-and-tops-garbage.pdf
% (find-LATEX "2019.mk")
% «.defs» (to "defs")
%
% «.SetCs-and-SetDs» (to "SetCs-and-SetDs")
% «.SetD-yoneda» (to "SetD-yoneda")
%
% «.J-ops» (to "J-ops")
% «.clop-to-Jop» (to "clop-to-Jop")
% «.Jop-to-top» (to "Jop-to-top")
% «.Jop-to-top-defs» (to "Jop-to-top-defs")
% «.def-j» (to "def-j")
% «.def-j-NT» (to "def-j-NT")
% «.def-j-obeys-J1-J2-J3» (to "def-j-obeys-J1-J2-J3")
%% «.def-j-example» (to "def-j-example")
%% «.clop-Jop-bij» (to "clop-Jop-bij")
% «.SetD-dense-closed» (to "SetD-dense-closed")
% «.SetD-sheaves» (to "SetD-sheaves")
% «.SetD-closure» (to "SetD-closure")
% «.topological-lemmas» (to "topological-lemmas")
\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")
\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")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% %L -- (find-dn6 "output.lua" "Deletecomments-class")
% %L deletecomments = function (bigstr) return DeleteComments.from(bigstr) end
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
%L forths["<-'"] = function () pusharrow("<-^{) }") end
%L kite = ".1.|2.3|.4.|.5."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="6pt"}, z):zfunction(kite):output()
%L -- mp = MixedPicture.new({def="dagKite", meta="s", scale="10pt"}, z):zfunction(kite):output()
%L -- mp = MixedPicture.new({def="dagKote", meta="s", scale="10pt"}, z):zfunction(kite):output()
\pu
% «defs» (to ".defs")
\def\Incs {\mathsf{Incs}}
\def\inc {\mathsf{inc}}
\def\CanSub {\mathsf{CanSub}}
\def\SubPoints{\mathsf{SubPoints}}
\def\Subsets {\mathsf{Subsets}}
\def\Can {\mathsf{Can}}
\def\can {\mathsf{can}}
\def\Eq {\mathsf{Eq}}
\def\eq {\mathsf{eq}}
\def\Futs {\mathsf{Futures}}
\def\Innerpts {\mathsf{Innerpoints}}
\def\Logic {\mathsf{Logic}}
\def\Po {\mathsf{Po}}
\def\Ob {\mathsf{Ob}}
\def\catH {\mathbf{H}}
\def\catK {\mathbf{K}}
\def\catT {\mathbf{T}}
\def\catW {\mathbf{W}}
\def\Clo {\textsc{Cl}}
\def\univ {\text{univ}}
\def\pcdot {(·)}
\def\opcdot {\ovl{(·)}}
\def\clop {\ovl{(·)}}
\def\SetC {\Set^\catC}
\def\SetD {\Set^\catD}
\def\SetH {\Set^\catH}
\def\SetK {\Set^\catK}
\def\SetT {\Set^\catT}
\def\calW {\mathcal{W}}
\def\chizi {χ_{01}}
\def\chizim {χ_{01m}}
\def\toM {\ton{\text{M}}}
\def\ph {\phantom}
\def\Jcan {{J_\mathrm{can}}}
\def\hasmax{\mathsf{hasmax}}
\def\trans {\mathsf{trans}}
\def\stab {\mathsf{stab}}
\def\Above {\mathop{\textsf{above}}}
\def\Covers {\mathop{\textsf{covers}}}
\def\JCovers {\mathop{\textsf{$J$-covers}}}
\def\RCovers {\mathop{\textsf{r-covers}}}
\def\RJCovers{\mathop{\textsf{r-$J$-covers}}}
\def\Downs {\mathsf{D}}
\def\Cst {\mathsf{CST}}
\def\sa#1#2{\expandafter\def\csname myarg#1\endcsname{#2}}
\def\ga#1{\csname myarg#1\endcsname}
\def\rotl#1{\rotatebox{90}{$#1$}}
\def\eqP{\sim_P}
\def\eqJ{\sim_J}
\def\eqL{\sim_L}
\def\eqR{\sim_R}
\def\eqS{\sim_S}
\def\TODO{(TODO)}
% «theorem» (to ".theorem")
% (find-es "tex" "newtheorem")
% (find-es "tex" "newcounter")
%
\newtheorem{thmsection} {My Theorem}[section]
\newtheorem{thmsubsection} {My Theorem}[subsection]
\newtheorem{thmsubsubsection}{My Theorem}[subsubsection]
\def\stepThm#1{\refstepcounter{#1}\csname the#1\endcsname}
\def\Theoremsection {{\bf Theorem \stepThm{thmsection}. }}
\def\Theoremsubsection {{\bf Theorem \stepThm{thmsubsection}. }}
\def\Theoremsubsubsection {{\bf Theorem \stepThm{thmsubsubsection}. }}
\def\Lemmasection {{\bf Lemma \stepThm{thmsection}. }}
\def\Lemmasubsection {{\bf Lemma \stepThm{thmsubsection}. }}
\def\Lemmasubsubsection {{\bf Lemma \stepThm{thmsubsubsection}. }}
\def\Conjecturesection {{\bf Conjecture \stepThm{thmsection}. }}
\def\Conjecturesubsection {{\bf Conjecture \stepThm{thmsubsection}. }}
\def\Conjecturesubsubsection{{\bf Conjecture \stepThm{thmsubsubsection}. }}
\def\Examplesection {{\bf Example \stepThm{thmsection}. }}
\def\Examplesubsection {{\bf Example \stepThm{thmsubsection}. }}
\def\Examplesubsubsection {{\bf Example \stepThm{thmsubsubsection}. }}
% \newcounter{Counts}[section]
% \newcounter{Countss}[subsection]
% \newcounter{Countsss}[subsubsection]
% \def\stepCount#1{\refstepcounter{#1}\csname the#1\endcsname}
% \def\Theoremsection {{\bf Theorem \stepThm{Counts}.}}
% \def\Theoremsubsection {{\bf Theorem \stepThm{Countss}.}}
% \def\Theoremsubsubsection{{\bf Theorem \stepThm{Countsss}.}}
\newpage
% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
% ____ _
% / ___| __ _ _ __| |__ __ _ __ _ ___ _
% | | _ / _` | '__| '_ \ / _` |/ _` |/ _ (_)
% | |_| | (_| | | | |_) | (_| | (_| | __/_
% \____|\__,_|_| |_.__/ \__,_|\__, |\___(_)
% |___/
% ____ _ ____ _ ____ _ ____
% / ___| ___| |_ / ___|___ __ _ _ __ __| | / ___| ___| |_| _ \ ___
% \___ \ / _ \ __| | / __| / _` | '_ \ / _` | \___ \ / _ \ __| | | / __|
% ___) | __/ |_| |___\__ \ | (_| | | | | (_| | ___) | __/ |_| |_| \__ \
% |____/ \___|\__|\____|___/ \__,_|_| |_|\__,_| |____/ \___|\__|____/|___/
%
% «SetCs-and-SetDs» (to ".SetCs-and-SetDs")
% (clgp 30 "SetCs-and-SetDs")
% (clga "SetCs-and-SetDs")
\section{Toposes of the form $\SetC$ and $\SetD$}
\label{SetCs-and-SetDs}
From here onwards we will reserve the symbol $\catC$ for small
categories and $\catD$ for ``DAG categories'', that we define as
follows: a category $\catD$ is a {\sl DAG category} iff there is a
{\sl finite} DAG $(P,A)$ such that $\catD$ is the transitive-reflexive
closure $(P,A^*)$ of $(P,A)$, regarded as a category.
We are especially interested in two kinds of DAG categories:
% (ph1p 5 "positional" "1.")
% (ph1 "positional")
%
%R local K, W, H = 1/ 1 \, 1/1 2 3\, 1/ 1 \
%R |2 3| \ 4 5 / |2 3|
%R | 4 | \4 5/
%R \ 5 /
%R H:tomp({zdef="H", scale="20pt", meta=nil}):addcells():addarrows():output()
%R K:tomp({zdef="K", scale="20pt", meta=nil}):addcells():addarrows():output()
%R W:tomp({zdef="W", scale="20pt", meta=nil}):addcells():addarrows():output()
% (jonp 27 "classifier-big-figure")
% (joe "classifier-big-figure")
%
%L myspec = "1232RL1"
%L tdims_mini = TCGDims {h=32, v=25, q=15, crh=8, crv=7, qrh=5}
%L tdims_big = TCGDims {h=110, v=110, crh=30, crv=45}
%L tspec_mini = TCGSpec.new("33; 32, 13", "?.?", "??.")
%L tspec_mini = TCGSpec.new("33; 32, 13")
%L tspec_big = TCGSpec.new("33; 32, 13")
%L tcg_T = TCGQ.newdsoa(tdims_mini, tspec_mini, {tdef="T", meta="1pt"}, "h v lr")
%L tcg_T :output()
%L
%L tspec_mini = TCGSpec.new("33; 32, 13")
%L tdims_micro = TCGDims {h=15, v=8, q=15, crh=3.5, crv=7, qrh=5}
%L tcg_Tbu = TCGQ.newdsoa(tdims_micro, tspec_mini, {tdef="Tbu", meta="1pt"}, "h b")
%L tcg_Tbu:output()
%L
%L mpnew({zdef="T"}, myspec):addlrs():print():output()
\pu
\begin{enumerate}
\item The ones coming from the ZDAGs of \cite{PH1}, sections 1--2,
with their objects labeled in the ``reading order'', as the
categories $\catH$ (``house''), $\catK$ (``kite''), and $\catW$
below:
%
$$\pu
\catH = \!\!\!\zha{H}
\qquad
\catK = \!\!\!\zha{K}
\qquad
\catW = \!\!\!\zha{W}
$$
\item ``2-column graphs'', like the one below:
%
$$\catT = \;\; \tcg{T}
$$
%
They will be discussed in the next section.
\end{enumerate}
%L tspec_mini = TCGSpec.new("33; 32, 13")
%L tdims_micro = TCGDims {h=15, v=8, q=15, crh=3.5, crv=7, qrh=5}
%L tcg_Tbu = TCGQ.newdsoa(tdims_micro, tspec_mini, {tdef="Tbu", meta="1pt"}, "h b")
%L tcg_Tbu:output()
\pu
The paper \cite{PH1} defines a language in which certain diagrams have
precise meanings as mathematical objects, but these meanings depends
on the context, and new meanings can be added. This bullet diagram
%
$$\dagKite•••••$$
%
can be interpreted as a subset of $\Z^2$ (section 1) and as a DAG with
arrows going downward (section 2); a diagram with `0's and `1's like
%
$$\dagKite00111$$
%
can be interpreted as:
\begin{enumerate}
\item a function, a characteristic function, or a subset (section 1),
\item a set or an open set in an arbitrary topology (section 11),
\item a stable subset (section 12),
\item an open set in the default topology (section 12),
\item an open set of an order topology (section 12),
\item a point in a certain partial order (section 13),
\item a point in a certain planar Heyting Algebra (in a ``ZHA'';
sections 4, 13, 16)
\end{enumerate}
Here we will add some new meanings to these lists. When we say
%
$$\catK = \dagKite••••• \qquad \text{or} \qquad \catT = \tcg{Tbu}
$$
%
these will be shorter versions of the definitions of the DAG
categories $\catK$ and $\catT$ in the beginning of the section, and
this
%
$$\dagKite00111 \ito \dagKite11111
$$
%
will be an inclusion in the category $\SetK$, that we can expand as:
%
%D diagram sub-K-left
%D 2Dx 100 +20 +20
%D 2D 100 A0
%D 2D / \
%D 2D +20 A1 A2
%D 2D \ /
%D 2D +20 A3
%D 2D |
%D 2D +20 A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> ∅ ∅ \{*\} \{*\} \{*\}
%D
%D (( A0 A1 ->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 ->
%D A3 A4 ->
%D ))
%D enddiagram
%D
%D diagram sub-K-right
%D 2Dx 100 +20 +20
%D 2D 100 A0
%D 2D / \
%D 2D +20 A1 A2
%D 2D \ /
%D 2D +20 A3
%D 2D |
%D 2D +20 A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> \{*\} \{*\} \{*\} \{*\} \{*\}
%D
%D (( A0 A1 ->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 ->
%D A3 A4 ->
%D ))
%D enddiagram
%D
%D diagram sub-K-inclusion
%D 2Dx 100 +85
%D 2D 100 A0 - A1
%D 2D
%D 2D +50 B0 - B1
%D 2D
%D ren B0 B1 ==> D E
%D
%D (( A0 .tex= \left(\diag{sub-K-left}\right) BOX
%D A1 .tex= \left(\diag{sub-K-right}\right) BOX
%D A0 A1 `->
%D # B0 B1 `-> .plabel= a T
%D ))
%D enddiagram
%D
$$\pu
\diag{sub-K-inclusion}
$$
% (ph1p 25 "topologies-on-ZSets" "12.")
% (ph1 "topologies-on-ZSets")
% (ph1p 29 "topologies-on-2CGs" "15.")
% (ph1 "topologies-on-2CGs")
Suppose that $A = \dagKite01000$ is an object of $\SetK$. This $A$ has
an arrow from a 1 to 0: the image of the morphism $2→4$ in $K$ by $A$
is a morphism from $\{*\}$ to $∅$ in $\Set$, but $\Hom(\{*\},∅)$ is
empty, so this is absurd. A diagram like $\dagKite01000$, ``with an
arrow $1→0$'', denotes a non-stable subset of a ZSet in \cite[section
12]{PH1}, and a non-open subset in \cite[section 15]{PH1}; here
it will denote something that is not an object of the DAG category
that we are dealing with.
\newpage
% __ __ _
% \ \ / /__ _ __ ___ __| | __ _
% \ V / _ \| '_ \ / _ \/ _` |/ _` |
% | | (_) | | | | __/ (_| | (_| |
% |_|\___/|_| |_|\___|\__,_|\__,_|
%
% «SetD-yoneda» (to ".SetD-yoneda")
% (clgp 32 "SetD-yoneda")
% (clga "SetD-yoneda")
\subsection{The classifier in a $\Set^\catD$ (via Yoneda)}
\label{SetD-yoneda}
% (find-maclanemoerdijkpage (+ 11 36) "For an arbitrary small category C,")
Most texts about basic topos theory define the classifier of a $\SetC$
directly, as we did in sections \ref{SetD-classifier}--\ref{SetD-chi}:
they define an object $Ω$ whose action on objects takes each $B∈\catC$
to the set of subfunctors of $\Hom(B,-)$ and whose action on morphisms
is the ``obvious'' one, and then they show that this $Ω$ obeys the
properties that we expect from the classifier.
The book \cite{MacLaneMoerdijk} does that but it also shows, in its
pages 36--39, that we can use Yoneda to prove that
$ΩB≅\Sub(\Hom(B,-))$. I struggled a lot to understand their proof, but
I found that when I specialize it to `$\SetD$'s it becomes easy to
visualize. Let me show how.
\msk
Let $(P,A)$ be a 2-column graph, let $\catD$ be $(P,A)$ regarded as a
category, and let $\catE$ be the topos $\SetD$. Let $Ω$ be any
classifier object in $\catE$. This $Ω$ is a functor from $\catD$ to
$\Set$, and:
\ssk
\Theoremsubsection The action on objects of $Ω$ takes each $B∈\catD$
to a set isomorphic to ${↓}{↓}B$.
\msk
% (favp 35 "yoneda-lemma")
% (fav "yoneda-lemma")
% (favp 40 "representable-functors")
% (fav "representable-functors")
The proof needs the two diagrams below. The one on the left is the
``standard Yoneda Lemma'': it is the diagram $\mathsf{Y}1$ of
\cite[section 7.2]{FavC} with its functor $R:\catB→\Set$ replaced by
$Ω:\catD→\Set$. The diagram on the right is the ``Yoneda Lemma for
representable functors'' --- the second diagram from \cite[section
7.6]{FavC} with its representable functor $R:\catB→\Set$ replaced by
$\Incs: (\Set^\catD)^\op → \Set$; its universal arrow is $\nameof{⊤}$,
that selects the element $(⊤:1 \monicto Ω) ∈ \Incs(Ω)$.
%
% (mmop 3 "Omega-in-presheaf")
% (mmo "Omega-in-presheaf")
%
%D diagram Omega-in-a-SetD
%D 2Dx 100 +50 +50 +55
%D 2D 100 A1 D1
%D 2D | |
%D 2D +20 A2 - A3 D2 - D3
%D 2D | | | |
%D 2D +20 A4 - A5 D4 - D5
%D 2D
%D 2D +20 B0 - B1 E0 - E1
%D 2D
%D 2D +15 C0 - C1 F0 - F1
%D 2D \ | \ |
%D 2D +20 C2 F2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 B Ω(B) C Ω(C)
%D ren B0 B1 C0 C1 C2 ==> \catD \Set \catD(B,-) \Set(1,Ω(-)) Ω(-)=Ω
%D ren D1 D2 D3 D4 D5 ==> 1 Ω \Incs(Ω) E \Incs(E)
%D ren E0 E1 ==> (\Set^\catD)^\op \Set
%D ren F0 F1 F2 ==> \Set^\catD(-,Ω) \Set(1,\Incs(-)) \Incs(-)=\Incs
%D
%D (( A1 A3 ->
%D A2 A3 |->
%D A2 A4 ->
%D A3 A5 ->
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D B0 B1 -> .plabel= a Ω
%D C0 C1 ->
%D C1 C2 <->
%D C0 C2 ->
%D # B0 relplace 0 -8 \catD
%D C0 relplace -22 0 {↓}B≅
%D ))
%D (( D1 D3 -> .plabel= r \sm{\nameof{⊤}\\(\univ)}
%D D2 D3 |->
%D D2 D4 <-
%D D3 D5 ->
%D D2 D5 harrownodes nil 20 nil |->
%D D4 D5 |->
%D E0 E1 -> .plabel= a \Incs
%D F0 F1 <->
%D F1 F2 <->
%D F0 F2 <->
%D E0 relplace 0 -7 \Set^\catD\phantom{...}
%D ))
%D enddiagram
%D
$$\pu
\diag{Omega-in-a-SetD}
$$
Now we have this sequence of isomorphisms:
$$\begin{array}{rcl}
Ω(B) & ≅ & \Set(1,Ω(B)) \\
& ≅ & \Set^\catD({↓}B,Ω) \\
& ≅ & \Incs({↓}B) \\
% & = & \Incs(\catD(B,-)) \\
% & = & \Incs(↓B) \\
\end{array}
$$
%
where the movement is:
%
% (find-latexinkscape-links "2020closures-and-J-ops/cla-1")
$$\includegraphics[height=3cm]{2020closures-and-J-ops/cla-1.pdf}$$
Let's look at an example. If $\catD$ is the category $\catT$ and $B =
▁3$ then:
%
$$\Logic(\SetT) = \zha{T}
\qquad
\begin{array}{rcl}
Ω(▁3) & ≅ & \Set(1,Ω(▁3)) \\
& ≅ & \Set^\catD({↓}(▁3),Ω) \\
& ≅ & \Incs({↓}(▁3)) \\
& ≅ & \Incs(13) \\
& ≅ & \Subsets(13) \\
& ≅ & \{00, 01, 02, 10, 11, 12, 13\} \\
% & = & \Incs(\catD(B,-)) \\
% & = & \Incs(↓B) \\
\end{array}
$$
% (jonp 2 "parts")
% (jon "parts")
% (jonp 34 "fig:five-sqconds")
% (joo "fig:five-sqconds")
\newpage
% _ _
% | | ___ _ __ ___ _ __ __ _| |_ ___ _ __ ___
% _ | |_____ / _ \| '_ \ / _ \ '__/ _` | __/ _ \| '__/ __|
% | |_| |_____| (_) | |_) | __/ | | (_| | || (_) | | \__ \
% \___/ \___/| .__/ \___|_| \__,_|\__\___/|_| |___/
% |_|
% «J-ops» (to ".J-ops")
% (clgp 6 "J-ops")
% (clga "J-ops")
\section{J-operators, slashings, and question marks}
% ____ _ __ _
% / ___| | ___ _ __ \ \ | |
% | | | |/ _ \| '_ \ _____\ \ _ | |
% | |___| | (_) | |_) | |_____/ / | |_| |
% \____|_|\___/| .__/ /_/ \___/
% |_|
%
% «clop-to-Jop» (to ".clop-to-Jop")
% (clgp 6 "clop-to-Jop")
% (clga "clop-to-Jop")
\subsection{Closure operators induce J-operators \TODO}
\label{clop-to-Jop}
Let $(P,A)$ be a 2-column graph. Let $\catE = \SetD$ be the DAG topos
generated by $(P,A)$, and let $H := \Logic(\catE)$. Let $\clop$ be a
closure operator on $\catE$. Define an operation $(·)^*: H→H$ by
defining $R^*$ as $\dom(\ovl{\inc(R,1)})$. More formally,
%
$$\begin{array}{rrcl}
(·)^*: & \Logic(\catE) &→& \Logic(\catE) \\
& R &↦& \dom(\ovl{\inc(R,1)}) \\
\end{array}
$$
And as a diagram:
%
%D diagram clop-to-Jop
%D 2Dx 100 +20 +20 +40 +20
%D 2D 100 A0 ------ A1
%D 2D | \ |
%D 2D +20 | A2 --|------------- A4
%D 2D | / | /
%D 2D +20 A5 ------ A6 ------ A7
%D 2D
%D ren A0 A1 ==> R T
%D ren A2 A4 ==> R^* T
%D ren A5 A6 A7 ==> 1 Ω Ω
%D
%D (( # Horizontal arrows:
%D A0 A1 >->
%D A2 A4 >->
%D A5 A6 >-> .plabel= b χ_{\inc(R,1)}
%D A6 A7 -> .plabel= b j
%D # A5 A7 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D A0 A5 `-> .PLABEL= _(0.40) \inc(R,1)
%D A0 A2 `->
%D A2 A5 `-> .PLABEL= ^(0.40) \ovl{\inc(R,1)}
%D
%D A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D ))
%D enddiagram
%D
$$\pu
\diag{clop-to-Jop}
$$
Note that we also have $R^* = \dom(σ(j∘χ_{\inc(R,1)}))$.
\msk
\Theoremsubsection
The operation $(·)^*$ defined above is a J-operator.
{\bf Proof.} The proofs of J1 and J2, i.e., of $R≤R^*$ and
$R^*=R^{**}$, are just the parts C1 and C2 of Theorem
\ref{thm:top-to-clop} with a slightly different notation: just rewrite
the $E$ as $1$, $D$ as $R$, $\ovl{D}$ as $R^*$, and $\ovl{\ovl{D}}$ as
$R^{**}$.
The proof of J3 is better done in two steps. First we establish the
notation, i.e., how the truth-values and their arrows to 1 will be
named, using the notation for intersection pullbacks that we defined
in Theorem \ref{thm:restr-clop-1}:
%
% (clgp 10 "top-to-clop")
% (clga "top-to-clop")
% (clga "top-to-clop" "thm:top-to-clop")
%
%D diagram C4-to-J3-notation-1
%D 2Dx 100 +35 +30 +35
%D 2D 100 A0 - A1 B0 - B1
%D 2D | | | |
%D 2D +30 A2 - A3 B2 - B3
%D 2D
%D ren A0 A1 A2 A3 ==> C{∧}D D C 1
%D ren B0 B1 B2 B3 ==> C^*{∧}D^* D^* C^* 1
%D
%D (( A0 A1 `-> .plabel= a (c∩d)''
%D A0 A2 `-> .plabel= l (c∩d)'
%D A0 A3 `-> .plabel= m (c∩d)
%D A1 A3 `-> .plabel= r d
%D A2 A3 `-> .plabel= b c
%D ))
%D (( B0 B1 `-> .plabel= a (c∩d)''
%D B0 B2 `-> .plabel= l (c∩d)'
%D B0 B3 `-> .plabel= m (c∩d)
%D B1 B3 `-> .plabel= r d
%D B2 B3 `-> .plabel= b c
%D ))
%D enddiagram
%D
%D diagram C4-to-J3-notation-2
%D 2Dx 100 +20
%D 2D 100 A0
%D 2D
%D 2D +20 A1
%D 2D
%D 2D +20 A2
%D 2D
%D ren A0 A1 A2 ==> C{∧}D (C∧D)^* 1
%D
%D (( A0 A1 `->
%D A0 A2 `-> .plabel= l c∩d
%D A1 A2 `-> .plabel= r \ovl{c∩d}
%D ))
%D enddiagram
%D
$$\pu
\diag{C4-to-J3-notation-1}
\qquad
\diag{C4-to-J3-notation-2}
$$
And here is the second step:
%
$$\def\c{c}
\def\d{d}
\begin{array}{rcl}
(C∧D)^* &=& \dom(\ovl{\c∩\d}) \\
&=& \dom(\ovl{\c}∩\ovl{\d}) \\
&=& \dom(\ovl{\c})∩\dom(\ovl{\d}) \\
&=& C^*∩D^* \\
\end{array}
%
\quad
%
\def\c{\inc(C,1)}
\def\d{\inc(D,1)}
\begin{array}{rcl}
(C∧D)^* &=& \dom(\ovl{\c∩\d}) \\
&=& \dom(\ovl{\c}∩\ovl{\d}) \\
&=& \dom(\ovl{\c})∩\dom(\ovl{\d}) \\
&=& C^*∩D^* \\
\end{array}
$$
\newpage
% _ __ _
% | | \ \ | |_ ___ _ __
% _ | | _____\ \ | __/ _ \| '_ \
% | |_| | |_____/ / | || (_) | |_) |
% \___/ /_/ \__\___/| .__/
% |_|
%
% «Jop-to-top» (to ".Jop-to-top")
% (clgp 7 "Jop-to-top")
% (clga "Jop-to-top")
\subsection{J-operators induce topologies \TODO}
Let's state this in its general form first, and then see an example
that clarifies what it means and how it works.
\msk
\Theoremsubsection
\label{thm:Jop-to-top-generic}
\begin{tabular}{rl}
Suppose that: & $\catD$ is a DAG category, \\
& $\catE$ is $\SetD$, \\
& $j$ is a topology in $\catE$, \\
& $\clop$ is the closure operator associated to $j$, \\
& $B$ is an object of $D$, \\
& $R$ is ${↓}B$ (so $R∈\Logic(E)$), \\
& $(q:Q \ito R)∈\Incs(R)$ (so $Q≤R$), \\
& $(\ovl{q}:\ovl{Q} \ito R)$ is the closure of $q$ (so $Q≤\ovl{Q}≤R$). \\
Then: & $RB=\{*\}$, \\
& $ΩB={↓}{↓}B={↓}R$, \\
& $(χ_qB)(*)=Q$, \\
& $(χ_{\ovl{q}}B)(*)=\ovl{Q}$, \\
and so: & $\begin{array}[t]{rcl}
jB(Q) &=& jB(χ_qB(*)) \\
&=& (jB∘χ_qB)(*) \\
&=& (j∘χ_q)(B)(*) \\
&=& χ_{\ovl{q}}(B)(*) \\
&=& \ovl{Q}. \\
\end{array}
$ \\
\end{tabular}
\msk
%D diagram Jop-to-top-generic
%D 2Dx 100 +20 +20 +40 +20
%D 2D 100 A0 ------ A1
%D 2D | \ |
%D 2D +20 | A2 --|------------- A4
%D 2D | / | /
%D 2D +20 A5 ------ A6 ------ A7
%D 2D
%D 2D +25 B0 ------ B1 ------ B2
%D 2D
%D 2D +25 C0 ------ C1
%D 2D +8 C2 ---------------- C3
%D 2D +8 C4 ------ C5
%D 2D
%D ren A0 A1 ==> Q T
%D ren A2 A4 ==> \ovl{Q} T'
%D ren A5 A6 A7 ==> R Ω Ω'
%D
%D ren B0 B1 B2 ==> RB ΩB ΩB
%D
%D ren C0 C1 ==> * Q
%D ren C2 C3 ==> * \ovl{Q}
%D ren C4 C5 ==> Q \ovl{Q}
%D
%D (( # Horizontal arrows:
%D A0 A1 >->
%D A2 A4 >->
%D A5 A6 >-> .plabel= b χ_q
%D A6 A7 -> .plabel= b j
%D A5 A7 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D A5 relplace -15 0 {↓}B=
%D
%D A0 A5 `-> .PLABEL= _(0.40) q
%D A0 A2 `->
%D A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D B0 B1 -> .plabel= b χ_qB
%D B1 B2 -> .plabel= b jB
%D B0 B2 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}B
%D
%D C0 C1 |->
%D C2 C3 |->
%D C4 C5 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{Jop-to-top-generic}
$$
\newpage
\Examplesubsection
\label{thm:Jop-to-top-1}
%
If we make $\catD=\catT$, $B=3▁$, $Q=11$, and $\ovl{Q}=21$ in the
previous diagram it becomes this:
%D diagram Jop-to-top-1
%D 2Dx 100 +20 +20 +40 +20
%D 2D 100 A0 ------ A1
%D 2D | \ |
%D 2D +20 | A2 --|------------- A4
%D 2D | / | /
%D 2D +20 A5 ------ A6 ------ A7
%D 2D
%D 2D +25 B0 ------ B1
%D 2D +8 B2 ---------------- B3
%D 2D +8 B4 ------ B5
%D 2D
%D ren A0 A1 ==> 11 T
%D ren A2 A4 ==> 21 T'
%D ren A5 A6 A7 ==> 32 Ω Ω'
%D
%D ren B0 B1 ==> (3▁,*) (3▁,11)
%D ren B2 B3 ==> (3▁,*) (3▁,21)
%D ren B4 B5 ==> (3▁,11) (3▁,21)
%D
%D (( # Horizontal arrows:
%D A0 A1 >->
%D A2 A4 >->
%D A5 A6 >-> .plabel= b χ_q
%D A6 A7 -> .plabel= b j
%D A5 A7 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D A5 relplace -15 0 {↓}3▁=
%D
%D A0 A5 `-> .PLABEL= _(0.40) q
%D A0 A2 `->
%D A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D B0 B1 |->
%D B2 B3 |->
%D B4 B5 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{Jop-to-top-1}
$$
% «Jop-to-top-defs» (to ".Jop-to-top-defs")
%
%L tdims_med = TCGDims {h=30, v=10, crh=11, crv=8}
%L tspec_med = TCGSpec.new("33; 32, 13")
%L tcg_med = TCGQ.newdsoa(tdims_med, tspec_med,
%L {tdef="Tmed", meta="1pt s"},
%L "h p")
%L tcg_med:Lput(3, "\\Ta"); tcg_med:Rput(3, "\\Tb")
%L tcg_med:Lput(2, "\\Tc"); tcg_med:Rput(2, "\\Td")
%L tcg_med:Lput(1, "\\Te"); tcg_med:Rput(1, "\\Tf")
%L tcg_med:output()
\pu
\def\Tmed#1#2#3#4#5#6{{
\def\Ta{#1} \def\Tb{#2}
\def\Tc{#3} \def\Td{#4}
\def\Te{#5} \def\Tf{#6}
\left(\!\!\!
\tcg{Tmed}
\!\right)
}}
\def\C#1{\{#1\}}
\def\UN{{\C{*}}}
\def\TT{{\Tmed
{\C{32}} {\C{13}}
{\C{20}} {\C{02}}
{\C{10}} {\C{01}}
}}
\def\TA{{\Tmed ∅∅ ∅∅ \UN\UN}}
\def\TB{{\Tmed ∅∅ \UN∅ \UN\UN}}
\def\TC{{\Tmed \UN∅ \UN\UN \UN\UN}}
Here is its internal view:
%
%D diagram Jop-to-top-big-ex
%D 2Dx 100 +30 +30 +50 +30
%D 2D 100 A0 ------ A1
%D 2D | \ |
%D 2D +30 | A2 --|------------- A4
%D 2D | / | /
%D 2D +30 A5 ------ A6 ------ A7
%D 2D
%D 2D +25 B0 ------ B1
%D 2D +8 B2 ---------------- B3
%D 2D +8 B4 ------ B5
%D 2D
%D ren A0 A1 ==> \TA \TT
%D ren A2 A4 ==> \TB \TT
%D ren A5 A6 A7 ==> \TC Ω Ω'
%D
%D ren B0 B1 ==> (3▁,*) (3▁,11)
%D ren B2 B3 ==> (3▁,*) (3▁,21)
%D ren B4 B5 ==> (3▁,11) (3▁,21)
%D
%D (( # Horizontal arrows:
%D A0 A1 >->
%D A2 A4 >->
%D A5 A6 >-> .plabel= b χ_q
%D A6 A7 -> .plabel= b j
%D A5 A7 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D A5 relplace -15 0 {↓}3▁=
%D
%D A0 A5 `-> .PLABEL= _(0.40) q
%D A0 A2 `->
%D A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D B0 B1 |->
%D B2 B3 |->
%D B4 B5 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{Jop-to-top-big-ex}
$$
I did not expand the `$Ω$'s because their internal views would be too
big -- see the last diagram in section \ref{SetD-classifier}. Note
that the images of $R$ by the monics $χ_q$ and $χ_{\ovl{q}}$ (that are
not inclusions!) are, respectively:
%
$$\Tmed {\C{11}} {∅}
{\C{10}} {\C{01}}
{\C{10}} {\C{01}}
\qquad
\text{and}
\qquad
\Tmed {\C{21}} {∅}
{\C{20}} {\C{01}}
{\C{10}} {\C{01}}
\;.
$$
\newpage
% «def-j» (to ".def-j")
% (clgp 9 "def-j")
% (clga "def-j")
\Theoremsubsection
\label{thm:Jop-to-top-formula}
\begin{tabular}{rl}
Suppose that: & $(P,A)$ is a 2-column graph, \\
& $\catD$ is $(P,A)$ as a DAG category, \\
& $\catE$ is $\SetD$, \\
& $H$ is $\Logic(\catE)$, \\
& $(·)^*$ is a J-operator on $H$. \\
Then the operation & $j = λB⠆P.λQ⠆{↓}Q.Q^*∧{↓}B$ \\
is a morphism & $j:Ω→Ω$ \\
that obeys & $j∘j=j$, \\
& $j∘⊤_Ω=⊤_Ω$, \\
& $∧∘j=(j×j)∘∧$, \\
i.e., & $j$ is a topology on $\catE$. \\
\end{tabular}
%D diagram Jop-to-top-def-j
%D 2Dx 100 +20 +20 +40 +20
%D 2D 100 A0 ------ A1
%D 2D | \ |
%D 2D +20 | A2 --|------------- A4
%D 2D | / | /
%D 2D +20 A5 ------ A6 ------ A7
%D 2D
%D 2D +25 B0 ------ B1 ------ B2
%D 2D
%D 2D +25 C0 ------ C1
%D 2D +8 C2 ---------------- C3
%D 2D +8 C4 ------ C5
%D 2D
%D ren A0 A1 ==> Q T
%D ren A2 A4 ==> Q^*{∧}{↓}B T'
%D ren A5 A6 A7 ==> R Ω Ω'
%D
%D ren B0 B1 B2 ==> RB ΩB ΩB
%D
%D ren C0 C1 ==> * Q
%D ren C2 C3 ==> * Q^*{∧}{↓}B
%D ren C4 C5 ==> Q Q^*{∧}{↓}B
%D
%D (( # Horizontal arrows:
%D A0 A1 >->
%D A2 A4 >->
%D A5 A6 >-> .plabel= b χ_q
%D A6 A7 -> .plabel= b j
%D A5 A7 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D A5 relplace -15 0 {↓}B=
%D
%D A0 A5 `-> .PLABEL= _(0.40) q
%D A0 A2 `->
%D A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D B0 B1 -> .plabel= b χ_qB
%D B1 B2 -> .plabel= b jB
%D B0 B2 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}B
%D
%D C0 C1 |->
%D C2 C3 |->
%D C4 C5 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{Jop-to-top-def-j}
$$
\msk
\def\adb{{∧}{↓}B}
% «def-j-NT» (to ".def-j-NT")
% (clgp 35 "def-j-NT")
% (clga "def-j-NT")
To prove that this $j:Ω→Ω$ is a natural transformation in $\SetD$ we
need to check that the square at the right here commutes:
%
%D diagram def-j-NT
%D 2Dx 100 +20 +25 +40 +50
%D 2D 100 A0 B0 - B1 E0 - E1
%D 2D | | | | |
%D 2D +17 | | | | E3'
%D 2D +8 A1 B2 - B3 E2 - E3
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> B C
%D ren B0 B1 B2 B3 ==> ΩB ΩB ΩC ΩC
%D ren C0 C1 ==> Ω Ω
%D ren E0 E1 E3' ==> Q Q^*\adb (Q{∧}{↓}B)^*{∧}{↓}C
%D ren E2 E3 ==> Q{∧}{↓}C (Q{∧}{↓}C)^*{∧}{↓}C
%D
%D (( A0 A1 -> .plabel= l f
%D B0 B1 -> .plabel= a jB
%D B0 B2 -> .plabel= l Ωf
%D B1 B3 -> .plabel= r Ωf
%D B2 B3 -> .plabel= a jC
%D C0 C1 -> .plabel= a j
%D ))
%D
%D (( E0 E1 |->
%D E0 E2 |->
%D E1 E3' |->
%D E2 E3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{def-j-NT}
$$
\newpage
% «def-j-obeys-J1-J2-J3» (to ".def-j-obeys-J1-J2-J3")
% (clgp 38 "def-j-obeys-J1-J2-J3")
% (clga "def-j-obeys-J1-J2-J3")
To prove that $j$ obeys J1, J2, J3 we need to check that the lower
three diagrams here commute:
%
%D diagram def-j-1
%D 2Dx 100 +20 +20 +20 +30 +25
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +20 A2 B2 C2 C3
%D 2D
%D ren A0 A1 A2 ==> Ω Ω Ω
%D ren B0 B1 B2 ==> Ω Ω Ω
%D ren C0 C1 C2 C3 ==> Ω×Ω Ω Ω×Ω Ω
%D
%D (( A0 A1 -> .plabel= a ⊤
%D A0 A2 -> .plabel= l ⊤
%D A1 A2 -> .plabel= r j
%D
%D B0 B1 -> .plabel= a j
%D B0 B2 -> .plabel= l j
%D B1 B2 -> .plabel= r j
%D
%D C0 C1 -> .plabel= a ∧
%D C0 C2 -> .plabel= l j×j
%D C1 C3 -> .plabel= r j
%D C2 C3 -> .plabel= a ∧
%D ))
%D enddiagram
%D
$$\pu
\diag{def-j-1}
$$
%D diagram def-j-2
%D 2Dx 100 +20 +20 +25 +30 +45
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +20 A2 B2 C2 C3
%D 2D
%D ren A0 A1 A2 ==> ΩB ΩB ΩB
%D ren B0 B1 B2 ==> ΩB ΩB ΩB
%D ren C0 C1 C2 C3 ==> ΩB{×}ΩB ΩB ΩB{×}ΩB ΩB
%D
%D (( A0 A1 -> .plabel= a jB
%D A0 A2 -> .plabel= l jB
%D A1 A2 -> .plabel= r jB
%D
%D B0 B1 -> .plabel= a ⊤_ΩB
%D B0 B2 -> .plabel= l ⊤_ΩB
%D B1 B2 -> .plabel= r jB
%D
%D C0 C1 -> .plabel= a λQ,R.Q{∧}R
%D C0 C2 -> .plabel= l jB×jB
%D C1 C3 -> .plabel= r jB
%D C2 C3 -> .plabel= a λQ,R.Q{∧}R
%D ))
%D enddiagram
%D
$$\pu
\diag{def-j-2}
$$
%D diagram def-j-3
%D 2Dx 100 +30 +30 +25 +45 +65
%D 2D 100 A0 - A1 B0 - B1 C0 - C1
%D 2D \ | \ | | |
%D 2D +17 \ A2' \ B2' | C3'
%D 2D +8 A2 B2 C2 - C3
%D 2D
%D ren A0 A1 A2' A2 ==> Q Q^*\adb (Q^*\adb)^*\adb Q^*\adb
%D ren B0 B1 B2' B2 ==> Q {↓}B ({↓}B)^*\adb {↓}B
%D ren C0 C1 C3' C2 C3 ==> (Q,R) Q{∧}R (Q{∧}R)^*\adb (Q^*\adb,R^*\adb) (Q^*\adb){∧}(R^*\adb)
%D
%D (( A0 A1 |->
%D A1 A2' |->
%D A0 A2 |-> .curve= _20pt
%D
%D B0 B1 |->
%D B1 B2' |->
%D B0 B2 |-> .curve= _20pt
%D
%D C0 C1 |->
%D C1 C3' |->
%D C0 C2 |->
%D C2 C3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{def-j-3}
$$
% \newpage
% «def-j-example» (to ".def-j-example")
% (clgp 42 "def-j-example")
% (clga "def-j-example")
% (clgp 28 "SetT-classifier-defs")
% (clga "SetT-classifier-defs")
% % «clop-Jop-bij» (to ".clop-Jop-bij")
% % (clgp 28 "clop-Jop-bij")
% % (clga "clop-Jop-bij")
% \subsection{A bijection \TODO}
%
% «SetD-dense-closed» (to ".SetD-dense-closed")
% (clgp 38 "SetD-dense-closed")
% (clga "SetD-dense-closed")
\subsection{Dense and closed maps in a $\SetD$ \TODO}
Let $\catD$ be a DAG topos with a J-operator. If $R$ and $S$ are two
truth-values in it with $R≤S$ we can name the inclusions between $R$,
$S$, and $1$ like this:
%
%D diagram ??
%D 2Dx 100 +15 +15
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2
%D 2D
%D ren A0 A1 A2 ==> R S 1
%D
%D (( A0 A1 `-> .plabel= a m
%D A0 A2 `-> .plabel= l r
%D A1 A2 `-> .plabel= r s
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%
and can use the Theorem \ref{thm:restr-clop-1} to calculate $\ovl{m}$
using just the J-operator. We have this:
%
%D diagram ??
%D 2Dx 100 +20
%D 2D 100 A0
%D 2D
%D 2D +20 A1
%D 2D
%D 2D +20 A2
%D 2D
%D ren A0 A1 A2 ==> R R^S{=}R^*{∧}S S
%D
%D (( A0 A1 `-> .plabel= r (dense)
%D A0 A2 `-> .plabel= l m
%D A1 A2 `-> .plabel= r \sm{\ovl{m}\\(closed)}
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%
where we call the mediating map $d$, and we know that $d$ is dense and
$\ovl{m}$ is closed by Theorem \ref{thm:dense-and-closed-2}.
This gives us lots of examples of dense and closed maps in a topos
with a J-operator. For example, if $R=11$ and $S=14$ in the figure
below, then $R^*=23$ and $R^S=R^*∧S=13$:
%
% (jonp 16 "valuations")
% (jov "valuations")
%
%L mp = mpnew({zdef="11-13-14", scale="12pt", meta="s"}, "1R2R3212RL1")
%L mp:addcuts("c 4321/0 0123|45|6")
%L mp:put(v"11", "R"):put(v"23", "R*", "R^*")
%L mp:put(v"14", "S"):put(v"13", "RS", "R^S")
%L mp:output()
%
%D diagram ??
%D 2Dx 100 +25
%D 2D 100 A0
%D 2D
%D 2D +25 A1
%D 2D
%D 2D +25 A2
%D 2D
%D ren A0 A1 A2 ==> 11 13{=}23{∧}14 14
%D ren A0 A1 A2 ==> 11 13=23∧14 14
%D
%D (( A0 A1 `-> .plabel= r (dense)
%D A0 A2 `-> # .plabel= l m
%D A1 A2 `-> .plabel= r (closed)
%D ))
%D enddiagram
%D
\pu
$$%\zha{O_A(P),J}
%\qquad
\zha{11-13-14}
\qquad
\qquad
\diag{??}
$$
By trying many examples of this factorization I got two conjectures:
\Conjecturesubsection an inclusion $R \ito R'$ in the logic is dense
iff both $R$ and $R'$ belong to the same region of the slashing,
\Conjecturesubsection an inclusion $S' \ito S$ in the logic is dense
iff $S'$ cannot be moved upwards toward $S$ without crossing a line of
the slashing.
They are both easy to prove. (...)
% «SetD-sheaves» (to ".SetD-sheaves")
% (clgp 39 "SetD-sheaves")
% (clga "SetD-sheaves")
\subsection{Sheaves in a $\SetD$ \TODO}
% (find-mclartypage (+ 4 196) "21. Topologies")
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 174) "(mu-)sheaf")
% (find-books "__cats/__cats.el" "johnstone-topostheory")
% (find-topostheorypage (+ 24 81) "3.2. Sheaves")
% (find-toposthepubpage 113 "3.2. Sheaves")
% (find-toposthepubtext 113 "3.2. Sheaves")
The usual definition of a sheaf in a topos $\catE$ with a topology $j$
is that an object $S∈\catE$ is a ($j$-)sheaf iff for every dense monic
$d: D \monicto E$ in $\catE$ every map $f: D \to S$ factors uniquely
through $d: D \monicto E$. I prefer to write this backwards: $S$ is a
sheaf iff for every dense monic $d: D \monicto E$ the map of hom-sets
$(∘d): \Hom(E,S) → \Hom(D,S)$ is a bijection. In a diagram:
%
%D diagram ??
%D 2Dx 100 +25 +40 +30
%D 2D 100 A0 B0 C0
%D 2D | \ |
%D 2D +25 A1 - A2 B1 C1
%D 2D
%D ren A0 A1 A2 ==> ∀D ∀E S
%D ren B0 B1 ==> \Hom(D,S) \Hom(E,S)
%D ren C0 C1 ==> g∘d g
%D
%D (( A0 A1 `-> .plabel= l \sm{∀d\\dense} sl_
%D A0 A2 -> .plabel= r ∀f
%D A1 A2 -> .plabel= b ∃!g
%D
%D B1 B0 -> .plabel= l \sm{∘d\\iso}
%D
%D C1 C0 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
In a $\SetD$ we can get lots of properties that sheaves must obey by
understanding what the condition above means on a very small family of
dense maps --- the ``basic dense maps''. Suppose that we have a DAG
with question marks $((P,A),Q)$ and that our topos $\catE$ with
topology $j$ is generated by that $((P,A),Q)$. For every point $B$ of
the set of question marks $Q$ let $bd(B): D \ito E$ be the inclusion
in which $E$ is ${↓}B$ and $D$ is $E$ minus the point $B$. We will
call these `$bd(B)$'s the {\sl basic dense maps} of our topos.
% % «SetD-closure» (to ".SetD-closure")
% % (clgp 41 "SetD-closure")
% % (clga "SetD-closure")
% \subsection{From question marks to a closure operator \TODO}
%
% %L -- (find-dn6 "tcgs.lua" "TCGQ")
% %L -- (find-dn6 "tcgs.lua" "TCGQ" "Lput =")
% %L TCGQ.__index.Lputs = function (tq, arr)
% %L if type(arr) == "string" then arr = split(arr) end
% %L for y,str in ipairs(arr) do tq:Lput(y, str) end
% %L return tq
% %L end
% %L TCGQ.__index.Rputs = function (tq, arr)
% %L if type(arr) == "string" then arr = split(arr) end
% %L for y,str in ipairs(arr) do tq:Rput(y, str) end
% %L return tq
% %L end
% %L
% %L tdims_clo = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7} -- with v arrows
% %L tspec_clo1 = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
% %L tspec_clo2 = TCGSpec.new("46; 11 22 34 45, 25", "....", "???...")
% %L tcg_clo1 = TCGQ.newdsoa(tdims_clo, tspec_clo1, {tdef="clo-1", meta="1pt p"}, "q h")
% %L tcg_clo2 = TCGQ.newdsoa(tdims_clo, tspec_clo2, {tdef="clo-2", meta="1pt p"}, "q h")
% %L tcg_clo1:Lputs("1 · · ·")
% %L tcg_clo2:Lputs("1 · · ·")
% %L tcg_clo1:Rputs("1 0 0 0 · ·")
% %L tcg_clo2:Rputs("1 0 0 0 · ·")
% %L tcg_clo1:output()
% %L tcg_clo2:output()
% \pu
% $$\tcg{clo-1}
% \qquad
% \tcg{clo-2}
% $$
% «topological-lemmas» (to ".topological-lemmas")
% (clgp 30 "topological-lemmas")
% (clga "topological-lemmas")
\subsection{Some topological lemmas \TODO}
Let $(X,\Opens(X))$ be a topological space.
\msk
\Lemmasubsection If $A,B⊆X$ then $\Int(A∩B) = \Int(A)∩\Int(B)$.
{\bf Proof.} Suppose that $c∈\Int(A)∩\Int(B)$. Then we have open sets
$W,V∈\Opens(X)$ that make all the inferences in the tree at the left
below true, and so $c∈\Int(A∩B)$. Now suppose that $d∈\Int(A∩B)$. We
have an open set $U∈\Opens(X)$ that makes all the inferences in the
tree at the right below true, and so $d∈\Int(A)∩\Int(B)$. This means
that $\Int(A)∩\Int(B)⊆\Int(A∩B)$ and $\Int(A∩B)⊆\Int(A)∩\Int(B)$, and
so $\Int(A∩B) = \Int(A)∩\Int(B)$.
%:
%: c∈\Int(A)∩\Int(B) c∈\Int(A)∩\Int(B)
%: ----------------- -----------------
%: c∈\Int(A) c∈\Int(B)
%: ----------- -----------
%: c∈V⊆\Int(A) c∈V⊆\Int(B)
%: ----------- -----------
%: c∈V⊆A c∈W⊆B
%: ------- -------
%: c∈V∩W⊆A c∈V∩W⊆B
%: -----------------------------
%: c∈V∩W⊆A∩B
%: -----------
%: c∈\Int(A∩B)
%:
%: ^top-lemma-1
%:
%:
%: d∈\Int(A∩B) d∈\Int(A∩B)
%: ------------- -------------
%: d∈U⊆\Int(A∩B) d∈U⊆\Int(A∩B)
%: ------------- -------------
%: d∈U⊆A∩B d∈U⊆A∩B
%: ------- -------
%: d∈U⊆A d∈U⊆B
%: --------- ---------
%: d∈\Int(A) d∈\Int(B)
%: --------------------------
%: d∈\Int(A)∩\Int(B)
%:
%: ^top-lemma-2
%:
\pu
$$\ded{top-lemma-1}$$
$$\ded{top-lemma-2}$$
\msk
\Lemmasubsection If $W,V∈\Opens(X)$, $W⊆V$, and $A⊆X$, then
$\Int(W∪A)∩V = \Int(W∪(A∩V))$.
{\bf Proof:}
%
$$\begin{array}{rcl}
\Int(W∪A)∩V &=& \Int(W∪A)∩\Int(V) \\
&=& \Int((W∪A)∩V) \\
&=& \Int((W∩V)∪(A∩V)) \\
&=& \Int(W∪(A∩V)). \\
\end{array}
$$
\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=2020clops-and-tops-garbage veryclean
make -f 2019.mk STEM=2020clops-and-tops-garbage pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "clg"
% End: