|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2021lindenhovius-j-to-X.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021lindenhovius-j-to-X.tex" :end))
% (defun p () (interactive) (find-LATEXsh "pdflatex 2021lindenhovius-j-to-X.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2021lindenhovius-j-to-X.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021lindenhovius-j-to-X.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021lindenhovius-j-to-X.pdf"))
% (defun e () (interactive) (find-LATEX "2021lindenhovius-j-to-X.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021lindenhovius-j-to-X"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2021lindenhovius-j-to-X.pdf"))
% (code-eec-LATEX "2021lindenhovius-j-to-X")
% (find-pdf-page "~/LATEX/2021lindenhovius-j-to-X.pdf")
% (find-sh0 "cp -v ~/LATEX/2021lindenhovius-j-to-X.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021lindenhovius-j-to-X.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021lindenhovius-j-to-X.pdf
% file:///tmp/2021lindenhovius-j-to-X.pdf
% file:///tmp/pen/2021lindenhovius-j-to-X.pdf
% http://angg.twu.net/LATEX/2021lindenhovius-j-to-X.pdf
% (find-LATEX "2019.mk")
% https://arxiv.org/submit/3842941
% https://arxiv.org/submit/3842941/view
% «.defs» (to "defs")
%
% «.title» (to "title")
% «.components» (to "components")
% «.proofs» (to "proofs")
% «.other-formula» (to "other-formula")
%
% «.arxiv» (to "arxiv")
% «.make» (to "make")
\documentclass[oneside,11pt]{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")
%
% (find-dednat6file "demo-write-dnt.tex")
\usepackage{ifluatex}
\ifluatex
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\else
\usepackage[utf8]{inputenc}
\input edrx21chars-d.tex % (find-LATEX "edrx21chars-d.tex")
\fi
%
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
%
% (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[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\ifluatex
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}
\else
\input\jobname.dnt % (find-LATEXfile "2021lindenhovius-j-to-X.dnt")
\def\pu{}
\fi
%L forths["<.>"] = function () pusharrow("<.>") end
%L forths["<-->"] = function () pusharrow("<-->") end
%L forths["|-->"] = function () pusharrow("|-->") end
%L forths["<--|"] = function () pusharrow("<--|") end
% «defs» (to ".defs")
\def\Downs {\mathcal{D}}
\def\Ddp {\Downs({↓}p)}
\def\singp {\{p\}}
\def\dnp {{↓}p}
\def\dnpo {{↓}p∖\{p\}}
\def\setofsc#1#2{\{\,#1\;:\;#2\,\}}
\def\nuc {(·)^*}
\def\Nucs {\mathsf{Nucs}}
\def\GrTops{\mathsf{GrTops}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (linfp 1 "title")
% (linfa "title")
\title{On a formula that is not in \\ ``Grothendieck Topologies in
Posets''}
\author{
% A.J.~Lindenhovius
% \and
Eduardo Ochs
}
\maketitle
\begin{abstract}
The paper \cite{Lindenhovius} shows that when $𝐏$ is an Artinian
poset and $𝐄$ is the topos $\Set^𝐏$ then there are bijections
between the set of subsets of $𝐏$, the set of Grothendieck
topologies on $𝐄$, and the set of nuclei on the Heyting Algebra
$\Sub(1_𝐄)$. It also shows that there are nice formulas for
converting between subsets, Grothendieck topologies, and nuclei, but
the formula for converting a nucleus to a subset is not spelled out
explicitly. These notes fix that gap.
% The paper ``Grothendieck Topologies on Posets'' by A.J.
% Lindenhovius shows that when $\mathbf{P}$ is an Artinian poset and
% $\mathbf{E}$ is the topos $\mathbf{Set}^\mathbf{P}$ then there are
% bijections between the set of subsets of $\mathbf{P}$, the set of
% Grothendieck topologies on $\mathbf{E}$, and the set of nuclei on
% the Heyting Algebra $\mathrm{Sub}(1_\mathbf{E})$. It also shows
% that there are nice formulas for converting between subsets,
% Grothendieck topologies, and nuclei, but the formula for
% converting a nucleus to a subset is not spelled out explicitly.
% These notes fix that gap.
\end{abstract}
Let $𝐏$ be a downward-directed poset, that we will also regard as a
category. Then $𝐄:=\Set^𝐏$ is a topos and $H:=\Sub(1_𝐄)$ is a Heyting
Algebra. Let's denote the set of all Grothendieck topologies on $𝐄$ by
$\GrTops(𝐏)$, the set of all nuclei on $H$ by $\Nucs(𝐏)$, and the set
of subsets of (the set of points of) $𝐏$ by $\Pts(𝐏)$. In
\cite{Lindenhovius} Bert Lindenhovius shows that when $𝐏$ is Artinian
we have bijections between $\Pts(𝐏)$, $\Nucs(𝐏)$, and $\GrTops(𝐏)$. He
uses notational conventions in which $J$ always denotes a Grothendieck
topology, $j$ always denotes a nucleus, and $X$ always denotes a
subset of $𝐏$, and he writes the components these bijections as
$(j↦J_j)$, $(J↦j_J)$, and so on; we will also write them here as
$(j↦J)$, $(J↦j)$, etc, and we will write the bijections as $(X↔j)$,
$(X↔J)$, and $(j↔J)$. Let's put all this in a diagram:
%
%D diagram bijections
%D 2Dx 100 +45 +40 +45
%D 2D 100 A0 - A1 B0 - B1
%D 2D | / | /
%D 2D +45 A2 - A3 B2 - B3
%D 2D
%D ren A0 A1 A2 ==> \Pts(𝐏) \Nucs(𝐏) \GrTops(𝐏)
%D ren B0 B1 B2 ==> X j J
%D
%D (( A0 A1 -> sl^ .plabel= a \smt{C.4.2}
%D A0 A1 <-- sl_ .plabel= b \smt{(e-mail)}
%D A0 A2 -> sl_ .plabel= l \smtt{2.8,}{C.4.1}
%D A0 A2 <- sl^ .plabel= r \smt{2.9}
%D A2 A1 <-> .plabel= m \smtt{B.8,}{B.25}
%D # A2 A3 <-->
%D ))
%D (( B0 B1 |-> sl^ .plabel= a \sm{(X↦j)}
%D B0 B1 <--| sl_ .plabel= b \sm{(j↦X)}
%D B0 B2 <-> .plabel= l \sm{(X↦J),\\(J↦X)}
%D B2 B1 <-> .plabel= m \sm{(j↦J),\\(J↦j)}
%D ))
%D enddiagram
%D
$$\pu
\diag{bijections}
$$
\newpage
% «components» (to ".components")
% (linfp 2 "components")
% (linfa "components")
He defines the components of these bijections as:
%
$$\begin{array}{rrcll}
(X↦j): & j_X(S) &=& X→S & \text{(C.4.2, C.2)} \\
(j↦X): & X_j &=& \setofsc {p∈𝐏} {p\not∈j(\dnpo)} & \text{(e-mail)} \\
[5pt]
(X↦J): & J_X(p) &=& \setofsc{S∈\Ddp}{X∩{↓}p⊆S} & \text{(2.8, C.4.1)} \\
(J↦X): & X_J &=& \setofsc{p∈𝐏}{J(p)=\{{↓}p\}} & \text{(2.9)} \\
[5pt]
(j↦J): & J_j(p) &=& \setofsc {S∈\Downs(\dnp)} {p∈j(S)} & \text{(B.8, B.25)} \\
(J↦j): & j_J(S) &=& \setofsc {p∈𝐏} {S∩{↓}p∈J(p)} & \text{(B.8, B.25)} \\
\end{array}
$$
The annotations like ``(C.4.2, C.2)'' indicate where these components
are defined. Note that one of the annotations says ``(e-mail)''; this
is because that formula doesn't appear explicitly in
\cite{Lindenhovius}, and so I (Eduardo) asked him (Bert) if that
formula was what I guessed it would be, and he replied with a formula
slightly shorter than my guess, and a proof...
\msk
These notes are just to make his formula and his proof available in a
public place. All the mathematical content here is by Bert
Lindenhovius, and all the typesetting was done by Eduardo Ochs, who
found Bert's proof hard to follow and decided to typeset it in Natural
Deduction form. {\sl Note:} when I wrote the first version of these
notes I listed Bert as the main author and me as the coauthor, but he
told me that he preferred to be credited only in the text. I insisted,
and explained that I would have never been able to find these proofs
by myself --- but he insisted more.
\bsk
If we combine $(j↦J)$ and $(J↦X)$ we get this:
%
$$\begin{array}{crcl}
(j↦J): & J_j(p) &=& \setofsc {S∈\Downs(\dnp)} {p∈j(S)} \\
(J↦X): & X_J &=& \setofsc {p∈𝐏} {J(p)=\{{↓}p\}} \\
(j↦J↦X): & X_{J_j} &=& \setofsc {p∈𝐏} { \setofsc {S∈\Downs(\dnp)} {p∈j(S)} =\{{↓}p\}} \\
& &=& \setofsc {p∈𝐏} {∀S∈\Downs(\dnp). \; ((p∈j(S))↔(S={↓}p))} \\
[5pt]
(j↦X): & X_j &=& \setofsc {p∈𝐏} {p\not∈j(\dnpo)} \\
\end{array}
$$
It is not obvious at all that $X_{J_j} = X_j$. We will prove that
$p∈X_j$ iff $p∈X_{J_j}$, where:
%
$$\begin{array}{rcl}
(p∈X_j) &=& (p\not∈j(\dnpo)) \\
(p∈X_{J_j}) &=& ∀S∈\Downs(\dnp). \; (p∈j(S))↔(S={↓}p) \\
\end{array}
$$
\newpage
% «proofs» (to ".proofs")
% (linfp 3 "proofs")
% (linfa "proofs")
\def\H#1{\hspace{#1cm}}
Look:
%:
%:
%: p∈X_{J_j}
%: ------------------ ---------------------------------
%: \dnpo∈\Downs(\dnp) ∀S∈\Downs(\dnp).(p∈j(S))↔(S=\dnp)
%: ------------------------------------------------------
%: (p∈j(\dnpo))↔(\dnpo=\dnp)
%: --------------------------------- --------------
%: (p\not∈j(\dnpo))↔(\dnpo\not=\dnp) \dnpo\not=\dnp
%: ----------------------------------------------------
%: p\not∈j(\dnpo)
%: --------------------
%: p∈X_j
%:
%: ^part-small
%:
\pu
$$\ded{part-small}$$
%:
%:
%: [S∈\Downs(\dnp)]^2
%: ------------------
%: S⊂\dnp [S\neq\dnp]^1 [S∈\Downs(\dnp)]^2
%: ------------------------------- --------------
%: p\not∈S S⊂\dnp
%: -------------------------------------
%: S⊂\dnpo p∈X_j
%: ------------- --------------
%: j(S)⊂j(\dnpo) \H{-1} p\not∈j(\dnpo)
%: ----------------------------------------------------
%: p\not∈j(S)
%: ------------------------1
%: (S\neq\dnp)→(p\not∈j(S))
%: ------------------------ -----------------
%: (p∈j(S))→(S=\dnp) \H{-1} (S=\dnp)→(p∈j(S))
%: -----------------------------------------------------
%: (p∈j(S))↔(S=\dnp)
%: ---------------------------------2
%: ∀S∈\Downs(\dnp).(p∈j(S))↔(S=\dnp)
%: ---------------------------------
%: p∈X_{J_j}
%:
%: ^part-big
%:
\pu
$$\ded{part-big}$$
This proves that $X_j$ and $X_{J_j}$ are equal.
\newpage
% «other-formula» (to ".other-formula")
% (linfp 4 "other-formula")
% (linfa "other-formula")
Now let's check that $X_j$ and $X'_j$ are equal,
where $X'_j$ is defined as:
$$\begin{array}{rcl}
X_j &=& \setofsc {p∈𝐏} {p\not∈j(\dnpo)} \\
X'_j &=& \setofsc {p∈𝐏} {j(\dnp)\not=j(\dnpo)} \\
\end{array}
$$
Proof:
%:
%:
%:
%: [p∈j(\dnpo)]^1
%: -------------- ---------- ------------
%: \dnp⊆j(\dnpo) \dnpo⊆\dnp \dnp⊆j(\dnp) [j(\dnp)=j(\dnpo)]^1
%: -------------------- ---------------- -----------------------------------
%: j(\dnp)⊆(j∘j)(\dnpo) j(\dnpo)⊆j(\dnp) \dnp⊆j(\dnp)=j(\dnpo)
%: ---------------------------------------- ---------------------
%: j(\dnp)⊆(j∘j)(\dnpo)=j(\dnpo)⊆j(\dnp) \dnp⊆j(\dnpo)
%: ------------------------------------- -------------
%: j(\dnp)=j(\dnpo) p∈j(\dnpo)
%: ----------------------------------------------------------1
%: (p∈j(\dnpo))↔(j(\dnp)=j(\dnpo))
%: ---------------------------------------
%: (p\not∈j(\dnpo))↔(j(\dnp)\not=j(\dnpo))
%: ---------------------------------------
%: p∈X_j↔p∈X'_j
%:
%: ^lemma
%:
%:
\pu
%
% (lindp 50 "B.6")
% (linda "B.6")
%
$$\ded{lemma}$$
The formula of $X'_j$ above is the one that I asked if it was correct;
Bert answered that yes, and showed that it is equivalent to the
slighty shorter formula for $X_j$.
%L write_dnt_file()
\pu
\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% _ _
% / \ _ ____ _(_)_ __
% / _ \ | '__\ \/ / \ \ / /
% / ___ \| | > <| |\ V /
% /_/ \_\_| /_/\_\_| \_/
%
% «arxiv» (to ".arxiv")
% (find-LATEX "2020favorite-conventions.tex" "make-for-arxiv")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
#export PATH=/usr/local/texlive/2016/bin/x86_64-linux:$PATH
export PATH=/usr/local/texlive/2019/bin/x86_64-linux:$PATH
#export PATH=/usr/local/bin:$PATH
which biber
biber --version
make -f 2019.mk STEM=2021lindenhovius-j-to-X veryclean
lualatex 2021lindenhovius-j-to-X.tex
biber 2021lindenhovius-j-to-X
pdflatex -record 2021lindenhovius-j-to-X.tex
# (find-LATEXfile "2021lindenhovius-j-to-X.fls" "biblatex/")
cd ~/LATEX/
flsfiles-zip 2021lindenhovius-j-to-X.fls 2021lindenhovius-j-to-X.zip
rm -rfv /tmp/2021lindenhovius-j-to-X.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/2021lindenhovius-j-to-X.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2021lindenhovius-j-to-X.zip
cd /tmp/edrx-latex/
pdflatex 2021lindenhovius-j-to-X.tex
pdflatex 2021lindenhovius-j-to-X.tex
cp -v 2021lindenhovius-j-to-X.pdf /tmp/
# (find-fline "/tmp/edrx-latex/")
# (find-fline "/tmp/edrx-latex/2021lindenhovius-j-to-X.bbl" "bbl format version")
# (find-pdf-page "/tmp/edrx-latex/2021lindenhovius-j-to-X.pdf")
# (find-pdf-text "/tmp/edrx-latex/2021lindenhovius-j-to-X.pdf")
# (find-fline "/tmp/2021lindenhovius-j-to-X.zip")
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021lindenhovius-j-to-X veryclean
make -f 2019.mk STEM=2021lindenhovius-j-to-X pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "linf"
% End: