Executable passport fibers

A passport compares monodromy subgroups up to conjugacy in the symmetric group. A subgroup itself has no decidable equality, so executable enumeration takes its elements as a finset. TauCeti.passportTriples filters connected triples by that finset, up to conjugacy, and by three ordered cycle partitions. TauCeti.passportClasses lists the resulting relabeling orbits as finsets of connected triples, without choosing representatives.

Whenever the input finset presents a conjugate of the reference subgroup of a TauCeti.PassportSpec, these computations give exactly its triples and classes. In particular, TauCeti.card_passportClasses identifies the computed cardinality with TauCeti.PassportSpec.passportSize.

The input need not be certified as a subgroup to run the computation. If it is not the element set of a subgroup, the fiber is empty: no conjugate of a monodromy group can equal it.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.5.

def TauCeti.passportTriples {n : ℕ} (G : Finset (Equiv.Perm (Fin n))) (lam0 lam1 laminf : Multiset ℕ) : Finset (ConnectedTriple n)

The connected triples with the specified ordered full cycle partitions and monodromy group conjugate to the supplied finset of permutations. Fixed points occur as parts equal to one.

Equations

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

@[simp]

theorem TauCeti.mem_passportTriples {n : ℕ} {G : Finset (Equiv.Perm (Fin n))} {lam0 lam1 laminf : Multiset ℕ} {t : ConnectedTriple n} : t ∈ passportTriples G lam0 lam1 laminf ↔ (∃ (τ : Equiv.Perm (Fin n)), Finset.image (⇑(MulAut.conj τ)) (↑t).monodromyFinset = G) ∧ (↑t).σ0.partition.parts = lam0 ∧ (↑t).σ1.partition.parts = lam1 ∧ (↑t).σinf.partition.parts = laminf

Membership in the computed triple fiber is conjugacy of the monodromy finset together with agreement of the ordered full cycle partitions.

theorem TauCeti.mem_passportTriples_iff_hasPassport {n : ℕ} (P : PassportSpec n) (G : Finset (Equiv.Perm (Fin n))) (hG : ∃ (ρ : Equiv.Perm (Fin n)), ↑G = ↑(P.conjugate ρ).G) (t : ConnectedTriple n) : t ∈ passportTriples G P.lam0 P.lam1 P.laminf ↔ PassportSpec.HasPassport t P

A finset presentation of any conjugate of the reference subgroup turns the computed membership test into passport membership.

theorem TauCeti.passportTriples_eq_filter {n : ℕ} (P : PassportSpec n) (G : Finset (Equiv.Perm (Fin n))) (hG : ∃ (ρ : Equiv.Perm (Fin n)), ↑G = ↑(P.conjugate ρ).G) : passportTriples G P.lam0 P.lam1 P.laminf = {t : ConnectedTriple n | PassportSpec.HasPassport t P}

The computed triple fiber is exactly the filter by the canonical passport predicate.

def TauCeti.passportClasses {n : ℕ} (G : Finset (Equiv.Perm (Fin n))) (lam0 lam1 laminf : Multiset ℕ) : Finset (Finset (ConnectedTriple n))

The passport classes specified by a monodromy finset and three ordered full cycle partitions, as a finset of relabeling orbits. Each orbit is listed once, with all its connected triples.

Equations

• TauCeti.passportClasses G lam0 lam1 laminf = Finset.image (fun (t : TauCeti.ConnectedTriple n) => (TauCeti.ConnectedIsoClass.mk t).orbitFinset) (TauCeti.passportTriples G lam0 lam1 laminf)

@[simp]

theorem TauCeti.mem_passportClasses {n : ℕ} {G : Finset (Equiv.Perm (Fin n))} {lam0 lam1 laminf : Multiset ℕ} {s : Finset (ConnectedTriple n)} : s ∈ passportClasses G lam0 lam1 laminf ↔ ∃ t ∈ passportTriples G lam0 lam1 laminf, (ConnectedIsoClass.mk t).orbitFinset = s

The members of the computed class fiber are the relabeling orbits of triples in the computed triple fiber.

theorem TauCeti.existsUnique_mem_passportClasses {n : ℕ} {G : Finset (Equiv.Perm (Fin n))} {lam0 lam1 laminf : Multiset ℕ} (t : ConnectedTriple n) (ht : t ∈ passportTriples G lam0 lam1 laminf) : ∃! s : Finset (ConnectedTriple n), s ∈ passportClasses G lam0 lam1 laminf ∧ t ∈ s

Every triple in the computed passport fiber lies in exactly one of its listed relabeling orbits, for arbitrary input finsets and ordered cycle partitions.

theorem TauCeti.passportClasses_eq_image_classSet {n : ℕ} (P : PassportSpec n) (G : Finset (Equiv.Perm (Fin n))) (hG : ∃ (ρ : Equiv.Perm (Fin n)), ↑G = ↑(P.conjugate ρ).G) : passportClasses G P.lam0 P.lam1 P.laminf = Finset.image ConnectedIsoClass.orbitFinset P.classSet

The computed class fiber consists exactly of the orbit finsets of the canonical passport class set. This equality supplies both soundness and completeness of the enumeration.

theorem TauCeti.orbitFinset_mem_passportClasses_iff {n : ℕ} (P : PassportSpec n) (G : Finset (Equiv.Perm (Fin n))) (hG : ∃ (ρ : Equiv.Perm (Fin n)), ↑G = ↑(P.conjugate ρ).G) (c : ConnectedIsoClass n) : c.orbitFinset ∈ passportClasses G P.lam0 P.lam1 P.laminf ↔ c.HasPassport P

A relabeling orbit belongs to the computed fiber exactly when its class has the passport.

theorem TauCeti.biUnion_passportClasses {n : ℕ} (G : Finset (Equiv.Perm (Fin n))) (lam0 lam1 laminf : Multiset ℕ) : (passportClasses G lam0 lam1 laminf).biUnion id = passportTriples G lam0 lam1 laminf

The union of the listed passport classes is exactly the computed triple fiber, for arbitrary input finsets and ordered cycle partitions.

theorem TauCeti.card_passportClasses {n : ℕ} (P : PassportSpec n) (G : Finset (Equiv.Perm (Fin n))) (hG : ∃ (ρ : Equiv.Perm (Fin n)), ↑G = ↑(P.conjugate ρ).G) : (passportClasses G P.lam0 P.lam1 P.laminf).card = P.passportSize

The computed class fiber has cardinality equal to the passport size.