Warning: this is an htmlized version!
The original is across this link,
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_2a_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 $(fg) \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}
  (fg)(a+da) &=& f(g(a+da)) \\
              &=& f(g(a)+g'(a)da) \\
              &=& f(g(a))+f'(g(a))g'(a)da \\
              &=& (fg)(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 $(fg)' =
(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: