feat(group_theory/perm/concrete_cycle): isomorphism between permutations and cycles #8226
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
…union' into pechersky/more-perm-cycle
…sjoint" This reverts commit a2a427a.
…-prod-disjoint-union
Previously, both `support_pow_le` and `support_gpow_le` had the power as an `int`. Now we properly differentiate the two and avoid slow defeq checks.
pechersky
added
the
awaiting-author
github-actions
bot
added
blocked-by-other-PR
github-actions
bot
removed
the
merge-conflict
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 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! |
pechersky
added
awaiting-review
Vierkantor
reviewed
Aug 17, 2021
Vierkantor
added
awaiting-author
pechersky
added
awaiting-review
Vierkantor
reviewed
Aug 18, 2021
Comment on lines
+364
to
+366
| { rw [to_list_eq_nil_iff.mpr hx, is_rotated_nil_iff', to_list_eq_nil_iff], | ||
| obtain ⟨k, rfl⟩ := h, | ||
| simpa using hx } |
There was a problem hiding this comment.
This seems like a good candidate for a separate lemma, along the lines of
lemma same_cycle.mem_support_iff {f : perm α} {x y : α} (h : same_cycle f x y) :
x ∈ support f ↔ y ∈ support f :=
sorry
Comment on lines
+343
to
+363
| { obtain ⟨_ | k, hk, hy⟩ := h.nat_of_mem_support _ hx, | ||
| { simp only [coe_one, id.def, pow_zero] at hy, | ||
| simp [hy] }, | ||
| use k.succ, | ||
| apply list.ext_le, | ||
| { simp only [length_rotate, length_to_list, ←hy], | ||
| congr' 1, | ||
| ext z, | ||
| rw [mem_support, mem_support], | ||
| by_cases hz : same_cycle f x z, | ||
| { rw [hz.cycle_of_apply, same_cycle.cycle_of_apply], | ||
| simpa using hz }, | ||
| { rw [cycle_of_apply_of_not_same_cycle hz, cycle_of_apply_of_not_same_cycle], | ||
| simpa using hz } }, | ||
| { intros n hn hn', | ||
| suffices : (f ^ ((n + k.succ) % (f.cycle_of x).support.card)) x = | ||
| (f ^ n) ((f ^ k.succ) x), | ||
| { simpa [nth_le_rotate, nth_le_to_list, ←hy], }, | ||
| rw [←cycle_of_pow_apply_self, ←mul_apply, ←pow_add, ←cycle_of_pow_apply_self f, | ||
| ←order_of_is_cycle, ←pow_eq_mod_order_of], | ||
| exact is_cycle_cycle_of _ (mem_support.mp hx) } }, |
There was a problem hiding this comment.
There are some good sublemmas to extract here:
f.to_list ((f ^ k) x) = (f.to_list x).rotate k(f ^ (n % (f.cycle_of x).support.card)) x = (f ^ n) x
Comment on lines
+429
to
+430
| { rw [cycle.mem_coe_iff, mem_to_list_iff], | ||
| exact ⟨⟨1, by simp⟩, mem_support.mpr hx⟩ }, |
There was a problem hiding this comment.
This can be extracted as a lemma f^n x ∈ f.to_list x ↔ x ∈ f.support.
| simp [cycle.form_perm_eq_form_perm_iff, (iff_not_comm.mp hs.nontrivial_iff), | ||
| (iff_not_comm.mp hs'.nontrivial_iff), ht] } } | ||
|
|
||
| -- why does the decidability of `cycle.nodup` fail otherwise? |
There was a problem hiding this comment.
Not sure what this refers to?
Vierkantor
added
awaiting-author
|
By the way, >500 lines of additions really is a lot to do in one PR, especially when it introduces multiple |
github-actions
bot
added
the
merge-conflict
This was referenced Aug 24, 2021
|
Closed in favor #9470 |
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.
In the following,
{α : Type*} [fintype α] [decidable_eq α].cycle.form_perm: the cyclic permutation created by looping over acycle αequiv.perm.to_list: thelistrepresentation of the cycle generated byf : perm αstarting fromx : αequiv.perm.to_cycle: thecyclerepresentation of the cycle generated byf : perm αwherehf : f.is_cycleequiv.perm.iso_cycle: the equivalence between cyclic permutationsf : perm αand the terms of
cycle αthat correspond to themequiv.perm.iso_cycle': the same equivalence asequiv.perm.iso_cyclebut with faster evaluation via
#evalc[1, 2, 3]to emulate notation of cyclic permutations(1 2 3)has_reprinstance for anyperm α, by representing thefinsetofcycle αthat correspond to the cycle factors.equiv.perm.is_cycle.exists_unique_cycle: there is only one nontrivialcycle αcorresponding to each cyclic
f : perm αA caveat:
Running
#evalon even a simple noncyclic permutationc[(1 : fin 7), 2, 3] * c[0, 5]to show it takes a long time. TODO: is this because computing the cycle factors is slow?