Stream: math-comp users

Topic: Cycles


view this post on Zulip Raul (Mar 13 2023 at 22:40):

Hi all,
I'm trying to work on a cycle demposition of permutations in a similar way it's done in mathcomp library for transpositions.
For defining cycles themselves I would prefer to be able to give a list, again similar to your transpositions.

Is it already in the library?

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2023 at 22:48):

fconnect and orbit defined in fingraph.v would be useful for that. I don't know whether their theory has been connected to that of symmetric groups.

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2023 at 22:49):

There is porbit in perm.v.

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2023 at 22:58):

Ah, so I guess your problem is that porbit does not return a list but a set (right?). Then using traject seems to be a solution.

view this post on Zulip Raul (Mar 13 2023 at 23:00):

Well, rather that I want to define the cycles out of a list given by me (along with a proof of uniq l).

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2023 at 23:08):

So, you want to give a cycle as a list, and obtain a permutation that has the given cycle?

view this post on Zulip Raul (Mar 13 2023 at 23:08):

Yes!

view this post on Zulip Raul (Mar 13 2023 at 23:10):

And proving that all the permutations are a product of disjoint cycles, but this might be done with porbits I guess.

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2023 at 23:23):

The function you want to prove injective would then be this one:

Definition fun_of_cycle (T : eqType) (xs : seq T) (x : T) : T :=
  nth x (rot 1 xs) (index x xs).

view this post on Zulip Raul (Mar 13 2023 at 23:34):

Corresponds exactly to nth_uniq.
Surely, I'll be able to work myself the other part out.
Thx!


Last updated: Jul 15 2024 at 20:02 UTC