|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: