Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: questions

Topic: Forward derivative composition pattern


view this post on Zulip Spencer Breiner (Jun 21 2021 at 18:16):

Much ink has been spilled in recent years based on the observation that reverse differential composes according to the Lens pattern. I'm wondering if there is a name for the corresponding pattern for the forward derivative? These should be related to opfibrations in a similar way that lenses are related to pointwise-opposite fibrations.

I'm generically interested in monoidal categories, rather than just Cartesian, so I'm looking for a definition something like this:
???((XX),(YY))=Z:CC(X,YZ)×C(ZX,Y)\mathrm{???}({X\choose X'},{Y\choose Y'})=\int^{Z:\mathbf{C}}\mathbf{C}(X,Y\otimes Z)\times\mathbf{C}(Z\otimes X',Y')

If it doesn't have a name yet, I'm tempted to call it a "fiber optic", since it models message-passing and I don't know any other optical components that aren't already taken (lenses, grates, prisms, etc.). Unfortunately, the term "fiber" is already overworked here, so I'm open to other suggestions.

view this post on Zulip Jules Hedges (Jun 21 2021 at 19:13):

When your base category is cartesian (in which case this category is fibrewise opposite of lenses), this category is called (the total category of) the "simple fibration" in Jacobs' Categorical Logic & Type Theory, it's a major topic of that book. Also in the cartesian case, in David Jaz Meyers' current draft book he calls these morphisms charts, and in Strathclyde we have recently been calling the general thing charts too. But it's early enough days that we could easily switch to calling them anything

view this post on Zulip Ben MacAdam (Jun 21 2021 at 21:48):

I think if you look at some of the Blute-Cockett-Seely papers on Cartesian Differential (Storage) Categories, you'll see they spend quite a bit of time talking about the simple fibration and how it relates to differentiation. I think a forward mode derivative is exactly a section of the simple fibration that satisfies some axioms, just as a reverse derivative is a section of the dual fibration to the simple fibration that satisfies some axioms (although I haven't thought about CDCs or RCDCs much at all lately, so I may be mistaken).

view this post on Zulip Jules Hedges (Jun 21 2021 at 22:05):

That's reassuring to know

view this post on Zulip Jules Hedges (Jun 21 2021 at 22:07):

When the base is just monoidal I don't think there's such a strong relationship between the 2 categories, since neither of them is a fibration

view this post on Zulip Spencer Breiner (Jun 21 2021 at 22:13):

Thanks for the pointer to the storage categories. That terminology is new to me, but it's no surprise they that they needed to work out the details of the construction. In the Cartesian case there is less need for new terminology, because we have this tight connection with fibrations. In the monoidal case I think the fibration/section gets replaced a coend, just like in the lens -> optic generalization.

What is the intuition behind the "chart" terminology? I couldn't immediately find the DJM draft that you mentioned.

view this post on Zulip Matteo Capucci (he/him) (Jun 22 2021 at 09:48):

Spencer Breiner said:

What is the intuition behind the "chart" terminology? I couldn't immediately find the DJM draft that you mentioned.

Here's the book Jules is talking about, though the main ideas are condensed in this extended abstract

view this post on Zulip Matteo Capucci (he/him) (Jun 22 2021 at 09:49):

The intuition is that a charts are maps between boundaries of systems, maps which do not represent interaction though, but simply a mapping

view this post on Zulip Matteo Capucci (he/him) (Jun 22 2021 at 09:51):

Indeed the main use of charts is to arrange two of them between the two boundaries of a system, hence producing a square whose vertical sides are lenses (representing a system dynamics) and whose horizontal sides are charts (representing a system being 'charted' into another)

view this post on Zulip Matteo Capucci (he/him) (Jun 22 2021 at 09:51):

All in all, these squares are a sophisticated version of simulations

view this post on Zulip Spencer Breiner (Jun 23 2021 at 21:51):

Following the previous discussion, I am now trying to understand @David Jaz's formulation of dynamical systems as double categories. I would like to understand better the formal analogy between a dynamical systems doctrine as a section of a bundle map and a vector field as a section of the tangent bundle.

(i) Presumably some part of the classical theory of differential equations (e.g., local existence of solutions?) should literally fall out by interpreting the general construction in the right context. What do the contexts/bundles/etc. look like here? For example, do we turn the base space into a category of open sets or a category of paths? Probably there are different routes one could take.

(ii) When we think about a vector field as defining an object of some doctrine of continuous dynamical systems, is this some kind of microcosm principle? I don't really know what that means, but I'd be curious whether it is and, if so, whether that tells us anything useful.

Probably the answer is "Go read the book", which I will hopefully get to some day.

view this post on Zulip Matteo Capucci (he/him) (Jun 24 2021 at 17:43):

I don't understand (i), but my answer to (ii) is a resounding 'yes!'