braid group word problem

Stream: new members

[Hannah Fechtner]

hi all, thought I ought to eventually actually introduce myself! I'm hoping to formalize a solution (Garside's, as elucidated in Dehornoy) to the word problem in braid groups (Artin's algebraic presentation). Should be putting in some pull requests for parts of this shortly

This is broken down into parts, some of the (nearly) finished ones including:

• localization of a non-commutative monoid (having cancellativity and right-common-multiples) - aka Ore localization
• presented monoids
• proof that the Ore localization of a presented monoid (by a set of generators and relations) is isomorphic to the presented group on those generators & relations
• definition of a braid monoid
• definition of a braid group
• proof that braid monoids have right-common multiples

Still need to show the braid monoid is cancellable, and then a big job of using the localization to get a canonical form for elements of the braid group

[Mario Carneiro]

Good to see you here Hannah. I would suggest you get on those early PRs soon (in particular, don't wait to be done with the full proof) because the reviews can take time that you can parallelize with your own work, and also because if the reviewers want to make changes to early definitions then you will want to know it ASAP.

[Hannah Fechtner]

goal is to make the first PR tonight :)