Skip to content
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.

Sign up for GitHub

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

Jump to bottom

conjugation of group elements #2178

Merged
merged 1 commit into from
Jan 3, 2025
Merged

conjugation of group elements #2178

merged 1 commit into from
Jan 3, 2025

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 3, 2025

Here are the basics on conjugation in groups.

@Alizter Alizter requested a review from jdchristensen January 3, 2025 03:22
@Alizter
Copy link
Collaborator Author

Alizter commented Jan 3, 2025

I chose the convention y * x * y^ since that is how we conjugate elsewhere in the library already. I am however starting to think the other y^ * x * y might be better since it is more commonly used in group theory. Not sure.

@Alizter
Copy link
Collaborator Author

Alizter commented Jan 3, 2025

Perhaps the best way forward is to have both and use them whenever they are needed. Any result about one will become a result about the other in the opposite group.

jdchristensen
jdchristensen approved these changes Jan 3, 2025
View reviewed changes
theories/Algebra/Groups/Group.v Outdated Show resolved Hide resolved
@jdchristensen
Copy link
Collaborator

I chose the convention y * x * y^ since that is how we conjugate elsewhere in the library already. I am however starting to think the other y^ * x * y might be better since it is more commonly used in group theory. Not sure.

I think y * x * y^ is fine. It has the advantage that grp_conj is a homomorphism from the group to the group of self-equivalences rather than an anti-homomorphism.

Perhaps the best way forward is to have both and use them whenever they are needed. Any result about one will become a result about the other in the opposite group.

In the opposite group, it'll turn out to be y^ * (x * y), which is different from y^ * x * y. So there are really four choices here.

@Alizter
conjugation of group elements
ec97d58 
Co-authored-by: Dan Christensen <jdc+github@uwo.ca>

Signed-off-by: Ali Caglayan <alizter@gmail.com>
@Alizter Alizter force-pushed the ps/rr/conjugation_of_group_elements branch from cbbfcd4 to ec97d58 Compare January 3, 2025 21:30
Alizter
Alizter commented Jan 3, 2025
View reviewed changes
theories/Algebra/Groups/Group.v
Comment on lines +1175 to +1181
(** Conjugation commutes with group homomorphisms. *)
Definition grp_homo_conj {G H : Group} (f : G $-> H) (x : G)
: f $o grp_conj x $== grp_conj (f x) $o f.
Proof.
intros z; simpl.
by rewrite !grp_homo_op, grp_homo_inv.
Defined.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added this lemma when rebasing.

@jdchristensen
Copy link
Collaborator

This LGTM.

@Alizter Alizter merged commit 1d51f2c into HoTT:master Jan 3, 2025
22 checks passed
@Alizter Alizter deleted the ps/rr/conjugation_of_group_elements branch January 3, 2025 23:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jdchristensen jdchristensen jdchristensen approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Alizter @jdchristensen