The normalizer formula for passport size

The normalizer of a passport's reference monodromy group acts on its generating triples. Every stabilizer is the centralizer, so every orbit has the same size. Counting the generating triples by orbits gives an exact division formula for the number of isomorphism classes in the passport in terms of the finite set of generating triples. The divisibility statement makes the natural-number quotient meaningful. A separate generating-triple count can evaluate the finite-set cardinality to obtain a formula in terms of cycle data.

References

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

theorem TauCeti.PassportSpec.card_generatingTripleOrbits_mul_card_normalizer_eq_card_generatingTriple_mul_card_centralizer {n : ℕ} (P : PassportSpec n) : Nat.card (MulAction.orbitRel.Quotient (↥(Subgroup.normalizer ↑P.G)) P.GeneratingTriple) * Nat.card ↥(Subgroup.normalizer ↑P.G) = Nat.card P.GeneratingTriple * Nat.card ↥(Subgroup.centralizer ↑P.G)

Counting generating triples orbit by orbit: the number of normalizer orbits times the normalizer order equals the number of generating triples times the centralizer order.

theorem TauCeti.PassportSpec.passportSize_mul_card_normalizer_eq_card_generatingTriple_mul_card_centralizer {n : ℕ} (P : PassportSpec n) (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) : P.passportSize * Nat.card ↥(Subgroup.normalizer ↑P.G) = Nat.card P.GeneratingTriple * Nat.card ↥(Subgroup.centralizer ↑P.G)

Counting generating triples orbit by orbit: the number of passport classes times the normalizer order equals the number of generating triples times the centralizer order.

theorem TauCeti.PassportSpec.card_normalizer_dvd_card_generatingTriple_mul_card_centralizer {n : ℕ} (P : PassportSpec n) : Nat.card ↥(Subgroup.normalizer ↑P.G) ∣ Nat.card P.GeneratingTriple * Nat.card ↥(Subgroup.centralizer ↑P.G)

The normalizer order divides the product of the generating-triple count and the centralizer order.

theorem TauCeti.PassportSpec.passportSize_eq_card_generatingTriples_mul_card_centralizer_div_card_normalizer {n : ℕ} (P : PassportSpec n) (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) : P.passportSize = P.generatingTriples.card * Nat.card ↥(Subgroup.centralizer ↑P.G) / Nat.card ↥(Subgroup.normalizer ↑P.G)

The passport-size formula in terms of the generating-triple finset: its elements form equal normalizer orbits, each having normalizer order divided by centralizer order elements.