Downcasing SDG

Anders Kock: A simple axiomatics for differentiation (1977)

• 1. Proposition 7

1. Proposition 7
================
Proposition 7: for any f: A --> A, the diagram
                          b |-> c

          \tdf
     A×A ------> A×A      b.b_a |------> c,c_a
      |           |         -              -
  \aa |           | \aa     |              |
      v           v         v              v
     A^D ------> A^D     da|->b+db |--> da|->c+dc
          f^D

                       b,b_a |--------> c,c_{b}b_a
		         -                   -
		         |                   v
		         v             da|->c+c_{b}b_{a}dx
		   da|->b+b_{a}da |--> da|->c(b+b_{a}da)


commutes, where \tdf: A×A -> A×A is the map with the description

  (a_0, a_1) -> (f(a_0), a_1·f'(a_0))
   b,b_a |--------> c,c_{b}b_a

Proof: it suffices to prove that the exponential adjoint diagram
commutes. The exponential diagram is the outer diagram in

            \tdf×D
      A×A×D ------> A×A×D          b,b_a,da |---------> c,c_a,da
        |   \         |                -   /               -
  \aa×D |    \ \czaa  | \aa×D          |    \---\          |
        v     v       v                v         v         |
      A^D×D --> A   A^D×D       (da|->b+db),da |-> b+db    |
        |   ev    \   |                -               /   |
  f^D×D |        f \  | ev             |                \  |
        v     ev    v v                v                 v v
      A^D×D --------> A         (da|->c+dc),da |--------> d+dc


         b,b_a,da |------------------------> c,c_{b}b_{a},da
            -	 /			            -
            |	  \-------\		            |
            v		   v                        v
    (da|->b+b_{a}da),da |-> b+b_{a}da   (da|->c+c_{b}b_{a}da),da
            -			     /            -  
            |			      \-----\     v
            v				     v c+c_{b}b_{a}da
  (da|->c(b+b_{a}da)),da |-------------------> c(b+b_{a}da)