category of group presentations #2172
Conversation
<!-- ps-id: 5e5a3494-92a5-4953-840c-c9564356a775 --> Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
ps/rr/category_of_group_presentations
branch
from
717248b to
56109f1
Compare
| (** Every group can be given a standard presentation. The set of generators are | ||
| the elements of the groups and the relations are such that the group operation | ||
| agrees with word concatenation. *) |
There was a problem hiding this comment.
| (** Every group can be given a standard presentation. The set of generators are | |
| the elements of the groups and the relations are such that the group operation | |
| agrees with word concatenation. *) | |
| (** Every group can be given a standard presentation. The generators are the elements of the group and the relations enforce that the group operation agrees with word concatenation. *) |
| exact ((freegroup_in (g * h))^ * freegroup_in g * freegroup_in h). | ||
| Defined. | ||
|
|
||
| (** Given a group, we have a homomorphism to the group presented by the standard presentation. *) |
There was a problem hiding this comment.
I think the map more naturally goes in the other direction.
|
|
||
| (** ** Category of group presentations *) | ||
|
|
||
| (** Group presentations together with their morphisms form a category. We can later show that this category is equivalent to the category of groups. *) |
There was a problem hiding this comment.
Below you say something that suggests that this true in every topos, so I'm confused.
Also, some more comment about the definition of GroupPresentationMorphism would be good. The first two entries are the same as giving homomorphisms FreeGroup (gq_generators p) $-> FreeGroup (gq_generators q) and FreeGroup (gq_rel_index p) $-> FreeGroup (gq_rel_index q), and the third entry says that these commute with the natural maps from latter groups to the former groups.
There was a problem hiding this comment.
I suspect that this is not true in every topos. But I haven't been able to definitely prove that. The reason I suspect, is because similar statements in set theory require AC or at least the boolean prime ideal theorem. I hope we can at least get an adjunction here, but I haven't been able to push this through due to lack of time.
|
There are some things I need to work out with this. I thought they would be easy to resolve but it looks like this PR is not ready. I don't have too much time to work on it any longer. I will come back to it at some point. |
Here is some material on group presentations. We show that group presentations with structure preserving morphisms form a category and that the group presented by a presentation construction becomes a functor. We give some related properties about the standard presentation including all finite groups being finitely presented.
This is in preparation for some WIP on Tietze equivalences which should be a factorisation theorem for presentation equivalences between finitely presented presentations.
Working at the level of morphisms of presentation is much cleaner than having to go through
group_gpsince you only have to deal with free groups.