wball/GroupTheory
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixed link in README

Browse source
This commit is contained in:
William Ball 2024-10-22 15:05:43 -07:00
parent 59f365a261
commit 64317340dd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
README.org
View file

@ -1,6 +1,6 @@
#+title: GroupTheory
Like [[https://forgejo.ballcloud.cc/Category-Theory][my category theory]] formalization, this is a formalization of basic group theory in Agda for learning purposes. My primary goal with this project was to get a better understanding of Agda by formalizing a topic I am very familiar with, rather one that I am actively learning. In particular, I wanted more practice working with different notions of equality, as this is something that comes up in formalizing category theory (you want to abstract over an arbitrary equivalence relation on hom-sets, rather than working with propositional equality, which can be very limiting, e.g. when working with functions as morphisms). As such, my goal, which I accomplished, was to formalize and prove the first isomorphism theorem, as that requires working with multiple groups, subgroups, and quotient groups, all of which require careful understanding of the equivalence relations involved and comfort in working with them.
Like [[https://forgejo.ballcloud.cc/wball/Category-Theory][my category theory]] formalization, this is a formalization of basic group theory in Agda for learning purposes. My primary goal with this project was to get a better understanding of Agda by formalizing a topic I am very familiar with, rather one that I am actively learning. In particular, I wanted more practice working with different notions of equality, as this is something that comes up in formalizing category theory (you want to abstract over an arbitrary equivalence relation on hom-sets, rather than working with propositional equality, which can be very limiting, e.g. when working with functions as morphisms). As such, my goal, which I accomplished, was to formalize and prove the first isomorphism theorem, as that requires working with multiple groups, subgroups, and quotient groups, all of which require careful understanding of the equivalence relations involved and comfort in working with them.
I have since learned more about how instance arguments work, which would have simplified the notation when working with multiple groups, though the current level of clarity isn't necessarily bad. I may come back and clean that up, as I learned a ton from this project, but regardless of the cleanliness of this library, it is a success in my books.