-
Notifications
You must be signed in to change notification settings - Fork 257
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
[Merged by Bors] - feat(LinearAlgebra/Matrix): define projective special linear group #7791
Conversation
shuxuezhuyi
commented
Oct 20, 2023
Do you have plans to prove theorems about |
Yes, but I will not prove many theorems about |
Ok sounds good. Looking forward to seeing some Fuchsian groups. maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alexjbest. |
It would also be good to add some API like we have for
lemmas Can you add that in this PR too actually? |
Actually thinking about it more, I'm not sure what lemmas even make sense, we don't have an actual coercion to matrices, so maybe this is fine like it is. |
I suspect that it might be problematic to instance a coercion from noncomputable def sl (a : ProjectiveSpecialLinearGroup n R) :
SpecialLinearGroup n R := Classical.choose a.exists_rep And I used it to instance |
That |
Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause |
This is a pretty bare definition, but unless someone has suggestions on what to add, I think we could merge it. maintainer merge |
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
/-- A projective special linear group is the quotient of a special linear group by its center.-/ | ||
abbrev ProjectiveSpecialLinearGroup : Type _ := | ||
SpecialLinearGroup n R ⧸ Subgroup.center (SpecialLinearGroup n R) |
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.
Is X / Subgroup.Center X
something worth naming in its own right?
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.
I think there is no standard name for this, so it would only confuse people.
bors merge |
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…7791) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>