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: community: our work

Topic: Jean-Baptiste Vienney

Jean-Baptiste Vienney (Dec 12 2021 at 03:13):

Hi everybody, I'm a french student in last year of engineering school and second year of master degree in mathematics/theoretical computer science. I'm not really sure of what I'm going to do next year. It seems difficult to me to get a paid a PhD somewhere as I'm far more excited by the work I'm going to explain than my courses.

I have some ideas related to linear logic which I want to develop. Let me explain this. At the beginning, there was linear logic (1987). After that came differential linear logic (around 2002) and differential categories (2006). There is also "A Categorical Quantum Logic" (2005) which is basically compact multiplicative linear logic with bi-products. I'm interested by the fact that some mathematical mechanism can be described in a more combinatorial way by logical systems, forgetting the details of the model and concentrating on the pure calculus. In linear logic, we are dealing with kind of linear mechanisms. In differential linear logic, we are dealing with linearity and differentiation. If we want to interpret this in vector spaces, we need infinite dimensional ones. What has been done with "A Categorical Quantum Logic", is adapting linear logic to the category of finite dimensional vector spaces (or finite sets if you want) but without the exponentials. Recently, @JS Pacaud Lemay (he/him) proved that the category of finite dimensional vector spaces cannot be endowed with a nontrivial structure of co-differential category. Differential or co-differential categories are similar to categorical models of differential linear logic where you forget additional structure and generalize a little to concentrate on differentiation. The intuition I think is that the exponentials of linear or differential linear logic are not compatible with finite dimensionality, they always produce infinite dimensional vector spaces. This is where a fifth system come in the game : bounded linear logic (1991), more precisely a very simple version of bounded linear logic. In the introduction of the paper, Girard (I guess because of the style but there are other writers) explains clearly that the goal of this logic is to concentrate on finite stuff. To do this he uses indexed exponentials which are in the simple version $!_{n}$ where $n \ge 0$ give the maximum number of times you can use the resource. I made the link with the work of JS, and it gives me the idea to introduce a new kind of differential category with such an indexed exponential, which I name graded differential categories. We are actually discussing of that with JS. Well, this is an interesting beginning, it gives some categorical structure to talk about polynomials for instance. But, there is more exciting. I want to see how to extract more dynamics from the category of finite dimensional vector spaces and doing a logic with that. One solution is to add such indexed exponentials to the "Categorical Quantum Logic". So, in the logic, you will have $!_{n}A$ and this is auto-dual : $(!_{n}A)^{\perp} = !_{n}A^{\perp}$. The most natural way to interpret this logic is to say that $A$ is a finite dimensional vector space and that $!_{n}A = A^{\otimes_{s}n}$. So this give you a logic of finite dimensional vector spaces and symmetric powers. I think a cool name could be "Linear Logic S" with a S like symmetric powers but also because it seems very related to $\lambda$-rings, but expressed with the operators $s^{n}$ and not the $\lambda^{n}$. I think this logic is really really interesting : it should express the equations of a $\lambda$-ring but in asymmetrical manner : you have all the natural morphisms and if you take the isomorphism classes of propositions, you get a $\lambda$-ring. The cut elimination seems really combinatorial and more beautiful than the one of linear logic or differential linear logic. I'm really wondering if it can mean something in quantum mechanics. I think you can also interpret $!_{n}A$ by a truncated Fock space $\underset{0 \le k \le n}{\bigoplus}A^{\otimes_{s}k}$, so it may signifies something. You also naturally have differentiation in this logic, but this is more differentiation of polynomials. This can really be an important logic for me : this is a descendant of all the descendants of linear logic, this can be related to quantum mechanic and this is similar to $\lambda$-rings.

Well, I wanted to explain this here because I'm really frustrated of not being able to communicate on this and not have any return. I'm also interested by the concept of public research as explained in another post. I hope somebody will read this and find it interesting. I don't know very much about $\lambda$-rings also and I know that there are some specialists here (like @John Baez and @Todd Trimble ) which can also be interested by linear logic. I looked at this thing because it's related to symmetric powers which seems important to me because they are everywhere in mathematics and thus it seems natural to me to integrate them in some logical system.

So my To-do list :

• Finish to write the paper on graded differential categories, maybe with JS.
• Write a paper to present linear logic S.
• Working on some other categorical/linear logical stuff related to this that I didn't explain but less interesting.
• Obtain my engineer degree and my mathematics degree.
• Finding what I do next year.

Morgan Rogers (he/him) (Dec 12 2021 at 12:04):

I'm happy to see another person with less experience contributing to this stream! Good luck with pursuing this project.
While I can sort of understand your optimism of capturing new operators into your logic, have you considered what these might mean on the logic side (how should it be interpreted, besides the specific semantics you've explained)?
Re the name (this is an issue I personally care about more than is reasonable): a letter is almost always a bad choice for a name, since it doesn't intrinsically carry any of the meaning you want it to convey. Take $\lambda$-ring, for example; if you hadn't met those before, the $\lambda$ could represent any of the things that $\lambda$ represents through maths, physics or computer science (it would arguably be more evocative it were at least a capital $\Lambda$ heh...)
Don't fix a name for this logic yet; find out what it does and how it behaves, and then give it a name that conveys that.

Jean-Baptiste Vienney (Dec 12 2021 at 13:31):

Concerning the name, I totally understand what you say, clarity is always better. It can be a good idea to fix the name at the end.

Now, concerning what this logic means : I don't know what can precisely be the usefulness of this is logic. But I have some reasons of considering it, I can say this, directly related to proof theory :

• I'm interested by finitism. In linear logic, a proof of $!A \vdash B$ can be interpreted as an algorithm which produces an output of type $B$ from an input of type $A$, used as many times as you want (maybe an infinite number of time). If you use $!_{n}$, a proof of $!_{n}A \vdash B$ is an algorithm which produce the output of type $B$ by using at most $n$ times the input of type A (or by using exactly $n$ times the input, I'm not really sure about this, the original interpretation in bounded linear logic is the first but it can be coherent to interpret with the second). This seems really more realistic to use $!_{n}$ than $!$ to describe algorithms. In any case, it also express a symmetry in the input : if you say that you use $n$ different entries of type A, which can be also an interpretation, the algorithm must be symmetric in these entries. These things are more easily interpreted with symmetric powers, the most simple is in the category of finite sets, if $A$ is a finite set, you can say that $!_{n}A$ is a multiset of $n$ elements in $A$. $\textit{The link with symmetric powers was not made in the paper on bounded linear logic}$. Now, it seems very natural for me. The goal was to interpret polynomial-time algorithm, and I now interepret a proof of $!_{n}A \vdash B$ directly as a polynomial application with symmetric powers, in the category of finite sets or finite dimensional vector spaces, as you want. So we go $\textit{from polyomial-time algorithm to polynomial applications}$.
• The passage from linear logic to differential linear logic was just this : in our models we have analytic functions that we can differentiate, $\textit{let us add proof rules to differentiate directly in the syntax}$. Here, I say, in our models we have polynomial application, so we do the same in order to being able to differentiate directly in the syntax.
• To differentiate, you add co-structural rules to the structural rules : co-dereliction, co-contraction and co-weakening. In fact, this is not directly differentiation which is given by these rules. $\textit{You symmetrize the structural rules and it makes sense}$. This is exactly the same here.
• It seems to me that the most symmetric logics are the most interesting ones. Another solution to symmetrize linear logic is to put $\otimes = (par)$ and $\oplus = \&$. This is what we do here. in addition to add co-structural rules. So, I want to understand what this $\textit{most symmetrical logic ever}$ means.
• But in fact, you can forget the previous point, and $\textit{you (can) just obtain a graded differential linear logic}$.

Jean-Baptiste Vienney (Dec 12 2021 at 13:47):

Now, what is the most general semantics ? $\textit{The easiest semantic is any compact closed category with biproducts and symmetric powers.}$ But this is just the most simple one.
If you want something complete, you can say :

• A compact closed category with biproducts
• with a graded co-monad $(!_{n})_{n \ge 0}$
• such that for any $A$, $(!_{n}A)_{n \ge 0}$ is a graded bimonoid
• with some coherence conditions

Maybe it gives you something like a graded bi-monad, maybe this is a monoidal monad... I'm not sure with the details.

Jean-Baptiste Vienney (Dec 12 2021 at 13:57):

A big question for me is : $\textit{What it means for quantum mechanics/computing ?}$
This is an extension of the categorical quantum logic by Ambramsky/Duncan. It seems that you can interpret $!_{n}A$ by a truncated Fock Space. $\textit{Does it allow you to express diagrammatically new quantum things ?}$ This is surely the case, but I'm not more familiar with Fock spaces and quantum field theory than with $\lambda$-rings. This is why, I would be very happy if somebody here understand this better than me.

Jean-Baptiste Vienney (Dec 12 2021 at 14:26):

But a big problem in this story is that if I don't find a PhD scholarship anywhere in the world, this logic will surely go to the trash. I hope it can be saved from such a bad fate even if I continue as a computer science engineer next year which is surely what I'm going to do.

I've interpreted "our work" := "our work in mathematics" which is more and more hardly equal to "our work to earn money".

Nicolas Blanco (Dec 12 2021 at 15:42):

Salut Jean-Baptiste,
That is quite interesting. Let me share a few quick thoughts.
I had a brief exchange with Mehrnoosh Sadrzadeh on Friday. It seems that lately she has been using truncated Fock spaces to act as a bounded exponential for f.d. vector spaces. This is in a linguistic context but you are probably aware of the tight connections between DisCoCat and CQM (Categorical Quantum Mechanics). So it might be of interest to you.
On my hand, I have been meaning to look more closely at the case of finite dimensional normed vector spaces. There is a great paper by Cockett, Seely and Blute on using Fock spaces as a model of exponential, especially in the case of Banach spaces. They make an interesting connection to holomorphic function at the end of the paper.
As a remark this example is not compact closed but properly *-autonomous.
About the PhD, I know how frustrating looking for fundings can be - I am myself looking for a postdoc position and it is exhausting ;) you should talk about your ideas with as much people as possible (this post is great for that). The ChoCoLa seminar is for example a great opportunity to met linear logicians.
Even if you don't manage to find fundings for this year and you go into an engineering position it doesn't mean that you will have to give up research. I did two years as an engineer between my LMFI master and my PhD and it was a great experience.
With your interests you might want to apply to Cambridge Quantum Computing or into a formal methods engineer position for example. At Clearsy, where I was working, they were several other people coming from LMFI. There are a some other companies that would be interested in people with a logic background and a few in people with a category theory background. If you need any pointers, feel free to ask.
More generally, I would be glad to discuss about research or anything of you want to. I won't have a lot of time in the near future but I can always make some room for a zoom meeting, or a meeting in Paris if you are near.

Jean-Baptiste Vienney (Dec 12 2021 at 16:36):

Salut Nicolas,
Oh, thank you for your support ! There are a lot of interesting things for me in your message. I'm going to think to all of that and surely ask you questions after.

Jean-Baptiste Vienney (Dec 12 2021 at 16:44):

Honestly I don't know DisCoCat. I'm very glad that somebody uses truncated Fock spaces. I didn't know so much if this thing is used. I've only seen that in theoretical physics paper by testing if "truncated" + "Fock spaces" gives something on Google.

Jean-Baptiste Vienney (Dec 12 2021 at 16:46):

I don't really understand what it will change if you take finite dimensional normed vector spaces instead of finite dimensional vector spaces. Is there anything who change on the categorical side ? Ah si, this is maybe better for differentiation. But if you are interested only by the multiplicative part, I don't know. Why do you use the norm ?

Jean-Baptiste Vienney (Dec 12 2021 at 16:54):

Yes, I know the paper of Cockett, Seely, Blute ! It should have play in important role for linear logic. It seems to me that it is the first to talk about differentiation. I've talked of these things with Blute, I'm probably going to do an internship at Ottawa with him this year.

Jean-Baptiste Vienney (Dec 12 2021 at 16:58):

Did you do research while you was working as an engineer ? I was thinking that with some more time, I can publish some papers and after that it will be easier to find a funding.

Jean-Baptiste Vienney (Dec 12 2021 at 16:59):

Oh I didn't know about Clearsy, it is near from me. I'm in Marseille.

Jean-Baptiste Vienney (Dec 12 2021 at 17:01):

Well, maybe I will contact you to know about your engineering experience and other things.

Alex Gryzlov (Dec 12 2021 at 23:15):

There's a programming language project called Granule which uses graded linear logic for expressing properties about resource usage in programs, it might be somewhat related.

Jean-Baptiste Vienney (Dec 12 2021 at 23:46):

Thank you ! I think the principal difference with what I propose is that there is not the co-structural rules which make the graded logic a differential logic (also not the compacity and biproducts but less important). But it seems to be a modern version of linear logic with graded exponentials, cool ! Basically my thing is graded differential linear logic or graded compact differential linear logic with bi-products. This is maybe the best names for these things.

Jean-Baptiste Vienney (Dec 12 2021 at 23:59):

Oh, I've just seen something very cool @Alex Gryzlov , the Granule project is recruiting somebody for a PhD beginning in august 2021 on something related to graded modality. It's maybe an occasion for me even it's not exactly my thing.

Jean-Baptiste Vienney (Dec 13 2021 at 00:13):

I’ve confused 2021 and 2022 :grinning_face_with_smiling_eyes: but no matter, maybe they will want somebody else for august 2022.

Jean-Baptiste Vienney (Dec 13 2021 at 00:16):

Or maybe we can discuss whether we can differentiate their programs.

Alex Gryzlov (Dec 17 2021 at 12:54):

By the way @Jean-Baptiste Vienney, if you're interested in modal logics and program verification, the lab of Aleks Nanevski in Madrid (where I currently work) is also looking for a category theorist (PhD/postdoc) to work on separation logic (formulated as a modal-like type theory) and/or effect systems.

Jean-Baptiste Vienney (Dec 17 2021 at 17:19):

Thank you ! But I want nevertheless to work on my project. At some point, it becomes more interesting for me to go working alone in some hut in mountains because my primarily goal is to understand something to the questions I ask myself and not only become a researcher.

But this position is for when @Alex Gryzlov ? I'm looking for something beginning around september 2022, not now.

Alex Gryzlov (Dec 17 2021 at 17:20):

I don't think there's a specific deadline for now, next year should be fine.

Jean-Baptiste Vienney (Dec 17 2021 at 17:21):

Ok, I remember this if the other possibilities don't work !

Nicolas Blanco (Jan 04 2022 at 14:11):

Salut Jean-Baptiste,
Sorry for the late reply and happy new year.

For the finite dimensional normed vector spaces, the point is that when you consider the category where the morphisms are contractive linear maps (maps that don't increase the norm) instead of bounded maps, you get a *-autonomous category where the par and the tensor are different while for vector spaces they are both interpreted by the tensor product. Similarly, the plus and with are distinct while in vector spaces they are given by the direct sum. I would be interested in looking at exponentials and differentiation in this context but I haven't yet.

To be fair, I didn't have time to do research as an engineer. The only time when I did, was when I was applying for the PhD. I would come back home from a day of work and write research proposals and stuffs. It was quite stressful though, and I wouldn't recommend turning it into a daily routine :sweat_smile:

There are more and more companies that are applying formal methods and similar. Though most of the ones I know in France don't do much research. When they allow their engineers to do some research most of the time it is after a couple of years of experience as an engineer, it is on really applied and concrete stuff and it is between 10 to 20% of your workload. It was the case at Clearsy for example.

Feel free to contact me, if you want to know more.

Jean-Baptiste Vienney (Aug 13 2022 at 05:29):

I’ve applied for giving a talk at Categories and Companions Symposium 2022 (CaCS2022) (on Zoom!).

Title : Differential and bialgebraic characterizations of symmetric powers

Abstract : In a $\mathbb{Q}^{+}$-linear symmetric monoidal category, symmetric powers can be defined as a special kind of split idempotent. The $n^{th}$ symmetric power of a R-module is the space of formal homogeneous polynomials of degree $n$ in the vectors of the module. By using ideas from differential categories, we can equivalently describe jointly all the symmetric powers of an object by means of two families of morphisms which express differentiation and multiplication of homogenous polynomials and must verify the Leibniz rule as well as the Euler identity. Equivalently it can be understood as bosonic annihilation and creation operators. A second characterization of all symmetric powers is in term of a special kind of graded bialgebra. We introduce the new concepts of graded differential category and special graded bialgebra on the road and explain that symmetric powers are also characterized as forming a special kind of graded codifferential category that we name homogeneous polynomial codifferential category.

Jean-Baptiste Vienney (Aug 30 2022 at 18:03):

Starting from the graph at the top and using the two rewriting rules in the top left corner, there is exactly one path to generate every permutation of $\mathfrak{S}_{n}$. This image is a proof of the case $n=4$. I'm so excited about this!! I will explain this in my talk and in a forthcoming paper!! bi4graphs.jpg

Jean-Baptiste Vienney (Nov 02 2022 at 20:15):

I've been accepted in PhD at the University of Ottawa, with Rick Blute and Phil Scott, to start in January!

Jean-Baptiste Vienney (Dec 07 2022 at 06:52):

I've been working for the last 6 months to find this statement and then prove it:

Theorem: Let $\mathcal{C}$ be a symmetric monoidal $\mathbb{Q}^{+}$-linear category with unit $I$. Let $(A_{n})_{n \ge 0}$ be a graded object in $\mathcal{C}$. Then $(A_{n})_{n \ge 0}$ is the family of the $n^{th}$ symmetric powers of $A_{1}$ if and only if there exist maps $(\nabla_{n,p}:A_{n}\otimes A_{p} \rightarrow A_{n+p})_{n,p \ge 0}$, $(\Delta_{n,p}:A_{n+p} \rightarrow A_{n} \otimes A_{p})_{n,p \ge 0}$, $\eta:I \rightarrow A_{0}$ and $\epsilon:A_{0} \rightarrow I$ such that these axioms are verified (with the obvious string diagram notations and where I write $n$ instead of $A_{n}$): axioms.png

A surprising fact is that there is no need to suppose any associativity, coassociativity, commutativity and cocommutativity: it's consequences of these axioms.

The proof is nothing but easy. I'm really close to the end. I hope to have finished writing it and the paper associated before January 1st. Then I will send it to Rick and Phil in order that they proofread it, and then submit it, and it will be my first paper and first chapter of my PhD thesis.

They have been nice enough to say that I will be the only author.

I think it's gonna be an important step in the story of the relation between linear logic and Fock spaces as started 30 years ago in Fock space: A Model of Linear Exponential Types, R. Blute, P. Panangaden, R. A. G. Seely (1994). This first intuition is going to be transformed in an actual logic of symmetric powers which says everything about them instead of just an incomplete semantic of linear logic.

Ideas from differential linear logic, graded linear logic, differential categories and categorical quantum mechanics have been taken into account in order to find this theorem.

Moreover, it presents symmetric powers as a special kind of connected graded Hopf algebra which are the object of current research in link with renormalization:

Renormalization in connected graded Hopf algebras

There is a lot of work to pursue after this first theorem and it will be the next chapters of my thesis but I'm not gonna reveal all my plans :smile: .

Jean-Baptiste Vienney (Jan 08 2023 at 21:14):

I'll give a talk at the Logic Seminar of the University of Ottawa, on January 25 at 3pm.

Title: Characterizing symmetric powers bialgebraically: a first step into the logic of usual linear mathematics

Abstract: I will first describe how we can hope for logical systems which would be able to prove isomorphisms or more generally equations encountered in various parts of linear mathematics eg. representation theory, homological algebra, algebraic topology… Examples of such isomorphisms or equations: Künneth theorem, Schur-Weyl duality, algebra of Schur functors, binomial theorem.

We will then start this program with a first modest step: I will state a bialgebraic characterization of symmetric powers (in symmetric monoidal Q+-linear categories) and go through the main steps of the proof. This theorem is meant as a preliminary to a logic of symmetric powers in characteristic 0.

Jean-Baptiste Vienney (Jan 08 2023 at 21:15):

If some people are interested, here is the zoom link for this seminar:
https://us02web.zoom.us/j/82110770520?pwd=dmdIcmMwKzgvM3hSZWIrR1kzUVpyUT09

Jean-Baptiste Vienney (Feb 11 2023 at 06:43):

I'm really happy to have been invited to give a (virtual) talk at the National Institute of Informatics in Tokyo by Shin-ya Katsumata! I'll talk about our project of graded differential categories / linear logic with @JS PL (he/him) as well as maybe some of my other ideas about graded linear logical mathematically inspired stuff! Shin-ya is really an expert on the subject of graded linear logic so that's great to reach him. But that's thanks to JS who told him about that!

Jean-Baptiste Vienney (Feb 12 2023 at 13:13):

Here is the deal for this talk.

Title: Graded differential categories and some other graded ideas

Abstract: Graded differential categories grade the exponential of differential categories by a rig. It allows more flexibility. Diff cats can be seen as the $0$-graded diff cats. In any symmetric monoidal category $\mathcal{C}$, coequalizer symmetric powers make $\mathcal{C}^{op}$ a $\mathbb{N}$-graded diff cat.

If we look at the characteristic $0$ case where $\mathcal{C}$ is enriched over $\mathbb{Q}^+$-modules, we obtain an equivalent definition of symmetric powers as a structure of $\mathbb{N}$-graded diff cat on $\mathcal{C}^{op}$ which verifies an additional axiom.

We can write a sequent calculus for graded bialgebra modalities with codereliction which are a special case of graded diff cats, realizing the idea of graded differential linear logic. If we allow the multiplication of proofs by coefficients in $\mathbb{Q}^+$, forcing the exponential to give symmetric powers can now be done syntactically by equating proofs under a form of $\eta$-equivalence involving the inference rules for the graded exponential.

I’ll say a word about Seely isomorphisms. Surprisingly it seems not possible to prove a graded version of the Seely isomorphism by adding additive connectors to graded linear logic. The costructural inference rules seem necessary making the graded Seely isomorphism a feature of graded linear logic specific to the differential extension.

I’ll explain how the differential graded story is better understood with the notion of Hasse-Schmidt derivative used in positive characteristic mathematics and how it simplifies equations or cut elimination when dealing with differentiation logically.

Finally, I’ll share some ideas about how combining graded exponentials with costructural inference rules could be adapted to make some mathematical concepts closer to logic such as Schur functors, modular representation theory of the finite general linear groups and the Steenrod algebra, or cyclic homology.

The work on graded diff cats has been done in collaboration with @JS PL (he/him) . I also thank my supervisors Rick Blute and @Philip Scott , as well as @John Baez and @Sacha Ikonicoff for usefull discussions on these matters.

John Baez (Feb 13 2023 at 02:14):

Is it too late to offer editorial corrections to this abstract?

Peter Arndt (Feb 13 2023 at 06:52):

Is it too late to ask for a link to the talk?

Jean-Baptiste Vienney (Feb 13 2023 at 08:05):

Hey, none of the two is too late

Jean-Baptiste Vienney (Feb 13 2023 at 08:13):

The talk should be on March 1. I just sent the abstract very early because I was too impatient.

Jean-Baptiste Vienney (Feb 13 2023 at 08:13):

John Baez said:

Is it too late to offer editorial corrections to this abstract?

Tell me! I gladly accept your offer.

Jean-Baptiste Vienney (Feb 13 2023 at 08:14):

Peter Arndt said:

Is it too late to ask for a link to the talk?

I'll ask Shin-ya. Thanks for your interest!

Jean-Baptiste Vienney (Feb 13 2023 at 08:15):

I guess there are already corrections to make on the English ahah.

Jean-Baptiste Vienney (Feb 13 2023 at 22:57):

What did you want to change to this abstract @John Baez?

Jean-Baptiste Vienney (Feb 13 2023 at 22:59):

I can still send a better version.

John Baez (Feb 13 2023 at 23:19):

Various things, starting with the singular-plural conflict here:

Graded differential categories grade the exponential of differential categories by a rig. It allows more flexibility.

"It" should be "they" since you are referring to a plural: "graded differential categories".

Jean-Baptiste Vienney (Feb 13 2023 at 23:21):

Hmm okay for this one. It's something which works in French but not in English apparently.

John Baez (Feb 13 2023 at 23:22):

Also, I don't know what "graded the exponential by a rig" means. I can try to guess what it means. You mean the hom-objects in a differential category become graded by a (fixed?) rig?

Jean-Baptiste Vienney (Feb 13 2023 at 23:23):

Oh no. It the exponential endofunctor $!:\mathcal{C} \rightarrow \mathcal{C}$ which is replaced by a family $(!_{r}:\mathcal{C} \rightarrow \mathcal{C})_{r \in R}$

Jean-Baptiste Vienney (Feb 13 2023 at 23:24):

Yes it's a fixed rig.

Jean-Baptiste Vienney (Feb 13 2023 at 23:25):

For instance you can take a grading on $\mathbb{N}$, $\mathcal{C}=FVec$ and $!_{n}A$ the $n^{th}$ symmetric power of $A$

John Baez (Feb 13 2023 at 23:25):

Okay, I get it. Thanks.

So here's my real point: I suspect very few people will understand the sentence "Graded differential categories grade the exponential of differential categories by a rig", since it probably requires understanding the word "rig" and some other concepts, and I doubt many people know all these things. I recommend a more gentle, friendly approach, since people tend to avoid talks where they can't understand even the first sentence of the abstract.

An abstract for a talk is an advertisement, not a summary of results.

Jean-Baptiste Vienney (Feb 13 2023 at 23:28):

Hmm okay. Are rig something really exotic for a computer scientist ?

John Baez (Feb 13 2023 at 23:36):

I don't know - I'm a mathematician. Most mathematicians don't know what rigs are, they don't know what differential categories are, and they don't know what "grading the exponential" means.

John Baez (Feb 13 2023 at 23:37):

You could explain all these things in a few sentences to most mathematicians, but they wouldn't be able to swallow the first sentence of your abstract without help.

Jean-Baptiste Vienney (Feb 13 2023 at 23:38):

Okay. You're absolutely right, especially for differential categories. I'm gonna try to rewrite a little bit this.

John Baez (Feb 13 2023 at 23:43):

Great.

(Mathematicians have trouble writing advertisements because they're not used to it. I always have to remind my students that the "research statements" they need to write when applying for jobs are actually advertisements. The goal is not to explain math. The people reading them don't want to learn math. They want to know if they should hire you.)

Jean-Baptiste Vienney (Feb 14 2023 at 00:14):

What about that ? It is a more "marketing" and friendly version.

Title: Graded differential categories

Abstract:

Differential categories are categories when we can differentiate morphisms of type $!A \rightarrow B$. They were introduced as the models of differential linear logic which is an extension of linear logic which allows differentiation. On the other hand, graded linear logic is another extension of linear logic which replaces the exponential $!A$ by a graded exponential $(!_{r}A)_{r \in R}$ where the grade $r$ is taken in a rig $R$ (ie. a ring without negatives).

I’ll explain how to combine the two to obtain graded differential categories and graded differential linear logic. It allows new examples of semantics with the possibility of recovering the non-graded case by taking the rig equal to 0. It also allows to obtain a graded version of the Seely isomorphism $!(A+B) = !A \otimes !B$ of linear logic.

We will finish by seeing how combining the ideas of graded linear logic and differential linear logic in yet other ways could allow to introduce various mathematical notions other than differentiation into linear logic, shining a new light on them even from a purely mathematical point of view.

Jean-Baptiste Vienney (Feb 14 2023 at 00:19):

I'm happy to see what people other than me and @JS PL (he/him) think of this ahah.

Jean-Baptiste Vienney (Feb 14 2023 at 00:20):

Cause it's difficult to be in the head of people other than oneself.

John Baez (Feb 14 2023 at 00:21):

It's tons better! I suggest however that you say a word about this beast $!A$ before using that symbol. Linear logicians know what this $!$ means. A lot of mathematicians and probably computer scientists don't.

John Baez (Feb 14 2023 at 00:22):

You say it's an exponential, but only later.

Jean-Baptiste Vienney (Feb 14 2023 at 00:22):

Ok, I try to add this.

John Baez (Feb 14 2023 at 00:22):

(I don't know how many people know what "an exponential" is. When you first said it I thought you meant an object $X^Y$ in a cartesian closed category - that's another meaning of "exponential" in category theory.)

Jason Erbele (Feb 14 2023 at 00:23):

I'd be a lot more interested to see a talk with this abstract vs. the previous one.

A couple of nit-picky details

• "when we can" in the first sentence should probably be "where we can".
• As a native English speaker, "allows to" / "allow to" sounds awkward. "X allows one to Y" sounds more idiomatic than "X allows to Y". "It also could allow to introduce various..." would sound better (to me) as "It also could allow the introduction of various..."

John Baez (Feb 14 2023 at 00:23):

Yes, nobody says "X allows to Y" in English.

John Baez (Feb 14 2023 at 00:24):

You can say "food allows one to eat" or "food enables eating" but not "food allows to eat".

Jean-Baptiste Vienney (Feb 14 2023 at 00:26):

Ok, thanks! I'll try to correct this and give you a yet better version.

John Baez (Feb 14 2023 at 00:26):

It's already so much better I feel my work is done.

Jean-Baptiste Vienney (Feb 14 2023 at 00:28):

Just wait two minutes I do it right now that's funny ahah

Jean-Baptiste Vienney (Feb 14 2023 at 00:33):

Title: Graded differential categories

Abstract:

Differential categories are categories with an endofunctor $!$ (the exponential) such that we can differentiate morphisms of type $!A \rightarrow B$. They were introduced as the models of differential linear logic which is an extension of linear logic which allows one to differentiate proofs. On the other hand, graded linear logic is another extension of linear logic which replaces the exponential $!A$ by a graded exponential $(!_{r}A)_{r \in R}$ where the grading $r$ is taken in a rig $R$ (ie. a ring without negatives).

I’ll explain how to combine the two to obtain graded differential categories and graded differential linear logic. It gives new examples of semantics with the possibility of recovering the non-graded case by taking the rig equal to $0$. It also allows one to obtain a graded version of the Seely isomorphism $!(A \& B) = !A \otimes !B$ of linear logic.

We will finish by seeing how combining the ideas of graded linear logic and differential linear logic in yet other ways seems promising to introduce various mathematical notions other than differentiation into linear logic, shining a new light on them even from a purely mathematical point of view.

Jean-Baptiste Vienney (Feb 14 2023 at 00:34):

John Baez said:

It's already so much better I feel my work is done.

Ok, thanks !!

John Baez (Feb 14 2023 at 00:58):

Differential categories are categories with an endofunctor !

It looks like you are very excited about this idea. :upside_down:

Jean-Baptiste Vienney (Feb 14 2023 at 01:00):

Of course, it is the most important part of linear logic for me!

John Baez (Feb 14 2023 at 01:00):

Right, but I just meant that it looks like you're ending the sentence with an exclamation mark.

Jean-Baptiste Vienney (Feb 14 2023 at 01:01):

ahah ok, I didn't get it

Jean-Baptiste Vienney (Feb 14 2023 at 01:03):

The goal of my life right now is just to make all the usual endofunctors of $Vec$ into some kind of exponential of some kind of linear logic haha.

John Baez (Feb 14 2023 at 01:04):

The only thing I don't like is that you aren't starting with an example of this $!$ thing, so it sounds very abstract. I might say something like this:

For any vector space $V$ one can form the vector space of polynomials $!V$, and one can also differentiate polynomials. This makes the category of vector spaces into an example of a differential category. These categories were introduced as the models of differential linear logic: an extension of linear logic which allows differentiation.

John Baez (Feb 14 2023 at 01:04):

Or something sort of like that: something that gives the reader a concrete example to think about.

Jean-Baptiste Vienney (Feb 14 2023 at 01:08):

Okay good idea, I'll think to that for next time but I can't send another mail to give a third version ahah.

Jean-Baptiste Vienney (Feb 14 2023 at 01:09):

I definitely must think a little bit more before sending mails ahah.

Jean-Baptiste Vienney (Feb 14 2023 at 01:10):

Anyway, people in the local seminars often come to all the seminars of the place so it's not a big deal.

Jason Erbele (Feb 14 2023 at 01:42):

Something I like about your abstract revision that is missing in John's example-driven stub is the explicit connection between the name "exponential" and the symbol "$!$". Something like "... one can use the exponential endomorphism, $!$, to form the vector space of polynomials..." offers the best of both worlds. There may be better ways to phrase it, but this recipe of "this is what it's called, this is the symbol used, and this is (an example of) what it does" is convenient for quickly introducing terms and symbols that will appear later while also showing the readers why they might care about the ideas behind the jargon.

John Baez (Feb 14 2023 at 22:26):

Jean-Baptiste Vienney said:

Anyway, people in the local seminars often come to all the seminars of the place so it's not a big deal.

Maybe not, but learning to write good abstract is a big deal, so it's good to practice it before you give a talk for a job interview.

Even now it can make the difference between faculty who read your abstract and think "okay, another boring talk I have to go to" and faculty who think "hmm, this one actually sounds interesting!"

Jean-Baptiste Vienney (Feb 18 2023 at 06:30):

The video of my talk of January 25 at the University of Ottawa is now online: Characterizing symmetric powers bialgebraically: a first step into the logic of usual linear mathematics. I realised how terrible my accent is when I tried to hear it a bit but I guess you can understand what I say. And I'm glad that this stuff is online where there is enough time to explain a bit my ideas in a convenient way, even if it's very incomplete (In particular, there is nothing on graded differential categories / linear logic although I speak of differentiation from a little bit different point of view). But I tried to give some elements of overall inspiration for me like how I'm a little bit inspired by the philosopher Ludwig Wittgenstein and some other folks. At the end there are a lot of ideas to potentially import various things into linear logic like Schur functors and Cyclic homology.

Jean-Baptiste Vienney (Feb 18 2023 at 06:48):

I don't say it but for example I got interested by the idea of putting exterior powers in linear logic these last days, in order to be able to speak about the determinants of some proofs directly in the sequent calculus.

Jean-Baptiste Vienney (Feb 18 2023 at 06:50):

I hope it could help to prove that some isomorphisms of linear logic are really isomorphisms without directly checking it via cut elimination on $f;f^{-1}$ and $f^{-1};f$.

Jean-Baptiste Vienney (Feb 18 2023 at 07:00):

For a funny anecdote, last year I got an English-speaking girlfriend so my English was progressively getting better but now that it is finished I'm getting as bad as before.

Jacques Carette (Feb 18 2023 at 19:02):

Are the slides available online somewhere? I tend to want to read them first, before committing to watching a long talk.

vikraman (Feb 18 2023 at 19:52):

I'm curious about what a graded Seely isomorphism looks like, so I'd like to read about it too.

Jean-Baptiste Vienney (Feb 18 2023 at 20:41):

Sure, here it is: Slides Ottawa.pdf

Jean-Baptiste Vienney (Feb 18 2023 at 20:42):

What I mean by a graded Seely isomorphism appears slide 9

Jean-Baptiste Vienney (Feb 18 2023 at 20:44):

There should be clear explanations about this in our paper GDiLL and Graded Differential Categories with @JS PL (he/him) that should be submitted to MFPS 2023. And I will also speak more of it in my next talk so I'll put my slides as well if you want (it's not clear if I could give a zoom link for the talk).

Jean-Baptiste Vienney (Feb 18 2023 at 20:46):

That's an interesting point and I realized only when we started to write this paper that one needs a graded and differential linear logic to obtain Graded Seely isomorphisms

Jean-Baptiste Vienney (Feb 18 2023 at 20:47):

So it tends to validate that the differential part is important.

Jean-Baptiste Vienney (Feb 18 2023 at 21:47):

Here is the slides without pauses which should be easier to read: Ottawa-without-pauses.pdf

Jean-Baptiste Vienney (Feb 20 2023 at 22:23):

Peter Arndt said:

Is it too late to ask for a link to the talk?

I got it @Peter Arndt. Here is the link:

https://zoom.us/j/91882161000?pwd=NDFoSnR2K0RxR0VWRDN3YjN6bUZwQT09
meeting id: 918 8216 1000
passcode: 378062

Wed 1 March, 8pm in EST

For the talk "Graded differential categories" with abstract somewhere above.

Peter Arndt (Feb 22 2023 at 11:16):

Thanks! I'll see whether my baby wakes me up at 2am of my timezone to attend the talk :baby:

Jean-Baptiste Vienney (Mar 01 2023 at 23:55):

Hi, just want to say that you can connect in this link in an hour and an half if you want to learn and discuss about "Graded differential categories, Graded differential linear logic and Symmetrized powers " and make a virtual visit in Tokyo! Or if you're bored and not sleeping in your part of the world and don't know what to do.

I will talk about these things which I know can interest a few ones! :

• The Graded Seely isomorphism: how we need the differential part of graded differential linear logic to obtain it and why it's mysterious! (I understood a few things last night!)
• The cyclic list functor (just one slide but I can say more! I have a graphic tablet and plenty of blank space on my slides and I think my talk is not very long) that many people talked about here a few days ago. I will not say if it gives a (graded) monad or not but I least I can explain my approach which is quite structured I think!
• What I mean by the term "Symmetrized powers": it's a word for talking at the same time about various functors obtained by symmetrizing a tensor power $A^{\otimes n}$ in different ways, it includes symmetric powers, exterior powers, Schur functors, cyclic powers (cylic lists in $\mathbf{Rel}$) and the spaces which appear in the cyclic homology complex. There will be only a few words on this also but I can explain a little bit more what I'm trying to do.
• All of this started by combining differential linear logic / categories with the idea of graded exponential modalities ie a family $(!_{r}:\mathcal{C} \rightarrow \mathcal{C})$ of endofunctors, graded by a rig $R$, in an additive symmetric monoidal category. I will mostly talk about this. It started when I sent an email to @JS PL (he/him) during my masters program to solve his problem that $\mathbb{FVec}$ is not a differential category, so I told him, but it is a graded differential category, you can define this thing! Not exactly, I told him that the category of all Hilbert spaces is a graded differential category and not a differential category which was quite silly since it's much easier to see this in $FVec$ but we have forgotten this category since then. After this I went in Canada to work with Rick Blute and Phil Scott and then got accepted in PhD there. Today, it diffuses to Japan!

Jean-Baptiste Vienney (Mar 28 2023 at 04:03):

I'm going to submit this abstract for a talk at CT 2023 (and at the 2023 CMS Summer Meeting in Ottawa): String diagrams for symmetric powers

Jean-Baptiste Vienney (Mar 28 2023 at 05:20):

See here for a version with complete definitions: :grinning_face_with_smiling_eyes: Abstract-CT2023.pdf

Jean-Baptiste Vienney (Jun 03 2023 at 03:02):

Unfortunately I'm not going to present this stuff to CT2023 but I will do it monday at the CMS summer meeting and in one week at FMCS. Here are my slides:
slides.

Jean-Baptiste Vienney (Jun 03 2023 at 03:03):

Tell me if you want to make some remark! I think it's some funny stuff.

Jean-Baptiste Vienney (Jun 03 2023 at 03:07):

I'm almost done with the preprint, I hope it's going to be my second paper (and the first written alone)!

Jean-Baptiste Vienney (Jun 03 2023 at 03:18):

One of the thing I want to do with that later is modifying a bit my diagrams to obtain a characterization of symmetric powers in terms of bosonic annihilation and creation operators and then put this in dagger compact closed category to obtain a graphical language to talk about bosons.

Jean-Baptiste Vienney (Jun 03 2023 at 03:21):

I'm excited by trying to do some "categorical quantum field theory" in the same way that people do categorical quantum computing stuff with string diagrams

Jean-Baptiste Vienney (Aug 19 2023 at 06:39):

Jean-Baptiste Vienney (Aug 19 2023 at 06:44):

Today, I thought to products, and as crazy as it sounds, I think I found a different definition which is equivalent to the usual one. The main difference is that there is no longer the "unique" of the universal property in the definition. It's an algebraic characterization but different from the characterixation of a category which possesses all finite products as a monoidal category + some axioms because it applies to just the product of $A$ and $B$, and gives a different characterization (it also works for the product of a family of objects). I think it is usefull. I was very excited and I wrote a note about that that I could submit as a paper maybe but I prefer than some people read it before to be sure that I'm not crazy or that it is not trivial folklore. It's a very quick read (3.5 pages) and you can skip 90% of the intro, which is more or less two pages long, if it doesn't interest you (it speaks about how the idea come from linear logic and its cut elimination process, on the other hand this intro can excit you to learn about linear logic if you like the rest of the note). I think it can be interesting to anybody here. It's about one of the most basic idea of category theory.
A-note-on-products.pdf

Jean-Baptiste Vienney (Aug 19 2023 at 06:48):

I was excited today because the paper that I submitted two weeks ago passed the first step and they have invited the reviewers, so I know that it is not complet crap :upside_down:

Jean-Baptiste Vienney (Aug 19 2023 at 06:50):

Any feedback on this note would be heavily appreciated.

Aaron David Fairbanks (Aug 19 2023 at 07:02):

To me this looks like the definition of the product $A \times B$ as a representing object for the presheaf $\text{Hom}(-, A) \times \text{Hom}(-, B)$. The maps $\langle \cdot,\cdot \rangle$ are the components of the natural isomorphism $\text{Hom}(-, A) \times \text{Hom}(-, B) \to \text{Hom}(-, A \times B)$ and $(p_1, p_2)$ is the universal element in $\text{Hom}(-, A) \times \text{Hom}(-, B)$.

Jean-Baptiste Vienney (Aug 19 2023 at 11:17):

Ok, I didn't know about this definition. If you unpack the definition as a representing object, you get that you require for $A \times B$ to be a product extactly these conditions:
Data (1):

• (D1.a) for every object $X$, a function $Hom(X,A) \times Hom(X,B) \cong Hom(X,A \times B)$, that I will denote $(f,g) \mapsto \langle f,g \rangle_X$

Axioms (1):

• (A1.a) for every object $X$, $\langle . , .\rangle_X$ is bijective
• (A1.b) $\langle u;f, u;g \rangle =u;\langle f, g \rangle$ when it makes sense

Jean-Baptiste Vienney (Aug 19 2023 at 11:18):

But that's not exactly the hypotheses of Proposition 2.1

Jean-Baptiste Vienney (Aug 19 2023 at 11:26):

What I require for $A \times B$ to be a product is exactly:
Data (2):

• (D2.a) for every object $X$, a function $Hom(X,A) \times Hom(X,B)$, that I will denote $(f,g) \mapsto \langle f,g \rangle_X{}$
• (D2.b) a function $p_1:A \times B \rightarrow A$
• (D2.c) a funtion $p_2:A \times B \rightarrow B$

Axioms (2):

• (A2.a)$\langle 1_A, 1_b \rangle = 1_{A \times B}$
• (A2.b)$\langle u;f , u;g \rangle = u; \langle f, g \rangle$ whenever it makes sense
• (A2.c)$\langle f,g \rangle;p_1 = f$
• (A2.d)$\langle f,g \rangle;p_2 = g$

Jean-Baptiste Vienney (Aug 19 2023 at 11:30):

I agree that in the two cases, you ask for a fuction (D1.a) = (D2.a) which verifies (A1.a)=(A2.a).

Jean-Baptiste Vienney (Aug 19 2023 at 11:33):

But the rest of the two sets of conditions $(1)$ and $(2)$ are differents.

Jean-Baptiste Vienney (Aug 19 2023 at 11:33):

What are the differences?

Jean-Baptiste Vienney (Aug 19 2023 at 11:34):

In the set $(1)$ you ask for $(A1.a)$, the bijectivity condition.

Jean-Baptiste Vienney (Aug 19 2023 at 11:35):

Whereas in the set $(2)$, you get rid of this bijectivity condition $(A1.a)$. And the price you have to pay is to replace this single condition by the three equations $(A2.a)$, $(A2.c)$, $(A2.d)$.

Jean-Baptiste Vienney (Aug 19 2023 at 11:36):

I can compare $(2)$ to another set of conditions, and that is really what's behind this idea.

Jean-Baptiste Vienney (Aug 19 2023 at 11:38):

Let's write $(3)$ for the conditions in the usual definition of the product $A \times B$.

Jean-Baptiste Vienney (Aug 19 2023 at 11:40):

Data (3):

• (D3.a) for every object $X$, a function $Hom(X,A) \times Hom(X,B)$, that I will denote $(f,g) \mapsto \langle f,g \rangle_X{}$ (that's the function which will give the unique morphism in the universal property)
• (D3.b) a function $p_1:A \times B \rightarrow A$
• (D3.c) a funtion $p_2:A \times B \rightarrow B$

Jean-Baptiste Vienney (Aug 19 2023 at 11:42):

Axiom (3):

• (A3.a)$\langle f,g \rangle_X$ is the unique morphism from $X$ to $A \times B$ such that $\langle f,g \rangle_X;p_1=f$ and $\langle f,g \rangle_X;p_2=g$
• (A3.b)$\langle f,g \rangle;p_1 = f$
• (A3.c)$\langle f,g \rangle;p_2 = g$

Jean-Baptiste Vienney (Aug 19 2023 at 11:44):

You see what I'm doing: the data $(2)$ and $(3)$ are exactly the same but the axioms are different. Whereas $(A2.c)=(A3.b)$ and $(A2.d)=(A3.c)$, the rest is different.

Jean-Baptiste Vienney (Aug 19 2023 at 11:45):

You have one one side $(A2.a)+(A2.b)$, two equations that the data must verify, and on the other side $(D3.a)$, the unicity condition. My goal was exactly that: replace the unicity condition by equations.

Jean-Baptiste Vienney (Aug 19 2023 at 11:46):

That's why I say "[The definition] is stated in terms of an algebraic structure rather than a universal property."

Jean-Baptiste Vienney (Aug 19 2023 at 11:48):

So, I still think that it is a new and interesting observation. But I will be very happy to be contradicted.

Jean-Baptiste Vienney (Aug 19 2023 at 11:51):

Moreover I think that the distance between the usual definition and the one in terms of representing object is smaller than the one between each of these definitions and mine. The first two ask for some uncity or bijectivity, whereas mine doesn't ask for anything like that, just equations.

Jean-Baptiste Vienney (Aug 19 2023 at 11:54):

The fact that I write a function $\langle . , . \rangle$ in my definition is kinda distracting and you can rewrite it without this function. The real issue is to get rid of the "unique" in the usual definition or the "unique antecedent" of the bijectivity in the definition in terms of representing object.

Jean-Baptiste Vienney (Aug 19 2023 at 11:58):

I hope that with this further discussion, it's easier to evaluate my development, whether it's interesting / not interesting and known / not known. That's what I want to know.

Jean-Baptiste Vienney (Aug 19 2023 at 12:01):

Maybe I should add some kind of discussion like what's above in the note?

Jean-Baptiste Vienney (Aug 19 2023 at 12:02):

That's really just an expansion of the second sentence of the abstract. That's maybe more intelligible like this.

Jean-Baptiste Vienney (Aug 19 2023 at 12:04):

I thought that people will immediatly see that my conditions are not the usual ones, but maybe I should insist one that (the reason for this difference from a socio-historical point of view is that as I explain in the introduction, my conditions are extracted from the cut-elimination process of linear logic, which is part of the proof-theory tradition, whereas the usual one comes from the mathematics tradition).

John Baez (Aug 19 2023 at 12:22):

What does (A2.b) mean? Is there an equation missing from this?

Jean-Baptiste Vienney (Aug 19 2023 at 12:23):

yes, thanks, fixed

John Baez (Aug 19 2023 at 14:13):

Okay, good. Your result is related to the result on page 47 here, and also the results here. However, all those results are about when a monoidal category is cartesian, not the product of two specific objects. And if your result is correct you may be able to combine it with the ideas in the links to get a better, "purely equational" theorem about when a monoidal category is cartesian.

Jean-Baptiste Vienney (Aug 19 2023 at 14:25):

Hmm I'm aware of this result. I can get conditions for when a category is a cartesian monoidal category by simply asking that the structure I ask for a couple $A,B$ is here for every such couple. In that case, $p_1:A \times B \rightarrow A$, $p_2:A \times B \rightarrow B$ and $\langle ., . \rangle_X:\mathcal{C}[X,A] \times \mathcal{C}[X,B] \rightarrow \mathcal{C}[X,A \times B]$ are probably natural transformations. But it doesn't look exactly like what you need for a monoidal category. It's of a different nature, more asymmetric.

John Baez (Aug 19 2023 at 14:30):

I actually pointed to at least two results, one or two involving diagonals and maps $e_A : A \to I$, and another involving diagonals and maps $p_1: A \otimes B \to A$, $p_2: A \otimes B \to B$. The nLab says about the latter result

This theorem is probably in Eilenberg and Kelly’s paper on closed categories, but they may not have been the first to note it.

However, this theorem as stated on the nLab result is a bit weak since the hypotheses wind up mentioning products! So it would be nice to use your ideas to improve that result.

John Baez (Aug 19 2023 at 14:32):

It's possible Eilenberg and Kelly stated the result in a better way.

Jean-Baptiste Vienney (Aug 19 2023 at 14:32):

Sorry, I don't know this second one.

Jean-Baptiste Vienney (Aug 19 2023 at 14:38):

It's probably a good idea to try this.

Jean-Baptiste Vienney (Aug 19 2023 at 14:41):

This result is on p.551 in the paper "Closed Categories".

Morgan Rogers (he/him) (Aug 19 2023 at 16:15):

You could compress two of the conditions into $v = \langle v; p_1, v; p_2 \rangle$, since that's all you use in the proof, and this is really an equation expressing that/how the map is surjective.

Morgan Rogers (he/him) (Aug 19 2023 at 16:20):

As far as it being new/interesting is concerned, you already point out that a connective in linear logic is typically interpreted as categorical product, so that connection isn't new. How do you imagine you could leverage this axiomatization of products to make it interesting?

Aaron David Fairbanks (Aug 19 2023 at 18:53):

This is like the difference between saying a map is invertible and giving a specific inverse.

An intermediate step between the representing object definition (1) and your definition (2) would be another definition where the data include an inverse natural transformation to $\langle\cdot,\cdot\rangle$ instead of $p_1$ and $p_2$. This would also be "algebraic" in that it is defined in terms of equations instead of bijectivity or unique existence of something.

Your definition comes from the Yoneda lemma: the inverse natural transformation is determined by the element it sends the identity to, $(p_1, p_2)$. This style of definition works for any universal property, not just products.

Jean-Baptiste Vienney (Aug 19 2023 at 19:22):

Could you detail a bit more the process to go from $(1)$ to $(2)$ and vice-versa using Yoneda lemma? I'm not super good in terms of Yoneda lemma.

Jean-Baptiste Vienney (Aug 19 2023 at 19:30):

Morgan Rogers (he/him) said:

As far as it being new/interesting is concerned, you already point out that a connective in linear logic is typically interpreted as categorical product, so that connection isn't new. How do you imagine you could leverage this axiomatization of products to make it interesting?

I was wondering how we could use this in terms of rewriting / cut-elimination. You can orient two of the equalities easily: $\langle f,g \rangle;p_1 \rightsquigarrow f$ and $\langle f,g \rangle;p_1 \rightsquigarrow g$, it as in linear logic. As to the third one, in linear logic you do $\langle v;f_1, v;f_2 \rangle \rightsquigarrow v;\langle f_1,f_2 \rangle$, so here maybe $v \rightsquigarrow \langle v;p_1, v;p_2 \rangle$. It looks like you can make a rewriting system with less rewriting rules than all the cut-elimination steps of linear logic which concern the connector $\&$.But it's maybe not going to eliminate all the $;$. I'm wondering if these three rules provide a confluent/terminating rewriting system when you start from a set of functions symbols $\{f,g,...\}$ and looks at all the words built using $;$, $\langle . , . \rangle$, $p_1$ and $p_2$.

Jean-Baptiste Vienney (Aug 19 2023 at 19:43):

Jean-Baptiste Vienney said:

Could you detail a bit more the process to go from $(1)$ to $(2)$ and vice-versa using Yoneda lemma? I'm not super good in terms of Yoneda lemma.

If this a general process that you can apply to every limit, then I would like to understand it better because it looks like a very good way to implement these limits in type theory.

Jean-Baptiste Vienney (Aug 19 2023 at 19:45):

For instance, I would be interested to apply this process to (co)equalizers.

Aaron David Fairbanks (Aug 19 2023 at 20:49):

Maybe it will help for clarity to be more specific about the "intermediate step".

Data (4):

• (D4.a) for every object $X$, a function $\text{Hom}(X,A) \times \text{Hom}(X,B) \to \text{Hom}(X, A \times B)$, denoted $(f,g) \mapsto \langle f,g \rangle$
• (D4.b) for every object $X$, a function $\text{Hom}(X, A \times B) \to \text{Hom}(X,A) \times \text{Hom}(X,B)$, denoted $a \mapsto (a_1,a_2)$

Axioms (4):

• (A4.a) $\langle a_1, a_2 \rangle = a$
• (A4.b) $( \langle f,g\rangle_1, \langle f,g\rangle_2) = (f,g)$
• (A4.c) $\langle u;f , u;g \rangle = u; \langle f, g \rangle$
• (A4.d) $((u;a)_1, (u;a)_2) = (u;a_1, u;a_2)$

(You could split up each axiom involving a pair of elements into two axioms if you want.)

This is the representing object definition with everything spelled out algebraically: an inverse pair of natural transformations from a representable presheaf to the presheaf $\text{Hom}(-,A) \times \text{Hom}(-,B)$ and vice versa. If we used any other presheaf instead besides $\text{Hom}(-,A) \times \text{Hom}(-,B)$, this definition would still make sense, giving a representing object for that presheaf. For example, for an arbitrary limit, the presheaf in the place of $\text{Hom}(-,A) \times \text{Hom}(-,B)$ would be the presheaf of cones.

Some details here are redundant. First of all, A4.d is redundant, because a bijective natural transformation has a natural inverse.

The Yoneda Lemma says that the natural transformations from a representable presheaf $\text{Hom}(-,Z)$ to a presheaf $F(-)$ are in bijection with elements of $F(Z)$. This is because we can reconstruct the natural transformation $\alpha$ from where it sends $1_Z$ (and any choice of $\alpha(1_Z)$ extends to a natural transformation). You reconstruct all of $\alpha$ from $\alpha(1_Z)$ by setting $\alpha(a) := a;\alpha(1_Z)$.

Now replace all equations involving the natural transformation $(\cdot_1,\cdot_2)$ with equations involving its value at the identity, $((1_{A \times B})_1, (1_{A \times B})_2)$, and call this $(p_1, p_2)$. So each appearance of $(a_1, a_2)$ gets replaced with $(a;p_1, a;p_2)$.

Data (5):

• (D5.a) for every object $X$, a function $\text{Hom}(X,A) \times \text{Hom}(X,B) \to \text{Hom}(X, A \times B)$, denoted $(f,g) \mapsto \langle f,g \rangle$
• (D2.b) an element $(p_1, p_2)$ in $\text{Hom}(A \times B,A) \times \text{Hom}(A \times B,B)$

Axioms (5):

• (A5.a) $\langle a;p_1, a;p_2 \rangle = a$
• (A5.b) $( \langle f,g\rangle;p_1, \langle f,g\rangle;p_2) = (f,g)$
• (A5.c) $\langle u;f , u;g \rangle = u; \langle f, g \rangle$

Finally, A5.a is equivalent in the presence of A5.c to $\langle p_1, p_2 \rangle = 1_{A \times B}$.

Jean-Baptiste Vienney (Aug 19 2023 at 22:08):

Thanks @Aaron David Fairbanks . We could talk of this later, I'd want to apply this to other (co)limits and see what it gives and if we can get some kind of sequent calculus from that.

Jean-Baptiste Vienney (Aug 19 2023 at 22:12):

And thanks @John Baez , @Morgan Rogers (he/him), @Matteo Capucci (he/him) . This discussion has been really useful to me!

Jean-Baptiste Vienney (Oct 30 2023 at 15:04):

I'd been dreaming about something the other day: I've learned the stuff about differentiation in computer science ie. differential categories, lambda-calculus, linear logic etc... has been conceived as a replacement for the use of topology in computer science ie. stuff related to Scott topology. So it looks like there are a differential and a continuous approach to computer science which are quite similar. It makes me think to the de Rham theorem which says that the de Rham cohomology of a smooth manifold is isomorphic to its singular cohomology, therefore the topological and differential approach are equivalent for this cohomology. If we do enough progress in the theory of differential categories, and relate it to topology, in particular locales, will we be able to understand more about these equivalences of differentiation and continuitity, at the same time in computer science and mathematics?

Jean-Baptiste Vienney (Nov 01 2023 at 03:58):

I have to choose a first title for my phd thesis (that I will have much time to change if needed).

I already like to think of title of papers I want to write but now it is even better. I think my projects are now clear and I can give a clear title:

Differentiation in category theory: Graded, Hasse-Schmidt, Relative

There are three different topics in the subject "differentiation in category theory", or three different categorical doctrines: differential categories (which are monoidal categories, axiomatizing differentiation, starting from the category of linear maps), cartesian differential categories (which are cartesian categories, axiomatizing differentiation, starting from the category of differentiable maps) and tangent bundle categories (axiomatizing the category of smooth manifolds and its tangent bundle). These three structures are related by universal constructions. What will do my thesis is providing three variants of each of these structures.

• the graded variants add a notion of degree to differentiable maps. It is mainly useful when considering polynomial maps: degree decreases by one when one differentiate. I'm not sure what would be a graded tangent bundle but it probably makes sense. The idea comes from graded linear logic where the modality $!$ is replaced by a family $!_r$ indexed by a semi-ring $R$ and implements it in the context of differential categories and differential linear logic. This idea of graded differential categories and the close concept of graded differential linear logic have already been published in a paper written with JS (here).
• the Hasse-Schmidt variants implement the idea of Hasse and Schmidt which was to replace the usual derivative of polynomials by a notion better appropriated in positive characteristic. By working on graded differential cactegories, I've kind of understood why this idea is important. Hasse-Schmidt derivatives have been used in the subject of "crystalline cohomology" and I think it's somehow useful for cohomology of schemes in positive characteristic. I've realised that the Hasse-Schmidt version of tangent bundle is something already known and usefull even for smooth manifolds. The Hasse-Schmidt tangent bundles are what is known as "higher-order tangent bundles". While the tangent bundle of first order gives a linear approximation of the manifold around a point, the tangent bundle of order $n$ gives an approximation by a polynomial of degree $n$. Of course, it will also for sure be useful in the category of commutative rings which is also a tangent bundle category.
• The relative variants come from the idea of relative comonad. In a differential category, we have the exponential modality $!$ which is a comonad. I want to generalize this by authorizing $!$ to be a relative comonad ie. $!A$ can live in a different category than $A$. I think it will be useful in order to consider spaces of functions where the functions live in a different space than the coordinates. For instance we could take the coordinates in an Euclidean space and the functions in an infinite-dimensional space like those considered in functional analysis.

Of course, if these $9$ things can be defined, you could also combine them but it doesn't look usefull in lot of situations to implement the graded, Hasse-Schmidt and relative ideas at the same time.

• Maybe I'll do a chapter "Miscellany" where I put the work which doesn't fit in the title but is related. For instance I proved a result about families of symmetric powers in a symmetric monoidal $\mathbb{Q}^+$-linear category which generalizes a result from 1992 about symmetric algebras of vector spaces over a field of characteristic $0$. That's the second paper I submitted (it's here) and I'm the first to cite this paper by Axelsson Reynir & Jón Magnússon since 1992 (A Characterization of symmetric and exterior algebras in characteristic zero). Moreover, Jón Magnússon is also one of the only person on this earth to have read my paper so far (Researchgate told me he read it), which is quite fun. Looks like we're both interested in this quite unpopular subject of bialgebraically characterizing symmetric algebras (the family of all symmetric powers of an object for me, but it is quite the same thing). In a few months probably, I'll submit another paper where I refine this result by characterizing symmetric powers by means of "annihilation/creator operators". This time it will be really more than what Reynir and Magnússon did, even in the category of vector spaces over a field of characteristic $0$.

John Baez (Nov 01 2023 at 11:58):

Unless there is already a paper called "Differentiation in category theory", I would recommend that as the title for your thesis. It's great that you've organized the subject into "graded, Hasse-Schmidt and relative" ideas. But almost nobody will read your thesis because of these extra words in the title, and many people will be intimidated by them. There may be 5 or 10 fans of Hasse-Schmidt differentiation in the world, but many more people will say "ugh, what's that? I don't know, I'm probably not interested in this".

John Baez (Nov 01 2023 at 12:00):

Another thing to keep in mind is that people only talk about the title of a paper if it's short enough. People will say things like "Hey, have you read Differentiation in Category Theory by Jean-Baptiste Vienney?" But they are very unlikely to say "Hey, have you read Differentiation in Category Theory: Graded, Hasse-Schmidt and Relative by Jean-Baptiste Vienney?"

John Baez (Nov 01 2023 at 12:01):

Think of Lawvere's thesis title: Functorial Semantics. Short and snappy. People remember it.

Jean-Baptiste Vienney (Nov 01 2023 at 12:25):

Hmm. But I've not invented "Differentiation in Category Theory"! All The important notions: differential categories, cartesian differential categories and tangent categories already exist.

My contribution is exactly to add these ideas of graded, Hasse-Schmidt, relative... They are just options you can add on top of everything already known...

John Baez (Nov 01 2023 at 12:28):

I don't think a thesis title is a claim that you've invented the subject. I think it's a description of what the thesis is about.

Jean-Baptiste Vienney (Nov 01 2023 at 12:29):

Ok, so I'll ask my supervisors if they think "Differentiation in Category Theory" is a good title. Thanks :smile:

John Baez (Nov 01 2023 at 12:30):

Sure! Or maybe there's some other title, that's more specific, but doesn't list 3 mysterious concepts that will only become interesting after someone reads the thesis.

Jean-Baptiste Vienney (Nov 01 2023 at 12:33):

Well, there isn't any other approach of differentiation in category theory than that. I mean nothing with as much papers published. So I think it's very good.

Jean-Baptiste Vienney (Nov 01 2023 at 13:31):

Something more: I think there isn't any good place to learn this subject quickly and easily. You have to read many papers to learn and get an overview of the subject. The only good ressources are some slides from JS. But I think something written would be better. So, one chapter presenting the three categorical structures in the theory, with their relations and the important exemples would be good. After this chapter I will repeat the same pattern adding grading, Hasse-Schmidt and relative stuff. Like this, after I've done my thesis, I will say to people: "If you want to learn about differential categories etc..., read the first chapter of my thesis. All the important ideas are here, it's explained in a straigthforward way and without much prerequisites. Nothing like this existed before I wrote it...."

Jean-Baptiste Vienney (Nov 01 2023 at 13:38):

I think people should not be obligated to go to conferences to learn about a research topic... The only way to learn about this topic today is to know some person who works on it, or go to conferences and listen to tutorials. That's not ideal...

Jean-Baptiste Vienney (Nov 01 2023 at 13:39):

The litterature is much too overwhelming to learn the subject in my opinion.

John Baez (Nov 01 2023 at 14:49):

Your thesis could be very helpful, then.... which is another reason I think it should have a simple title: that will make it attractive to beginners.

John Baez (Nov 01 2023 at 14:49):

But I am always trying to make things fun and easy to understand: your advisor may have a different attitude.

Jean-Baptiste Vienney (Nov 01 2023 at 15:08):

I completely agree with that and I like a lot that some people here share this opinion.

I think that also everybody should have access to the most updated information on mathematics easily. For lot of people the way of developping mathematics is to do research in the secret and then offer some good project to the students they have the most consideration for. But this is not how I did. I have always been a good student but not the brightest one (I mean not at the most extreme level like being able to be accepted in the world best universities etc...). I struggled a bit to find a place to be accepted in Phd. What I did is to answer a question in a paper by JS by proposing the idea of graded differential linear logic / categories. And I got accepted in a phd program in part thanks to that. I try to share all my research ideas in order that if anybody in this world is quite an adventurer he can take a similar path. I would like math to become something a bit more like open source software development where everybody can contribute easily and without a war of egos.

Jean-Baptiste Vienney (Nov 01 2023 at 15:15):

I very much like my supervisors but I feel uncomfortable with their habits sometimes: like when they say that this guy or that guy is a great guy in front of their friends to help him have a better reputation

Jean-Baptiste Vienney (Nov 01 2023 at 15:18):

In fact a few people did that: saying that I'm a good guy in front of their friends and it's weird

John Baez (Nov 01 2023 at 15:26):

It's better than being told you're a bad guy. :upside_down:

Jean-Baptiste Vienney (Nov 01 2023 at 15:51):

Yes sure haha. I don't feel so bad honnestly. It feels nice also to be considered by people for sure.

But lot of people didn't succeed to enter the social circle of research in mathematics and I feel bad for them when I become myself part of all the usual social habits. All the people who didn't get accepted in a phd program but were very passionate... We don't see them but they are real people and maybe they will feel bad about this all their life.

Jean-Baptiste Vienney (Nov 01 2023 at 15:52):

If they could have access to the latest developments and build on top of it in their free time if they find it fun and succeed to do it, it would be a good progress for humankind.

Jean-Baptiste Vienney (Nov 01 2023 at 15:54):

I'm sure I'm very much in an utopia in my mind but anyway, there is progress to be made on these matters.

Kevin Arlin (Nov 01 2023 at 16:13):

Can confirm that if you write a nice self-contained introduction to prior art on differentiation in category theory for your first chapter I will definitely read it.

Kevin Arlin (Nov 01 2023 at 16:14):

(and then hopefully the rest too!)

Eric Forgy (Nov 01 2023 at 17:32):

I'd love to see a thesis on differentiation in category theory especially if it had a nice self-contained introduction / survey :+1:

Chris Grossack (they/them) (Nov 02 2023 at 17:15):

Adding to the chorus of people saying "I'd read the first chapter, and hopefully the rest"

Jean-Baptiste Vienney (Feb 12 2024 at 23:52):

I don't want to be too much off-topic in the topic on Prüfer rings, so I put my story here:

If you take multiplicative additive linear logic, you make it compact closed ie. $"parr" = \otimes$ and you add a distributivity of $\oplus$ over $\&$ and of $\&$ over $\oplus$, then you can interpret $\otimes$ by the product of numbers in $\mathbb{Q}_{>0}$, the $\oplus$ by the gcd, the $\&$ by the lcm, the negation by the inverse and obtain a logic where a sequent $a \vdash b$ can be interpreted as $a$ divides $b$ with $a,b \in \mathbb{Q}_{>0}$ where (*) You define the gcd by taking the min of the p-adic valuations of the two numbers, the lcm by taking the max. And you have amazingly a De Morgan Duality $gcd(a^{-1},b^{-1})=lcm(a,b)^{-1}$, in addition to the multiplicative one, $(ab)^{-1}=a^{-1}b^{-1}$.

Then, I realized that in fact I'm already working with fractional ideals and that something like "nonzero finitely-generated fractional ideals of any Prüfer semiring" seem to verify all the same conditions I want. I've been very excited by this the previous days. Something surprising for someone who knows about linear logic is that the model in $\mathbb{Q}_{>0}$ and probably the models with ideals of Prüfer (semi)rings give a compact closed categories with products and coproducts which are not biproducts which seems to contradict the paper Finite products are biproducts in a compact closed category. But in fact not, the subtlety is that this paper applies only if you have binary products AND an empty product but in the models of arithmetic, you don't have an initial object (it is not 1 because here all the numbers $1/n$ divides $1$ :)).

Jean-Baptiste Vienney (Feb 12 2024 at 23:58):

(*) you define that $a$ divides $b$ iff $v_p(a) \le v_p(b)$ for all prime number $p$ with $v_p(a),v_p(b) \in \mathbb{Z}$

Jean-Baptiste Vienney (Feb 13 2024 at 00:01):

I’m struggling a lot with rendering my message… I wanted to correct that you start with mutliplicative additive linear logic without initial and terminal object.

Jean-Baptiste Vienney (Feb 13 2024 at 00:04):

$\oplus -> lcm$, $\& -> gcd$. I can’t modify my message else it doesn’t render anymore…

Jean-Baptiste Vienney (Feb 13 2024 at 18:19):

I want to write a bit more about my math life today. The main points are these ones:

• I must pass some courses and comprehensive exams for my PhD and it's far from a trivial task.

• I'm barely not doing any research anymore because I need to work on this. However, I start doing a bit of research just a few hours from time to time. I think it's better for my mind and maybe my supervisor will be happy also to see me excited about several ideas as usual.

• This summer I will not have any course, so I will be able to do a lot of research! I will go to the conference on Differential linear logic and differential lambda calculus in Marseille in May. In fact, I will go in France during all the month of May. I think I can't do a talk at the conference but I can come with a poster, so I will make a poster with three little sections talking about three ideas, with a just a few lines for each one. These ideas are:
  1) Differential categories and graded linear logic can be combined into the notion of graded differential category. (Topic of my first paper, with JS Lemay)
  2) Symmetric powers can be characterized as the "binomial graded bimonoids" in the appropriate symmetric monoidal categories. (Topic of my second paper "String diagram for symmetric powers I")
  3) Hasse-Schmidt derivative and differential categories can be combined in the notion of Hasse-Schmidt differential categories. (not yet a paper)

• During the whole summer, I will work on writing more or less 4 papers:
  a) A paper on Hasse-Schmidt differential categories
  b) A paper on higher-order tangent categories. Quick idea: it is combining the notion of tangent category with the notion of higher-order tangent bundle from differential geometry
  c) The paper "String diagram for symmetric powers II". Quick idea: it is about a characterization of symmetric powers in appropriate symmetric monoidal categories via "creation/annihilation operators"
  d) A paper on "A sequent calculus for elementary arithmetic" Quick idea: it is about doing arithmetic with categorical logic, with inspiration from linear logic

• I don't remember but I think it's in July or August. I will go to the conference FMCS 2024 in Kananaskis. I think I will talk about the logic for arithmetic.

Morgan Rogers (he/him) (Feb 14 2024 at 09:30):

Jean-Baptiste Vienney said:

• I'm barely not doing any research anymore because I need to work on this.

Don't resent this too much; remember that this is part of the job too, and that there will often be things besides research to do in any position you're in. It can be frustrating at first when you're used to being a student who can devote almost all of their time to studying the thing that interests them, but being a researcher is about more than just doing research :)

Jean-Baptiste Vienney (Feb 14 2024 at 14:36):

Thank you for the kind words :)

Jean-Baptiste Vienney (Mar 03 2024 at 15:59):

Hi, just wanted to say that I've been looking again at the explanations about determinants and adjugates in the discussion named "Nakayama's lemma" which is in a deprecated stream (involving in particular @Todd Trimble , @Patrick Nicodemus and @Aaron David Fairbanks ), and I think I can define the notion of determinant (and adjugate) in a purely category-theoretic setting (that I would like to call "meta(compact closed symmetric monoidal) cartesian left additive category with negation and coequalizer exterior powers"). I can say what is a finite-dimensional object in such a category and should be able to prove that an "additive map" from a a finite-dimensional object to itself is an isomorphism if and only if some element of a commutative ring, named the determinant of f is a unit (this ring being of the form $\mathcal{C}[I,I]$ where $I$ is the monoidal unit of the symmetric monoidal category of "additive maps").

I don't want to talk about this right now, but it seems to work perfectly and I think it will be written and on the ArXiv in a few months and I will say it here for people who could be interested. I will write that I thank the people who I've just tagged as well as the other ones for the helpful discussion on Zulip.

Jean-Baptiste Vienney (Apr 09 2024 at 03:42):

Yeah, my paper "String diagrams for symmetric powers I" is accepted for publication in Compositionality provided I revise it following the two reviews. They asked me to make quite a few revisions but these are all good points to make the paper more intelligible to people, including typesetting correctly, giving much more informal explanations of the intuitions and motivations, and correct sometimes the structure in definitions / lemmas / proofs etc... This is only my second paper and the first that I write alone so I guess it is normal that I have still to learn on how to write a good paper.

Jean-Baptiste Vienney (May 11 2024 at 19:51):

• I'll come to the conference on differential linear logic and differential lambda calculus (in Marseille) next week with this poster! Some time ago I introduced with JS Lemay the notion of graded differential category which is a graded version of the more classical notion of differential category. This poster is about a new theorem: under mild conditions every differential category is also a $\mathbb{N}$-graded differential category (for instance any cocomplete monoidal closed differential category is also a $\mathbb{N}$-graded differential category but we really don't need as much as "cocomplete and monoidal closed" for the theorem to apply to a differential category). This is absolutely fresh research :fish: and I'm excited by the fact that a lot of people who could be interested in this result are going to see my poster (moreover the posters will be hung during the whole conference in the hall of the auditorium and they said that there are not so many posters so it should be quite visible.

Jean-Baptiste Vienney (May 11 2024 at 19:55):

(by the way if ever someone look at the poster, differential category = additive symmetric monoidal category + differential modality on it) The poster is bone dry because I just wanted to expose the theorem clearly and also there will be a tutorial on differential categories during the conference and finally I will be able to give intuitive explanations to people if they talk with me.

Jean-Baptiste Vienney (May 11 2024 at 20:05):

• After the conference, in ten days or so, I'll visit Ralph (Sarkis) in Lyon to go to the monthly seminar Chocola at ENS Lyon one day and also work a few more days together. I guess we'll try to finally write our paper on section-retraction + monoid in a monoidal category/monad/operad/algebra over monad etc..

Jean-Baptiste Vienney (May 11 2024 at 20:14):

By the way in terms of ecology, I should say that I've taken a plane to go to France for one month after being one year and a half in Canada without my family but while I'm France I only use the train to go from one city to another one (something that it is more difficult to realize in Canada, because of the size of the country).

Jean-Baptiste Vienney (May 11 2024 at 20:15):

I know it would be better if I stayed one year in France but I can't really do that cause I'm doing a PhD in Ottawa.