Can you provide me with some Category Theory / Diagram Chase

Stream: general

[Daniel Donnelly]

https://leanprover-community.github.io/theories/category_theory.html

Is all I found, and that page literally has nothing on it that I can use as a new person to Lean4. Just show me how to declare a category, some objects / arrows, and possibly the proof that id for each object X is unique. That would teach me a lot.

[Heather Macbeth]

@Daniel Donnelly Have you seen this tutorial? https://github.com/leanprover-community/lftcm2020/tree/master/src/exercises_sources/thursday/category_theory

[Daniel Donnelly]

@Heather Macbeth that shows me a lot, but what are the solutions to those exercises?

[Johan Commelin]

Should be in the same repo, different folder.

[Heather Macbeth]

https://github.com/leanprover-community/lftcm2020/tree/master/src/solutions/thursday/category_theory

[Henrik Böving]

Considering that you are using Lean 4 that tutorial will probably not be that useful since Lean 4 doesn't have all the category theory definitions from mathlib yet. If you are into mathematics and want to do Lean 4 right now you usually have to build up your own theory.

[Daniel Donnelly]

Found it. Thank you! I should go through these before asking any more questions. This will make me learn Lean4 as a side effect

[Henrik Böving]

No this will make you learn Lean 3 as a side effect.

[Kevin Buzzard]

@Daniel Donnelly there is essentially no mathematics in Lean 4. There is a gigantic mathematics library in Lean 3 called mathlib with lots of category theory, and there's even more category theory in the Liquid Tensor Experiment, a Lean 3 project which builds on mathlib. The computer scientists are writing a program which will translate all of Lean 3's mathematics into Lean 4. It's not ready yet.

[Daniel Donnelly]

@Henrik Böving okay Henrik, thank you. Please define Category for me? I can take it from there, leave some of the parts out so that I can complete if that makes it easier. I just want to see what the proof looks like for id uniqueness. Also, is it possible to have side effects to the Lean4 code? For example can I communicate to another program that is displaying a CD (commutative diagram)? I know about Widgets, but I'm talking about my own thing which will allow a two-way communication between the diagram editor and Lean4 code/interpreter.
Iow if the user types "f:A \to B" in Lean4, that will be drawn and vise versa.

[Kevin Buzzard]

Please define Category for me?

Are you still talking about Lean 4, in which case you will have to do everything from scratch, or are you talking about Lean 3, where you can work with 5 years worth of category theory development?

[Daniel Donnelly]

@Kevin Buzzard I guess I should just install Lean3, but what about writing to a file or socket - can Lean3 do that?

[Kevin Buzzard]

Don't ask me about computer science! I'm just a number theorist :-)

[Daniel Donnelly]

@Kevin Buzzard I think I'm asking a dumb question anyway, I'm not sure how/where the data will flow yet.

[Henrik Böving]

Daniel Donnelly said:

Henrik Böving okay Henrik, thank you. Please define Category for me? I can take it from there, leave some of the parts out so that I can complete if that makes it easier. I just want to see what the proof looks like for id uniqueness. Also, is it possible to have side effects to the Lean4 code? For example can I communicate to another program that is displaying a CD (commutative diagram)? I know about Widgets, but I'm talking about my own thing which will allow a two-way communication between the diagram editor and Lean4 code/interpreter.
Iow if the user types "f:A \to B" in Lean4, that will be drawn and vise versa.

I can definitely try to define a category but I'm a computer scientist with almost no category theory background so the mathematicians will probably jump at me :P

We can have side effects and what not in Lean 4 sure, Lean 4 is also a full blown programming language on top of being a theorem prover and things like the lean 4 compiler itself, our project management tool, our documentatino tool etc. are all written in pure Lean.

[Daniel Donnelly]

Decided to Keep going with Lean4. If Mathlib is converted to Lean4 by the time I'm ready great. If not I'll copy the essentials from the Lean3 mathlib, converting them to Lean4 by hand. I can only really move as fast as my own project will allow anyway. But if I can comehow parse Lean4, then when the category library is imported, I could have all that visual content generated automatically. Thus I can bootstrap off of existing Lean4 efforts.

[Kevin Buzzard]

I suspect that formalising the basics of category theory in mathlib4 following the lean 3 script would be a welcome addition.

[Kevin Buzzard]

I learnt a bunch of stuff about lean 4 by manually porting stuff from lean 3