Generating triples of a passport and the normalizer action

A connected permutation triple lies in a passport when its monodromy subgroup is conjugate to the reference subgroup P.G and its ordered full cycle partitions are the ones recorded by P. Relabeling the sheets can always move the monodromy subgroup onto P.G itself, and this file describes what is left of that freedom. A generating triple of P is a permutation triple whose monodromy subgroup is P.G on the nose and whose cycle partitions are those of P; since the monodromy subgroup is by definition generated by the first two components, this is a pair of generators of P.G with prescribed cycle data, the third component being determined.

A relabeling carrying one generating triple of P to another necessarily normalizes P.G, so for a passport of nonzero degree whose reference subgroup is transitive, the isomorphism classes inside that passport are the orbits of the normalizer N_{S_n}(P.G) acting by simultaneous conjugation on the generating triples, and the size of that passport is the number of those orbits. Both hypotheses are needed, and are the two conjuncts of TauCeti.PassportSpec.IsAdmissible that make a generating triple connected. This is the shape in which passport sizes are computed: generating triples of a fixed subgroup with fixed cycle data are counted inside that subgroup, and the count is then divided by the normalizer action rather than by the whole symmetric group. The normalizer is not P.G itself: two generating triples of P.G can be conjugate in the symmetric group only through an element normalizing P.G, and inner conjugation is in general a proper subgroup of that.

Main declarations

• TauCeti.PassportSpec.IsGeneratingTriple and TauCeti.PassportSpec.GeneratingTriple: the generating triples of a passport, and the type they form.
• TauCeti.PassportSpec.exists_isGeneratingTriple_smul and TauCeti.PassportSpec.mem_normalizer_of_monodromyGroup_smul_eq: a connected triple in a passport is isomorphic to a generating triple of it, uniquely up to the normalizer.
• TauCeti.PassportSpec.generatingTripleOrbitsEquivClasses: for a passport of nonzero degree with transitive reference subgroup, the orbits of the normalizer on the generating triples of that passport are the isomorphism classes in it.
• TauCeti.PassportSpec.passportSize_eq_card_generatingTripleOrbits: under the same hypotheses, the passport size is the number of those orbits.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.5.
• M. Musty, S. Schiavone, J. Sijsling, J. Voight, A database of Belyi maps, ANTS XIII, The Open Book Series 2 (2019), 375–392, §2.

Generating triples of a passport

def TauCeti.PassportSpec.IsGeneratingTriple {n : ℕ} (P : PassportSpec n) (t : PermutationTriple n) : Prop

A permutation triple is a generating triple of the passport P when its monodromy subgroup is the reference subgroup P.G itself — not merely a conjugate of it — and its ordered full cycle partitions are those recorded by P.

By TauCeti.PermutationTriple.closure_pair_eq_monodromyGroup the first condition says that the first two components generate P.G.

Equations

• P.IsGeneratingTriple t = (t.monodromyGroup = P.G ∧ t.cycleData.1 = P.lam0 ∧ t.cycleData.2.1 = P.lam1 ∧ t.cycleData.2.2 = P.laminf)

theorem TauCeti.PassportSpec.isGeneratingTriple_iff {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} : P.IsGeneratingTriple t ↔ t.monodromyGroup = P.G ∧ t.cycleData.1 = P.lam0 ∧ t.cycleData.2.1 = P.lam1 ∧ t.cycleData.2.2 = P.laminf

The defining characterization of a generating triple.

theorem TauCeti.PassportSpec.IsGeneratingTriple.monodromyGroup_eq {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (ht : P.IsGeneratingTriple t) : t.monodromyGroup = P.G

A generating triple of P has the reference subgroup as its monodromy subgroup.

theorem TauCeti.PassportSpec.IsGeneratingTriple.cycleData_eq {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (ht : P.IsGeneratingTriple t) : t.cycleData = (P.lam0, P.lam1, P.laminf)

A generating triple of P has the cycle data recorded by P.

theorem TauCeti.PassportSpec.IsGeneratingTriple.σ0_mem {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (ht : P.IsGeneratingTriple t) : t.σ0 ∈ P.G

The components of a generating triple of P lie in the reference subgroup.

theorem TauCeti.PassportSpec.IsGeneratingTriple.σ1_mem {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (ht : P.IsGeneratingTriple t) : t.σ1 ∈ P.G

The 1-component of a generating triple of P lies in the reference subgroup.

theorem TauCeti.PassportSpec.IsGeneratingTriple.σinf_mem {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (ht : P.IsGeneratingTriple t) : t.σinf ∈ P.G

The ∞-component of a generating triple of P lies in the reference subgroup.

theorem TauCeti.PassportSpec.IsGeneratingTriple.isConnected {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (ht : P.IsGeneratingTriple t) : t.IsConnected

A generating triple of a passport of nonzero degree with transitive reference subgroup is connected.

@[simp]

theorem TauCeti.PassportSpec.isGeneratingTriple_conjugate_smul_iff {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).IsGeneratingTriple (τ • t) ↔ P.IsGeneratingTriple t

Conjugating both the reference subgroup and the triple by the same relabeling does not change whether the triple is a generating triple.

theorem TauCeti.PassportSpec.isGeneratingTriple_iff_monodromyGroup_eq_and_hasPassport {n : ℕ} {P : PassportSpec n} {s : ConnectedTriple n} : P.IsGeneratingTriple ↑s ↔ (↑s).monodromyGroup = P.G ∧ HasPassport s P

A connected triple is a generating triple of P exactly when it lies in the passport P and its monodromy subgroup is the reference subgroup itself.

theorem TauCeti.PassportSpec.exists_isGeneratingTriple_smul {n : ℕ} {P : PassportSpec n} {s : ConnectedTriple n} (hs : HasPassport s P) : ∃ (τ : Equiv.Perm (Fin n)), P.IsGeneratingTriple (τ • ↑s)

Every connected triple in a passport is isomorphic to a generating triple of that passport: some relabeling carries its monodromy subgroup onto the reference subgroup.

theorem TauCeti.PassportSpec.IsGeneratingTriple.smul {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} {τ : Equiv.Perm (Fin n)} (hτ : τ ∈ Subgroup.normalizer ↑P.G) (ht : P.IsGeneratingTriple t) : P.IsGeneratingTriple (τ • t)

Conjugating a generating triple of P by an element normalizing the reference subgroup gives another generating triple of P.

theorem TauCeti.PassportSpec.mem_normalizer_of_monodromyGroup_smul_eq {n : ℕ} {P : PassportSpec n} {t : PermutationTriple n} {τ : Equiv.Perm (Fin n)} (ht : t.monodromyGroup = P.G) (hτt : (τ • t).monodromyGroup = P.G) : τ ∈ Subgroup.normalizer ↑P.G

A relabeling carrying a triple with monodromy subgroup P.G to another such triple normalizes the reference subgroup: this is the exact residual freedom left after pinning the monodromy subgroup down to P.G itself.

@[reducible, inline]

abbrev TauCeti.PassportSpec.GeneratingTriple {n : ℕ} (P : PassportSpec n) : Type

The generating triples of a passport: the permutation triples whose monodromy subgroup is the reference subgroup P.G itself and whose cycle partitions are those recorded by P. For a passport of nonzero degree with transitive reference subgroup, the normalizer of P.G acts on this type with the isomorphism classes of the passport as orbits.

Equations

• P.GeneratingTriple = { t : TauCeti.PermutationTriple n // P.IsGeneratingTriple t }

@[instance_reducible]

instance TauCeti.PassportSpec.GeneratingTriple.instSMulSubtypePermFinMemSubgroupNormalizerCoeG {n : ℕ} {P : PassportSpec n} : SMul (↥(Subgroup.normalizer ↑P.G)) P.GeneratingTriple

Simultaneous conjugation by an element normalizing the reference subgroup, acting on the generating triples of a passport.

Equations

• TauCeti.PassportSpec.GeneratingTriple.instSMulSubtypePermFinMemSubgroupNormalizerCoeG = { smul := fun (τ : ↥(Subgroup.normalizer ↑P.G)) (g : P.GeneratingTriple) => ⟨↑τ • ↑g, ⋯⟩ }

@[simp]

theorem TauCeti.PassportSpec.GeneratingTriple.coe_smul {n : ℕ} {P : PassportSpec n} (τ : ↥(Subgroup.normalizer ↑P.G)) (g : P.GeneratingTriple) : ↑(τ • g) = ↑τ • ↑g

Conjugation by a normalizing element acts on the underlying permutation triple.

@[instance_reducible]

instance TauCeti.PassportSpec.GeneratingTriple.instMulActionSubtypePermFinMemSubgroupNormalizerCoeG {n : ℕ} {P : PassportSpec n} : MulAction (↥(Subgroup.normalizer ↑P.G)) P.GeneratingTriple

Equations

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

def TauCeti.PassportSpec.GeneratingTriple.toConnectedTriple {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : ConnectedTriple n

A generating triple of a passport of nonzero degree with transitive reference subgroup, as a connected triple.

Equations

• TauCeti.PassportSpec.GeneratingTriple.toConnectedTriple hn hG g = ⟨↑g, ⋯⟩

@[simp]

theorem TauCeti.PassportSpec.GeneratingTriple.coe_toConnectedTriple {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : ↑(toConnectedTriple hn hG g) = ↑g

The connected triple attached to a generating triple has the same underlying triple.

theorem TauCeti.PassportSpec.GeneratingTriple.hasPassport_toConnectedTriple {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : HasPassport (toConnectedTriple hn hG g) P

A generating triple of P lies in the passport P.

def TauCeti.PassportSpec.GeneratingTriple.toClass {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : ConnectedIsoClass n

The isomorphism class of a generating triple.

Equations

• TauCeti.PassportSpec.GeneratingTriple.toClass hn hG g = TauCeti.ConnectedIsoClass.mk (TauCeti.PassportSpec.GeneratingTriple.toConnectedTriple hn hG g)

theorem TauCeti.PassportSpec.GeneratingTriple.hasPassport_toClass {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : (toClass hn hG g).HasPassport P

The isomorphism class of a generating triple of P lies in the passport P.

@[simp]

theorem TauCeti.PassportSpec.GeneratingTriple.toClass_smul {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (τ : ↥(Subgroup.normalizer ↑P.G)) (g : P.GeneratingTriple) : toClass hn hG (τ • g) = toClass hn hG g

Conjugating a generating triple by a normalizing element does not change its isomorphism class.

@[simp]

theorem TauCeti.PassportSpec.GeneratingTriple.toClass_eq_toClass_iff {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) {g g' : P.GeneratingTriple} : toClass hn hG g = toClass hn hG g' ↔ (MulAction.orbitRel (↥(Subgroup.normalizer ↑P.G)) P.GeneratingTriple) g g'

Two generating triples of a passport have the same isomorphism class exactly when they lie in one orbit of the normalizer of the reference subgroup.

theorem TauCeti.PassportSpec.GeneratingTriple.exists_toClass_eq {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) {c : ConnectedIsoClass n} (hc : c.HasPassport P) : ∃ (g : P.GeneratingTriple), toClass hn hG g = c

Every isomorphism class in a passport is the class of one of its generating triples.

The normalizer formulation of a passport

noncomputable def TauCeti.PassportSpec.generatingTripleOrbitsEquivClasses {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) : MulAction.orbitRel.Quotient (↥(Subgroup.normalizer ↑P.G)) P.GeneratingTriple ≃ { c : ConnectedIsoClass n // c.HasPassport P }

The normalizer formulation. For a passport of nonzero degree whose reference subgroup is transitive, the isomorphism classes of connected triples in that passport are exactly the orbits of the normalizer of the reference subgroup acting by simultaneous conjugation on the generating triples of the passport.

Equations

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

@[simp]

theorem TauCeti.PassportSpec.generatingTripleOrbitsEquivClasses_apply_mk_coe {n : ℕ} {P : PassportSpec n} (hn : n ≠ 0) (hG : MulAction.IsPretransitive (↥P.G) (Fin n)) (g : P.GeneratingTriple) : ↑((generatingTripleOrbitsEquivClasses hn hG) (Quotient.mk'' g)) = GeneratingTriple.toClass hn hG g

The normalizer formulation sends the orbit of a generating triple to its isomorphism class.

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

The size of a passport of nonzero degree whose reference subgroup is transitive is the number of orbits of the normalizer of that subgroup on its generating triples.