## Stream: general

### Topic: Can you provide me with some Category Theory / Diagram Chase

#### Daniel Donnelly (Jun 28 2022 at 09:25):

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 (Jun 28 2022 at 09:26):

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

#### Daniel Donnelly (Jun 28 2022 at 09:28):

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

#### Johan Commelin (Jun 28 2022 at 09:28):

Should be in the same repo, different folder.

#### Heather Macbeth (Jun 28 2022 at 09:29):

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

#### Henrik Böving (Jun 28 2022 at 09:30):

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 (Jun 28 2022 at 09:30):

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 (Jun 28 2022 at 09:30):

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

#### Kevin Buzzard (Jun 28 2022 at 09:33):

@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 (Jun 28 2022 at 09:33):

@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 (Jun 28 2022 at 09:34):

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 (Jun 28 2022 at 09:35):

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

#### Kevin Buzzard (Jun 28 2022 at 09:36):

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

#### Daniel Donnelly (Jun 28 2022 at 09:37):

@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 (Jun 28 2022 at 09:38):

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 (Jun 28 2022 at 20:13):

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 (Jun 28 2022 at 21:17):

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

#### Kevin Buzzard (Jun 28 2022 at 21:17):

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

Last updated: Dec 20 2023 at 11:08 UTC