|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2010kockdiff.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010kockdiff.tex && latex 2010kockdiff.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010kockdiff.tex && pdflatex 2010kockdiff.tex"))
% (eev "cd ~/LATEX/ && Scp 2010kockdiff.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010kockdiff.dvi"))
% (find-dvipage "~/LATEX/2010kockdiff.dvi")
% (find-pspage "~/LATEX/2010kockdiff.ps")
% (find-pspage "~/LATEX/2010kockdiff.pdf")
% (find-xpdfpage "~/LATEX/2010kockdiff.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf 2010kockdiff.pdf 2010kockdiff.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010kockdiff.ps 2010kockdiff.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010kockdiff.ps 2010kockdiff.dvi && ps2pdf 2010kockdiff.ps 2010kockdiff.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010kockdiff.pdf" (ee-twupfile "LATEX/2010kockdiff.pdf") 'over)
% (ee-cp "~/LATEX/2010kockdiff.pdf" (ee-twusfile "LATEX/2010kockdiff.pdf") 'over)
% (find-twusfile "LATEX/" "2010kockdiff")
% http://angg.twu.net/LATEX/2010kockdiff.pdf
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2010kockdiff.dnt
%*
% (eedn4-51-bounded)
%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\def\cz{\check}
\par Notes (very preliminary!) on downcasing:
\par Kock, Anders: A simple axiomatics for differentiation.
\par Math. Scand. 40 (1977), no. 2, 183-193.
\par http://www.mscand.dk/
\par http://www.mscand.dk/article.php?id=2356
\msk
\par The idea of ``downcasing'' is detailed here:
\par http://angg.twu.net/math-b.html\#internal-diags-in-ct
\par http://angg.twu.net/LATEX/2010diags.pdf
\par Its section 17 is about ``ring objects of line type''.
\def{\mathsf{d}}
\newpage
Diagrams for the definition of the map $\aa$:
%D diagram diag0
%D 2Dx 100 +40
%D 2D 100 A×A×A b,b',c
%D 2D | -
%D 2D | |
%D 2D v v
%D 2D +30 A b+b'c
%D 2D
%D (( A×A×A A -> .plabel= l \sm{ð(a_1,a_2,a_3).\\a_1+(a_2·a_3)}
%D b,b',c b+b'c |->
%D ))
%D enddiagram
%D
$$\diag{diag0}$$
%D diagram diag1
%D 2Dx 100
%D 2Dx 100 +40 +40 +50
%D 2D 100 A×A×D <--| A×A b,b_a,a <===== b,b_a
%D 2D | | - -
%D 2D | | | |
%D 2D v v v v
%D 2D +30 A |----> A^D b+b_aa ===> a|->(b+b_aa)
%D 2D
%D (( A×A×D A×A A A^D
%D @ 0 @ 1 <-|
%D @ 0 @ 2 -> .plabel= l \cz\aa @ 1 @ 3 -> .plabel= r \aa
%D @ 2 @ 3 |->
%D ))
%D (( b,b_a,a b,b_a
%D b+b_aa a|->(b+b_aa)
%D @ 0 @ 1 <=
%D @ 0 @ 2 |-> .plabel= l \cz\aa @ 1 @ 3 -> .plabel= r \aa
%D @ 2 @ 3 =>
%D
%D ))
%D enddiagram
%D
$$\diag{diag1}$$
\msk
K77's Proposition 1: $\aa:A×A \to A^D$ is a morphims of ring objects.
% (find-LATEX "2008sdg.tex" "ring-object-tan-space")
%D diagram TR-as-ring-object
%D 2Dx 100 +35 +60
%D 2D 100 1 =====> T\R <============== (T\R)^2
%D 2D
%D 2D +20 {}1 =====> (A×A) <========== (A×A)×(A×A)
%D 2D
%D 2D +20 * |----> (0,0)
%D 2D +6 {}* |----> (1,0)
%D 2D +6 (a+b,a_x+b_x) <-----| (a,a_x),(b,b_x)
%D 2D +6 (ab,a_xb+b_xa) <----| (a,a_x),(b,b_x){}
%D 2D
%D (( 1 T\R -> sl^ .plabel= a 0
%D 1 T\R -> sl_ .plabel= b 1
%D T\R (T\R)^2 <- sl^ .plabel= a +
%D T\R (T\R)^2 <- sl_ .plabel= b ·
%D ))
%D (( {}1 (A×A) -> sl^ .plabel= a 0
%D {}1 (A×A) -> sl_ .plabel= b 1
%D (A×A) (A×A)×(A×A) <- sl^ .plabel= a +
%D (A×A) (A×A)×(A×A) <- sl_ .plabel= b ·
%D ))
%D (( (a+b,a_x+b_x) .tex= (b+c,b_a+c_a) (a,a_x),(b,b_x) .tex= (b,b_a),(c,c_a)
%D (ab,a_xb+b_xa) .tex= (bc,b_ac+bc_a) (a,a_x),(b,b_x){} .tex= (b,b_a),(c,c_a)
%D ))
%D (( * (0,0) |->
%D {}* (1,0) |->
%D (a+b,a_x+b_x) (a,a_x),(b,b_x) <-|
%D (ab,a_xb+b_xa) (a,a_x),(b,b_x){} <-|
%D ))
%D enddiagram
%D
$$\diag{TR-as-ring-object}$$
%D diagram diag3-std
%D 2Dx 100 +60
%D 2D 100 A0 <----- A1
%D 2D | |
%D 2D | |
%D 2D | v
%D 2D +30 | A3'
%D 2D | ^
%D 2D v |
%D 2D +20 A2' v
%D 2D +10 A2 <----- A3
%D 2D
%D (( A0 .tex= (A×A) A1 .tex= (A×A)×(A×A)
%D A2' .tex= A^D A3' .tex= A^D×A^D y+= 10
%D A2 .tex= A^D A3 .tex= (A×A)^D
%D A0 A1 <- .plabel= a *
%D A0 A2 -> .plabel= l \aa A1 A3' -> .plabel= r \aa×\aa A3' A3 <-> .plabel= r \cong
%D A2 A3 <- .plabel= b m^D
%D ))
%D enddiagram
%D
$$\diag{diag3-std}$$
%:*+*{+}*
%D diagram diag3-dnc
%D 2Dx 100 +90
%D 2D 100 A0 <----- A1
%D 2D | |
%D 2D | |
%D 2D | v
%D 2D +30 | A3'
%D 2D | ^
%D 2D v |
%D 2D +20 A2' v
%D 2D +10 A2 <----- A3
%D 2D
%D (( A0 .tex= (bc,b_ac+bc_a) A1 .tex= (b,b_a),(c,c_a)
%D A2' .tex= da|->bc+(b_ac+bc_a)da A3' .tex= (da|->b+b_ada),(da|->c+c_ada) y+= 10
%D A2 .tex= da|->(b+b_ada)(c+c_ada) A3 .tex= da|->(b+b_ada,c+c_ada)
%D A0 A1 <- .plabel= a *
%D A0 A2' -> .plabel= l \aa A1 A3' -> .plabel= r \aa×\aa A3' A3 <-> .plabel= r \cong
%D A2 A3 <- .plabel= b m^D
%D ))
%D enddiagram
%D
$$\diag{diag3-dnc}$$
\newpage
\def\defas{\;:=\;}
\def\zeroT{\ulcorner 0 \urcorner {}^T}
\def\oneT {\ulcorner 1 \urcorner {}^T}
\def\plusT{+^T}
\def\dotT {·^T}
\def\zeroD{\ulcorner 0 \urcorner {}^D}
\def\oneD {\ulcorner 1 \urcorner {}^D}
\def\plusD{+^D}
\def\dotD {·^D}
\def\plushat{\hat+}
\def\aacz{\check\aa}
The translation to $ð$-calculus:
\msk
Let $\zeroT \defas ð*.(0,0)$.
Let $\oneT \defas ð*.(1,0)$.
Let $\plusT \defas ð((b,b_a),(c,c_a)).(b+c, b_a+c_a)$.
Let $\dotT \defas ð((b,b_a),(c,c_a)).(bc, b_ac+bc_a)$.
Then $(\zeroT, \oneT, \plusT, \dotT)$ is a ring object.
\msk
Let $\zeroD \defas ð*.ðda.0$.
Let $\oneD \defas ð*.ðda.1$.
Let $\plusD \defas ð(f_\DD,g_\DD),ðda.(f(da)+g(da))$.
Let $\dotD \defas ð(f_\DD,g_\DD),ðda.(f(da)g(da))$.
Then $(\zeroD, \oneD, \plusD, \dotD)$ is a ring object.
\msk
Let $\aacz \defas ð(b,b_a,da).(b+b_ada)$.
Let $\aa \defas ð(b,b_a).ðda.(b+b_ada)$.
Then $\aa$ is a ring homomorphism.
\msk
Let $\plushat \defas ða.ðda.(a+da)$.
Let $\tau \defas ða.\ang{a,1}$.
Then $\tau;\aa = \plushat$.
\msk
Let $\bb^\nat \defas ðf_\DD.f_\DD(0)$.
Then $\aa;\bb^\nat = \pi$.
\msk
From now on let's suppose that $\aa$ is an iso.
Let $\bb \defas \aa³;\pi$.
Let $\gg \defas \aa³;\pi'$.
Then $\bb = \bb^\nat$.
\msk
Let's now define the derivative of a function $f:A \to A$.
Let $f' \defas ða.\gg(ðda.f(a+da))$.
\msk
First Taylor lemma: $ð(a,da).f(a+da) = ð(a,da).f(a)+f'(a)da$.
Abbreviated form: $f(a+da) = f(a)+f'(a)da$.
\msk
Let $(f+g) \defas ða.f(a)+g(a)$.
Let $(fg) \defas ða.f(a)g(a)$.
Let $(f¢g) \defas ða.f(g(a))$.
\msk
Product rule:
%
$$\begin{array}{rcl}
(fg)(a+da) &=& f(a+da)g(a+da) \\
&=& (f(a)+f'(a)da)(g(a)+g'(a)da) \\
&=& f(a)g(a) + (f'(a)g(a)+f(a)g'(a))da + f'(a)g'(a)da^2 \\
&=& f(a)g(a) + (f'(a)g(a)+f(a)g'(a))da \\
&=& (fg)(a) + (f'g+fg')(a)da \\
\end{array}
$$
Chain rule:
%
$$\begin{array}{rcl}
(f¢g)(a+da) &=& f(g(a+da)) \\
&=& f(g(a)+g'(a)da) \\
&=& f(g(a))+f'(g(a))g'(a)da \\
&=& (f¢g)(a)+((f'¢g)g')(a)da \\
\end{array}
$$
% ----------------------------------------
\newpage
\def\corn#1{\ulcorner#1\urcorner}
%:*×*{×}*
(Section 17 of the ``Internal Diagrams'' paper:)
\msk
Let $(R, \corn0, \corn1, +, ·)$ be a commutative ring in a CCC. That
means: we have a diagram
%
%D diagram ring-object
%D 2Dx 100 +35 +35
%D 2D 100 A0 ====> A1 <============== A2
%D 2D
%D 2D +20 a0 |---> b0
%D 2D +6 a1 |---> b1
%D 2D +6 b2 <-------------| c2
%D 2D +6 b3 <-------------| c3
%D 2D
%D (( A0 .tex= 1 A1 .tex= A A2 .tex= A×A
%D a0 .tex= * b0 .tex= 0
%D a1 .tex= * b1 .tex= 1
%D b2 .tex= a+b c2 .tex= a,b
%D b3 .tex= ab c3 .tex= a,b
%D ))
%D (( A0 A1 -> sl^ .plabel= a \corn0
%D A0 A1 -> sl_ .plabel= b \corn1
%D A1 A2 <- sl^ .plabel= a +
%D A1 A2 <- sl_ .plabel= b ·
%D a0 b0 |->
%D a1 b1 |->
%D b2 c2 <-|
%D b3 c3 <-|
%D ))
%D enddiagram
%D
$$\diag{ring-object}$$
%
and the morphisms $\corn0$, $\corn1$, $+$, $·$ behave as expected.
Let $D$ be the set of zero-square infinitesimals of $A$, i.e.,
$\sst{ÝA}{^2=0}$; $D$ can be defined categorically as an equalizer.
If we take $A:=\R$, then $D=\{0\}$; but if we let $A$ be a ring with
nilpotent infinitesimals, then $\{0\} \subsetneq A$.
% Our notation will suggest that we are in $\R$, though.
\msk
The main theorem of [Kock77] says that if the map
%
$$\begin{array}{rrcl}
\aa: & A×A & \to & (D{\to}A) \\
& (a,b) & \mto & ð¨D.(a+b) \\
\end{array}
$$
%
is invertible, then we can use $\aa$ and $\aa³$ to {\sl define} the
derivative of maps from $A$ to $A$ --- {\sl every} morphism $f: A \to
A$ in the category $\catC$ will be ``differentiable'' ---, and the
resulting differentiation operation $f \mapsto f'$ behaves as
expected: we have, for example, $(fg)'=f'g+fg'$ and $(f¢g)' =
(f'¢g)g'$.
Commutative rings with the property that their map $\aa$ is invertible
are called {\sl ring objects of line type}. ROLTs are hard to
construct, so most of the proofs about them have to be done in a very
abstract setting. However, if we can use the following downcasings for
$\aa$ and $\aa³$ --- note that $\bb=(\aa³;)$, that $\cc=(\aa³;')$,
and that these notations do not make immediately obvious that $\aa$
and $\aa³$ are inverses ---,
%
%D diagram aa-and-aa-inverse
%D 2Dx 100 +30 +30 +15 +40 +40
%D 2D 100 A0 <-- A1 --> A2 b0 <-- b1 --> b2
%D 2D ^ |^ ^ ^ |^ ^
%D 2D \ || / \ || /
%D 2D \ v| / \ v| /
%D 2D +30 A3 b3
%D 2D
%D 2D +15 B0 <-- B1 --> B2 C0 <-- C1 --> C2
%D 2D ^ |^ ^ ^ |^ ^
%D 2D \ || / \ || /
%D 2D \ v| / \ v| /
%D 2D +30 B3 C3
%D 2D
%D (( A0 .tex= A A1 .tex= A×A A2 .tex= A
%D A3 .tex= (D{->}A)
%D @ 0 @ 1 <- .plabel= a
%D @ 1 @ 2 -> .plabel= a '
%D @ 0 @ 3 <- .plabel= l \bb # \sm{\bb\;:=\\\aa³;}
%D @ 1 @ 3 -> sl_ .PLABEL= _(0.42) \aa
%D @ 1 @ 3 <- sl^ .PLABEL= ^(0.38) \aa³
%D @ 2 @ 3 <- .plabel= r \cc
%D ))
%D (( B0 .tex= a B1 .tex= a,b B2 .tex= b
%D B3 .tex= (\mapsto"a+b)
%D @ 0 @ 1 <-| .plabel= a
%D @ 1 @ 2 |-> .plabel= a '
%D @ 0 @ 3 <-| .plabel= l \bb
%D @ 1 @ 3 |-> .PLABEL= _(0.43) \aa
%D @ 2 @ 3 <-| .plabel= r \cc
%D ))
%D (( C0 .tex= f(0) C1 .tex= (f(0),f'(0)) C2 .tex= f'(0)
%D C3 .tex= (\mapsto"f())
%D @ 0 @ 1 <-| .plabel= a
%D @ 1 @ 2 |-> .plabel= a '
%D @ 0 @ 3 <-| .plabel= l \bb
%D @ 1 @ 3 <-| .PLABEL= ^(0.43) \aa³
%D @ 2 @ 3 <-| .plabel= r \cc
%D ))
%D enddiagram
%D
$$\diag{aa-and-aa-inverse}$$
%
and then all the proofs in the first two sections of [Kock77] can be
reconstructed from half-diagrammatic, half-$ð$-calculus-style proofs,
done in the archetypal language, where the intuitive content is clear.
This will be shown in a sequel to [OchsHyp].
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: