Coend calculus in Lean

Stream: new members

[fosco]

Hi everyone! I am a category theorist who recently started to study Lean, and I have watched a few videos of the LftCM series on youtube.

I'm here because I got in touch with @Scott Morrison : I would like to define dinatural transformations and co/ends in Lean with the goal of certifying theorems proved via coend calculus. I have written a book on coends, and I believe that this project is feasible and a good service to the fast-expanding Lean community and to category theorists.

It seems that the part of the category theory library in lean relevant to coends has still to be written. If this is correct, I'd like to do it myself.
I tried to do it in agda-categories, and decided, after a painful day of reading through the library, that Lean is much better suited for this purpose. :smile:

If anyone is willing to collaborate on this project, and teach me something in that direction, hit me up!

[Scott Morrison]

I think we have everything you need in the library to get started. I would suggest trying to write a definition of dinat_trans, and posting it here, and we'll tell you if you're doing something horribly wrong. :-)

[Scott Morrison]

I can post the "stub", i.e. the import, open, and variables commands you'd need, or you can puzzle it out yourself, as you prefer. :-)

[fosco]

yes, please: a stub would be very helpful. I have completed the natural number game to get a grip of the fundamental tactics, but I am still a little bit unsure about how (with what) to fill a blank file

[Scott Morrison]

(I'm curious, by the way: how do you feel about https://ncatlab.org/nlab/show/dinatural+transformation#dinaturality_versus_extranaturality?)

[Bryan Gin-ge Chen]

(Side note: you've posted in the mathlib4 stream, but note that mathlib proper is in Lean 3 at the moment. mathlib4 is currently just a testing ground for the forthcoming port to Lean 4. I guess we could probably move this thread to the #maths stream, which more of us follow.)

[Notification Bot]

This topic was moved here from #mathlib4 > Coend calculus in Lean by Scott Morrison

[Scott Morrison]

I put it in #new members, since it is an introduction. I'll make a separate thread in #maths to start @fosco off.

[fosco]

Scott Morrison said:

(I'm curious, by the way: how do you feel about https://ncatlab.org/nlab/show/dinatural+transformation#dinaturality_versus_extranaturality?)

I prefer to work with dinaturality, when teaching or when I handle Set-categories, and with extranaturality, when working with generally enriched categories.

[fosco]

Bryan Gin-ge Chen said:

(Side note: you've posted in the mathlib4 stream, but note that mathlib proper is in Lean 3 at the moment. mathlib4 is currently just a testing ground for the forthcoming port to Lean 4. I guess we could probably move this thread to the #maths stream, which more of us follow.)

Whoops, sorry!