The passport of a connected permutation triple

Every connected permutation triple determines a passport: its monodromy subgroup is the reference subgroup and its three full cycle partitions are the ordered partition data. The resulting passport is admissible and contains the original triple.

The reference subgroup depends on the numbering of the sheets. Relabeling a triple therefore conjugates its passport rather than fixing it literally. The passport membership relation removes this choice: a connected triple belongs to passportOf t exactly when its monodromy subgroup is conjugate to that of t and its ordered cycle data agrees with that of t.

Main declarations

• TauCeti.ConnectedTriple.passportOf: the passport determined by a connected triple.
• TauCeti.ConnectedTriple.isAdmissible_passportOf: this passport is admissible.
• TauCeti.ConnectedTriple.hasPassport_passportOf: the triple belongs to its passport.
• TauCeti.ConnectedTriple.hasPassport_passportOf_iff: the characteristic property of the passport of a triple.

References

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

Construction and projections

noncomputable def TauCeti.ConnectedTriple.passportOf {n : ℕ} (t : ConnectedTriple n) : PassportSpec n

The passport determined by a connected permutation triple: its monodromy subgroup together with its ordered full cycle partitions.

Equations

• t.passportOf = { G := (↑t).monodromyGroup, lam0 := (↑t).cycleData.1, lam1 := (↑t).cycleData.2.1, laminf := (↑t).cycleData.2.2 }

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_G {n : ℕ} (t : ConnectedTriple n) : t.passportOf.G = (↑t).monodromyGroup

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_lam0 {n : ℕ} (t : ConnectedTriple n) : t.passportOf.lam0 = (↑t).cycleData.1

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_lam1 {n : ℕ} (t : ConnectedTriple n) : t.passportOf.lam1 = (↑t).cycleData.2.1

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_laminf {n : ℕ} (t : ConnectedTriple n) : t.passportOf.laminf = (↑t).cycleData.2.2

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_smul {n : ℕ} (tau : Equiv.Perm (Fin n)) (t : ConnectedTriple n) : (tau • t).passportOf = t.passportOf.conjugate tau

Relabeling the sheets conjugates the reference subgroup of the attached passport and leaves its ordered cycle data unchanged.

Admissibility and the characteristic property

@[simp]

theorem TauCeti.ConnectedTriple.hasPassport_passportOf {n : ℕ} (t : ConnectedTriple n) : PassportSpec.HasPassport t t.passportOf

Every connected triple belongs to the passport it determines.

@[simp]

theorem TauCeti.ConnectedTriple.isAdmissible_passportOf {n : ℕ} (t : ConnectedTriple n) : t.passportOf.IsAdmissible

The passport determined by a connected triple is admissible.

noncomputable def TauCeti.ConnectedTriple.orderedPassportOf {n : ℕ} (t : ConnectedTriple n) : OrderedPassport n

The admissible ordered passport attached to a connected triple.

Equations

• t.orderedPassportOf = ⟨t.passportOf, ⋯⟩

@[simp]

theorem TauCeti.ConnectedTriple.coe_orderedPassportOf {n : ℕ} (t : ConnectedTriple n) : ↑t.orderedPassportOf = t.passportOf

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_partition {n : ℕ} (t : ConnectedTriple n) (i : Fin 3) : t.passportOf.partition i = ((↑t).component i).partition.parts

The indexed partition of the attached passport is the full partition of the component.

theorem TauCeti.ConnectedTriple.hasPassport_passportOf_iff {n : ℕ} (t t' : ConnectedTriple n) : PassportSpec.HasPassport t' t.passportOf ↔ (∃ (tau : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj tau)) (↑t').monodromyGroup = (↑t).monodromyGroup) ∧ (↑t').cycleData = (↑t).cycleData

A connected triple belongs to passportOf t exactly when its monodromy subgroup is conjugate to that of t and its ordered full cycle data agrees with that of t.

theorem TauCeti.ConnectedTriple.hasPassport_iff_exists_conjugate_passportOf {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) : PassportSpec.HasPassport t P ↔ ∃ (tau : Equiv.Perm (Fin n)), t.passportOf.conjugate tau = P

A connected triple belongs to a passport exactly when that passport is obtained from the triple's attached passport by conjugating its reference subgroup.

theorem TauCeti.ConnectedTriple.mk_mem_classSet_passportOf {n : ℕ} (t : ConnectedTriple n) : ConnectedIsoClass.mk t ∈ t.passportOf.classSet

The isomorphism class of a connected triple lies in the class set of its attached passport.

theorem TauCeti.ConnectedTriple.passportSize_passportOf_pos {n : ℕ} (t : ConnectedTriple n) : 0 < t.passportOf.passportSize

The passport attached to a connected triple has positive size.

theorem TauCeti.ConnectedTriple.mk_mem_classSet_passportOf_iff {n : ℕ} (t t' : ConnectedTriple n) : ConnectedIsoClass.mk t' ∈ t.passportOf.classSet ↔ (∃ (tau : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj tau)) (↑t').monodromyGroup = (↑t).monodromyGroup) ∧ (↑t').cycleData = (↑t).cycleData

Membership in the class set of passportOf t has the same characteristic description as membership of a representative triple.