search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
456 stars 139 forks source link

Transfer `Group` definitions to `AbGroup` #663

Open barrettj12 opened 2 years ago

barrettj12 commented 2 years ago

A lot of the theory of groups has been developed in Algebra.Group: subgroups, quotients, etc. Most of this will also apply to abelian groups.

However, at present, it is quite a pain to use these results with an AbGroup - one has to cast it to a Group, apply the result, then transform it back into an AbGroup, which involves providing each time a proof of commutativity. These proofs are usually "trivial" but kind of tedious to give.

It would be nice to transfer some of the theory from Algebra.Group to Algebra.AbGroup. This should be as simple as providing wrappers for the the corresponding Group definitions, and giving the proof of commutativity once and for all.

mortberg commented 2 years ago

Can't you just open the group modules with the underlying group of the abelian group and get access to all the results?

barrettj12 commented 2 years ago

Sure. I'm more talking about stuff like taking the quotient of an abelian group by a subgroup, or using e.g. Subgroup→Group to turn a Subgroup (AbGroup→Group A) into an AbGroup ℓ. The point is, it would be nice to have interfaces for all of these which deal directly with AbGroup rather than Group.

mortberg commented 2 years ago

Ah I see. I wondered how annoying this would get when I wrote some of the code for groups. I wonder if there is a solution which involves writing less boilerplate code... This kind of problem will occurs in many places

barrettj12 commented 2 years ago

I think there's inevitably gonna be boilerplate somewhere, so better to have it written once and for all in the library.