% (find-LATEX "2020groth-tops.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020groth-tops.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2020groth-tops.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2020groth-tops.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020groth-tops.pdf"))
% (defun e () (interactive) (find-LATEX "2020groth-tops.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020groth-tops"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2020groth-tops.pdf"))
% (find-pdf-page   "~/LATEX/2020groth-tops.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020groth-tops.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020groth-tops.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020groth-tops.pdf
%               file:///tmp/2020groth-tops.pdf
%           file:///tmp/pen/2020groth-tops.pdf
% http://angg.twu.net/LATEX/2020groth-tops.pdf
% (find-LATEX "2019.mk")

% «.newnode-at»		(to "newnode-at")
% «.sieves-MM-diagrams»	(to "sieves-MM-diagrams")
% «.grotop-Jcan»	(to "grotop-Jcan")
% «.grotop-J»		(to "grotop-J")
% «.grotop-on-C»	(to "grotop-on-C")
% «.big-J-to-small-j»	(to "big-J-to-small-j")
% «.small-j-to-big-J»	(to "small-j-to-big-J")
% «.embedding»		(to "embedding")
% «.nuclei»		(to "nuclei")
% «.nuclei-my»		(to "nuclei-my")
% «.partial-order»	(to "partial-order")
% «.archetypal»		(to "archetypal")

\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")
%
\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 dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu


\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}
\long\def\ColorBrown #1{{\color{Brown}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}
\long\def\ColorOrange#1{{\color{orange}#1}}

\def\calS{\mathcal{S}}
\def\covers{\text{ covers }}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\Sieveson{\mathsf{Sieves\_on}}
\def\Coveringsieveson{\mathsf{Covering\_sieves\_on}}
\def\Coveringsieveson{\mathsf{Covsieves\_on}}
\def\can{{\mathrm{can}}}
\def\Jcan{{J_\mathrm{can}}}
\def\Grotop{{\mathsf{Gro\_top}}}
\def\SetCop{\Set^{\catC^\op}}

\def\hasmax{\mathsf{hasmax}}
\def\trans {\mathsf{trans}}
\def\stab  {\mathsf{stab}}

% «newnode-at»  (to ".newnode-at")
% (find-es "dednat" "at:")
%
%L Node = Class {
%L   type       = "Node",
%L   __tostring = function (node) return mytostring(node) end,
%L   __index    = {
%L     v    = function (node) return v(node.x,node.y) end,
%L     setv = function (node,v) node.x=v[1]; node.y=v[2]; return node end,
%L   },
%L }
%L storenode = function (node)
%L     node = Node(node)
%L     table.insert(nodes, node)
%L     node.noden = #nodes         -- nodes[node.noden] == node
%L     if node.tag then            -- was: "and not nodes[node.tag]"...
%L       nodes[node.tag] = node    -- nodes[node.tag] == node
%L     end
%L     return node
%L   end
%L 
%L tow = function (vv, ww, a, b)
%L     local diff = ww-vv
%L     local diffrot90 = v(diff[2], -diff[1])
%L     return vv + (a or 0.5)*diff + (b or 0)*diffrot90
%L   end
%L ats_to_vs = function (str)
%L     return (str:gsub("@(%w+)", "nodes[\"%1\"]:v()"))
%L   end
%L forths["newnode:"] = function ()
%L     local tag = getword()
%L     ds:push(storenode({tag=tag, TeX=phantomnode}))
%L   end
%L forths["at:"] = function ()
%L     local node = ds:pick(0)
%L     local vexpr = getword()
%L     node:setv(expr(ats_to_vs(vexpr)))
%L   end



%  ____  _                       __  __ __  __ 
% / ___|(_) _____   _____  ___  |  \/  |  \/  |
% \___ \| |/ _ \ \ / / _ \/ __| | |\/| | |\/| |
%  ___) | |  __/\ V /  __/\__ \ | |  | | |  | |
% |____/|_|\___| \_/ \___||___/ |_|  |_|_|  |_|
%                                              
% «sieves-MM-diagrams»  (to ".sieves-MM-diagrams")
% (grtp 1 "sieves-MM-diagrams")
% (grt    "sieves-MM-diagrams")

Sieves on a category $\catC$:

(See \cite[pages 38, 109]{MacLaneMoerdijk})
%
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11  38) "Sieve on C =")
% (find-maclanemoerdijkpage (+ 11 109) "Definition 1. A Grothendieck Topology")
%
%D diagram sieves-MM1-so
%D 2Dx     100 +13
%D 2D  100 B   C
%D 2D
%D 2D  +13 A
%D 2D
%D (( A B -> .plabel= l g
%D    B C -> .plabel= a f
%D
%D ))
%D enddiagram
%D
%D diagram sieves-MM1-3
%D 2Dx     100  +40 +65 +50  +20
%D 2D  100 A0 - A1  C0       D1
%D 2D      |     |  |         |
%D 2D  +20 A2 - A3  C1  D2 - D3
%D 2D
%D 2D  +10 B0'
%D 2D  +7  B0 - B1
%D 2D
%D ren A0 A1 C0 ==> C \Sieveson(C) S
%D ren A2 A3 C1 ==> D \Sieveson(D) h^*(S):=
%D ren B0'      ==> \catC\phantom{{}^\op}
%D ren B0    B1 ==> \catC^\op \Set
%D ren D2 D3 D1 ==> B D C
%D
%D (( A0 A1 |->
%D    A0 A2 <- .plabel= l h
%D    A1 A3 -> .plabel= r h^*
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    B0' place
%D    B0 B1  -> .plabel= a \Sieveson
%D    C0 C1 |->
%D
%D    newnode: C1' at: @C1+v(0,8)
%D      .TeX= \setofst{m}{\cod(m)=D,\;h∘m∈S} place
%D
%D    D2 D3 -> .plabel= a m
%D    D3 D1 -> .plabel= r h
%D ))
%D enddiagram
%D
$$\pu
  \begin{array}{c}
    \begin{array}{rcl}
             t_C &:=& \setofst{f}{\cod(f)=C} \\
    \Sieveson(C) &:=& \setofst{S⊆t_C}{
                        ∀\scalebox{0.75}{$
                         \pdiag{sieves-MM1-so}
                         $}.\psm{f∈S \\↓\\ f∘g∈S}
                       } \\
    \end{array}
    \\
    \\
    \diag{sieves-MM1-3} \\
  \end{array}
$$

\bsk
\bsk

Sieves on a topological space $\Opens(X)$:

(See \cite[page 70]{MacLaneMoerdijk})
%
% (find-maclanemoerdijkpage (+ 11  69) "2. Sieves and Sheaves")
% (find-maclanemoerdijkpage (+ 11  70) "a sieve S on U")
%
%D diagram sieves-MMT-3
%D 2Dx     100  +45 +60 +45  +20
%D 2D  100 A0 - A1  C0       D1
%D 2D      |     |  |         |
%D 2D  +20 A2 - A3  C1  D2 - D3
%D 2D
%D 2D  +10 B0'
%D 2D  +7  B0 - B1
%D 2D
%D ren A0 A1 C0 ==> U \Sieveson(U) \calS
%D ren A2 A3 C1 ==> V \Sieveson(V) (V⊆U)^*(\calS):=
%D ren B0'      ==> \Opens(X)\phantom{{}^\op}
%D ren B0    B1 ==> \Opens(X)^\op \Set
%D ren D2 D3 D1 ==> W V U
%D
%D (( A0 A1 |->
%D    A0 A2 <- .plabel= l  V⊆U
%D    A1 A3 -> .plabel= r (V⊆U)^*
%D    A0 A3 harrownodes nil 20 nil |->
%D    A2 A3 |->
%D    B0' place
%D    B0 B1  -> .plabel= a \Sieveson
%D    C0 C1 |->
%D
%D    newnode: C1' at: @C1+v(0,13)
%D      .TeX= \hstarSdef place
%D
%D    D2 D3 -> .plabel= a W⊆V
%D    D3 D1 -> .plabel= r V⊆U
%D ))
%D enddiagram
%D
$$\pu
  \def\seup{\rotatebox{90}{$\scriptstyle ⊆$}}
  \def\hstarSdef{
      \begin{array}{c}
        \setofst{W∈\Opens(V)}{W∈\calS} \\
        =\calS∩\Opens(V) \\
      \end{array}
    }
  \begin{array}{c}
    \begin{array}{rcl}
             t_U &:=& \setofst{V⊆\Opens(X)}{V⊆U} \\
                  &=& \Opens(U) \\
    \Sieveson(U) &:=& \setofst{\calS⊆t_U}{
                        ∀\psm{V&⊆&U\\\seup\\W}.
                         \psm{V∈S \\↓\\ W∈\calS}
                       } \\
                  &=& \calD(t_U) \\
                  &=& \calD(\Opens(U)) \\
    \end{array}
    \\
    \\
    \diag{sieves-MMT-3} \\
  \end{array}
$$




\newpage

%   ____           _                    _                   
%  / ___|_ __ ___ | |_ ___  _ __       | |   ___ __ _ _ __  
% | |  _| '__/ _ \| __/ _ \| '_ \   _  | |  / __/ _` | '_ \ 
% | |_| | | | (_) | || (_) | |_) | | |_| | | (_| (_| | | | |
%  \____|_|  \___/ \__\___/| .__/   \___/   \___\__,_|_| |_|
%                          |_|                              
%
% «grotop-Jcan»  (to ".grotop-Jcan")

Motivating case:

Start with the case $\Sieveson: \Opens(X)^\op \to \Set$.

A ``sieve on $U$'' is an element $\calS∈\Sieveson(U)$.

We say that a sieve $\calU$ on $U$ ``covers $U$'' iff $\bigcup \calU = U$.

Let $\Jcan(U) := \setofst{\calU∈\Sieveson(U)}{\bigcup \calU = U}$.

This $\Jcan$ is a subfunctor of $\Sieveson: \Opens(X)^\op \to \Set$...

Its action on morphisms is a restriction of the one in $\Sieveson$;

we can define it as $\Jcan(V⊆U)(\calU) := \calU∩\Opens(V)$.

This $\Jcan$ obeys these three properties:

\msk

$\begin{array}{rcl}
  \hasmax_\Jcan &:=& (∀U∈\Opens(X).\Opens(U)∈\Jcan(U)) \\
  \trans_\Jcan  &:=& (∀V⊆U.∀\calU∈\Jcan(U).(V⊆U)^*(\calU)∈\Jcan(V)) \\
  \stab_\Jcan   &:=& \pmat{
                      ∀U.∀\calU∈\Jcan(U).∀\calS∈\Sieveson(U). \\
                      (∀V∈\calU.((V⊆U)^*(\calS)∈\Jcan(V)))→(\calS∈\Jcan(U))
                     } \\
  \end{array}
$

\msk

We will define ``Grotopness'' as their conjunction:
%
$$\Grotop_\Jcan := \hasmax_\Jcan ∧ \trans_\Jcan ∧ \stab_\Jcan$$

And we will draw $\Grotop_\Jcan$ in this way:

%D diagram groth-top-usual
%D 2Dx     100 +35 +60
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  U                     (\Opens(U)∈\Jcan(U))
%D ren B1    B3 ==>  U                     (\calU∈\Jcan(U))
%D ren C1    C3 ==>  V                     (\calU∩\Opens(V)∈\Jcan(V))
%D ren D1 D2 D3 ==>  U \calS                    (\calS∈\Jcan(U))
%D ren E1 E2 E3 ==> ∀V \calS∩\Opens(V) (∀V{∈}\,\calU.\,\calS∩\Opens(V)∈\Jcan(V))
%D
%D (( A1 place A3 place
%D    C1 B1 ->
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= \calU place
%D    newnode: E1' at: @D1+v(7,9)  .TeX= \rotatebox{60}{$\in$} place
%D    E1 D1 ->
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{groth-top-usual}
$$

It turns out that $\Grotop_\Jcan$ is true.

\msk

We will generalize this to:

A {\sl Grothendieck topology on $\Opens(X)$} is any operation $J$

that takes each $U∈\Opens(X)$ to a subset $J(U) ⊆ \Sieveson(U)$

that obeys $\Grotop_J$.

The property $\trans_J$ will guarantee that this $J$

is a subfunctor of $\Sieveson: \Opens(X)^\op \to \Set$.



\newpage

%   ____           _                    _ 
%  / ___|_ __ ___ | |_ ___  _ __       | |
% | |  _| '__/ _ \| __/ _ \| '_ \   _  | |
% | |_| | | | (_) | || (_) | |_) | | |_| |
%  \____|_|  \___/ \__\___/| .__/   \___/ 
%                          |_|            
%
% «grotop-J»  (to ".grotop-J")
% (grtp 3 "grotop-J")
% (grt    "grotop-J")

First generalization...

Start with the case $\Sieveson: \Opens(X)^\op \to \Set$.

Let $J$ be an operation that takes

each $U∈\Opens(X)$ to a subset $J(U)⊆\Sieveson(U)$.

Define $\hasmax_J$, $\trans_J$, $\stab_J$ as:

\msk

$\begin{array}{rcl}
  \hasmax_J &:=& (∀U∈\Opens(X).\Opens(U)∈J(U)) \\
  \trans_J  &:=& (∀V⊆U.∀\calU∈J(U).(V⊆U)^*(\calU)∈J(V)) \\
  \stab_J   &:=& \pmat{
                      ∀U.∀\calU∈J(U).∀\calS∈\Sieveson(U). \\
                      (∀V∈\calU.((V⊆U)^*(\calS)∈J(V)))→(\calS∈J(U))
                     } \\
  \end{array}
$

\msk

We will define $\Grotop_J$ as their conjunction:
%
$$\Grotop_J := \hasmax_J ∧ \trans_J ∧ \stab_J$$

and we will say that this $J$ is a Grothendieck topology on $\Opens(X)$

iff $\Grotop_J$ is true.

\msk

We will draw $\Grotop_J$ in this way:

%D diagram groth-top-on-O(X)
%D 2Dx     100 +35 +60
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  U                     (\Opens(U)∈J(U))
%D ren B1    B3 ==>  U                     (\calU∈J(U))
%D ren C1    C3 ==>  V                     (\calU∩\Opens(V)∈J(V))
%D ren D1 D2 D3 ==>  U \calS                    (\calS∈J(U))
%D ren E1 E2 E3 ==> ∀V \calS∩\Opens(V) (∀V{∈}\,\calU.\,\calS∩\Opens(V)∈J(V))
%D
%D (( A1 place A3 place
%D    C1 B1 ->
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= \calU place
%D    newnode: E1' at: @D1+v(7,9)  .TeX= \rotatebox{60}{$\in$} place
%D    E1 D1 ->
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{groth-top-on-O(X)}
$$



\newpage

%   ____           _                               ____ 
%  / ___|_ __ ___ | |_ ___  _ __     ___  _ __    / ___|
% | |  _| '__/ _ \| __/ _ \| '_ \   / _ \| '_ \  | |    
% | |_| | | | (_) | || (_) | |_) | | (_) | | | | | |___ 
%  \____|_|  \___/ \__\___/| .__/   \___/|_| |_|  \____|
%                          |_|                          
%
% «grotop-on-C»  (to ".grotop-on-C")

Second generalization:

Start with the case $\Sieveson: \catC^\op \to \Set$.

Let $J$ be an operation that takes

each $C∈\catC$ to a subset $J(C)⊆\Sieveson(C)$.

Define $\hasmax_J$, $\trans_J$, $\stab_J$ as:

\msk

$\begin{array}{rcl}
  \hasmax_J &:=& (∀C∈\catC.\;t_C∈J(C)) \\
  \trans_J  &:=& (∀(h:D→C).\,∀S∈J(C).\,h^*(S)∈J(D)) \\
  \stab_J   &:=& \pmat{
                      ∀C∈\catC.\,∀S∈J(C).\,∀R∈\Sieveson(C). \\
                      (∀(h:D→C)∈S.(h^*(R)∈J(D)))→(R∈J(C))
                     } \\
  \end{array}
$

\msk

We will define $\Grotop_J$ as their conjunction:
%
$$\Grotop_J := \hasmax_J ∧ \trans_J ∧ \stab_J$$

and we will say that this $J$ is a Grothendieck topology on $\catC$

iff $\Grotop_J$ is true.

\msk

We will draw $\Grotop_J$ in this way:

%D diagram groth-top-on-C
%D 2Dx     100 +35 +70
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  C                     (t_C∈J(C))
%D ren B1    B3 ==>  C                     (S∈J(C))
%D ren C1    C3 ==>  D                     (h^*(S)∈J(D))
%D ren D1 D2 D3 ==>  C R                   (R∈J(C))
%D ren E1 E2 E3 ==> ∀D h^*(R) (∀(h:D→C)∈S.\,h^*(R)∈J(D))
%D
%D (( A1 place A3 place
%D    C1 B1 -> .plabel= l h
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= S place
%D    newnode: E1' at: @D1+v(6,5)  .TeX= \rotatebox{38}{$\in$} place
%D    E1 D1  -> .plabel= l ∀h
%D    D2 E2 |->
%D    D3 E3  <-
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{groth-top-on-C}
$$

\msk

This is exactly the definition in \cite[page 109]{MacLaneMoerdijk} ---

I have just reorganized it in a more visual way.

% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11  38) "Sieve on C =")
% (find-maclanemoerdijkpage (+ 11 110) "Definition 1. A Grothendieck Topology")




\newpage

% «big-J-to-small-j»  (to ".big-J-to-small-j")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 222) "Theorem 2")

From \cite[page 222]{MacLaneMoerdijk}:

Theorem 2. Every Grothendieck topology $J$ on a small category $\catC$
determines a Lawvere-Tierney topology $j$ on the presheaf topos
$\SetCop$.

(...)
%
$$\begin{array}{rcl}
        j_C(S) &=& \setofst{g}{g^*(S) ∈ J(\dom(g))} \\
    j_U(\calS) &=& \setofst{V∈\Opens(U)}{(V⊆U)^*(\calS) ∈ J(V)} \\
               &=& \setofst{V∈\Opens(U)}{\calS∩\Opens(V) ∈ J(V)} \\
       (j_U)_0 &=& λ\calS∈\calD(\Opens(U)). \\
                && \;\;\;\; \setofst{V∈\Opens(U)}{\calS∩\Opens(V) ∈ J(V)} \\
  \end{array}
$$

\bsk

% «small-j-to-big-J»  (to ".small-j-to-big-J")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11 233) "V.4 Lawvere-Tierney Subsumes Grothendieck")

From \cite[page 233]{MacLaneMoerdijk}:

Theorem 1. If $\catC$ is a small category, the Grothendieck topologies
$J$ on $\catC$ correspond exactly to Lawvere-Tierney topologies on the
presheaf topos $\SetCop$.

(...)

Now any Lawvere-Tierney topology $j:Ω→Ω$ on $\SetCop$ classifies the
subobject $J \monicto Ω$ defined as in (1.2) by:
%
$$\begin{array}{rcl}
        S∈J(C) &\text{iff}& \quad j_C(S) = t_C \\
    \calS∈J(U) &\text{iff}& \quad j_U(\calS) = \Opens(U) \\
          J(U) &=& \setofst{\calS∈\calD(\Opens(U))}{j_U(\calS) = \Opens(U)} \\
           J_0 &=& λU∈\Opens(U).\;\setofst{\calS∈\calD(\Opens(U))}{j_U(\calS) = \Opens(U)} \\
  \end{array}
$$

\newpage

% «embedding»  (to ".embedding")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11 480) "IX.4. Embeddings and Surjections of Locales")
% (find-maclanemoerdijkpage (+   11 481)   "Definition 1")

From \cite[page 481]{MacLaneMoerdijk}:

Definition 1. A map $f:Y→X$ of locales is an embedding iff the
corresponding morphism of frames $f^{-1}: \Opens(X)→\Opens(Y)$ is
surjective.

Recall that for a map $f:Y→X$ of locales, the corresponding frame map
$f^{-1}:\Opens(X) → \Opens(Y)$, considered as a map of posets, has a
right adjoint $f_*: \Opens(Y)→\Opens(X)$ (Lemma 1.1). The unit and
counit of this adjunction between posets state that $U≤f_*f^{-1}U$ for
any $U∈\Opens(X)$, and that $f^{-1}f_*V≤V$. Moreover, the triangular
identities for the adjunction reduce to the equalities:
%
$$(...) \quad \text{and} \quad (...)$$

%D diagram ??
%D 2Dx     100 +25 +25  +50 +25 +25
%D 2D  100 A0' A0  B0 - B1  C0  C0'
%D 2D      |   |   |     |   |
%D 2D  +20 A1' A1  B2 - B3  C1  C1'
%D 2D    
%D 2D  +15         D0 = D1
%D 2D
%D 2D  +15         E0 - E1
%D 2D
%D ren A0' A0 B0 B1 C0 C0' ==> \Opens(Y) f^{-1}f_*V f^{-1}U U            U \Opens(X)
%D ren A1' A1 B2 B3 C1 C1' ==> \Opens(Y)          V   V    f_*V f_*f^{-1}U \Opens(X)
%D ren    D0 D1    ==>        \Opens(Y) \Opens(X)
%D ren    E0 E1    ==>               Y         X
%D
%D (( C1 .TeX= \mat{f_*f^{-1}U\\=jU}
%D    A0' A1' -> .plabel= l ε=\id
%D    A0  A1  -> .plabel= l ε_V=\id
%D    B0 B1 <-|
%D    B0 B2 ->
%D    B1 B3 ->
%D    B0 B3 harrownodes nil 20 nil <->
%D    B2 B3 |->
%D    C0  C1  -> .plabel= r η_U
%D    C0' C1' -> .plabel= r η=j
%D    D0 D1 <- sl^ .plabel= a f^{-1}
%D    D0 D1 -> sl_ .plabel= b f_*\;\text{(injective)}
%D    E0 E1 -> .plabel= a f
%D    E0 E1 -> .plabel= b \text{embedding}
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

For embeddings/inclusions $f:Y \ito X$ we have

$\Opens(Y) = \setofst{Y∩U}{U∈\Opens(X)}$

\bsk

Monad:
%
%D diagram ??
%D 2Dx     100  +30  +30
%D 2D  100 A0 - A1 - A2
%D 2D
%D 2D  +20 B0 - B1 - B2
%D 2D
%D ren A0 A1 A2 ==> U jU jjU
%D ren B0 B1 B2 ==> \Opens(X) \Opens(X) \Opens(X)
%D
%D (( A0 A1 -> .plabel= a η_U
%D    A1 A2 <- .plabel= a μ_U
%D    B0 B1 -> .plabel= a η
%D    B1 B2 <- .plabel= a μ
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

We can start from the monad, i.e., from $j$ obeying etcetcetc,

and build $(X_j,\Opens(X_j)) := (Y,\Opens(Y))$ as:

$X_j := X$, $\Opens(X_j) := \setofst{U∈\Opens(X)}{jU=U}$.




\newpage

% (jonp 3 "basic-definitions")
% (jos    "basic-definitions")

\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
\input 2019J-ops-defs.tex      % (find-LATEX "2019J-ops-defs.tex")

%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7}   -- with v arrows
%L tspec_PA  = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L tspec_PA :mp  ({zdef="O_A(P)"})  :addlrs():print()            :output()
%L tspec_PAQ:mp  ({zdef="O_A(P),J"}):addlrs():print()            :output()
%L tspec_PA :tcgq({tdef="(P,A)",   meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L tspec_PAC = TCGSpec.new("46; 11 22 34 45, 25", "?...", "???...")
%L tspec_PAC:mp  ({zdef="closed-op"}) :addlrs():print()            :output()
%L tspec_PAC:tcgq({tdef="closed-op", meta="1pt p"}, "lr q h v ap") :output()
%L 
\pu
%$$\tcg{(P,A)} \;\; \squigbij \;\;\; \zha{O_A(P)}$$
$$\tcg{(P,A),Q} \;\; \squigbij \;\;\; \zha{O_A(P),J}$$


%D diagram ??-1
%D 2Dx     100 +30
%D 2D  100     _6
%D 2D  +15     _5
%D 2D  +15 4_  _4
%D 2D  +15 3_  _3
%D 2D  +15 2_  _2
%D 2D  +15 1_  _1
%D 2D
%D ren 1_ 2_ 3_ 4_       ==> \ur11 \ur22 \ur34 \ur45
%D ren _1 _2 _3 _4 _5 _6 ==> \ul01 \ul02 \ul03 \ul04 \ul25 \ul26
%D
%D (( 4_ 3_ = # ->
%D    3_ 2_ ->
%D    2_ 1_ = # ->
%D
%D    _6 _5 ->
%D    _5 _4 ->
%D    _4 _3 ->
%D    _3 _2 = # ->
%D    _2 _1 = # ->
%D    
%D    4_ _5 = # ->
%D    3_ _4 ->
%D    2_ _2 ->
%D    1_ _1 ->
%D    
%D    2_ _5 <-
%D ))
%D enddiagram
%D
%D diagram ??-2
%D 2Dx     100 +30
%D 2D  100     _6
%D 2D  +15     _5
%D 2D  +15 4_  _4
%D 2D  +15 3_  _3
%D 2D  +15 2_  _2
%D 2D  +15 1_  _1
%D 2D
%D ren 1_ 2_ 3_ 4_       ==> \ur11 \ur22 \ur34 \ur45
%D ren _1 _2 _3 _4 _5 _6 ==> \ul01 \ul02 \ul03 \ul04 \ul25 \ul26
%D
%D (( 4_ 3_ = # ->
%D    3_ 2_ ->
%D    2_ 1_ = # ->
%D
%D    _6 _5 ->
%D    _5 _4 ->
%D    _4 _3 ->
%D    _3 _2 = # ->
%D    _2 _1 = # ->
%D    
%D    4_ _5 = # ->
%D  # 3_ _4 ->
%D  # 2_ _2 ->
%D    2_ _3 ->
%D  # 1_ _1 ->
%D    
%D  # 2_ _5 <-
%D ))
%D enddiagram
%D
%D diagram ??-3
%D 2Dx     100 +30
%D 2D  100     _6
%D 2D  +15     _5
%D 2D  +15 4_  _4
%D 2D  +15 3_  _3
%D 2D  +15 2_  _2
%D 2D  +15 1_  _1
%D 2D
%D ren 1_ 2_ 3_ 4_       ==> 1▁ 2▁ 3▁ 4▁
%D ren _1 _2 _3 _4 _5 _6 ==> ▁1 ▁2 ▁3 ▁4 ▁5 ▁6
%D ren 1_ 2_ 3_ 4_       ==> \ur11 \ur22y \ur34 \ur45y
%D ren _1 _2 _3 _4 _5 _6 ==> \ul01 \ul02 \ul03y \ul04y \ul25 \ul26y
%D
%D (( 4_ 3_ = # ->
%D    3_ 2_ ->
%D    2_ 1_ = # ->
%D
%D    _6 _5 ->
%D    _5 _4 ->
%D    _4 _3 ->
%D    _3 _2 = # ->
%D    _2 _1 = # ->
%D    
%D    4_ _5 = # ->
%D  # 3_ _4 ->
%D  # 2_ _2 ->
%D    2_ _3 ->
%D  # 1_ _1 ->
%D    
%D  # 2_ _5 <-
%D ))
%D enddiagram
%D
$$\pu
  \def\ur#1#2{#1\underline{#2}}
  \def\ul#1#2{\underline{#1}#2}
  \diag{??-1}
  \qquad
  \diag{??-2}
  \qquad
  \diag{??-3}
$$



\newpage

% «nuclei»  (to ".nuclei")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11 470) "IX. Localic Topoi")
% (find-maclanemoerdijkpage (+   11 480)   "IX.4. Embeddings and Surjections of Locales")
% (find-maclanemoerdijkpage (+   11 483)     "nucleus")

From \cite[page 483]{MacLaneMoerdijk}:

An operator $j: \Opens(X) → \Opens(X)$ satisfying the identities (2),
(3'), (4) is called a {\sl nucleus} on the locale $X$. This nucleus
determines the domain locale $Y$. Indeed, as stated at the start of of
this paragraph, if $f:X→Y$ is an embedding of locales, then
$\Opens(Y)$ is isomorphic to the set of fixed points
$\setofst{U∈\Opens(X)}{jU=U}$ of the nucleus $j=f_*f^{-1}$. The
converse of this observation also holds:

\msk

Proposition 3: Let $j:\Opens(X)→\Opens(X)$ be a nucleus on a locale
$X$. Then the poset of $j$-fixed points $\setofst{U∈\Opens(X)}{jU=U}$
is a frame, and $j$ defines a surjective frame-morphism from
$\Opens(X)$ into this frame of fixed points.

\msk

The locale corresponding to this frame of fixed points
$\setofst{U∈\Opens(X)}{jU=U}$ is usually denoted by $X_j$ --- so the
corresponding frame is:
%
$$\Opens(X_j) = \setofst{U∈\Opens(X)}{jU=U}.$$

\bsk


% «nuclei-my»  (to ".nuclei-my")

An operator $J: H→H$ satisfying the identities $P≤P^*$, $P^* =
P^{**}$, $(P∧Q)^* = P^*∧Q^*$ is called a {\sl nucleus} on the locale
$H$. This nucleus determines the domain locale $Y$. Indeed, as stated
at the start of of this paragraph, if $f:X→Y$ is an embedding of
locales, then $\Opens(Y)$ is isomorphic to the set of fixed points
$\setofst{U∈\Opens(X)}{jU=U}$ of the nucleus $j=f_*f^{-1}$. The
converse of this observation also holds:

\msk

Proposition 3: Let $j:\Opens(X)→\Opens(X)$ be a nucleus on a locale
$X$. Then the poset of $j$-fixed points $\setofst{U∈\Opens(X)}{jU=U}$
is a frame, and $j$ defines a surjective frame-morphism from
$\Opens(X)$ into this frame of fixed points.

\msk

The locale corresponding to this frame of fixed points
$\setofst{U∈\Opens(X)}{jU=U}$ is usually denoted by $X_j$ --- so the
corresponding frame is:
%
$$\Opens(X_j) = \setofst{U∈\Opens(X)}{jU=U}.$$






\newpage

% «partial-order»  (to ".partial-order")


{

\def\P{P}
\def\Q{Q}

Let $𝐛P≡(\P,≤)$ be a partial order.

``$D$ is a down-set of $\P$'' means: $D⊆\P$ and

$∀p_1,p_2∈\P.(p_1≤p_2)→(p_2∈D→p_1∈D)$.

$\calD(𝐛P) := \setofst{D⊆\P}{D \text{ is a down-set of } 𝐛P}$.

Note that $\calD(𝐛P) ⊆ \Pts(\P)$.

\msk

Let $𝐛Q≡(\Q,≤,⊤,∧)$ be a partial order

with maximal element $⊤$ and binary meet operation $∧$.

``$U$ is an up-set of $𝐛Q$'' means $U⊆\Q$ and

$∀q_1,q_2∈\Q.(q_1≤q_2)→(q_1∈U→q_2∈U)$.

``$U$ is closed by binary meets'' means

$∀q_1,q_2∈\Q.(q_1∈U∧q_2∈U)→(q_1∧q_2∈U)$.

``$U$ is a filter in $𝐛Q$'' means:

$U$ is an up-set of $𝐛Q$ closed by binary meets, with $⊤∈U$.

$\calU(𝐛Q) := \setofst{U⊆\Q}{U \text{ is a up-set of } 𝐛Q}$.

$\calF(𝐛Q) := \setofst{U⊆\Q}{U \text{ is a filter on } 𝐛Q}$.

Note that $\calU(𝐛Q), \calF(𝐛Q) ⊆ \Pts(\Q)$.

}

\newpage

% «archetypal»  (to ".archetypal")
% (grtp 2 "archetypal")
% (grt     "archetypal")

Archetypal case:

$(X,\Opens(X))$ is a topological space.

$\Opens(X) ≡ (\Opens(X),⊆)$ is a partial order.

$\Opens(U) ≡ (\Opens(U),⊆)$ is a partial order for any $U∈\Opens(X)$.

``$\calS$ is a sieve on $U$'' means $\calS∈\calD(\Opens(U))$.

``$\calU$ is a covering sieve on $U$'' means $\calU∈\calD(\Opens(U))$
and $\bigcup \calU = U$.

$\Sieveson(U) := \setofst{\calS}{\text{$\calS$ is a sieve on $U$}}$

$\Sieveson(V⊆U)(\calS) := (V⊆U)^*(\calS) := \calS∩\Opens(V)$

$\Coveringsieveson(U) := \setofst{\calU}{\text{$\calU$ is a covering sieve on $U$}}$

$\Coveringsieveson(V⊆U)(\calU) := (V⊆U)^*(\calU) := \calU∩\Opens(V)$

$\Jcan(U) := \Coveringsieveson(U)$

$\Jcan(V⊆U)(\calU) := (V⊆U)^*(\calU) := \calU∩\Opens(V)$

$\hasmax_\Jcan := (∀U∈\Opens(X).\Opens(U)∈\Jcan(U))$

$\trans_\Jcan := (∀V⊆U.∀\calU∈\Jcan(U).(V⊆U)^*(\calU)∈\Jcan(V))$

$\stab_\Jcan := \pmat{
   ∀U.∀\calU∈\Jcan(U).∀\calS∈\Sieveson(U). \\
   (∀V∈\calU.((V⊆U)^*(\calS)∈\Jcan(V)))→(\calS∈\Jcan(U))
   }$

$\Grotop_\Jcan := \hasmax_\Jcan ∧ \trans_\Jcan ∧ \stab_\Jcan$

$\Grotop_\Jcan$ is true.

\newpage

Grotopness (on topological spaces):

$(X,\Opens(X))$ is a topological space.

$\Opens(X) ≡ (\Opens(X),⊆)$ is a partial order.

$\Opens(U) ≡ (\Opens(U),⊆)$ is a partial order for any $U∈\Opens(X)$.

``$\calS$ is a sieve on $U$'' means $\calS∈\calD(\Opens(U))$.

\ColorGray{
``$\calU$ is a covering sieve on $U$'' means $\calU∈\calD(\Opens(U))$
and $\bigcup \calU = U$.
}

$\Sieveson(U) := \setofst{\calS}{\text{$\calS$ is a sieve on $U$}}$

$\Sieveson(V⊆U)(\calS) := (V⊆U)^*(\calS) := \calS∩\Opens(V)$

\ColorGray{
$\Coveringsieveson(U) := \setofst{\calU}{\text{$\calU$ is a covering sieve on $U$}}$

$\Coveringsieveson(V⊆U)(\calU) := (V⊆U)^*(\calU) := \calU∩\Opens(V)$
}

$J(U) ⊆ \Sieveson(U)$

$J(V⊆U)(\calU) := (V⊆U)^*(\calU) := \calU∩\Opens(V)$

$\hasmax_J := (∀U∈\Opens(X).\Opens(U)∈J(U))$

$\trans_J := (∀V⊆U.∀\calU∈J(U).(V⊆U)^*(\calU)∈J(V))$

$\stab_J := \pmat{
   ∀U.∀\calU∈J(U).∀\calS∈\Sieveson(U). \\
   (∀V∈\calU.((V⊆U)^*(\calS)∈J(V)))→(\calS∈J(U))
   }$

$\Grotop_J := \hasmax_J ∧ \trans_J ∧ \stab_J$


\msk

A Grothendieck topology $J$ on $\Opens(X)$

is a subfunctor $J:\Opens(X)^\op→\Set$

of $\Sieveson:\Opens(X)^\op→\Set$

that obeys $\Grotop_J$.




\newpage


From Lindenhovius, p.8., with a different notation:
%
% (find-books "__cats/__cats.el" "lindenhovius-gtop")
%


%
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+ 11  38) "Sieve on C =")
% (find-maclanemoerdijkpage (+ 11 109) "Definition 1. A Grothendieck Topology")

From Mac Lane/Moerdijk, p.109:


\newpage

% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11 110)   "Definition 1. A Grothendieck Topology")

From Mac Lane/Moerdijk, p.110:

Definition 1. A (Grothendieck) topology on a category $\catC$ is a
function $J$ which assigns to each object $C$ of $\catC$ a collection
$J(C)$ of sieves on $C$, in such a way that:

(i) the maximal sieve $t_C = \setofst{f}{\cod(f)=C}$ is in $J(C)$;

(ii) (stability axiom) if $S∈J(C)$, then $h^*(S)∈J(D)$ for any arrow
$h:D→C$;

(iii) (transitivity axiom) if $S∈J(C)$ and $R$ is any sieve on $C$
such that $h^*(R)∈J(D)$ for all $h:D→C$ in $S$, then $R∈J(C)$.

$$
\begin{array}{rcl}
          J(C) &⊆& \Sieveson(C) \\
          J(C) &∈& \Pts(\Sieveson(C)) \\
             J &:& (C:\catC) → \Pts(\Sieveson(C)) \\
  \hasmax_J &:=& ∀C.\;t_C∈J(C) \\
    \trans_J &:=& ∀(h:D→C).\;∀S∈J(C).\;h^*(S)∈J(D) \\
     \stab_J &:=& ∀C.∀S∈J(C).\;∀R∈\Sieveson(X). \\
                       && (∀(D\ton{h}C).\;h^*(R)∈J(D)) → (R∈J(C)) \\
\end{array}
$$

We draw $(J, \mathsf{hasmaxs}_J, \trans_J, \stab_J)$ as:
%
% See:
% (excp 6 "downcasing-2")
% (exc    "downcasing-2")
%
%D diagram groth-top-MM-p110
%D 2Dx     100 +25 +50
%D 2D  100 A1  A2  A3
%D 2D
%D 2D  +12 B1  B2  B3
%D 2D       |   |   | 
%D 2D  +17 C1  C2  C3
%D 2D
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1 A2 A3 ==>  C   t_C          (t_C∈J(C))
%D ren B1 B2 B3 ==>  C     S            (S∈J(C))
%D ren C1 C2 C3 ==>  D h^*(S)      (h^*(S)∈J(D))
%D ren D1 D2 D3 ==>  C     R            (R∈J(C))
%D ren E1 E2 E3 ==> ∀D h^*(R) (∀h∈S.\;h^*(R)∈J(D))
%D
%D (( A1 place  A3 place
%D    B1 C1 <- .plabel= l h
%D    # B2 C2 |->
%D    B3 C3  ->
%D
%D    newnode: D0 at: @D1+v(12,0) .TeX= S place
%D    newnode: in at: @D1+v(6,3) .TeX= \rotatebox{32}{$∈$} place
%D    D1 E1 <- .plabel= l ∀h
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{groth-top-MM-p110}
$$

\newpage

\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=2020groth-tops veryclean
make -f 2019.mk STEM=2020groth-tops pdf

% Local Variables:
% coding: utf-8-unix
% ee-tla: "grt"
% End:
