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

feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C #8559

Open
wants to merge 24 commits into
base: master
Choose a base branch
from
Open

feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C #8559

wants to merge 24 commits into from

Conversation

shadasali
Copy link
Collaborator

We defined dihedral_to_complex_hom to provide the canonical homomorphism of the dihedral group
into the linear isometries of ℂ.

Open in Gitpod

@shadasali shadasali added the awaiting-review The author would like community review of the PR label Aug 5, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 5, 2021
@bryangingechen bryangingechen changed the title feat(Analysis/Complex/Isometry): Homomorphism from Dihedral Group into Linear Isometries of C feat(analysis/complex/isometry): Homomorphism from Dihedral Group into Linear Isometries of C Aug 5, 2021
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 6, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 6, 2021
Ruben-VandeVelde
Ruben-VandeVelde reviewed Aug 8, 2021
View reviewed changes
src/analysis/complex/circle.lean Outdated Show resolved Hide resolved
src/analysis/complex/circle.lean Outdated Show resolved Hide resolved
src/analysis/complex/circle.lean Outdated Show resolved Hide resolved
@shadasali
Copy link
Collaborator Author

The import hierarchy was changed in #8424 so that analysis.special_functions.trigonometric indirectly imports analysis.complex.isometry. Therefore, I had to change the structure of the PR to adjust to these changes.

@shadasali shadasali added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 12, 2021
@jcommelin jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 26, 2021
jcommelin
jcommelin reviewed Aug 28, 2021
View reviewed changes
src/analysis/complex/dihedral.lean Outdated Show resolved Hide resolved
src/analysis/complex/dihedral.lean Outdated Show resolved Hide resolved
src/analysis/complex/dihedral.lean Outdated Show resolved Hide resolved
src/analysis/complex/dihedral.lean Outdated Show resolved Hide resolved
src/analysis/complex/dihedral.lean Outdated Show resolved Hide resolved
@jcommelin
Copy link
Member

@shadasali I pushed a cleanup. Now I need to run. I suggest that you look at the diff to learn some tricks that I applied.

eric-wieser
eric-wieser reviewed Aug 28, 2021
View reviewed changes
src/analysis/special_functions/trigonometric.lean Outdated
@@ -2377,6 +2378,18 @@ by rw [log, exp_add_mul_I, ← of_real_sin, sin_arg, ← of_real_cos, cos_arg hx
mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), ← mul_assoc,
mul_div_cancel' _ (of_real_ne_zero.2 (mt abs_eq_zero.1 hx)), re_add_im]

lemma exp_map_circle_surjective : function.surjective exp_map_circle :=
Copy link
Member

Choose a reason for hiding this comment

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

Wouldn't it be easier and more useful to show by first showing that complex.arg ∘ coe is a right-inverse, then using function.right_inverse.surjective?

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 27, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 15, 2021
@eric-wieser
Copy link
Member

I resolved the merge conflicts just to see what's left here, but didn't actually check if the merge builds. @shadasali, do you plan to come back to this, or shall I mark it "please adopt"?

@hrmacbeth
Copy link
Member

Note that some of the work here has now been carried out independently by @urkud -- I'm thinking in particular of the lemmas in src/analysis/special_functions/complex/log.lean. So it should not just be updated to master, but also reworked to depend on the newly-developed theory.

@hrmacbeth hrmacbeth mentioned this pull request Dec 15, 2021
Closed
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Dec 15, 2021
@YaelDillies
Copy link
Collaborator

Let me mention here that a student is currently formalising the same result on the Xena discord.

@YaelDillies YaelDillies added t-algebra Algebra (groups, rings, fields etc) and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Apr 20, 2023
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@pechersky pechersky pechersky left review comments

@jcommelin jcommelin jcommelin left review comments

@hrmacbeth hrmacbeth hrmacbeth left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields etc) too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
9 participants
@shadasali @jcommelin @eric-wieser @hrmacbeth @YaelDillies @urkud @pechersky @Ruben-VandeVelde @semorrison