feat(group_theory/perm/sign): Add equiv.perm.move, to move an item in a permutation
#4739
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
added
the
blocked-by-other-PR
…in a permutation Also provides a decomposition to convert any swap into a series of adjacent swaps
eric-wieser
force-pushed
the
eric-wieser/perm-move
branch
from
c2e20f2
to
1c13a10
Compare
eric-wieser
commented
Oct 22, 2020
Comment on lines
+790
to
+793
| /-- | ||
| A permutation that swaps `i` with `i+1`. | ||
| -/ | ||
| def adj_swap [add_monoid α] [has_one α] (i : α) : perm α := equiv.swap i (i + 1) |
There was a problem hiding this comment.
Frustratingly I can't actually use this definition for fin ℕ
There was a problem hiding this comment.
Suggested change
| /-- | |
| A permutation that swaps `i` with `i+1`. | |
| -/ | |
| def adj_swap [add_monoid α] [has_one α] (i : α) : perm α := equiv.swap i (i + 1) | |
| variables {ι : Type*} [decidable_eq ι] [has_zero ι] [has_one ι] [has_add ι] -- castable to ℕ | |
| /-- | |
| A permutation that swaps `i` with `i+1`. | |
| -/ | |
| def adj_swap (i : ι) : perm ι := equiv.swap i (i + 1) | |
| /-- The set of adjacent swaps needed to perform a move -/ | |
| def move_components (i j : ℕ) : list (perm ι) := | |
| (((list.range' j (i - j) ++ (list.range' i (j - i)).reverse).map nat.cast).map adj_swap) |
What about that @eric-wieser?
There was a problem hiding this comment.
That's a good idea, thanks! I think I was shelving this PR until @Vierkantor wraps up or abandons their has_enum typeclass, or whatever it was; but I'll try that approach when I revive it!
There was a problem hiding this comment.
(or, feel free to adopt this branch yourself)
github-actions
bot
added
the
merge-conflict
bryangingechen
removed
the
blocked-by-other-PR
github-actions
bot
removed
the
merge-conflict
|
I would prefer to see the right abstraction in place so that |
github-actions
bot
added
the
merge-conflict
|
This PR/issue depends on: |
semorrison
added
the
too-late
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This was written in the hopes it would provide some building blocks for breaking up the proofs in #3770