Timeline for Examples of formalisation of abelian categories
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 20, 2022 at 10:47 | answer | added | Niels | timeline score: 5 | |
| Apr 12, 2022 at 19:48 | comment | added | Adam Topaz | Just to add to what was said above, I want to mention that the argument we have in the liquid tensor experiment for the snake lemma is just a diagram chase, but with pseudoelements. The key construction is the connecting map, and its definition can be found here for those who might be interested: github.com/leanprover-community/lean-liquid/blob/… | |
| Apr 12, 2022 at 17:11 | comment | added | Kevin Buzzard | @Ricky yes this is somehow the point. One could imagine writing something down and saying it's the snake lemma or whatever, but I was wondering whether there had been some developments of the theory of abelian categories which had attempted to use a formalisation of the snake lemma to do other things; in informal maths it's used all over the place to prove results about cohomology groups for example. Has anyone formalised anything like this in any prover? | |
| Apr 12, 2022 at 17:09 | comment | added | Kevin Buzzard | Thanks @GuyCoder . I started tagging explicit provers then realised I'd run out of tags. | |
| Apr 12, 2022 at 17:08 | history | edited | Kevin Buzzard |
edited tags
|
|
| Apr 12, 2022 at 13:22 | comment | added | jmc | On top of that, you want everything to be functorial wrt maps of short exact sequence (or long exact sequences, or whatever gadget you are considering). On paper that's "obvious". In a theorem prover you can quickly paint yourself in a nasty corner. | |
| Apr 12, 2022 at 13:03 | comment | added | Ricky | I've participated in the proof of the snake lemma, and it wasn't very hard, or at least not a lot harder than with pen and paper. (I mean, without Freyd-Mitchell is really annoying even on paper). The real problem is when one wants to use it. We usually think that the first row is the "row of kernels", but of course this is not really precise, in the sense that "being the kernel" is an evil notion. We want that the elements of the first row satisfy the universal property of the kernel and so on. It is this kind of difficulties that are really different when working with a theorem prover. | |
| Apr 12, 2022 at 13:00 | history | edited | Kevin Buzzard | CC BY-SA 4.0 |
add clarifying comment
|
| Apr 12, 2022 at 12:53 | history | asked | Kevin Buzzard | CC BY-SA 4.0 |