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

[Merged by Bors] - feat(data/equiv/fintype): computable bijections and perms from/to fintype #6959

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(data/equiv/fintype): computable bijections and perms from/to fintype #6959

wants to merge 13 commits into from

Conversation

pechersky
Copy link
Collaborator

@pechersky pechersky commented Mar 30, 2021 •
edited by github-actions bot

Using exhaustive search, we can upgrade embeddings from fintypes into
equivs, and transport perms across embeddings. The computational
performance is poor, so the docstring suggests alternatives when an
explicit inverse is known.

Open in Gitpod

@pechersky
feat(data/equiv/fintype): computable bijections and perms from/to fin…
a9cbaf4 
…type

Using exhaustive search, we can upgrade embeddings from fintypes into
equivs, and transport perms across embeddings. The computational
performance is poor, so the docstring suggests alternatives when an
explicit inverse is known.
@pechersky pechersky added the awaiting-review The author would like community review of the PR label Mar 30, 2021
@pechersky pechersky mentioned this pull request Mar 30, 2021
Closed
2 tasks
@pechersky
Copy link
Collaborator Author

Should via_embedding have a noncomputable version that does not assume fintype, and a fintype alternative? Is there a good way to bundle an embedding with its partial inverse?

@eric-wieser
Copy link
Member

Is there a good way to bundle an embedding with its partial inverse?

Yes, function.left_inverse

@pechersky
Copy link
Collaborator Author

I do wonder whether this definition is particularly useful vs using subtype_congr directly.

Transporting a perm across an embedding seems like the more natural way to think about what is going mathematically. The fact that it is formalized as a split perm over the sum type of subtypes is an implementation detail, in my opinion.

@pechersky @eric-wieser
Update src/data/equiv/basic.lean
f791c20 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 31, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 31, 2021
Vierkantor
Vierkantor reviewed Mar 31, 2021
View reviewed changes
src/data/equiv/fintype.lean Outdated Show resolved Hide resolved
src/group_theory/perm/sign.lean Outdated Show resolved Hide resolved
src/data/equiv/basic.lean Outdated Show resolved Hide resolved
src/data/equiv/basic.lean Outdated Show resolved Hide resolved
src/data/equiv/basic.lean Outdated Show resolved Hide resolved
src/data/equiv/basic.lean Show resolved Hide resolved
src/data/equiv/basic.lean Outdated Show resolved Hide resolved
src/data/equiv/fintype.lean Outdated Show resolved Hide resolved
src/data/equiv/basic.lean Show resolved Hide resolved
@Vierkantor Vierkantor 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 Mar 31, 2021
@pechersky pechersky 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 Mar 31, 2021
@github-actions github-actions bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Mar 31, 2021
@github-actions
Copy link

github-actions bot commented Apr 1, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 1, 2021
Vierkantor
Vierkantor approved these changes Apr 1, 2021
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Looks good to me with @eric-wieser's suggestions.

bors d+

src/data/equiv/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Apr 1, 2021

✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@Vierkantor Vierkantor added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 1, 2021
@pechersky
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 2, 2021
@pechersky
feat(data/equiv/fintype): computable bijections and perms from/to fin…
7337702 
…type (#6959)

Using exhaustive search, we can upgrade embeddings from fintypes into
equivs, and transport perms across embeddings. The computational
performance is poor, so the docstring suggests alternatives when an
explicit inverse is known.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@bors
Copy link

bors bot commented Apr 2, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/equiv/fintype): computable bijections and perms from/to fintype [Merged by Bors] - feat(data/equiv/fintype): computable bijections and perms from/to fintype Apr 2, 2021
@bors bors bot closed this Apr 2, 2021
@bors bors bot deleted the pechersky/fintype-computable-equiv branch April 2, 2021 04:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@pechersky @eric-wieser @Vierkantor