[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2007dnc-sdg"))
;;    http://angg.twu.net/2007dnc-sdg.html
;; file:///home/edrx/TH/L/2007dnc-sdg.html
#]
[lua: LR = R ]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
]
[_TARGETS
  Kock         => http://home.imf.au.dk/kock/
  Kock-axdiff      => http://www.mscand.dk/issue.php?year=1977&volume=40
  Kock-afef        => http://www.tac.mta.ca/tac/volumes/1999/n10/n10.ps
  Kock-fefcde      => ftp://ftp.imf.au.dk/pub/kock/ODE5.ps
  Kock-ttfact      => http://www.dimap.ufrn.br/pipermail/logica-l/2006-August/000438.html
  Kock-sdg         => http://home.imf.au.dk/kock/sdg99.pdf
]

[#
(code-xpdf      "dnckock" "~/LATEX/2006nov26_kock77.pdf")
(code-pdftotext "dnckock" "~/LATEX/2006nov26_kock77.pdf")
;; (find-dnckockpage 1)
;; (find-dnckocktext)
#]

[htmlize [J Downcasing SDG]

[P [__ Kock Anders Kock]: [__ Kock-axdiff A simple axiomatics for differentiation] (1977)]

[WITHINDEX
[#
 # «.proposition-7»	(to "proposition-7")
 #]
[RULE ----------------------------------------]

[tsec «proposition-7»  (to ".proposition-7")
[++N]. 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)
]

]
]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]