Branch-point action on ordered passports

Permuting the branch points reorders the three cycle partitions and leaves the reference monodromy subgroup unchanged. Reindexing is contravariant, so this is a right action of Perm (Fin 3), written as a left action of its opposite group. The action preserves admissibility and agrees with the branch-point operations on connected triples.

OrderedPassport carries an admissible specification, including its reference subgroup. Its branch-point orbit has at most six elements. Passing from an ordered passport to its branch-point orbit gives a coarser invariant than equality of ordered passports. The witnesses in Passport.Examples show that the torus passport changes under an exchange of branch points, while the passport of the degree-one cyclic triple has a singleton orbit.

References

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

def TauCeti.PassportSpec.reindexBranchPoints {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : PassportSpec n

Reorder the three partitions of a passport, retaining its reference subgroup.

Equations

• P.reindexBranchPoints ρ = { G := P.G, lam0 := P.partition (ρ 0), lam1 := P.partition (ρ 1), laminf := P.partition (ρ 2) }

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_G {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).G = P.G

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_lam0 {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).lam0 = P.partition (ρ 0)

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_lam1 {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).lam1 = P.partition (ρ 1)

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_laminf {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).laminf = P.partition (ρ 2)

@[simp]

theorem TauCeti.PassportSpec.partition_reindexBranchPoints {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) (i : Fin 3) : (P.reindexBranchPoints ρ).partition i = P.partition (ρ i)

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_one {n : ℕ} (P : PassportSpec n) : P.reindexBranchPoints 1 = P

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_reindexBranchPoints {n : ℕ} (P : PassportSpec n) (ρ σ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).reindexBranchPoints σ = P.reindexBranchPoints (ρ * σ)

Reindexing twice composes the permutations in the order of application.

@[simp]

theorem TauCeti.PassportSpec.reindexBranchPoints_conjugate {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).reindexBranchPoints ρ = (P.reindexBranchPoints ρ).conjugate τ

Reordering the branch points commutes with changing the reference subgroup by conjugacy.

@[simp]

theorem TauCeti.PassportSpec.isAdmissible_reindexBranchPoints_iff {n : ℕ} (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : (P.reindexBranchPoints ρ).IsAdmissible ↔ P.IsAdmissible

Admissibility is invariant under reordering the branch points.

@[instance_reducible]

instance TauCeti.PassportSpec.instMulActionMulOppositePermFinOfNatNat {n : ℕ} : MulAction (Equiv.Perm (Fin 3))ᵐᵒᵖ (PassportSpec n)

The right action on passport specifications permutes their ordered partitions.

Equations

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

@[simp]

theorem TauCeti.PassportSpec.smul_eq_reindexBranchPoints {n : ℕ} (P : PassportSpec n) (ρ : (Equiv.Perm (Fin 3))ᵐᵒᵖ) : ρ • P = P.reindexBranchPoints (MulOpposite.unop ρ)

@[instance_reducible]

instance TauCeti.OrderedPassport.instMulActionMulOppositePermFinOfNatNat {n : ℕ} : MulAction (Equiv.Perm (Fin 3))ᵐᵒᵖ (OrderedPassport n)

The branch-point action restricts to admissible specifications.

Equations

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

@[simp]

theorem TauCeti.OrderedPassport.coe_smul {n : ℕ} (ρ : (Equiv.Perm (Fin 3))ᵐᵒᵖ) (P : OrderedPassport n) : ↑(ρ • P) = ρ • ↑P

theorem TauCeti.OrderedPassport.card_orbit_le_six {n : ℕ} (P : OrderedPassport n) : Nat.card ↑(MulAction.orbit (Equiv.Perm (Fin 3))ᵐᵒᵖ P) ≤ 6

A branch-point orbit contains at most six ordered passports.

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_reindexBranchPoints {n : ℕ} (t : ConnectedTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).passportOf = t.passportOf.reindexBranchPoints ρ

Taking a passport commutes with all six branch-point operations.

@[simp]

theorem TauCeti.ConnectedTriple.orderedPassportOf_reindexBranchPoints {n : ℕ} (t : ConnectedTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).orderedPassportOf = MulOpposite.op ρ • t.orderedPassportOf

The refined ordered passport is equivariant for branch-point reindexing.

@[simp]

theorem TauCeti.PassportSpec.hasPassport_reindexBranchPoints_iff {n : ℕ} (t : ConnectedTriple n) (P : PassportSpec n) (ρ : Equiv.Perm (Fin 3)) : HasPassport (t.reindexBranchPoints ρ) (P.reindexBranchPoints ρ) ↔ HasPassport t P

Reordering a triple and its passport preserves passport membership, in both directions.