|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2010kockdiff-utf8.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2010kockdiff-utf8.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2010kockdiff-utf8.pdf"))
% (defun e () (interactive) (find-LATEX "2010kockdiff-utf8.tex"))
% (defun u () (interactive) (find-latex-upload-links "2010kockdiff-utf8"))
% (find-pdf-page "~/LATEX/2010kockdiff-utf8.pdf")
% (find-sh0 "cp -v ~/LATEX/2010kockdiff-utf8.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2010kockdiff-utf8.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2010kockdiff-utf8.pdf
% file:///tmp/2010kockdiff-utf8.pdf
% file:///tmp/pen/2010kockdiff-utf8.pdf
% http://angg.twu.net/LATEX/2010kockdiff-utf8.pdf
% (find-LATEX "2019.mk")
\documentclass[oneside]{book}
\usepackage[colorlinks,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")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\directlua{tf:processuntil(texlines:nlines())}
% %L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
% \pu
%L addabbrevs("\"", " ", "->", "→", "|->", "↦")
%L addabbrevs("<=", "≤", "!!", "^{**}", "!", "^*")
\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_aδa ===> δa|->(b+b_aδa)
%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_aδa δa|->(b+b_aδa)
%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].
\newpage
% (find-kockdiffpage (+ -182 184) "(definition of \aa)")
%D diagram first-maps
%D 2Dx 100 +40
%D 2D 100 A0 -> A1
%D 2D +20 B0 -> B1
%D 2D +20 C0 -> C1
%D 2D
%D ren A0 A1 ==> A×A A
%D ren B0 B1 ==> A×A A
%D
%D (( A0 A1 -> .plabel= a + A0 A1 -> .plabel= b a,b↦a+b
%D
%D ))
%D (( B0 B1 @ 0 @ 1 -> .plabel= a + @ 0 @ 1 -> .plabel= b a,b↦a·b
%D ))
%D enddiagram
%D
$$\pu
\diag{first-maps}
$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "NONE"
% End: