Passports of permutation triples

A passport records the coarse invariants of a connected permutation triple: the conjugacy class of its monodromy subgroup in the ambient symmetric group and the ordered full cycle partitions at the three branch points. This file introduces passport specifications and the membership relation between connected triples (TauCeti.ConnectedTriple) and passports, together with its descent to isomorphism classes (TauCeti.ConnectedIsoClass).

The cycle partitions include fixed points. Admissibility therefore says that each partition has positive parts summing to the degree. The degree is also required to be nonzero: transitivity on Fin 0 is vacuous, but there is no connected degree-zero triple.

Main definitions

• TauCeti.PassportSpec: a reference monodromy subgroup and three ordered cycle partitions.
• TauCeti.PassportSpec.IsAdmissible: well-formed passport data.
• TauCeti.PassportSpec.HasPassport: membership of a connected triple in a passport.
• TauCeti.ConnectedIsoClass.HasPassport: the same membership, descended to isomorphism classes.

References

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

Passport specifications

structure TauCeti.PassportSpec (n : ℕ) : Type

A passport specification in degree n: a reference monodromy subgroup and the ordered full cycle partitions at 0, 1, and ∞.

The subgroup is compared only up to conjugacy in Perm (Fin n) by HasPassport.

• G : Subgroup (Equiv.Perm (Fin n))

  A reference representative for the conjugacy class of the monodromy subgroup.

• lam0 : Multiset ℕ

  The full cycle partition at 0.

• lam1 : Multiset ℕ

  The full cycle partition at 1.

• laminf : Multiset ℕ

  The full cycle partition at ∞.

theorem TauCeti.PassportSpec.ext_iff {n : ℕ} {x y : PassportSpec n} : x = y ↔ x.G = y.G ∧ x.lam0 = y.lam0 ∧ x.lam1 = y.lam1 ∧ x.laminf = y.laminf

theorem TauCeti.PassportSpec.ext {n : ℕ} {x y : PassportSpec n} (G : x.G = y.G) (lam0 : x.lam0 = y.lam0) (lam1 : x.lam1 = y.lam1) (laminf : x.laminf = y.laminf) : x = y

def TauCeti.PassportSpec.partition {n : ℕ} (P : PassportSpec n) (i : Fin 3) : Multiset ℕ

The cycle partition at a branch point, numbered 0, 1, 2 for 0, 1, ∞.

Equations

• P.partition i = ![P.lam0, P.lam1, P.laminf] i

@[simp]

theorem TauCeti.PassportSpec.partition_zero {n : ℕ} (P : PassportSpec n) : P.partition 0 = P.lam0

@[simp]

theorem TauCeti.PassportSpec.partition_one {n : ℕ} (P : PassportSpec n) : P.partition 1 = P.lam1

@[simp]

theorem TauCeti.PassportSpec.partition_two {n : ℕ} (P : PassportSpec n) : P.partition 2 = P.laminf

theorem TauCeti.PassportSpec.ext_partition {n : ℕ} {P Q : PassportSpec n} (hG : P.G = Q.G) (h : ∀ (i : Fin 3), P.partition i = Q.partition i) : P = Q

Passport specifications agree when their reference groups and indexed partitions agree.

def TauCeti.PassportSpec.IsAdmissible {n : ℕ} (P : PassportSpec n) : Prop

A passport is admissible when its degree is nonzero, its reference subgroup is transitive, and its three multisets are partitions of the degree into positive parts.

Equations

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

theorem TauCeti.PassportSpec.isAdmissible_iff_partition {n : ℕ} (P : PassportSpec n) : P.IsAdmissible ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥P.G) (Fin n) ∧ ∀ (i : Fin 3), (P.partition i).sum = n ∧ ∀ j ∈ P.partition i, 0 < j

Admissibility expressed uniformly over the three branch points.

theorem TauCeti.PassportSpec.IsAdmissible.ne_zero {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) : n ≠ 0

theorem TauCeti.PassportSpec.IsAdmissible.isPretransitive {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) : MulAction.IsPretransitive (↥P.G) (Fin n)

theorem TauCeti.PassportSpec.IsAdmissible.sum_lam0 {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) : P.lam0.sum = n

theorem TauCeti.PassportSpec.IsAdmissible.sum_lam1 {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) : P.lam1.sum = n

theorem TauCeti.PassportSpec.IsAdmissible.sum_laminf {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) : P.laminf.sum = n

theorem TauCeti.PassportSpec.IsAdmissible.pos_of_mem_lam0 {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) {i : ℕ} (hi : i ∈ P.lam0) : 0 < i

theorem TauCeti.PassportSpec.IsAdmissible.pos_of_mem_lam1 {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) {i : ℕ} (hi : i ∈ P.lam1) : 0 < i

theorem TauCeti.PassportSpec.IsAdmissible.pos_of_mem_laminf {n : ℕ} {P : PassportSpec n} (hP : P.IsAdmissible) {i : ℕ} (hi : i ∈ P.laminf) : 0 < i

def TauCeti.PassportSpec.HasPassport {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) : Prop

A connected triple has passport P when its monodromy subgroup is conjugate to P.G and its ordered full cycle partitions are those specified by P.

Equations

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

theorem TauCeti.PassportSpec.hasPassport_iff {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) : HasPassport t P ↔ (∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) (↑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 passport membership.

@[simp]

theorem TauCeti.PassportSpec.hasPassport_smul_iff {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : ConnectedTriple n) (P : PassportSpec n) : HasPassport (τ • t) P ↔ HasPassport t P

Relabeling a connected triple does not change its passport membership.

theorem TauCeti.PassportSpec.hasPassport_iff_of_equivalent {n : ℕ} {t t' : ConnectedTriple n} (h : (MulAction.orbitRel (Equiv.Perm (Fin n)) (ConnectedTriple n)) t t') (P : PassportSpec n) : HasPassport t P ↔ HasPassport t' P

Isomorphic connected triples have exactly the same passport memberships.

def TauCeti.PassportSpec.conjugate {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : PassportSpec n

Replace the reference subgroup of a passport by a conjugate representative.

Equations

• P.conjugate τ = { G := Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) P.G, lam0 := P.lam0, lam1 := P.lam1, laminf := P.laminf }

@[simp]

theorem TauCeti.PassportSpec.partition_conjugate {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) (i : Fin 3) : (P.conjugate τ).partition i = P.partition i

@[simp]

theorem TauCeti.PassportSpec.conjugate_G {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).G = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) P.G

@[simp]

theorem TauCeti.PassportSpec.conjugate_lam0 {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).lam0 = P.lam0

@[simp]

theorem TauCeti.PassportSpec.conjugate_lam1 {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).lam1 = P.lam1

@[simp]

theorem TauCeti.PassportSpec.conjugate_laminf {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).laminf = P.laminf

@[simp]

theorem TauCeti.PassportSpec.isAdmissible_conjugate_iff {n : ℕ} (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).IsAdmissible ↔ P.IsAdmissible

Conjugating the reference subgroup preserves admissibility.

@[simp]

theorem TauCeti.PassportSpec.hasPassport_conjugate_iff {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : HasPassport t (P.conjugate τ) ↔ HasPassport t P

Passport membership depends on the reference subgroup only through its conjugacy class.

theorem TauCeti.PassportSpec.isAdmissible_of_hasPassport {n : ℕ} {t : ConnectedTriple n} {P : PassportSpec n} (htP : HasPassport t P) : P.IsAdmissible

Any passport containing a connected triple is admissible.

@[reducible, inline]

abbrev TauCeti.OrderedPassport (n : ℕ) : Type

An ordered passport is an admissible specification with the branch points still ordered. The reference subgroup is retained as data; passport membership compares it up to conjugacy.

Equations

• TauCeti.OrderedPassport n = { P : TauCeti.PassportSpec n // P.IsAdmissible }

def TauCeti.ConnectedIsoClass.HasPassport {n : ℕ} (c : ConnectedIsoClass n) (P : PassportSpec n) : Prop

An isomorphism class of connected triples has passport P when one, equivalently every, representative has passport P.

Equations

• c.HasPassport P = Quotient.liftOn' c (fun (t : TauCeti.ConnectedTriple n) => TauCeti.PassportSpec.HasPassport t P) ⋯

@[simp]

theorem TauCeti.ConnectedIsoClass.hasPassport_mk {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) : (mk t).HasPassport P ↔ PassportSpec.HasPassport t P

The passport membership of an isomorphism class is that of any representative.

theorem TauCeti.ConnectedIsoClass.isAdmissible_of_hasPassport {n : ℕ} {c : ConnectedIsoClass n} {P : PassportSpec n} (hcP : c.HasPassport P) : P.IsAdmissible

A passport containing an isomorphism class of connected triples is admissible.

@[simp]

theorem TauCeti.ConnectedIsoClass.hasPassport_conjugate_iff {n : ℕ} (c : ConnectedIsoClass n) (P : PassportSpec n) (τ : Equiv.Perm (Fin n)) : c.HasPassport (P.conjugate τ) ↔ c.HasPassport P

Conjugating the reference subgroup does not change membership of an isomorphism class.