% (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:
