Property Table of Algebraic Structures
This project is, first and foremost, an exercise I did for myself - to better get a grasp of the many terms and concepts of group theory and category theory.
The exercise is quite simple: to fill up some huge spreadsheets, mapping each and every algebraic structure (for example, the natural numbers ℕ with the operator +) to each common property of algebra (for example, “associativity”). The goal is also to have the relevant proofs in each cell as extra annotations.
I have begun to implement all of these proofs using lean, with the valuable help of the wonderful Joseph Dimos. The end goal is to create a large database of the properties of mathematical structures, such that one may query for any example structure with the desired properties that suit their mathematical needs.
Here are the (as-of-yet quite incomplete) tables in question: