### Downcasing differential categories

2007nov05: You are not expected to understand this!
I am only using this file to store some diagrams about differential categories, in DNC notation (see my math page)...

Version: 2007dec17.

Quick index:
1. E-mail to Seely (1)
======================
First, consider a function "f:A->B":

f: A --> B
a |-> f(a)

Let's write it like this (we're putting our physicist's hats on):

b:=f(a)
a |-------> b

We're seeing it as relating the value of two variables - the output,
b, is a function of the input; the rule "b:=f(a)" tells us how to
calculate the output from the input.

Now let's think that A is a one-dimensional vector space, whose points
are the possible values of a, and B is another one-dimensional vector
space, whose points are the possible values for b. If our f is a
linear function A->B (I will not write the arrow as a lollipop), then
we can write b:=f(a) as

b:=ka
a |-----> b

where k is a constant.

Now let's make things worse. A becomes a two-dimensional vector space,
X×Y, and B becomes a three-dimensional vector space, Z×W×T, where X is
the space of the possible values for a variable x, and the same for
the other letters: Y, Z, W, T. Now the value of A is a point in a
two-dimensional space; we can think of it as being the pair of
(numeric) values (x,y) - and the same for b: b=(z,w,t).

A linear transformation f:A->B sets the value of b from the value of
a; or, in freshman's terms, it sets the value of (z,w,t) from the
value of (x,y). It can be, for example, that f is like this:

z:=1x+2y
w:=3x+4y
t:=5x+6y
(x,y) |--------> (z,w,t)
a |--------> b

Now let me pick the case where A and B are both one-dimensional again,
but I will look at a polynomial function, b := 3a^2 + 4a, and I will
represent it as a linear function from !A to B.

!A is an infinite-dimensional space; a point in !A is a certain
quantity of a^0, plus a certain quantity of a^1, plus a certain
quantity of a^2, etc - note that I'm sort of confusing variables and
the base elements of vector spaces, that is not some random macarronic
dialect of mathematics, it's the trick that makes everything work...
anyway, ahead; writing the tensor product as "@", the basis of A is
{a}, and the basis of !A is {a^0, a, a@a, a@a@a, a@a@a@a, ...}, where
a^0 is the 0-th @-power of a; in another notation, this basis is {1,
a, a^2, a^3, a^4, ...}.

The polynomial b := 3a^2 + 4a now becomes

b:=3a^2+4a
(1,a,a^2,...) |----------> b
!A -----------> B,

a linear function.

This is just the beginning, of course - but I've worked out all
diagrams until D.2 in page 8, and some diagrams and equations ahead of
that, and everything became very nice in this notation - only the
dotted lines seem to need some tricks that I don't have yet... Just
for curiosity, here are two diagrams (with no explanations here, but I
can provide them later):

\           /            \           /
A  \         / !A        da \         / !a'
\       /                \       /
=================        =================
|       |       |        |       |       |
|    !A |       |        |    !a | a^3 := 3a'^2da
|    ___|___    |        |    ___|___    |
|   |       |   |        |   |       |   |
|   |   f   |   |        |   |   f   |   |
|   |_______|   |        |   |_______|   |
|       |       |        |       |       |
|     B |       |        |     b := a^3  |
|_______|_______|        |_______|_______|
|                        |
B |                b_{a}da := 3a'^2da
|                        |

The differential combinator:

\           /            \           /
A  \         / !A        da \         / !a'
\       /                \       /
===============          ===============
|                        |
!A |                    d!a | a^3 := 3a'^2da
_______|_______          _______|_______
|       |       |        |       |       |
|    !A |       |        |    !a |       |
|    ___|___    |        |    ___|___    |
|   |       |   |        |   |       |   |
|   |   f   |   |        |   |   f   |   |
|   |_______|   |        |   |_______|   |
|       |       |        |       |       |
|     B |       |        |     b := a^3  |
|_______|_______|        |_______|_______|
|                        |
B |                     db := 3a'^2da
|                        |

In these examples I'm always pretending that A and B are
one-dimensional - everything works when they are more-dimensional, but
then I use some dictionary tricks to "read" the downcased diagrams as
something some general; formally, the downcased names for the wires
become just abstract names for things that are more complex - but
there is some precise relation between these abstract names (they're
not totally abstract or arbitrary) and the "real things" behind
them...


2. Diagrams (1)
===============

[D.1] Constant maps:
(here a^0 := 0 da ⊗ a^0)

\           /
a \         / !a
\       /
=================
|       |  	    |
|  (·0) | a^0   |
|    ___|___    |
|   |       |   |
|   |   e   |   |
|   |_______|   |
|       |	    |
|       | 1	    |
|_______|_______|
|
| 1
|

\              /               |              |                     |         |
a \            / a^7            |              | a^7                 |         | a^7
\          /                 |            __|__                 a |       __|__
=============================      a |           /     \                  |      /     \
|             |             |        |          |  \DD  |                  \    |  \DD  |
|        (·8) | a^8         |        |           \_____/                    \___ \_____/
|           __|__           |        |           /     \                        \/     \
|          /     \          |         \         / a^2   \                  _____/\      \ a^4
|         |  \DD  |         |          \       /         |                /       \      |
|          \_____/          |      ===============       | a^5       a^3 /     ===============
|          /     \          |      |      |      |       |              /      |      |      |
|     a^3 /       \ a^5     |      | (·3) | a^3  |       |             /       | (·5) | a^5  |
|   _____/_       _\_____   |      |   ___|___   |    ___|___       ___|___    |   ___|___   |
|  |       |     |       |  |      |  |       |  |   |       |     |       |   |  |       |  |
|  |   f   |     |   g   |  |  =   |  |   f   |  |   |   g   |  +  |   f   |   |  |   g   |  |
|  |_______|     |_______|  |      |  |_______|  |   |_______|     |_______|   |  |_______|  |
|         \       /         |      |      |      |      /              |       |     /       |
|        b \     / c        |      |     b \     |     /                \      |    / c      |
|          _\___/_          |      |________\____|    / c              b \     |___/_________|
|         |       |         |                \       /                    \       /
|         |   @   |         |                 \     /                      \     /
|         |_______|         |                 _\___/_                      _\___/_
|             |             |                |       |                    |       |
|             | b@c         |                |   @   |                    |   @   |
|_____________|_____________|                |_______|                    |_______|
|                                  |                            |
| b@c                              | b@c                        | b@c
|                                  |                            |

[D.3] Linear maps:

\           /
a \         / a^0           |       |
\       /	         |       | a^0
=================	         |    ___|___
|       |  	    |	         |   |       |
|  (·1) | a^1   |	       a |   |  \ee  |
|    ___|___    |	         |   |_______|
|   |       |   |	         |       :
|   |  \ee  |   |	         |       : 1
|   |_______|   |	         |       :
|       |	    |	         | .....'
|       | a	    |   =        O'
|    ___|___    |	         |
|   |       |   |	         | a
|   |   f   |   |	      ___|___
|   |_______|   |	     |       |
|       |	    |	     |   f   |
|       | b	    |	     |_______|
|_______|_______|	         |
|		         | b
| b		         |
|

[D.4] Chain rule:

|               |
|               | a^11
|             __|__
a |            /     \
\           /                 |           |  \DD  |
a \         / a^11	         |            \_____/
\       /		         |            /     \
=======================	         |       a^3 /       \ a^8
|           |           |	          \         /         \
|     (·12) | a^12      |	      =================     ___\___________
|    _______|_______    |	      |       |       |    |    \          |
|   |       |       |   |	      |  (·4) | a^4   |    |     \ a^4     |
|   |       | a^4   |   |	      |    ___|___    |    |    __\____    |
|   |    ___|___    |   |	      |   |       |   |    |   |       |   |
|   |   |       |   |   |	      |   |   f   |   |    |   |   f   |   |
|   |   |   f   |   |   |	      |   |_______|   |    |   |_______|   |
|   |   |_______|   |   |	      |        \      |    |       |       |
|   |       |       |   |	      |       b \     |    |      _|_ b    |
|   |      _|_ b    |   |	 =    |__________\____|    |_____/___\_____|
|   |_____/___\_____|   |	                  \               /
|           |           |	                 b \             / b^2
|           | b^3       |	                    \           /
|        ___|___        |	                  =================
|       |       |       |	                  |       |       |
|       |   g   |       |	                  |  (·3) | b^3   |
|       |_______|       |	                  |    ___|___    |
|           |           |	                  |   |       |   |
|           | c         |	                  |   |   g   |   |
|___________|___________|	                  |   |_______|   |
|		                  |       |       |
|		                  |       | c     |
|_______|_______|
|
| c
|


3. Vector spaces
================
Fix a base field for our vector spaces: R, C, Q,
an arbitrary field K - it doesn't matter.
Let's denote by FinVec the category of finite-dimensional
vector spaces over that base field; morphisms are linear
transformations.
Each morphism in FinVec has a "dual", or "transpose",
going in the opposite direction.
A good notation (?) for morphisms:

/1 2\
|3 4|
\5 6/
R^2 -------> R^3            c := 1a + 2b
/c\	      d := 3a + 4b
/a\          | |            e := 5a + 6b
| | |------> |d|      a,b |--------------> c,d,e
\b/          | |
\e/

We should be able to do a lot using morphisms
that are not as general as these - matrices that
are all 0s, with just one entry being a 1.
An example:

d:=a
a,b |------> c,d,e

Then our previous morphism is:

1(c:=a) + 2(c:=b) +
3(d:=a) + 4(d:=b) +
5(e:=a) + 6(e:=b)


4. The differential box
=======================

\           /            \           /
A  \         / !A	     da \         / !a'
\       /    	         \       /
=================	     =================
|       |       |	     |       |       |
|    !A |       |	     |    !a | a^3 := 3a'^2da
|    ___|___    |	     |    ___|___    |
|   |       |   |	     |   |       |   |
|   |   f   |   |	     |   |   f   |   |
|   |_______|   |	     |   |_______|   |
|       |       |	     |       |       |
|     B |       |	     |     b := a^3  |
|_______|_______|	     |_______|_______|
|	     	             |
B |	     	     b_{a}da := 3a'^2da
|        	             |


5. The differential combinator
==============================

\           /            \           /
A  \         / !A	     da \         / !a'
\       /    	         \       /
===============   	      ===============
|                        |
!A |                    d!a | a^3 := 3a'^2da
_______|_______          _______|_______
|       |       |	     |       |       |
|    !A |       |	     |    !a |       |
|    ___|___    |	     |    ___|___    |
|   |       |   |	     |   |       |   |
|   |   f   |   |	     |   |   f   |   |
|   |_______|   |	     |   |_______|   |
|       |       |	     |       |       |
|     B |       |	     |     b := a^3  |
|_______|_______|	     |_______|_______|
|	     	             |
B |	     	          db := 3a'^2da
|        	             |


6. Comonad structure
====================
Two natural transformations, ε and δ,

ε        δ
X <----- !X -----> !!X

Obeying the duals of what would be this,
if I downcased my favourite monad:
(ηT;μ)=(Tη;μ)=id
(μT;μ)=(Tμ;μ)

TX --ηT--> TTX --μ--> TX       x,a |---> x,a,1 |----> x,a1
TX --Tη--> TTX --μ--> TX       x,a |---> x,1,a |----> x,1a
TX ---------id------> TX       x,a |----------------> x,a

TTTX --μT--> TTX --μ--> TX   x,a,b,c |---> x,a,bc |---> x,a(bc)
TTTX --Tμ--> TTX --μ--> TX   x,a,b,c |---> x,ab,c |---> x,(ab)c

The duals are:
(δ;ε!)=(δ;!ε)=id
(δ;δ!)=(δ;!δ)

!X <--ε!-- !!X <--δ-- !X
!X <--!ε-- !!X <--δ-- !X
!X <---------id------ !X

!!!X <--δ!-- !!X <--δ-- !X
!!!X <--!δ-- !!X <--δ-- !X


7. Coalgebra modalities
=======================
The comonad (!,δ,ε) is a _coalgebra modality_
if we are given, for every object X, maps:

e
⊤ <----- !X -----> !X⊗!X

Obeying:

-- !X --             !X --------> !X⊗!X
id /    |   \ id          |             |
/   Δ |    \          Δ |             | Δ⊗1
v      v     v           v    1⊗Δ      v
!X <---- !!X ---> !X      !X⊗!X -----> !X⊗!X⊗!X
1⊗e     e⊗1

And this ("δ is a morphism of comonoids"):

δ                         δ
!X -----> !!X          !X ----------> !!X
\       |            |              |
e \      | e        Δ |              |
\     v            v    δ⊗δ       v
---> ⊤          !X⊗!X ------> !!X⊗!!X


8. The term calculus
====================
The new rule:

a;b|-c  a|-b  a|-db
(Dt)     -------------------
a|-c_{b}db

or, in long form:

a:A,b:B|-c(a,b):C   a:A|-b(a):B   a:A|-db(a):B
----------------------------------------------
a:A|-c_b(a,b(a))db(a):C

The equations ([S07], slide 20): the usual ones (?), plus these:

(Dt.1)   (c+c')_{b}db=c_{b}db+c'_{b}db
0_{b}db=0

(Dt.2)   c_{b}(db+db')=c_{b}db+c_{b}db'

(Dt.3a)  b_{b}db=db

(Dt.3b)  c_{(b,b')}(db,0)=c_{b}db
c_{(b,b')}(0,db')=c_{b'}db'

(Dt.4)   (c,c')_{b}db=(c_{b}db,c'_{b}db)

(Dt.5)   e_{b}db=e_{c}c_{b}db

(Dt.6)   (c_{b}db)_{db}db'=c_{b}db'


9. The term calculus: long version
==================================
Longer version, showing all the hypotheses:

a,b|-c   a,b|-c'   a|-b   a|-db
(Dt.1)   --------------------------------
a|-(c+c')_{b}db=c_{b}db+c'_{b}db

[a,b|-0]   a|-b   a|-db
-----------------------
a|-0_{b}db=0

a,b|-c   a|-b   a|-db   a|-db'
(Dt.2)   ---------------------------------
a|-c_{b}(db+db')=c_{b}db+c_{b}db'

[a,b|-b]   a|-b   a|-db
(Dt.3a)  -----------------------
a|-b_{b}db=db

a,b,b'|-c   a|-b   a|-b'   a|-db
(Dt.3b)  --------------------------------
a|-c_{(b,b')}(db,0)=c_{b}db

a,b,b'|-c   a|-b   a|-b'   a|-db
--------------------------------
a|-c_{(b,b')}(0,db')=c_{b'}db'

a,b|-c   a,b|-c'   a|-b   a|-db
(Dt.4)   ----------------------------------
a|-(c,c')_{b}db=(c_{b}db,c'_{b}db)

a,b,c|-e   a,b|-c   a|-b   a|-db
(Dt.5)   ----------------------------------
a|-e_{b}db=e_{c}c_{b}db

a,b|-c   a|-b   a|-db   a|-db'
(Dt.6)   ------------------------------
a|-(c_{b}db)_{db}db'=c_{b}db'


10. The D combinator
====================
In the categorical setting the D works like this:

dx,x       x
-        -
|D[f]    |f
v        v
dy        y
(=y_{x}dx)

In the term calculus the derivative works on one of the variables, not
on all at once, so we need a trick to convert between the two:

a
-
|<<⟦a|-db⟧,0>,<⟦a|-b⟧,1>>
v
(db,0),(b,a)            b,a
-                   -
|D[⟦a,b|-c⟧]        |⟦a,b|-c⟧
v                   v
c_{(b,a)}(db,0)          c
=c_{b}db
=dc

So:

⟦a|-c_{b}db⟧ := <<⟦a|-db⟧,0>,<⟦a|-b⟧,1>> D [⟦a,b|-c⟧]

[Note: [S07] uses "b" before "a"...]

In the other direction,

D[⟦x|-y⟧] = dx,x|-y_{x}dx

(dx,x),x'|-y    dx,x|-x    dx,x|-dx
-----------------------------------
dx,x|-y_{x}dx

a,b|-c  a|-b  a|-db
(Dt)     -------------------
a|-c_{b}db

And the other direction?