Cycle lengths of a group element acting on a finite set

For a group acting on a finite set, the full cycle type of the permutation induced by an element is the multiset of sizes of the orbits of its cyclic subgroup. The acting group itself need not be finite. This connects permutation cycle lengths, including fixed points, to an orbit calculation in the original group.

The comparison uses Equiv.Perm.fullCycleType_eq_map_card_orbit and TauCeti.map_card_orbit_eq_of_orbit_eq: the permutation and the original group element have the same integer powers acting on the carrier, hence the same orbits.

For a free action (IsCancelSMul), such as the left-regular action of a group on itself, every orbit of the cyclic subgroup generated by g has orderOf g elements, so the full cycle type of g is Multiset.replicate (Nat.card X / orderOf g) (orderOf g) (MulAction.fullCycleType_toPerm_eq_replicate). The raw cycle type omits fixed points: for g ≠ 1 a free action has none, so the raw cycle type has the same parts (MulAction.cycleType_toPerm_eq_replicate, and MulAction.cycleType_toPerm_self for the regular action), while the identity has empty raw cycle type. Transported along a bijection e : G ≃ α, the regular action keeps its full cycle type (Equiv.fullCycleType_permutationRepresentation).

theorem MulAction.fullCycleType_toPerm_eq_map_card_orbit {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [Fintype X] [DecidableEq X] (g : G) : (toPerm g).fullCycleType = Multiset.map (fun (ω : orbitRel.Quotient (↥(Subgroup.zpowers g)) X) => Nat.card ↑ω.orbit) Finset.univ.val

The cycle lengths of the permutation induced by a group element are the sizes of the orbits of the cyclic subgroup it generates, including the singleton orbits.

theorem MulAction.fullCycleType_toPerm_eq_replicate {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] [Fintype X] [DecidableEq X] (g : G) : (toPerm g).fullCycleType = Multiset.replicate (Nat.card X / orderOf g) (orderOf g)

The cycle type of a free action. If G acts freely on a finite set X, then every cycle of the permutation induced by g has length orderOf g, so its full cycle type consists of Nat.card X / orderOf g parts equal to orderOf g. For the left-regular action of a finite group on itself, an element of order d in a group of order m thus acts with m / d cycles of length d.

theorem MulAction.cycleType_toPerm_eq_replicate {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] [Fintype X] [DecidableEq X] {g : G} (hg : g ≠ 1) : (toPerm g).cycleType = Multiset.replicate (Nat.card X / orderOf g) (orderOf g)

The raw cycle type of a free action. If G acts freely on a finite set X, then an element g ≠ 1 has no fixed points, so the cycle type of the permutation it induces, which omits fixed points, agrees with its full cycle type: Nat.card X / orderOf g parts equal to orderOf g. (The identity induces the identity permutation, whose cycle type is empty.)

@[simp]

theorem MulAction.cycleType_toPerm_self {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {g : G} (hg : g ≠ 1) : (toPerm g).cycleType = Multiset.replicate (Fintype.card G / orderOf g) (orderOf g)

The raw cycle type of the left-regular action. In a finite group of order m, left multiplication by an element g ≠ 1 of order d has no fixed points, so its cycle type is d ^ (m / d). (Left multiplication by 1 is the identity, whose cycle type is empty.)

@[simp]

theorem Equiv.fullCycleType_permutationRepresentation {G : Type u_1} {α : Type u_2} [Group G] [Fintype α] [DecidableEq α] (e : G ≃ α) (g : G) : (e.permutationRepresentation g).fullCycleType = Multiset.replicate (Fintype.card α / orderOf g) (orderOf g)

The regular image of g on a finite type α is a product of card α / d disjoint d-cycles, where d is the order of g.