Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% (find-angg "LATEX/2010kockdiff-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2010kockdiff-new.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2010kockdiff-new.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2010kockdiff-new; makeindex 2010kockdiff-new"))
% (defun e () (interactive) (find-LATEX "2010kockdiff-new.tex"))
% (defun u () (interactive) (find-latex-upload-links "2010kockdiff-new"))
% (find-xpdfpage "~/LATEX/2010kockdiff-new.pdf")
% (find-sh0 "cp -v  ~/LATEX/2010kockdiff-new.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2010kockdiff-new.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2010kockdiff-new.pdf
%               file:///tmp/2010kockdiff-new.pdf
%           file:///tmp/pen/2010kockdiff-new.pdf
% http://angg.twu.net/LATEX/2010kockdiff-new.pdf
\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\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-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")
\directlua{tf:processuntil(texlines:nlines())}

% \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% \directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

%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
% End: