-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(group_theory/presented_group): define presented groups #1118
Conversation
define group conjugates and normal closure
Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate.
Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate
(mergify uses the title for the commit message, I think) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This isn't the entirety of the universal property. We also need the (easy) fact that the extension is unique (amongst homomorphisms sending the generators to the specified places).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we also complete the UMP by defining the map of : α -> presented_group rels
and the proof that to_group f (of a) = f a
Co-Authored-By: Keeley Hoek <keeley@hoek.io>
I've now added the definition of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few minor comments about names.
…er-community#1118) * feat(group_theory/conjugates) : define conjugates define group conjugates and normal closure * feat(algebra/order_functions): generalize strict_mono.monotone (leanprover-community#1022) * trying to merge * feat(group_theory\presented_group): define presented groups Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate. * feat(group_theory\presented_group): define presented groups Presented groups are defined as a quotient of a free group by the normal subgroup the relations generate * Update src/group_theory/presented_group.lean Co-Authored-By: Keeley Hoek <keeley@hoek.io> * Uniqueness of extension * Tidied up to_group.unique * Removed unnecessary line * Changed naming
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list