|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2021lindenhovius-june.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021lindenhovius-june.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2021lindenhovius-june.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2021lindenhovius-june.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021lindenhovius-june.pdf"))
% (defun e () (interactive) (find-LATEX "2021lindenhovius-june.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021lindenhovius-june"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2021lindenhovius-june.pdf"))
% (code-eec-LATEX "2021lindenhovius-june")
% (find-pdf-page "~/LATEX/2021lindenhovius-june.pdf")
% (find-sh0 "cp -v ~/LATEX/2021lindenhovius-june.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2021lindenhovius-june.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2021lindenhovius-june.pdf
% file:///tmp/2021lindenhovius-june.pdf
% file:///tmp/pen/2021lindenhovius-june.pdf
% http://angg.twu.net/LATEX/2021lindenhovius-june.pdf
% (find-LATEX "2019.mk")
% «.1» (to "1")
\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
%\printbibliography
% «1» (to ".1")
% (linjp 1 "1")
% (linja "1")
{\bf E-mail from Bert Lindenhovius, 2021jun30}
% https://mail.google.com/mail/ca/u/0/#inbox/QgrcJHrtvWmlxhvCBggGFXMszBggGkmQmdv
\def\Downs{\mathsf{D}}
\def\singp{\{p\}}
\def\setofsc#1#2{\{\,#1\;:\;#2\,\}}
\def\nuc {(·)^*}
\def\Nucs {\mathsf{Nucs}}
\def\GrTops{\mathsf{GrTops}}
\def\dno {{↓}^\circ}
\def\dnu {{↓}u}
\def\dnus {(\dnu)^*}
\def\dnou {\dno u}
\def\dnous {(\dnou)^*}
\def\dnouss{(\dnou)^{**}}
I think you are correct, but I think the expression can be simplified:
$X_j= \setofsc{p\in P}{p\notin j({↓}p∖\singp)}$.
Reason: by (iii) of Definition B.6, it follows that $j$ is monotone.
Now $p$ in $j({↓}p∖\singp)$ implies ${↓}p⊆ j({↓}p∖\singp)$ and by (ii)
of Def. B.6, we obtain $j({↓}p)⊆ (j∘j)({↓}p∖\singp))=j({↓}p∖\singp)⊆
j({↓}p)$ (last inclusion because $j$ is monotone). Conversely, if
$j({↓}p∖\singp)=j({↓}p)$, then by (i) of Def. B.6 we have ${↓}p⊆
j({↓}p)=j({↓}p∖\singp)$, hence $p$ in $j({↓}p∖\singp)$ if and only if
$j({↓}p∖\singp)=j({↓}p)$.
%:
%:
%: [p∈j({↓}p∖\singp)]^1
%: ------------------- ------------------
%: {↓}p⊆j({↓}p∖\singp) j\;\text{monotone} [j({↓}p)=j({↓}p∖\singp)]^1
%: ----------------------- ---------------------- ---------------------------B.6.(i)
%: {↓}p⊆(j∘j)({↓}p∖\singp) j({↓}p∖\singp)⊆j({↓}p) {↓}p⊆j({↓}p)=j({↓}p∖\singp)
%: -------------------------------------------------- ---------------------------
%: j({↓}p)⊆(j∘j)({↓}p∖\singp))=j({↓}p∖\singp)⊆j({↓}p) {↓}p⊆j({↓}p∖\singp)
%: -------------------------------------------------- -------------------
%: j({↓}p)=j({↓}p∖\singp) p∈j({↓}p∖\singp)
%: ----------------------------------------------------------------------1
%: (p∈j({↓}p∖\singp))↔(j({↓}p)=j({↓}p∖\singp))
%:
%: ^reason
%:
%:
%:
%:
%: [u∈\dnous]^1
%: ----------- ----------
%: \dnu⊆\dnous \dnou⊂\dnu [\dnus=\dnous]^1
%: ------------ ------------ m -----------------B.6.(i)
%: \dnu⊆\dnouss \dnous⊂\dnus \dnu⊆\dnus=\dnous
%: ----------------------------- -----------------
%: \dnus⊆\dnouss=\dnous⊂\dnus \dnu⊆\dnous
%: ----------------------------- -----------
%: \dnus=\dnous u∈\dnous
%: -----------------------------------------1
%: (u∈\dnous)↔(\dnus=\dnous)
%:
%: ^reason2
%:
%:
\pu
%
% (lindp 50 "B.6")
% (linda "B.6")
%
$$\ded{reason}$$
\bsk
In my notation...
%
$$\ded{reason2}$$
% (lindp 12 "2.9")
% (linda "2.9")
\newpage
In order to show that the expression for $X_j$ is correct, I find it
easiest is to start with the subset $X_J$ associated by a Grothendieck
topology $J$ on $P$, which by Lemma 2.9 is given by all $p$ in $P$
such that $J(p)={{↓}p}$.
By Theorem B.25, to any nucleus $j$, we can associate at Grothendieck
topology $J_j$ by $J_j(p) = \setofsc{S \in \Downs({↓}p)}{p \in j(S)}$
Hence, to $j$ we can associate the subset $X_{J_j}$ of $P$ consisting
of all $p$ such that $J_j(p)=\{{↓}p\}$, i.e., all $p$ such that ${↓}p$
is the only downset $S$ of ${↓}p$ with $p$ in $j(S)$. Then
$X_{J_j}=X_j$ as defined above, which can be seen as follows.
%
$$\begin{array}{lcr}
J_j(p) &=& \setofsc{S∈\Downs({↓}p)}{p∈j(S)} \\
X_J &=& \setofsc {p∈P} {J(p)=\{{↓}p\}} \\
X_{J_j} &=& \setofsc {p∈P} {\setofsc{S∈\Downs({↓}p)}{p∈j(S)}=\{{↓}p\}} \\
&=& \setofsc {p∈P} {∀S∈\Downs({↓}p). (p∈j(S))↔(S={↓}p)} \\
(p∈X_{J_j}) &=& ∀S∈\Downs({↓}p). (p∈j(S))↔(S={↓}p) \\
\\
X_j &=& \setofsc{p∈P}{p\not∈j({↓}p∖\singp)} \\
(p∈X_j) &=& p\not∈j({↓}p∖\singp) \\
\end{array}
$$
Let $p$ in $X_{J_j}$. Let ${↓}p∖\singp$. Since ${↓}p$ is the only
downset $S$ of ${↓}p$ with $p$ in $j(S)$, we cannot have $p$ in
$j({↓}p∖\singp)$, so $p\in X_j$.
%:
%:
%: p∈X_{J_j}
%: ---------------------------------
%: {↓}p∖\singp∈\Downs({↓}p) ∀S∈\Downs({↓}p).(p∈j(S))↔(S={↓}p)
%: ------------------------------------------------------------
%: (p∈j({↓}p∖\singp))↔({↓}p∖\singp={↓}p)
%: -------------------------------------
%: (p\not∈j({↓}p∖\singp))↔({↓}p∖\singp\not={↓}p)
%: -------------------------------
%: p\not∈j({↓}p∖\singp)
%: --------------------
%: p∈X_j
%:
%: ^foo
%:
\pu
$$\ded{foo}$$
\newpage
Conversely, if $p$ in $X_j$, let $S$ in $\Downs({↓}p)$ such that
$S\neq {↓}p$. Then we must have that $p\notin S$, hence $S⊆
{↓}p∖\singp$, hence $j(S)⊆ j({↓}p∖\singp)$, and since $j({↓}p∖\singp)$
does not contain, neither does $j(S)$. We conclude that ${↓}p$ is the
only downset $S$ of ${↓}p$ such that $p$ in $j(S)$, whence $p$ in
$X_j$.
Best,
Bert
\def\H#1{\hspace{#1cm}}
%:
%:
%: [S∈\Downs({↓}p)]^2
%: ------------------
%: S⊂{↓}p [S\neq{↓}p]^1 [S∈\Downs({↓}p)]^2
%: ------------------------------- --------------
%: p\not∈S S⊂{↓}p
%: -------------------------------------
%: S⊂{↓}p∖\{p\} p∈X_j
%: ------------------ -------------------
%: j(S)⊂j({↓}p∖\{p\}) \H{-1} p\not∈j({↓}p∖\{p\})
%: ----------------------------------------------------
%: p\not∈j(S)
%: ------------------------
%: (S\neq{↓}p)→(p\not∈j(S))
%: ------------------------ =================
%: (p∈j(S))→(S={↓}p) \H{-1} (S={↓}p)→(p∈j(S))
%: -----------------------------------------------------
%: (p∈j(S))↔(S={↓}p)
%: ---------------------------------2
%: ∀S∈\Downs({↓}p).(p∈j(S))↔(S={↓}p)
%: ---------------------------------
%: p∈X_{J_j}
%:
%: ^foo
%:
\pu
$$\ded{foo}$$
\newpage
Garbage:
$$\begin{array}{lcr}
X_J &=& \setofsc {p∈P} {J(p)=\{{↓}p\}} \\
(J↦X)(J) &=& \setofsc {p∈P} {J(p)=\{{↓}p\}} \\
(J↦X) &=& λJ.\setofsc {p∈P} {J(p)=\{{↓}p\}} \\
(J↦𝓨) &=& λJ∈\GrTops(𝐃).\setofst {u∈𝐃} {J(u)=\{{↓}u\}} \\
𝓨 &=& \setofst {u∈𝐃} {J(u)=\{{↓}u\}} \\
\end{array}
$$
$$\begin{array}{lcr}
J_j(p) &=& \setofsc{S∈\Downs({↓}p)}{p∈j(S)} \\
(j↦J)(j)(p) &=& \setofsc{S∈\Downs({↓}p)}{p∈j(S)} \\
(j↦J) &=& λj.λp.\setofsc{S∈\Downs({↓}p)}{p∈j(S)} \\
(\nuc↦J) &=& λ\nuc∈\Nucs(...).λu∈𝐃.\setofst{𝓢∈Ω(u)}{u∈𝓢^*} \\
J &=& λu∈𝐃.\setofst{𝓢∈Ω(u)}{u∈𝓢^*} \\
J(u) &=& \setofst{𝓢∈Ω(u)}{u∈𝓢^*} \\
\\
𝓨 &=& \setofst {u∈𝐃} {J(u)=\{{↓}u\}} \\
&=& \setofst {u∈𝐃} {\setofst{𝓢∈Ω(u)}{u∈𝓢^*}=\{{↓}u\}} \\
&=& \setofst {u∈𝐃} {∀𝓢∈Ω(u). (u∈𝓢^*)↔(𝓢={↓}u)} \\
\end{array}
$$
\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=2021lindenhovius-june veryclean
make -f 2019.mk STEM=2021lindenhovius-june pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "linj"
% End: