|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2022ebl.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2022ebl.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex -record 2022ebl.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2022ebl.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2022ebl.pdf"))
% (defun e () (interactive) (find-LATEX "2022ebl.tex"))
% (defun o () (interactive) (find-LATEX "2021excuse.tex"))
% (defun o () (interactive) (find-LATEX "2021groth-tops-children.tex"))
% (defun u () (interactive) (find-latex-upload-links "2022ebl"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022ebl.pdf"))
% (code-eec-LATEX "2022ebl")
% (find-pdf-page "~/LATEX/2022ebl.pdf")
% (find-sh0 "cp -v ~/LATEX/2022ebl.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2022ebl.pdf /tmp/2C7.pdf")
% (find-sh0 "cp -v ~/LATEX/2022ebl.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2022ebl.pdf
% file:///tmp/2022ebl.pdf
% file:///tmp/pen/2022ebl.pdf
% http://angg.twu.net/LATEX/2022ebl.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2022ebl" "ebl")
%
% (find-LATEXfile "2022ebl-abs.tex")
% (find-LATEXfile "2022ebl-abs.tex" "book of abstracts")
% «.defs» (to "defs")
% «.title» (to "title")
% «.modern» (to "modern")
% «.Jcan-1» (to "Jcan-1")
% «.Jcan-2» (to "Jcan-2")
% «.in-a-certain-order» (to "in-a-certain-order")
% «.abcd» (to "abcd")
% «.context» (to "context")
% «.propositions» (to "propositions")
% «.types-in-physics» (to "types-in-physics")
% «.indefinite-article» (to "indefinite-article")
% «.lns-and-telescopes» (to "lns-and-telescopes")
% «.grtops-via-telescopes» (to "grtops-via-telescopes")
% «.bottle-order» (to "bottle-order")
% «.bottle-R» (to "bottle-R")
% «.bottle-R-2» (to "bottle-R-2")
% «.bottle-R-3» (to "bottle-R-3")
% «.why-bottle» (to "why-bottle")
% «.convs-on-names» (to "convs-on-names")
% «.vis-dn-clos-1» (to "vis-dn-clos-1")
% «.bottle-defs» (to "bottle-defs")
%\documentclass[oneside,12pt]{article}
\documentclass[oneside]{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}
\usepackage{stmaryrd} % (find-es "tex" "stmaryrd")
%
% (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{edrx21} % (find-LATEX "edrx21.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.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")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
%head=1.25cm,
%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
%a4paper,
top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
]{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
% «defs» (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
% (find-LATEX "edrx21.sty" "colors-2019")
% (find-LATEX "edrx21defs.tex")
% (find-LATEX "edrx21defs.tex" "colors")
\def\undresult #1{\underbrace{#1}_{\text{result}}}
\def\undfilt #1{\underbrace{#1}_{\text{filt}}}
\def\undfilter #1{\underbrace{#1}_{\text{filter}}}
\def\undgen #1{\underbrace{#1}_{\text{gen}}}
\def\undgenerator#1{\underbrace{#1}_{\text{generator}}}
\def\undvt #1{\underbrace{#1}_{\text{v:T}}}
\def\undvartype #1{\underbrace{#1}_{\text{var:type}}}
\def\undcontext #1{\underbrace{#1}_{\text{context}}}
\def\Jcan{J_{\text{can}}}
\def\R{\mathbb{R}}
\def\Opens{\mathcal{O}}
\def\calS{\mathcal{S}}
\def\catC{\mathbf{C}}
\catcode`«=13 \def«{\llangle}
\catcode`»=13 \def»{\rrangle}
%\def\univ{\text{(univ)}}
%\def\nameof#1{\ulcorner#1\urcorner}
%\def\Rings{\mathbf{Rings}}
%
%\def\V{\mathbf{T}}
%\def\F{\mathbf{F}}
%\def\smile{\ensuremath{{=})}}
%\def\frown{\ensuremath{{=}(}}
%\def\smirk{\ensuremath{{=}/}}
%
%\def\und#1#2{\underbrace{#1}_{#2}}
%\def\und#1#2{\underbrace{#1}_{\text{#2}}}
%\def\ug#1{\und{#1}{gen}}
%\def\uf#1{\und{#1}{filt}}
%\def\ue#1{\und{#1}{expr}}
%\def\uC#1{\und{#1}{context}}
%\def\uCH#1{\und{#1}{context / hypotheses}}
%\def\uvt#1{\und{#1}{v:T}}
%\def\uterm#1{\und{#1}{term}}
%\def\utype#1{\und{#1}{type}}
%\def\uconc#1{\und{#1}{conclusion}}
%
%\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
%\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}
%
%% pos-spec colors
%% (find-es "tex" "xcolor")
%% (find-xcolorpage 17 "2.4 Predefined colors")
%% (find-xcolortext 17 "2.4 Predefined colors")
%\def\Cnum#1{{\color{magenta}#1}}
%\def\Cnum#1{{\color{Red1}#1}}
%\def\Cnum#1{{\color{violet}#1}}
%\def\Cnum#1{{\color{orange}#1}}
%\def\Cstr#1{{\color{violet}#1}}
%\def\Cstr#1{{\color{Red1}#1}}
%\def\Csex#1{{\color{Red1}#1}}
\def\pdiag#1{\left(\diag{#1}\right)}
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\cocolor{}
\def\cocolor{\color{DarkGreen!80!black}}
\def\co#1{{%
\cocolor%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\pco#1{\par\co{#1}}
% «verbatim» (to ".verbatim")
%\directlua{dofile "2021excuse.lua"} % (find-LATEX "2021excuse.lua")
%\def\myhbox#1#2#3{\setbox0=\hbox{#3}\ht0=#1\dp0=#2\box0}
%\def\verbahbox#1{\hbox{\tt#1}}
%\def\verbahbox#1{\myhbox{7pt}{2pt}{{\tt#1}}}
%% (find-dednat6 "tug-slides.tex" "bgcolorhbox")
%\def\bgcolorhbox#1#2{{%
% \setbox0\hbox{#2}%
% \setbox0\vbox{\vskip\fboxsep\box0\vskip\fboxsep}%
% \setbox0\hbox{\kern\fboxsep\box0\kern\fboxsep}%
% {\color{#1}{\smashedvrule{\wd0}{\ht0}{\dp0}}}%
% \box0%
% }}
%\def\bgbox#1{\bgcolorhbox{YellowOrangeLight}{#1}}
%
%\def\myvcenter#1{\begin{matrix}#1\end{matrix}}
%\catcode`\^^O=13 \def*{{\color{red}*}}
% From:
% (find-LATEX "2018-1-LA-material.tex" "defs")
\def\tabl#1{\begin{tabular}{l}#1\end{tabular}}
\def\tablt#1{\begin{tabular}[t]{l}#1\end{tabular}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}
\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\ren{\operatorname{ren}}
\def\app{\operatorname{app}}
\def\pair{\operatorname{pair}}
\def\cur{\mathsf{cur}}
\def\uncur{\mathsf{uncur}}
\def\ren{\mathsf{ren}}
\def\app{\mathsf{app}}
\def\pair{\mathsf{pair}}
\def\Ran{\mathsf{Ran}}
\def\Dn {\Downarrow}
% \def∧{\&}
\def\namedfunction#1#2#3#4#5{
\begin{array}{rrcl}
#1: & #2 & → & #3 \\
& #4 & ↦ & #5 \\
\end{array}
}
\def\IPLai{\text{IPL}_{{∧}{→}}}
\def\NDai {\text{ND} _{{∧}{→}}}
%\noedrxfooter % (find-LATEX "edrxheadfoot.tex")
\def\drafturl{http://angg.twu.net/LATEX/2020-1-C2.pdf}
\def\drafturl{http://angg.twu.net/math-b.html\#2021-excuse-tt}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
\setlength{\parindent}{0em}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
% (ebl2022p 1 "title")
% (ebl2022a "title")
\thispagestyle{empty} % (find-es "tex" "thispagestyle")
\begin{center}
\vspace*{0.5cm}
\begin{tabular}{c}
\phantom{a}\\[-15pt]
{\Large {\bf On a way to visualize some}} \\[1pt]
{\Large {\bf Grothendieck Topologies}} \\[1pt]
\\[-9pt]
\ColorGray{(talk @ XX EBL)}\\[-5pt]
\\[-9pt]
{\tiny\url{http://angg.twu.net/math-b.html#2022-ebl}}\\[8pt]
Eduardo Ochs \\
Salvador, 2022sep13 \\
\end{tabular}
\end{center}
\newpage
% «modern» (to ".modern")
% (ebl2022p 2 "modern")
% (ebl2022a "modern")
{\bf A definition}
A {\sl modern mathematician} is someone who is trying to learn proof
assistants, and who is trying to translate its mathematical knowledge
into the language of proof assistants.
\bsk
\msk
I am a ``modern mathematician'' in that sense.
I am learning Agda (slowly).
\newpage
% «Jcan-1» (to ".Jcan-1")
% (ebl2022p 3 "Jcan-1")
% (ebl2022a "Jcan-1")
% (find-LATEX "2022ebl-abs.tex")
{\bf Canonical Grothendieck Topology}
The {\sl canonical Grothendieck topology} \standout{on $\R$}, $\Jcan$,
is easy to define, but the definition takes several steps...
\begin{enumerate}
\item for each open set $U \in \Opens(\R)$ a {\sl sieve on $U$} is a
subset of $\Opens(U)$ that is downward-closed;
\item for each $U \in \Opens(\R)$ we write $\Omega(U)$ for the set of
all sieves on $U$;
\item we say that a sieve $\calS \in \Omega(U)$ is {\sl covering} when
$\bigcup \calS = U$;
\item for each $U \in \Opens(\R)$ we define $\Jcan(U)$ as the set of
covering sieves on $U$.
\end{enumerate}
\newpage
% «Jcan-2» (to ".Jcan-2")
% (ebl2022p 4 "Jcan-2")
% (ebl2022a "Jcan-2")
% (find-LATEX "2022ebl-abs.tex")
\def\Rd#1{\ColorRed{#1}}
{\bf Canonical Grothendieck Topology (2)}
The {\sl canonical Grothendieck topology} \standout{on
$(X,\Opens(X))$}, $\Rd{\Jcan}$,
is easy to define, but the definition takes several steps...
\begin{enumerate}
\item for each open set $U \in \Opens(\Rd{X})$ a {\sl sieve on $U$}
is a subset of $\Opens(U)$ that is downward-closed;
\item for each $U \in \Opens(\Rd{X})$ we write $\Omega(U)$ for the
set of all sieves on $U$;
\item we say that a sieve $\calS \in \Omega(U)$ is {\sl covering} when
$\bigcup \calS = U$;
\item for each $U \in \Opens(\Rd{X})$ we define $\Jcan(U)$ as the set
of covering sieves on $U$.
\end{enumerate}
\newpage
% «in-a-certain-order» (to ".in-a-certain-order")
% (ebl2022p 5 "in-a-certain-order")
% (ebl2022a "in-a-certain-order")
To a ``modern mathematician'' these
definitions feel very wrong.
\msk
In, ahem, ``modern mathematics'', things
have to be defined in a certain order.
\msk
That order is very similar to how we
write ``generators'' and ``filters'' in set
comprehensions. For example:
%
$$\begin{array}{rl}
& \setofst
{\undresult{(x,y)}}
{\undgenerator{x∈\{0,…,5\}},
\undgenerator{y∈\{0,…,x\}},
\undfilter{x^2+y^2≤25}
} \\
\\[-5pt]
⇒
& \setofsc
{\undgenerator{x∈\{0,…,5\}},
\undgenerator{y∈\{0,…,x\}},
\undfilter{x^2+y^2≤25}
}
{\undresult{(x,y)}}
\\
\end{array}
$$
\newpage
% «abcd» (to ".abcd")
% (ebl2022p 6 "abcd")
% (ebl2022a "abcd")
\scalebox{0.9}{\def\colwidth{11cm}\firstcol{
A {\sl series of (four) generators}
is something like this:
%
$$\begin{array}{rcl}
a &∈& A, \\
b &∈& B(a), \\
c &∈& C(a,b), \\
d &∈& D(a,b,c) \\
\end{array}
$$
where:
%
$$\begin{tabular}{rlll}
$a$ & is a variable, &
$A$ & is an expression that yields a set, \\
$b$ & is a variable, &
$B(a)$ & is an expression that yields a set \\
&&& and that may depend on $a$, \\
$c$ & is a variable, &
$C(a,b)$ & is an expression that yields a set \\
&&& and that may depend on $a$ and $b$, \\
$d$ & is a variable, &
$D(a,b,c)$ & is an expression that yields a set \\
&&& and that may depend on $a$, $b$, and $c$ \\
\end{tabular}
$$
}\anothercol{
}}
\newpage
% «context» (to ".context")
% (ebl2022p 7 "context")
% (ebl2022a "context")
% (excp 38 "contexts")
% (exca "contexts")
A {\sl context} with four declarations
in Dependent Type Theory (DTT)
is something like this:
%
$$\begin{array}{rcl}
a &:& A, \\
b &:& B(a), \\
c &:& C(a,b), \\
d &:& D(a,b,c) \\
\end{array}
$$
Hints for beginners:
think that the `:'s are `$∈$'s,
and think that the types
$A, B(a), C(a,b), D(a,b,c)$
are sets.
\newpage
% «propositions» (to ".propositions")
% (ebl2022p 8 "propositions")
% (ebl2022a "propositions")
% (find-books "__logic/__logic.el" "martin-lof")
% (find-martinlofittpage (+ 6 6) "Propositions")
{\bf Propositions}
\scalebox{0.75}{\def\colwidth{12.5cm}\firstcol{
(From Martin-Löf's {\sl Intuitionistic Type Theory}, p.6):
\ssk
Classically, a proposition is nothing but a truth value, that is, an
element of the set of truth values, whose two elements are the true
and the false. Because of the difficulties of justifying the rules for
forming propositions by means of quantification over infinite domains,
when a proposition is understood as a truth value, this explanation is
rejected by the intuitionists and replaced by saying that
\begin{quote}
a proposition is defined by laying down what counts as a proof of
the proposition,
\end{quote}
and that
\begin{quote}
a proposition is true if it has a proof, that is, if a proof of it
can be given.
\end{quote}
Thus, intuitionistically, truth is identified with provability,
though of course not (because of Godel's incompleteness theorem)
with derivability within any particular formal system.
}\anothercol{
}}
\newpage
% «types-in-physics» (to ".types-in-physics")
% (ebl2022p 9 "types-in-physics")
% (ebl2022a "types-in-physics")
{\bf Types in Physics}
\scalebox{0.85}{\def\colwidth{10.5cm}\firstcol{
When I tried to study Physics I tried to assign types to variables.
% I never formalized this properly, but here are the main ideas...
\msk
An instant, $t$, would be an element of the set of all instants.
A horizontal position, $x$, would be an element of the set of all
horizontal positions.
The set of all instants and the set of horizontal positions would be
two ``different'' (?!?!) copies of $\R$. Suppose that these copies
were called $T$ and $X$.
The notation $⟦·⟧$ is pronounced ``the space of''.
There is a ``dictionary of types'' that assigned to most
\standout{names} of variables their ``types''... so:
%
$$\begin{array}{rcl}
t, t_0, t_1 &∈& T \\
x, x_0, x_1 &∈& X \\
⟦t⟧, ⟦t_0⟧, ⟦t_1⟧ &=& T \\
⟦x⟧, ⟦x_0⟧, ⟦x_1⟧ &=& X \\
\end{array}
$$
}\anothercol{
}}
\newpage
% «indefinite-article» (to ".indefinite-article")
% (ebl2022p 10 "indefinite-article")
% (ebl2022a "indefinite-article")
% (misp 32 "indefinite-articles")
% (misa "indefinite-articles")
When $P$ is a proposition
I write $⟦P⟧$ for the set/space of all proofs of $P$,
and I write $«P»$ for \standout{a} proof of $P$...
\msk
\phantom{m}
(Indefinite article! $↑$)
\bsk
A few months ago I finished a paper called
``On the Missing Diagrams in Category Theory'',
and it explains these tricks with ``the space of''
and indefinite articles.
\msk
Link:
{\footnotesize
% http://angg.twu.net/math-b.html\#md
\url{http://angg.twu.net/math-b.html#md}
}
\newpage
{\bf Values for contexts}
\scalebox{0.9}{\def\colwidth{10.5cm}\firstcol{
\vspace*{-0.2cm}
$$\begin{array}{rl}
& \setofst
{\undresult{(x,y)}}
{\undgenerator{x∈\{0,…,5\}},
\undgenerator{y∈\{0,…,x\}},
\undfilter{x^2+y^2≤25}
} \\
\\[-5pt]
⇒
& \setofsc
{\undgenerator{x∈\{0,…,5\}},
\undgenerator{y∈\{0,…,x\}},
\undfilter{x^2+y^2≤25}
}
{\undresult{(x,y)}}
\\
\\[-5pt]
⇒
& \setofsc
{\undcontext{
{\undgenerator{x∈\{0,…,5\}},
\undgenerator{y∈\{0,…,x\}},
\undfilter{«x^2+y^2≤25»}}}}
{\undresult{(x,y)}}
\\
\end{array}
$$
A {\sl value} for the context above
is a triple like this:
%
$$(x,y,«x^2+y^2≤25»)$$
}\anothercol{
}}
\newpage
% «lns-and-telescopes» (to ".lns-and-telescopes")
% (ebl2022p 12 "lns-and-telescopes")
% (ebl2022a "lns-and-telescopes")
{\bf Long names and telescopes}
\scalebox{0.85}{\def\colwidth{9cm}\firstcol{
In Agda these are roughly equivalent:
%
$$\begin{array}{rcl}
a &:& A, \\
b &:& B(a), \\
c &:& C(a,b), \\
〈d,e,f〉 &:& Σd⠆D(a,b,c). \\
&& Σe⠆E(a,b,c,d), \\
&& Σf⠆F(a,b,c,d,e) \\
\multicolumn{3}{l}{
\;\;\;
\ColorRed{\textsf{open}}\; 〈d,e,f〉,
}\\
g&:&G(a,b,c,d,e,f), \\
h&:&H(a,b,c,d,e,f,g) \\
\end{array}
%
\qquad
%
\begin{array}{rcl}
a &:& A, \\
b &:& B(a), \\
c &:& C(a,b), \\
d &:& D(a,b,c), \\
e &:& E(a,b,c,d), \\
f &:& F(a,b,c,d,e), \\
〈d,e,f〉 &=& (d,e,f), \\
g &:& G(a,b,c,d,e,f), \\
h &:& H(a,b,c,d,e,f,g) \\
\end{array}
$$
\bsk
See: ``{\sl 25 Years of AutoMATH}''
and N.G. de Bruijn's paper from 1991:
``{\sl Telescopic Mappings in Typed Lambda Calculus}''
}\anothercol{
}}
\newpage
% «grtops-via-telescopes» (to ".grtops-via-telescopes")
% (ebl2022p 13 "grtops-via-telescopes")
% (ebl2022a "grtops-via-telescopes")
{\bf Grothendieck Topologies via telescopes}
Now the natural thing to do would be to define
Grothendieck Topologies in Agda-ish pseudocode,
and then close the parts of the telescope
that are made of proof terms, like:
%
$$«\Opens(X) \text{ is a topology on } X»$$
I tried to do that, and it didn't help.
What worked for me was to ignore all
the proof terms, and to try to obtain
values for contexts like:
%
$$(X, \Opens(X), U, \calS, \calU, V)$$
\newpage
% «bottle-R» (to ".bottle-R")
% (ebl2022p 14 "bottle-R")
% (ebl2022a "bottle-R")
{\bf The bottle topology in $\R$}
\sa{A_1}{A_1}
\sa{A_2}{A_2} \sa{A_3}{A_3}
\sa{A_4}{A_4} \sa{A_5}{A_5}
\sa{i A_1}{[2,3]}
\sa{i A_2}{[1,2)} \sa{i A_3}{(3,4]}
\sa{i A_4}{(-∞,1)} \sa{i A_5}{(4,+∞)}
\def\Gr#1{\ColorGray{#1}}
\def\OR {\Opens (\R)}
\def\OBR{\Opens_B(\R)}
\def\Grnw{\Gr{↖}}
\def\Grne{\Gr{↗}}
% (find-es "tex" "array")
\def\thincmat#1{{
\setlength{\arraycolsep}{0pt}
\cmat{#1}
}}
\def\thinmat#1{{
\setlength{\arraycolsep}{0pt}
\mat{#1}
}}
\sa{A 12345}{
\thincmat{
\ga{A_1}, && \\
\Gr{↓} &\Gr{↘}& \\
\ga{A_2}, && \ga{A_3}, \\
\Gr{↓} && \Gr{↓} \\
\ga{A_4}, && \ga{A_5} \\
}}
\sa{i A 12345}{
\thincmat{
\ga{i A_1}, && \\
\Gr{↓} &\Gr{↘}& \\
\ga{i A_2}, && \ga{i A_3}, \\
\Gr{↓} && \Gr{↓} \\
\ga{i A_4}, && \ga{i A_5} \\
}}
Let:
%
$$\begin{array}{rcl}
\calA_5 &=& \ga{A 12345} \;\;=\;\; \ga{i A 12345}, \\
\\[-5pt]
\calA_{32} &=& \setofst{\bigcup \calA'}{\calA'⊆\calA_5}, \\
\\[-5pt]
\OBR &=& \OR ∩ \calA_{32}, \\
\end{array}
$$
Then $(\R,\OBR)$ is a
topological space
with 10 open sets...
\newpage
% «bottle-R-2» (to ".bottle-R-2")
% (ebl2022p 15 "bottle-R-2")
% (ebl2022a "bottle-R-2")
{\bf The bottle topology in $\R$ (2)}
\def\itwo#1#2{\sm{(-∞,#1)∪\\(#2,+∞)}}
\sa{i 32}{(-∞,+∞)}
\sa{i 22}{\itwo23}
\sa{i 21}{\itwo24} \sa{i 12}{\itwo13}
\sa{i 20}{(-∞,2)} \sa{i 11}{\itwo14} \sa{i 02}{(3,+∞)}
\sa{i 10}{(-∞,1)} \sa{i 01}{(4,+∞)}
\sa{i 00}{∅}
\sa{bottle in R}{{
\setlength{\arraycolsep}{-3pt}
\mat{
&& \ga{i 32} \\
&&& \Grnw \\
&&&& \ga{i 22} \\
&&& \Grne && \Grnw \\
&& \ga{i 21} &&&& \ga{i 12} \\
& \Grne && \Grnw && \Grne && \Grnw \\
\ga{i 20} &&&& \ga{i 11} &&&& \ga{i 02} \\
& \Grnw && \Grne && \Grnw && \Grne \\
&& \ga{i 10} &&&& \ga{i 01} \\
&&& \Grnw && \Grne \\
&&&& \ga{i 00} \\
}}}
$$\ga{bottle in R}$$
\newpage
% «bottle-R-3» (to ".bottle-R-3")
% (ebl2022p 16 "bottle-R-3")
% (ebl2022a "bottle-R-3")
{\bf The bottle topology in $\R$ (3)}
{\footnotesize
See my ``Planar Heyting Algebras for Children'':
\url{http://angg.twu.net/math-b.html#zhas-for-children-2}
}
\sa{bottle in R l_r}{
\setlength{\arraycolsep}{1pt}
\mat{
3▁ && \\
\Gr{↓} &\Gr{↘}& \\
2▁ && ▁2 \\
\Gr{↓} && \Gr{↓} \\
1▁ && ▁1 \\
}}
\sa{bottle in R lr}{{
\setlength{\arraycolsep}{1pt}
\mat{
&& {32} \\
&&& \Grnw \\
&&&& {22} \\
&&& \Grne && \Grnw \\
&& {21} &&&& {12} \\
& \Grne && \Grnw && \Grne && \Grnw \\
{20} &&&& {11} &&&& {02} \\
& \Grnw && \Grne && \Grnw && \Grne \\
&& {10} &&&& {01} \\
&&& \Grnw && \Grne \\
&&&& {00} \\
}}}
$$(\Opens\left(
\ga{bottle in R l_r}
\right),⊆)
\qquad
=
\qquad
\scalebox{0.9}{$
\ga{bottle in R lr}
$}
$$
\newpage
% «why-bottle» (to ".why-bottle")
% (ebl2022p 17 "why-bottle")
% (ebl2022a "why-bottle")
{\bf Why ``bottle''?}
From Bagpuss, episode 1:
\bsk
% (find-es "imagemagick" "convert")
% (find-fline "~/tmp/bagpuss_bottle.jpg")
% (find-fline "~/tmp/" "bagpuss_bottle.jpg")
% (setq eepitch-preprocess-regexp "^")
% (setq eepitch-preprocess-regexp "^%T ")
%
%T * (eepitch-shell)
%T * (eepitch-kill)
%T * (eepitch-shell)
%T cd ~/LATEX/2022ebl/
%T cp -iv ~/tmp/bagpuss_bottle.jpg .
%T convert bagpuss_bottle.jpg bagpuss_bottle.pdf
%T laf
%T # (find-pdf-page "~/LATEX/2022ebl/bagpuss_bottle.pdf")
\includegraphics[width=6cm]{2022ebl/bagpuss_bottle.pdf}
\newpage
% «convs-on-names» (to ".convs-on-names")
% (ebl2022p 18 "convs-on-names")
% (ebl2022a "convs-on-names")
{\bf Conventions on names}
Here the diagram at the right
{\sl complements} the diagram on the left...
\def\rotl#1{\rotatebox{90}{$#1$}}
\def\rotr#1{\rotatebox{270}{$#1$}}
\def\ptab#1{\left(\begin{tabular}{c}#1\end{tabular}\right)}
\sa{o P(X)}{\Pts(X)}
\sa{o O(X)}{\Opens(X)}
\sa{o O(U)}{\Opens(U)}
\sa{o A}{A}
\sa{o U}{U}
\sa{o V}{V}
\sa{o a}{a}
\sa{o x}{x}
\sa{i P(X)}{\ptab{all \\ subsets \\ of $X$}}
\sa{i O(X)}{\ptab{all open \\ subsets \\ of $X$}}
\sa{i O(U)}{\ptab{all open \\ subsets \\ of $U$}}
\sa{i A}{\ptab{a \\ subset \\ of $X$}}
\sa{i U}{\ptab{an open \\ subset \\ of $X$}}
\sa{i V}{\ptab{an open \\ subset \\ of $U$}}
\sa{i a}{\ptab{a \\ point \\ of $X$}}
\sa{i x}{\ptab{a \\ point \\ of $V$}}
$$\setlength{\arraycolsep}{1pt}
\begin{matrix}
\ga{o a} & ∈ & \ga{o A} & ∈ & \ga{o P(X)} \\
& & & & \rotl{⊆} \\
& & \ga{o U} & ∈ & \ga{o O(X)} \\
& & \rotl{⊆} & & \rotl{⊆} \\
\ga{o x} & ∈ & \ga{o V} & ∈ & \ga{o O(U)} \\
\end{matrix}
%
\qquad
%
\scalebox{0.8}{$
\begin{matrix}
\ga{i a} & ∈ & \ga{i A} & ∈ & \ga{i P(X)} \\
& & & & \rotl{⊆} \\
& & \ga{i U} & ∈ & \ga{i O(X)} \\
& & \rotl{⊆} & & \rotl{⊆} \\
\ga{i x} & ∈ & \ga{i V} & ∈ & \ga{i O(U)} \\
\end{matrix}
$}
$$
\newpage
% «vis-dn-clos-1» (to ".vis-dn-clos-1")
% (ebl2022p 10 "vis-dn-clos-1")
% (ebl2022a "vis-dn-clos-1")
{\bf Visualizing downward-closedness}
A {\sl sieve} $\calS$ on $U$ is a subset of $\Opens(U)$
that is ``downward-closed'', i.e.:
%
$$∀V,W∈\Opens(U).\;
\pmat{V \\ \text{above} \\ W}
→
\pmat{V∈\calS \\ ↓ \\ W∈\calS}
$$
$$∀V,W∈\Opens(U).\;
\pmat{V \\ \rotl{⊆} \\ W}
→
\pmat{V∈\calS \\ ↓ \\ W∈\calS}
$$
\newpage
% «bottle-defs» (to ".bottle-defs")
% (grcp 1 "introduction")
% (grca "introduction")
% (find-LATEX "2021groth-tops-children.tex" "Bottle")
\makeatletter
\def\BottleSetArgs#1{\BottleSetArgs@#1}
\def\BottleSetArgs@#1#2#3#4#5{%
\sa{32}{#1}\sa{20}{#2}\sa{21}{#3}\sa{22}{#4}\sa{10}{#5}%
\BottleSetArgs@@}
\def\BottleSetArgs@@#1#2#3#4#5{%
\sa{11}{#1}\sa{12}{#2}\sa{00}{#3}\sa{01}{#4}\sa{02}{#5}%
}
\makeatother
%
%R local Bottle = 7/ !ga{32} \
%R | !ga{22} |
%R | !ga{21} !ga{12} |
%R |!ga{20} !ga{11} !ga{02}|
%R | !ga{10} !ga{01} |
%R \ !ga{00} /
%R Bottle:tomp({zdef="Bottle-5pt", scale="5pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle-6pt", scale="6pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle-8pt", scale="8pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle^2", scale="52pt", meta=nil}):addcells():addarrows():output()
\pu
\def\bo #1{{ \BottleSetArgs{#1}\zha{Bottle-5pt} }}
\def\pbo #1{{\left( \BottleSetArgs{#1}\zha{Bottle-5pt} \right)}}
\def\bbo #1{{\left[ \BottleSetArgs{#1}\zha{Bottle-5pt} \right]}}
\def\pwbo#1{{\left( \BottleSetArgs{#1}\zha{Bottle-8pt} \right)}}
% «WideBottle» (to ".WideBottle")
% (find-LATEX "2021groth-tops-defs.tex" "WideBottle")
% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests")
% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests" "WideBottle")
\makeatletter
\def\WideBottleSetArgs#1{\WideBottleSetArgs@#1}
\def\WideBottleSetArgs@#1#2#3#4#5{%
\sa{32}{#1}\sa{33}{#2}\sa{20}{#3}\sa{21}{#4}\sa{22}{#5}%
\WideBottleSetArgs@@}
\def\WideBottleSetArgs@@#1#2#3#4#5{%
\sa{23}{#1}\sa{10}{#2}\sa{11}{#3}\sa{12}{#4}\sa{13}{#5}%
\WideBottleSetArgs@@@}
\def\WideBottleSetArgs@@@#1#2#3#4{%
\sa{00}{#1}\sa{01}{#2}\sa{02}{#3}\sa{03}{#4}%
}
\makeatother
%R local WideBottle = 7/ !ga{33} \
%R | !ga{32} !ga{23} |
%R | !ga{22} !ga{13} |
%R | !ga{21} !ga{12} !ga{03}|
%R |!ga{20} !ga{11} !ga{02} |
%R | !ga{10} !ga{01} |
%R \ !ga{00} /
%R WideBottle:tomp({zdef="WideBottle", scale="7pt", meta="s"}):addcells():output()
%R WideBottle:tomp({zdef="WideBottleMed", scale="10pt", meta=""}):addcells():output()
\pu
\def\wibo #1{{ \WideBottleSetArgs{#1} \zha{WideBottle} }}
\def\pwibo#1{{\left( \WideBottleSetArgs{#1} \zha{WideBottle} \right)}}
\def\wiBo #1{{ \WideBottleSetArgs{#1} \zha{WideBottleMed} }}
\def\pwiBo#1{{\left( \WideBottleSetArgs{#1} \zha{WideBottleMed} \right)}}
\newpage
{\bf Visualizing downward-closedness (2)}
General case: $(X, \Opens(X), U, \calS)$
Particular case: $(\R, \Opens_B(\R), 21, \{00, 01, 10, 11, 20\})$
$$\begin{array}{rcc}
\Opens_B(\R) &⇒& \pwbo{{32} {20}{21}{22} {10}{11}{12} {00}{01}{02}} \\
\\[-5pt]
\Opens(21) ⊆ \Opens_B(\R) &⇒& \pbo{0 110 110 110} \\
\\[-5pt]
\{00, 01, 10, 11, 20\} ⊆ \Opens(21) &⇒& \pbo{· 10· 11· 11·} \\
\end{array}
$$
\newpage
{\bf Everything is finite, so...}
Every intersection of open sets is an open set.
Every intersection of covering sieves is a covering sieve.
\bsk
\phantom{mmmmmmmmmm} $↑$ Huh???
\newpage
{\bf Mac Lane/Moerdijk, p.110, translated}
\msk
{\bf Definition.} A {\sl Grothendieck Topology} on a category
$\Opens(X)$ is a function $J$ which assigns to each object $U$ of
$\Opens(U)$ a collection $J(U)$ of sieves on $U$, in such a way that:
\msk
(J1) The maximal sieve $t(U) = \setofst{V∈\Opens(X)}{V⊆U}$ is in
$J(U)$;
\msk
(J2) (stability axiom) if $\calU∈J(U)$, then $(V⊆U)^*(\calU)∈J(V)$ for
any open set $V∈\Opens(U)$;
\msk
(J3) (transitivity axiom) if $\calU∈J(U)$ and $\calS$ is any sieve on
$U$ such that $(U⊆V)^*(\calS)∈J(V)$ for all $V∈\Opens(U)$ in $\calU$,
then $\calS∈J(U)$.
\newpage
{\bf Grothendieck Topologies backwards}
My favorite way to present GroTops ---
obs: it was the way that worked for me ---
is to start with the canonical GroTop, $\Jcan$,
then check that it obeys the axioms J1, J2, and J3,
and only them look for other GroTops that also
obey J1, J2, and J3...
%
$$\begin{array}{rcl}
Ω(U) &=& \setofst{\calS∈\Opens(U)}{\calS \text{ is a sieve on } U} \\
&=& \setofst{\calS∈\Opens(U)}{\calS \text{ is downward-closed}} \\
\Jcan(U) &=& \setofst{\calS}{
\calS \text{ is a sieve on } U,
\calS \text{ covers } U
} \\
&=& \setofst{\calS ∈ Ω(U)}
{\bigcup \calS = U
} \\
J(U) &=& \setofst{\calS}{
\calS \text{ is a sieve on } U,
\calS \text{ $J$-covers } U
} \\
&=& \setofst{\calS ∈ Ω(U)}
{\calS ∈ J(U)
} \\
\end{array}
$$
\newpage
{\bf Grothendieck Topologies backwards (2)}
\scalebox{0.87}{\def\colwidth{12cm}\firstcol{
One of the consequences of J1, J2, J3, is this:
If $\calU'$ and $\calU''$ are $J$-covering sieves on $U$,
i.e., if $\calU',\calU'' ∈ J(U)$,
then $\calU'∩\calU''$ is a $J$-covering sieve on $U$,
i.e., $\calU'∩\calU'' ∈ J(U)$...
\ssk
\standout{If everything is finite} then:
%
$$\begin{array}{rcl}
\bigcap J(U) &∈& J(U) \\
↑(\bigcap J(U)) &=& J(U) \\
\end{array}
$$
So every $J(U)$ has a minimal element,
and is generated by it.
\msk
The topology $\Opens_B(\R)$ has only 10 `$U$'s.
We can try to draw these maps:
%
$$\begin{array}{rcc}
U &\mapsto& \bigcap J(U) \\
U &\mapsto& ↑(\bigcap J(U)) \\
\end{array}
$$
}\anothercol{
}}
\newpage
{\bf All sieves of a certain form}
I will write this (note the square brackets!!!):
%
$$\scalebox{1.5}{$
%\bbo{0 123 456 789}
\bbo{· ?0· ??· 11·}
$}
$$
for the set of all sieves of that form. So:
%
$$\scalebox{0.9}{$
\bbo{· ?0· ??· 11·}
= \left\{
\pbo{· 00· 00· 11·},
\pbo{· 00· 10· 11·},
\pbo{· 00· 11· 11·},
\pbo{· 10· 10· 11·},
\pbo{· 10· 11· 11·}
\right\}
$}
$$
\newpage
{\bf Some big figures}
Next page: $\Jcan$ on $\Opens_B(\R)$.
After that: $Ω$ on $\Opens_B(\R)$.
\msk
For more figures --- including a way to find
all GroTops on a given finite topology ---
see these (very unfinished) notes:
\ssk
{\footnotesize
% http://angg.twu.net/math-b.html#2021-groth-tops
\url{http://angg.twu.net/math-b.html\#2021-groth-tops}
}
\newpage
\vspace*{-1.25cm}
\hspace*{0.25cm}
$\Jcan =
\left(
\BottleSetArgs{
{\bbo{1 111 111 111}}
{\bbo{· 1·· 1·· 1··}} {\bbo{· 1?· 1?· 11·}} {\bbo{· 1?? 1?? 111}}
{\bbo{· ··· 1·· 1··}} {\bbo{· ··· 1?· 11·}} {\bbo{· ··· 1?? 111}}
{\bbo{· ··· ··· 1··}} {\bbo{· ··· ··· 11·}} {\bbo{· ··· ··· 111}}}
\scalebox{0.65}{$
\zha{Bottle^2}
$}
\right)
$
\newpage
\vspace*{-1.25cm}
\hspace*{0.5cm}
$Ω =
\left(
\BottleSetArgs{
{\bbo{? ??? ??? ???}}
{\bbo{· ?·· ?·· ?··}} {\bbo{· ??· ??· ??·}} {\bbo{· ??? ??? ???}}
{\bbo{· ··· ?·· ?··}} {\bbo{· ··· ??· ??·}} {\bbo{· ··· ??? ???}}
{\bbo{· ··· ··· ?··}} {\bbo{· ··· ··· ??·}} {\bbo{· ··· ··· ???}}}
\scalebox{0.65}{$
\zha{Bottle^2}
$}
\right)
$
\newpage
% Tests:
% $\bo{0 123 456 789} \bbo{0 123 456 789} \pwbo{· {20}{21}· {10}{11}· {00}{01}·}$
% (misp 32 "indefinite-articles")
% (misa "indefinite-articles")
%\printbibliography
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "ebl2022"
% End: