Stabilizers of generating triples

The normalizer of a passport's reference monodromy group acts on its generating triples. Every generating triple has the same stabilizer: the centralizer of that reference group, viewed as a subgroup of the normalizer. Orbit-stabilizer then gives the size of each orbit. This per-orbit equation uses no total generating-triple count.

The result uses only the fact that the first two permutations generate the reference group; no connectedness or admissibility hypothesis is needed.

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.

@[simp]

theorem TauCeti.PassportSpec.stabilizer_generatingTriple_eq_centralizer_subgroupOf {n : ℕ} (P : PassportSpec n) (g : P.GeneratingTriple) : MulAction.stabilizer (↥(Subgroup.normalizer ↑P.G)) g = (Subgroup.centralizer ↑P.G).subgroupOf (Subgroup.normalizer ↑P.G)

The stabilizer of any generating triple under the normalizer action is the centralizer of the reference monodromy group, regarded as a subgroup of its normalizer.

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

Orbit-stabilizer for a generating triple, with its stabilizer expressed as the centralizer of the reference monodromy group.