[Merged by Bors] - feat(group_theory/perm/cycle_type): Cycle type of a permutation

[tb65536]

This PR defines the cycle type of a permutation.

At some point we should prove the bijection between partitions and conjugacy classes.

---

• depends on: [Merged by Bors] - feat(group_theory/perm/*): facts about the cardinality of the support of a permutation #6951
• depends on: [Merged by Bors] - feat(group_theory/perm/sign): Order of product of disjoint permutations #6998
• depends on: [Merged by Bors] - feat(group_theory/perm/cycles): Applying cycle_of to an is_cycle #7000

[bryangingechen]

(I canceled the builds of fc5b7c4 and 35c67a3 because our GitHub actions queue is backed up.)

[github-actions]

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

• [Merged by Bors] - feat(group_theory/perm/*): facts about the cardinality of the support of a permutation #6951
• [Merged by Bors] - feat(group_theory/perm/sign): Order of product of disjoint permutations #6998
• [Merged by Bors] - feat(group_theory/perm/cycles): Applying cycle_of to an is_cycle #7000

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

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

[jcommelin]

@awainverse was this not already somewhere else? You know this part of the library best. Is this the correct place for the instance, or should it go somewhere in data/nat/*?

[awainverse]

It's been a minute, but it looks like the only global instances of gcd_monoid anywhere are polynomial.gcd_monoid and int.gcd_monoid. There is also unique_factorization_monoid.to_gcd_monoid, which is not an instance because it would cause a loop. Perhaps it's better if this just goes in ring_theory/int/basic next to int.gcd_monoid? I told @tb65536 it could go in either place.

[tb65536]

It seems weird to me to put this in ring_theory/int/basic when this doesn't use facts about the integers.

[awainverse]

(In case it's not clear, either place is actually still fine with me)

[tb65536]

I should mention that the gcd_monoid instance is also in #7180

[Julian-Kuelshammer]

I'm happy to close #7180 but I'm wondering whether it makes more sense to deduce the normalization_monoid part from unique (units nat) which already exists - althought in the very weird ring_theory/int/basic. I think it would be better to move it to data/nat/basic where one can also find this fact (not as an instance).

[fpvandoorn]

This is a very nice development. The statements look great. The proofs overall look pretty clean as well, I have some minor comments.
I haven't looked before at permutations in mathlib, but the library seems to work very nicely!

How far away are you to showing that two permutations are conjugates iff they have the same cycle type? That seems like a nice fact.

[awainverse]

@fpvandoorn, I have progress towards that conjugacy result at #7024, and most of the rest at the branch disjoint_conj. It's coming soon! We may also end up with a proof closer to what's familiar as @pechersky develops a function to construct a cycle from a list.

[fpvandoorn]

bors d+

[bors]

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

[tb65536]

bors r+

[fpvandoorn]

Generally please wait to bors r+ until Github actions has succeeded al steps, it's annoying if bors tries to merge a failing build (in this case it's probably fine, since the linter passed the previous commit).

[tb65536]

Generally please wait to bors r+ until Github actions has succeeded al steps, it's annoying if bors tries to merge a failing build (in this case it's probably fine, since the linter passed the previous commit).

Ah, thanks for mentioning this.

[pechersky]

@fpvandoorn, I have progress towards that conjugacy result at #7024, and most of the rest at the branch disjoint_conj. It's coming soon! We may also end up with a proof closer to what's familiar as @pechersky develops a function to construct a cycle from a list.

You can view the https://github.com/leanprover-community/mathlib/tree/pechersky/list-rotate-cycle branch I have, which merged in some commits from your disjoint_conj branch. One can define a perm from a list via list.form_perm, with a proof that the support of that perm is equal to the list if the list is nodup. I've also shown that list.form_perm l is is_cycle when nodup l and l is at least two elements.

There is also a cycle type defined which is the quotient of lists by rotation. That also has a perm defined on it via a lift from list.

I haven't proved things about conjugacy, but I think with my refactor of perm.support, perm.disjoint, and the proofs I have about the way that form_perm works, like form_perm l (l.nth_le k _) = l.nth_le ((k + 1) % l.length) _, I hope that that makes it easier to prove things about such constructed perms.

One more note -- the support refactor is at #7118, generalizing perm.support to be set instead of finset. That breaks some of the proofs in the branch that are from disjoint_conj, and I haven't fixed that yet.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests