Generating counts by cycle type

A cycle type in a permutation subgroup can contain several conjugacy classes of that subgroup. Consequently, counting product-one triples with prescribed cycle types requires a sum over three sets of conjugacy classes. The generating count below applies this sum to the subgroup-lattice generating counts, and identifies it with generating triples of the prescribed cycle types.

References

• S. K. Lando and A. K. Zvonkin, Graphs on Surfaces and Their Applications, §1.5.
• M. Musty, S. Schiavone, J. Sijsling and J. Voight, A database of Belyi maps, §2.

noncomputable def Subgroup.genCountType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (lam0 lam1 laminf : Multiset ℕ) : ℕ

The number of product-one triples generating G with three specified full cycle types. Each type is refined into the conjugacy classes of G that it meets.

Equations

• One or more equations did not get rendered due to their size.

theorem Subgroup.genCountType_def {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (lam0 lam1 laminf : Multiset ℕ) : G.genCountType lam0 lam1 laminf = ∑ C0 ∈ G.classesOfFullCycleType lam0, ∑ C1 ∈ G.classesOfFullCycleType lam1, ∑ Cinf ∈ G.classesOfFullCycleType laminf, (TauCeti.generatingProductOneTriples C0 C1 Cinf ⊤).card

The class-sum formula for the generating count with prescribed full cycle types.

noncomputable def Subgroup.generatingTriplesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (lam0 lam1 laminf : Multiset ℕ) : Finset (↥G × ↥G × ↥G)

The product-one triples of G that generate G and have the prescribed cycle types.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.mem_generatingTriplesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) {lam0 lam1 laminf : Multiset ℕ} {p : ↥G × ↥G × ↥G} : p ∈ G.generatingTriplesOfFullCycleType lam0 lam1 laminf ↔ p.2.2 * p.2.1 * p.1 = 1 ∧ TauCeti.productOneGeneratedSubgroup p = ⊤ ∧ (↑p.1).fullCycleType = lam0 ∧ (↑p.2.1).fullCycleType = lam1 ∧ (↑p.2.2).fullCycleType = laminf

theorem Subgroup.card_generatingTriplesOfFullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (lam0 lam1 laminf : Multiset ℕ) : (G.generatingTriplesOfFullCycleType lam0 lam1 laminf).card = G.genCountType lam0 lam1 laminf

Summing the generating counts over the three class refinements counts exactly the triples of the prescribed cycle types.