ACompleteAxiomatisation of Partial
            Differentiation
             Gordon Plotkin
          ACTSeminar,May2020
  Cartesian differential categories
      Thegoalofthepresentpaperistodevelopanaxioma-
      tization which directly characterizes the smooth maps:
      in other words, to characterize the coKleisli structure
      of differential categories directly. This leads us to the
      notion of a Cartesian differential category. This notion
      embodies the multi-variable differential calculus which,
      being a fundamental tool of modern mathematics, is
      well worth studying in its own right.
     Blute, Cockett & Seely, Cartesian differential categories, 2009
   Left additive cartesian categories
           Eachhomsetisacommutativemonoid.
           Composition is left additive:
                           0f = 0    (f + g)h = fh + gh
      Amorphismf is additive iff f- (ie right composition with f) is
      additive.
           Theproduct structure is compatible:
               Theprojections
                                    x ←x×y →y
               are additive
               Tupling preserves additivity:
                              f : x → y,g : x → z additive
                               hf,gi : x → y ×z additive
  Example: Finite powers of R and smooth maps
        Thegradient
                        ∇(f):Rn → Rn
        of a smooth map f(x ,:::,xn) of n-arguments is
                       1
                   ∇(f)(v) = h ∂f (v),:::, ∂f (v)i
                           ∂x      ∂x
                            1        n
        Thedifferential
                      D[f]:Rn ×Rn → Rm
        of a smooth map
                       n    m
                     f :R →R =hf ,:::,f i
                                1    m
        is
                                                 T
         D[f](v,w) = h∇(f )(v)·w,:::,∇[f ](v)·wi (= J(f)(v)w )
                      1           n