Passport sizes from generating counts

For a nonzero degree and a pretransitive monodromy group, the class sum for generating triples gives the passport size after multiplying by the centralizer order and dividing by the normalizer order.

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.

theorem TauCeti.PassportSpec.card_generatingTriples_eq_genCountType {n : ℕ} (P : PassportSpec n) : P.generatingTriples.card = P.G.genCountType P.lam0 P.lam1 P.laminf

The class sum genCountType is the number of generating triples of a passport, before quotienting by its normalizer.

theorem TauCeti.PassportSpec.card_normalizer_dvd_genCountType_mul_card_centralizer {n : ℕ} (P : PassportSpec n) : Nat.card ↥(Subgroup.normalizer ↑P.G) ∣ P.G.genCountType P.lam0 P.lam1 P.laminf * Nat.card ↥(Subgroup.centralizer ↑P.G)

The normalizer order divides the generating count by cycle type times the centralizer order. This is the exact divisibility behind the natural-number passport-size formula.

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

For nonzero degree and a pretransitive monodromy group, a passport's size is the generating count by cycle type times the centralizer order divided by the normalizer order.