UniMath
UniMath copied to clipboard
UniMath
cleanup in abelian groups
Some things which could be nicer about the file of monoids and groups:
- [x] Split up the file
Monoids_and_Groups.vin two or more parts - [x] Define kernels and images for
monoidsgroups, not just abelian groups - [ ] Move results in
CategoryTheory.categories.abgrswhich do not mention categories toAlgebra
@fpvandoorn -- how about adding your picture to your github profile? I like seeing faces.
Kernels of monoid maps are not important, because you can't recover a quotient monoid Y of a monoid X from the kernel of the projection map X --> Y, so why bother defining them?
What rationale is there for splitting the file up into parts, aside from it being large? What parts would you split it up into?
how about adding your picture to your github profile?
ok
Kernels of monoid maps are not important, because you can't recover a quotient monoid Y of a monoid X from the kernel of the projection map X --> Y, so why bother defining them?
Ok, but then we should at least do it for groups, not just abelian groups
What rationale is there for splitting the file up into parts, aside from it being large? What parts would you split it up into?
- It can be easier to find results in smaller files, if the separation of topics between the files is clear.
- It takes shorter to compile the file, if you are working in it.
I think Monoids_and_Groups.v should definitely be split up into two files Monoids.v and Groups.v. You can go one step further and have files like Subgroup.v QuotientGroup.v ProductGroup.v FreeGroup.v, etc.
UniMath/CategoryTheory/categories/abgrs.v line 650-ish. I'm moving what I needed in #831.
Oh, well that's why kernel and cokernel are defined in abgr.v -- the category is shown there to be an abelian category. And that's also why kernel and cokernels are not defined in grs.v -- the category of groups is not an abelian category. Nevertheless, one could add those definitions to grs.v -- at least it's a category where the natural map from the coimage to the image of a map is an isomorphism, and that can be useful. Moving the underlying algebraic facts from CategoryTheory to Algebra would be sensible.
In any case, the item "Define kernels and images for monoids groups, not just abelian groups" (in your original issue text) doesn't quite belong under the heading "Some things which could be nicer about the file of monoids and groups", because it doesn't concern the file Algebra/Monoids_and_Groups.v.
#958 takes care of defining kernels for monoids instead of just abelian groups. I do in fact define it for monoids, but I don't think it really matters: the definition is identical for monoids and groups, and it's just as easy to use either way.
