The conjugacy classes of a cycle type in a group of permutations

An S_n-cycle type can meet several conjugacy classes of a subgroup G ≤ S_n, and can meet none, so the elements of G of a prescribed full cycle type are counted by a sum over a finite index set of G-classes rather than by a single class size. This file names that index set, for a group of permutations of any finite carrier, and identifies the union of those classes with the elements of that cycle type. A finite group has only finitely many conjugacy classes, so the classes of a given cycle type form a Finset, and the count over them is a finite sum of class sizes.

Main results

• TauCeti.Subgroup.classesOfFullCycleType: the conjugacy classes of G whose members have full cycle type mu.
• TauCeti.Subgroup.iUnionClassesOfFullCycleType: the set of the elements of G of full cycle type mu, the union of those classes.
• TauCeti.Subgroup.mem_iUnionClassesOfFullCycleType: an element of G is a member of one of the classes of type mu exactly when it has full cycle type mu.
• TauCeti.Subgroup.mem_iUnion_classesOfFullCycleType: that same characterization with the union of the classes written out.

noncomputable def Subgroup.classesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (mu : Multiset ℕ) : Finset (ConjClasses ↥G)

The conjugacy classes of the subgroup G whose members have full cycle type mu.

One S_n-cycle type can meet several G-classes, and can meet none, so the elements of G of a prescribed cycle type are counted by a sum over this index set rather than by one class size.

Equations

• G.classesOfFullCycleType mu = {C : ConjClasses ↥G | ∃ (g : ↥G), ConjClasses.mk g = C ∧ (↑g).fullCycleType = mu}

@[simp]

theorem Subgroup.mem_classesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} {mu : Multiset ℕ} {C : ConjClasses ↥G} : C ∈ G.classesOfFullCycleType mu ↔ ∃ (g : ↥G), ConjClasses.mk g = C ∧ (↑g).fullCycleType = mu

noncomputable def Subgroup.iUnionClassesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (mu : Multiset ℕ) : Set ↥G

The elements of G of full cycle type mu: the union of the conjugacy classes recorded by TauCeti.Subgroup.classesOfFullCycleType. This is the set whose membership TauCeti.Subgroup.mem_iUnionClassesOfFullCycleType characterizes, and the set whose size is the sum of those class sizes.

Equations

• G.iUnionClassesOfFullCycleType mu = ⋃ C ∈ G.classesOfFullCycleType mu, C.carrier

theorem Subgroup.mem_iUnion_classesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (mu : Multiset ℕ) (g : ↥G) : g ∈ ⋃ C ∈ G.classesOfFullCycleType mu, C.carrier ↔ (↑g).fullCycleType = mu

An element of G is a member of one of its classes of type mu exactly when it has full cycle type mu. One cycle type can meet several classes, and this says that the union of the classes recorded by TauCeti.Subgroup.classesOfFullCycleType is exactly the set of elements of that type.

@[simp]

theorem Subgroup.mem_iUnionClassesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} {mu : Multiset ℕ} {g : ↥G} : g ∈ G.iUnionClassesOfFullCycleType mu ↔ (↑g).fullCycleType = mu

The same characterization as TauCeti.Subgroup.mem_iUnion_classesOfFullCycleType, read on the named set TauCeti.Subgroup.iUnionClassesOfFullCycleType, whose left-hand side is in simp normal form and so normalizes membership to the cycle-type condition.

theorem Subgroup.mem_classesOfFullCycleType_mk {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (mu : Multiset ℕ) (g : ↥G) : ConjClasses.mk g ∈ G.classesOfFullCycleType mu ↔ (↑g).fullCycleType = mu

A conjugacy class of a permutation subgroup has a specified full cycle type if and only if one (hence every) representative has that type.