|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2026vdepaiva.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2026vdepaiva.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2026vdepaiva.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2026vdepaiva.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2026vdepaiva.pdf"))
% (defun e () (interactive) (find-LATEX "2026vdepaiva.tex"))
% (defun o () (interactive) (find-LATEX "2026vdepaiva.tex"))
% (defun u () (interactive) (find-latex-upload-links "2026vdepaiva"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2026vdepaiva.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (code-eec-LATEX "2026vdepaiva")
% (find-pdf-page "~/LATEX/2026vdepaiva.pdf")
% (find-sh0 "cp -v ~/LATEX/2026vdepaiva.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2026vdepaiva.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2026vdepaiva.pdf")
% file:///home/edrx/LATEX/2026vdepaiva.pdf
% file:///tmp/2026vdepaiva.pdf
% file:///tmp/pen/2026vdepaiva.pdf
% http://anggtwu.net/LATEX/2026vdepaiva.pdf
% https://anggtwu.net/LATEX/2026vdepaiva.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2 DiagForth1")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2026vdepaiva" "2" "vdp2026" "vdp")
% «.geometry» (to "geometry")
% «.edrx26a» (to "edrx26a")
% «.biber» (to "biber")
% «.edrx26b» (to "edrx26b")
% «.edrx26c» (to "edrx26c")
% «.defs» (to "defs")
% «.footer» (to "footer")
% «.defs-T-and-B» (to "defs-T-and-B")
%
% «.title» (to "title")
% «.toc» (to "toc")
% «.links» (to "links")
% «.proposition-1» (to "proposition-1")
% «.proposition-1-compat» (to "proposition-1-compat")
% «.proposition-1-basic» (to "proposition-1-basic")
% «.proposition-1-imp» (to "proposition-1-imp")
%
% «.writetoc» (to "writetoc")
% «.references» (to "references")
% ;-- defs
\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-LATEX "dednat7-test1.tex")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
% «geometry» (to ".geometry")
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
% «edrx26a» (to ".edrx26a")
\usepackage{edrx26a} % (find-LATEX "edrx26a.sty")
%
% «biber» (to ".biber")
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-ab.bib} % (find-LATEX "catsem-ab.bib")
%\addbibresource{education.bib} % (find-LATEX "education.bib")
%
\begin{document}
% «edrx26b» (to ".edrx26b")
\input edrx26b.tex % (find-LATEX "edrx26b.tex")
% «edrx26c» (to ".edrx26c")
% (find-LATEX "edrx26c.tex")
%L processsubfile "edrx26c.tex" -- runs the "%L"s
\input edrx26c % loads the defs
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
% «footer» (to ".footer")
% (find-LATEX "edrxheadfoot.tex")
\def\drafturl{http://anggtwu.net/LATEX/2026-1-C2.pdf}
\def\drafturl{http://anggtwu.net/2026.1-C2.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
% «defs-T-and-B» (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}
\def\P#1{\left(#1\right)}
%L require "DiagForth1" -- (find-angg "LUA/DiagForth1.lua")
\pu
%L forths["-"] = function () pusharrow("-") end
\pu
% ;-- title
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (vdp2026p 1 "title")
% (vdp2026a "title")
\thispagestyle{empty}
\begin{center}
\vspace*{1.2cm}
\par {\bf \Large Notes on Valeria de Paiva's}
\par \ssk
\par {\bf \Large Tecnhical Report (1991)}
\bsk
Eduardo Ochs - RCN/PURO/UFF
Psicopata do CEFET
\url{https://anggtwu.net/math-b.html}
\end{center}
%\newpage
% ;-- toc
% «toc» (to ".toc")
% (to "writetoc")
% ;-- links
% «links» (to ".links")
% (vdp2026p 2 "links")
% (vdp2026a "links")
%{\bf Links}
%
%\scalebox{0.6}{\def\colwidth{16cm}\firstcol{
%}\anothercol{
%}}
%L forths["ab!"] = function ()
%L node_a = ds:pick(1)
%L node_b = ds:pick(0)
%L end
%L forths["abc!"] = function ()
%L node_a = ds:pick(2)
%L node_b = ds:pick(1)
%L node_c = ds:pick(0)
%L end
%L forths["a@"] = function () ds:push(node_a) end
%L forths["b@"] = function () ds:push(node_b) end
%L forths["c@"] = function () ds:push(node_c) end
%L forths["ab@"] = function () dxyrun "a@ b@" end
%L forths["<-|-"] = function () dxyrun "ab! ab@ <- .plabel= m \\scriptscriptstyle| ab@ <-" end
%L forths["\\'"] = function () dxyrun "abc! a@ c@ - a@ c@ midpoint .TeX= {} b@ ->" end
%L
%L forthe["\\'-name:"] = "w"
%L forths["\\'-name:"] = function (TeX)
%L dxyrun "\\'"
%L dxyrun "b@ c@ midpoint"
%L forths["relplace"](-4,0,TeX)
%L end
\newpage
% ;-- proposition-1
% «proposition-1» (to ".proposition-1")
% (vdp2026p 99 "proposition-1")
% (vdp2026a "proposition-1")
\SLIDE{Proposition 1}
%D diagram Prop-1
%D 2Dx 100 +30 +25 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +30 A2 A3
%D 2D
%D 2D +30 A4 A5 B4 B5
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> U X V Y W Z
%D ren B0 B1 B4 B5 ==> U X W Z
%D
%D (( A0 A1 <-|- .plabel= a α
%D A2 A3 <-|- .plabel= a β
%D A4 A5 <-|- .plabel= a γ
%D A0 A2 -> .plabel= l f
%D A2 A4 -> .plabel= l g
%D A0 A1 A3 \'-name: F
%D A2 A3 A5 \'-name: G
%D
%D B0 B1 <-|- .plabel= a α
%D B4 B5 <-|- .plabel= a γ
%D B0 B4 -> .plabel= l h
%D B0 B1 B5 \'-name: H
%D ))
%D enddiagram
\pu
\scalebox{0.55}{\def\colwidth{10cm}\firstcol{
Proposition 1, p.4,
a.k.a: ``composition needs checking''.
\msk
Lets suppose that we are in $\Set$.
Let's omit the types when they can be inferred from the diagrams, {\sl
and let's use dependent variables.}
\msk
So $A≡(U,X,α)$ is a triple
$(U∈\Sets,X∈\Sets,α:U×X→\{0,1\})$,
So $B≡(V,Y,β)$ is a triple
$(V∈\Sets,Y∈\Sets,β:V×Y→\{0,1\})$,
\msk
and a morphism $(f,F):A→B$
is actually a triple
%
$$\pmat{f:U→V, \\ F:U×Y→X, \\ [∀(u,y).α→β]:\ldots}$$
in which the $[∀(u,y).α→β]$ is a guarantee/witness for:
%
$$\begin{array}{l}
∀(u,y).α→β \\
≡ \; ∀(u,y).α(u,x)→β(v,y) \\
≡ \; ∀(u,y).α(u,x(u,y))→β(v(u),y) \\
≡ \; ∀(u,y).α(u,F(u,y))→β(f(u),y) \\
\end{array}
$$
}\anothercol{
$$\scalebox{1.5}{$
\diag{Prop-1}
$}
$$
\bsk
\bsk
We want to compose the
$(f,F,[∀(u,y).α→β])$ with the
$(g,G,[∀(v,z).β→γ])$,
and obtain a:
%
$$(h,H,[∀(u,z).α→γ]).$$
}}
\newpage
% ;-- proposition-1-compat
% «proposition-1-compat» (to ".proposition-1-compat")
% (vdp2026p 4 "proposition-1-compat")
% (vdp2026a "proposition-1-compat")
\SLIDE{Proposition 1: compatibility conditions}
%D diagram Prop-1-compat
%D 2Dx 100 +30 +25 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +30 A2 A3
%D 2D
%D 2D +30 A4 A5 B4 B5
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> U X V Y W Z
%D ren B0 B1 B4 B5 ==> U X W Z
%D
%D (( # A0 A1 <-|- .plabel= a α
%D # A2 A3 <-|- .plabel= a β
%D # A4 A5 <-|- .plabel= a γ
%D A0 A2 -> .plabel= l f
%D A2 A4 -> .plabel= l g
%D A0 A1 A3 \'-name: F
%D A2 A3 A5 \'-name: G
%D
%D # B0 B1 <-|- .plabel= a α
%D # B4 B5 <-|- .plabel= a γ
%D B0 B4 -> .plabel= l h
%D B0 B1 B5 \'-name: H
%D ))
%D enddiagram
\pu
\sa {body:....wz} {\phantom{a}\\\phantom{a}\\w&z}
\sa {body:..v..z} {\phantom{a}\\v&\\&z}
\sa {body:..vy..} {\phantom{a}\\v&y\\\phantom{a}}
\sa {body:..vywz} {\phantom{a}\\v&y\\w&z}
\sa {body:u....z} {u&\\\phantom{a}\\&z}
\sa {body:u..y..} {u&\\&y\\\phantom{a}}
\sa {body:ux....} {u&x\\\phantom{a}\\\phantom{a}}
\sa {body:ux..wz} {u&x\\\phantom{a}\\w&z}
\sa {body:uxvy..} {u&x\\v&y\\\phantom{a}}
\sa {body:uxvywz} {u&x\\v&y\\w&z}
\sa {(..vy..)} {\psm{\ga{body:..vy..}}}
\sa {(....wz)} {\psm{\ga{body:....wz}}}
\sa {(..v..z)} {\psm{\ga{body:..v..z}}}
\sa {(..vywz)} {\psm{\ga{body:..vywz}}}
\sa {(u....z)} {\psm{\ga{body:u....z}}}
\sa {(u..y..)} {\psm{\ga{body:u..y..}}}
\sa {(ux....)} {\psm{\ga{body:ux....}}}
\sa {(ux..wz)} {\psm{\ga{body:ux..wz}}}
\sa {(uxvy..)} {\psm{\ga{body:uxvy..}}}
\sa {(uxvywz)} {\psm{\ga{body:uxvywz}}}
\sa {big(..vy..)} {\pmat{\ga{body:..vy..}}}
\sa {big(....wz)} {\pmat{\ga{body:....wz}}}
\sa {big(..v..z)} {\pmat{\ga{body:..v..z}}}
\sa {big(..vywz)} {\pmat{\ga{body:..vywz}}}
\sa {big(u....z)} {\pmat{\ga{body:u....z}}}
\sa {big(u..y..)} {\pmat{\ga{body:u..y..}}}
\sa {big(ux....)} {\pmat{\ga{body:ux....}}}
\sa {big(ux..wz)} {\pmat{\ga{body:ux..wz}}}
\sa {big(uxvy..)} {\pmat{\ga{body:uxvy..}}}
\sa {big(uxvywz)} {\pmat{\ga{body:uxvywz}}}
\sa {{..vy..}} {\csm{\ga{body:..vy..}}}
\sa {{....wz}} {\csm{\ga{body:....wz}}}
\sa {{..v..z}} {\csm{\ga{body:..v..z}}}
\sa {{..vywz}} {\csm{\ga{body:..vywz}}}
\sa {{u....z}} {\csm{\ga{body:u....z}}}
\sa {{u..y..}} {\csm{\ga{body:u..y..}}}
\sa {{ux....}} {\csm{\ga{body:ux....}}}
\sa {{ux..wz}} {\csm{\ga{body:ux..wz}}}
\sa {{uxvy..}} {\csm{\ga{body:uxvy..}}}
\sa {{uxvywz}} {\csm{\ga{body:uxvywz}}}
\scalebox{0.55}{\def\colwidth{8.5cm}\firstcol{
Let's forget $α$, $β$ and $γ$ for a while,
and let's consider $f$, $F$, $g$ and $G$ as
compatibility conditions...
\msk
I will write $\psm{u,&x, \\ v,&y, \\ w,&z}$, \standout{with} commas,
for a tuple that only obeys
$u∈U$, $x∈X$, $\ldots$, $z∈Z$,
and will write $\psm{u&x \\ v&y \\ w&z}$, \standout{without} commas,
for $\psm{u,&x, \\ v,&y, \\ w,&z}$ plus guarantees for the
``obvious'' compatibility conditions,
that in this case are:
%
$$\begin{array}{l}
[v=v(u)], \\{}
[x=x(u,y)], \\{}
[w=w(v)], \\{}
[y=y(v,z)] \\
\end{array}
\quad
\text{i.e.,}
\quad
\begin{array}{l}
[v=f(u)], \\{}
[x=F(u,y)], \\{}
[w=g(v)], \\{}
[y=G(v,z)] \\
\end{array}
$$
So:
\ssk\par $\ga{(uxvywz)}$ has 4 compatibility conditions,
\ssk\par $\ga{(uxvy..)}$ has 2 compatibility conditions,
\ssk\par $\ga{(..vywz)}$ has 2 compatibility conditions,
\ssk\par $\ga{(u..y..)}$ has 0 compatibility conditions...
}\def\colwidth{12cm}\anothercol{
$$\scalebox{1.5}{$
\diag{Prop-1-compat}
$}
$$
\bsk
\bsk
...and $\ga{(ux..wz)}$ has these compatibility conditions:
%
$$\begin{array}{rcl}
w &=& w(v(u)) \\
&=& g(f(u)) \\\\[-5pt]
x &=& x(u,y) \\
&=& x(u,y(v,z)) \\
&=& x(u,y(v(u),z)) \\
&=& F(u,G(f(u),z)) \\
\end{array}
$$
}}
\newpage
% ;-- proposition-1-basic
% «proposition-1-basic» (to ".proposition-1-basic")
% (vdp2026p 99 "proposition-1-basic")
% (vdp2026a "proposition-1-basic")
\SLIDE{Proposition 1: basic pullbacks}
%D diagram prop-1-basic
%D 2Dx 100 +30 +30 +30
%D 2D 100 A1 A2 A3
%D 2D
%D 2D +25 B0 B1 B3
%D 2D
%D 2D +25 C1 C2 C3
%D 2D
%D ren A1 A2 A3 ==> \ga{{u..y..}} \ga{{uxvy..}} \ga{{ux....}}
%D ren B0 B1 B3 ==> \ga{{u....z}} \ga{{uxvywz}} \ga{{..vy..}}
%D ren C1 C2 C3 ==> \ga{{..v..z}} \ga{{..vywz}} \ga{{....wz}}
%D
%D (( A1 A2 <-> A2 A3 ->
%D B0 B1 <->
%D C1 C2 <-> C2 C3 ->
%D B1 A2 -> A2 B3 ->
%D B1 C2 -> C2 B3 ->
%D ))
%D enddiagram
\pu
\scalebox{0.65}{\def\colwidth{6cm}\firstcol{
Now let's write $\ga{{uxvywz}}$
for the space of all (compatible)
tuples of the form $\ga{(uxvywz)}$,
and do the same for all other
combinations of letters...
\bsk
We have the maps at the right,
and the diamond at the middle
is a pullback.
\bsk
Note that:
$α$ is defined on $\ga{{ux....}}$,
$β$ is defined on $\ga{{..vy..}}$,
$γ$ is defined on $\ga{{....wz}}$,
$α→β$ is defined on $\ga{{u..y..}}$,
$β→γ$ is defined on $\ga{{..v..z}}$, and
$α→γ$ is defined on $\ga{{u....z}}$...
}\def\colwidth{10cm}\anothercol{
$$\scalebox{1.5}{$
\diag{prop-1-basic}
$}
$$
}}
\newpage
% ;-- proposition-1-imp
% «proposition-1-imp» (to ".proposition-1-imp")
% (vdp2026p 99 "proposition-1-imp")
% (vdp2026a "proposition-1-imp")
\SLIDE{Proposition 1: the implication}
\scalebox{0.7}{\def\colwidth{8cm}\firstcol{
$$\scalebox{1.0}{$
\diag{Prop-1}
$}
$$
\bsk
\bsk
Remember that want to compose the
$(f,F,[∀(u,y).α→β])$ with the
$(g,G,[∀(v,z).β→γ])$,
and obtain a:
%
$(h,H,[∀(u,z).α→γ]).$
\msk
We saw that
$h(u) = g(f(u))$ and
$H(u,z) = F(u,G(f(u),z))$.
}\anothercol{
We still need to check this:
\msk
$\pmat{ \P{∀\ga{(u..y..)}.α→β} & ∧ \\\\[-9pt]
\P{∀\ga{(..v..z)}.β→γ} \\
} →$
\ssk
$\;\;\;\, \P{∀\ga{(u....z)}.α→γ}$
\bsk
\bsk
Sketch of the proof:
%
%:
%: ∀\ga{(u..y..)}.α→β ∀\ga{(..v..z)}.β→γ
%: ------------------ ------------------
%: ∀\ga{(uxvy..)}.α→β ∀\ga{(..vywz)}.β→γ
%: ------------------ ------------------
%: ∀\ga{(uxvywz)}.α→β ∀\ga{(uxvywz)}.β→γ
%: ----------------------------------------
%: ∀\ga{(uxvywz)}.α→γ
%: ------------------
%: ∀\ga{(u....z)}.α→γ
%:
%: ^prop-1-imp
%:
\pu
$$\ded{prop-1-imp}$$
}}
% ;-- writetoc
% «writetoc» (to ".writetoc")
\directlua{toclines:writetoc()}
% Writes in: (find-LATEXfile "2026vdepaiva.mytoc")
% See: (to "toc")
% ;-- references
% «references» (to ".references")
%\printbibliography
% ;-- write-dnt-file
% «write-dnt-file» (to ".write-dnt-file")
% (find-fline "~/LATEX/" "2026vdepaiva.dnt")
% (find-fline "~/LATEX/2026vdepaiva.dnt")
%L write_dnt_file ("2026vdepaiva.dnt")
\pu
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2026vdepaiva")
% Local Variables:
% coding: utf-8-unix
% outline-regexp: "% +;--"
% ee-tla: "vdp"
% ee-tla: "vdp2026"
% End: