Permuting the branch points of a permutation triple

A permutation triple t = (a, b, c) = (σ0, σ1, σinf), with c * b * a = 1, records the monodromy of a cover of the sphere branched over the three ordered points 0, 1, ∞. Reordering the three branch points gives a new triple, whose components are the old ones in a new order, each up to conjugacy; the conjugators are exactly what is needed to keep the product relation. This file defines the five nonidentity resulting operations:

operation	branch points exchanged	formula
swap01	0 ↔ 1	(b, a, b⁻¹ * c * b)
swap1Inf	1 ↔ ∞	(a, b⁻¹ * c * b, b)
swap0Inf	0 ↔ ∞	(c, b, b * a * b⁻¹)
rot	0 → 1 → ∞ → 0	(b, c, a)
rotInv	0 → ∞ → 1 → 0	(b⁻¹ * c * b, a, a * b * a⁻¹)

Geometrically they, together with the identity operation, are the pullbacks along the six Möbius transformations permuting 0, 1, ∞.

Main results

• The last three operations are defined as composites of swap01 and swap1Inf: rot is swap01 then swap1Inf, rotInv is swap1Inf then swap01, and swap0Inf is swap01, then swap1Inf, then swap01; the table above gives their components.
• TauCeti.PermutationTriple.swap01_swap01, TauCeti.PermutationTriple.rot_rot_rot and TauCeti.PermutationTriple.rotInv_rotInv_rotInv hold on the nose, whereas TauCeti.PermutationTriple.swap1Inf_swap1Inf, TauCeti.PermutationTriple.swap0Inf_swap0Inf, TauCeti.PermutationTriple.rotInv_rot and TauCeti.PermutationTriple.rot_rotInv are relabelings by an explicit component. The relabeling cannot be dropped: TauCeti.PermutationTriple.exists_swap1Inf_swap1Inf_ne and TauCeti.PermutationTriple.exists_rotInv_rot_ne.
• TauCeti.PermutationTriple.swap01_smul and its siblings: each operation commutes with relabeling, hence preserves isomorphism of triples (TauCeti.PermutationTriple.Equivalent.swap01 and its siblings). Up to isomorphism the two exchanges swap01 and swap1Inf are involutions whose composite rotInv has order three, which are the Coxeter relations of the symmetric group on the three branch points.
• The monodromy group, connectedness, the Euler characteristic, the genus and the geometry type are unchanged by all five nonidentity operations, while the cycle data, the cycle counts and the order triple are permuted accordingly.
• TauCeti.PermutationTriple.reindexBranchPoints: the operation attached to a permutation ρ of the branch points, numbered 0, 1, 2 : Fin 3; its component over i is conjugate to the old component over ρ i (TauCeti.PermutationTriple.isConj_component_reindexBranchPoints).
• The action of (Perm (Fin 3))ᵐᵒᵖ on TauCeti.PermutationTriple.IsoClass n: the six operations form a right action of the symmetric group on isomorphism classes of triples, generated by swap01 and swap1Inf subject to the Coxeter relations.
• TauCeti.ConnectedTriple.reindexBranchPoints and the action of (Perm (Fin 3))ᵐᵒᵖ on TauCeti.ConnectedIsoClass n: since reordering preserves connectedness, the operations and the action restrict to connected triples and to their isomorphism classes (TauCeti.ConnectedIsoClass.op_smul_mk).

Implementation notes

Reordering the branch points is contravariant: applying swap01 and then swap1Inf gives rot, whose branch-point permutation 0 → 1 → ∞ → 0 is the product (0 1) * (1 ∞) of their labels in the order of application. The operations therefore induce a right action of the symmetric group, and only on isomorphism classes, since swap1Inf is an involution only up to relabeling.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.5.
• E. Girondo, G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press 2012, §4.
• Tau Ceti Project, Belyi branch-point operations prototype.

The five nonidentity operations

def TauCeti.PermutationTriple.swap01 {n : ℕ} (t : PermutationTriple n) : PermutationTriple n

Exchange the branch points 0 and 1: (a, b, c) ↦ (b, a, b⁻¹ * c * b).

Equations

• t.swap01 = { σ0 := t.σ1, σ1 := t.σ0, σinf := t.σ1⁻¹ * t.σinf * t.σ1, product_eq_one := ⋯ }

def TauCeti.PermutationTriple.swap1Inf {n : ℕ} (t : PermutationTriple n) : PermutationTriple n

Exchange the branch points 1 and ∞: (a, b, c) ↦ (a, b⁻¹ * c * b, b).

Equations

• t.swap1Inf = { σ0 := t.σ0, σ1 := t.σ1⁻¹ * t.σinf * t.σ1, σinf := t.σ1, product_eq_one := ⋯ }

def TauCeti.PermutationTriple.swap0Inf {n : ℕ} (t : PermutationTriple n) : PermutationTriple n

Exchange the branch points 0 and ∞: (a, b, c) ↦ (c, b, b * a * b⁻¹).

Equations

• t.swap0Inf = t.swap01.swap1Inf.swap01

def TauCeti.PermutationTriple.rot {n : ℕ} (t : PermutationTriple n) : PermutationTriple n

Rotate the branch points 0 → 1 → ∞ → 0: (a, b, c) ↦ (b, c, a), with no conjugation.

Equations

• t.rot = t.swap01.swap1Inf

def TauCeti.PermutationTriple.rotInv {n : ℕ} (t : PermutationTriple n) : PermutationTriple n

Rotate the branch points 0 → ∞ → 1 → 0: (a, b, c) ↦ (b⁻¹ * c * b, a, a * b * a⁻¹). This is not the inverse of TauCeti.PermutationTriple.rot on triples, only on isomorphism classes; see TauCeti.PermutationTriple.rotInv_rot.

Equations

• t.rotInv = t.swap1Inf.swap01

@[simp]

theorem TauCeti.PermutationTriple.swap01_σ0 {n : ℕ} (t : PermutationTriple n) : t.swap01.σ0 = t.σ1

@[simp]

theorem TauCeti.PermutationTriple.swap01_σ1 {n : ℕ} (t : PermutationTriple n) : t.swap01.σ1 = t.σ0

@[simp]

theorem TauCeti.PermutationTriple.swap01_σinf {n : ℕ} (t : PermutationTriple n) : t.swap01.σinf = t.σ1⁻¹ * t.σinf * t.σ1

@[simp]

theorem TauCeti.PermutationTriple.swap1Inf_σ0 {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.σ0 = t.σ0

@[simp]

theorem TauCeti.PermutationTriple.swap1Inf_σ1 {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.σ1 = t.σ1⁻¹ * t.σinf * t.σ1

@[simp]

theorem TauCeti.PermutationTriple.swap1Inf_σinf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.σinf = t.σ1

@[simp]

theorem TauCeti.PermutationTriple.swap0Inf_σ0 {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.σ0 = t.σinf

@[simp]

theorem TauCeti.PermutationTriple.swap0Inf_σ1 {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.σ1 = t.σ1

@[simp]

theorem TauCeti.PermutationTriple.swap0Inf_σinf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.σinf = t.σ1 * t.σ0 * t.σ1⁻¹

@[simp]

theorem TauCeti.PermutationTriple.rot_σ0 {n : ℕ} (t : PermutationTriple n) : t.rot.σ0 = t.σ1

@[simp]

theorem TauCeti.PermutationTriple.rot_σ1 {n : ℕ} (t : PermutationTriple n) : t.rot.σ1 = t.σinf

@[simp]

theorem TauCeti.PermutationTriple.rot_σinf {n : ℕ} (t : PermutationTriple n) : t.rot.σinf = t.σ0

@[simp]

theorem TauCeti.PermutationTriple.rotInv_σ0 {n : ℕ} (t : PermutationTriple n) : t.rotInv.σ0 = t.σ1⁻¹ * t.σinf * t.σ1

@[simp]

theorem TauCeti.PermutationTriple.rotInv_σ1 {n : ℕ} (t : PermutationTriple n) : t.rotInv.σ1 = t.σ0

@[simp]

theorem TauCeti.PermutationTriple.rotInv_σinf {n : ℕ} (t : PermutationTriple n) : t.rotInv.σinf = t.σ0 * t.σ1 * t.σ0⁻¹

Composites and relations

@[simp]

theorem TauCeti.PermutationTriple.swap01_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.swap01 = t

Exchanging 0 and 1 twice is the identity on triples, on the nose.

theorem TauCeti.PermutationTriple.swap01_involutive {n : ℕ} : Function.Involutive swap01

Exchanging 0 and 1 is an involution on triples.

@[simp]

theorem TauCeti.PermutationTriple.swap1Inf_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.swap1Inf = t.σ0 • t

Exchanging 1 and ∞ twice relabels the triple by its first component.

@[simp]

theorem TauCeti.PermutationTriple.swap0Inf_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.swap0Inf = t.σ1 • t

Exchanging 0 and ∞ twice relabels the triple by its second component.

@[simp]

theorem TauCeti.PermutationTriple.rot_rot_rot {n : ℕ} (t : PermutationTriple n) : t.rot.rot.rot = t

The rotation 0 → 1 → ∞ → 0 has order three on triples.

@[simp]

theorem TauCeti.PermutationTriple.rotInv_rotInv_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.rotInv.rotInv = t

The rotation 0 → ∞ → 1 → 0 has order three on triples.

@[simp]

theorem TauCeti.PermutationTriple.rotInv_rot {n : ℕ} (t : PermutationTriple n) : t.rot.rotInv = t.σ1 • t

The two rotations compose to the relabeling by the second component.

@[simp]

theorem TauCeti.PermutationTriple.rot_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.rot = t.σ0 • t

The two rotations, in the other order, compose to the relabeling by the first component.

theorem TauCeti.PermutationTriple.exists_swap1Inf_swap1Inf_ne : ∃ (t : PermutationTriple 3), t.swap1Inf.swap1Inf ≠ t

TauCeti.PermutationTriple.swap1Inf is not an involution on triples.

theorem TauCeti.PermutationTriple.exists_rotInv_rot_ne : ∃ (t : PermutationTriple 3), t.rot.rotInv ≠ t

TauCeti.PermutationTriple.rotInv is not a left inverse of TauCeti.PermutationTriple.rot on triples.

Relabeling and isomorphism classes

@[simp]

theorem TauCeti.PermutationTriple.swap01_smul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : (τ • t).swap01 = τ • t.swap01

Exchanging 0 and 1 commutes with relabeling the sheets.

@[simp]

theorem TauCeti.PermutationTriple.swap1Inf_smul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : (τ • t).swap1Inf = τ • t.swap1Inf

Exchanging 1 and ∞ commutes with relabeling the sheets.

@[simp]

theorem TauCeti.PermutationTriple.swap0Inf_smul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : (τ • t).swap0Inf = τ • t.swap0Inf

Exchanging 0 and ∞ commutes with relabeling the sheets.

@[simp]

theorem TauCeti.PermutationTriple.rot_smul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : (τ • t).rot = τ • t.rot

Rotating the branch points commutes with relabeling the sheets.

@[simp]

theorem TauCeti.PermutationTriple.rotInv_smul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : (τ • t).rotInv = τ • t.rotInv

Rotating the branch points backwards commutes with relabeling the sheets.

theorem TauCeti.PermutationTriple.Equivalent.swap01 {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.swap01.Equivalent t'.swap01

Exchanging 0 and 1 preserves isomorphism of triples.

theorem TauCeti.PermutationTriple.Equivalent.swap1Inf {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.swap1Inf.Equivalent t'.swap1Inf

Exchanging 1 and ∞ preserves isomorphism of triples.

theorem TauCeti.PermutationTriple.Equivalent.swap0Inf {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.swap0Inf.Equivalent t'.swap0Inf

Exchanging 0 and ∞ preserves isomorphism of triples.

theorem TauCeti.PermutationTriple.Equivalent.rot {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.rot.Equivalent t'.rot

Rotating the branch points preserves isomorphism of triples.

theorem TauCeti.PermutationTriple.Equivalent.rotInv {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.rotInv.Equivalent t'.rotInv

Rotating the branch points backwards preserves isomorphism of triples.

theorem TauCeti.PermutationTriple.equivalent_swap1Inf_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.swap1Inf.Equivalent t

Up to isomorphism, exchanging 1 and ∞ is an involution.

theorem TauCeti.PermutationTriple.equivalent_swap0Inf_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.swap0Inf.Equivalent t

Up to isomorphism, exchanging 0 and ∞ is an involution.

theorem TauCeti.PermutationTriple.equivalent_rotInv_rot {n : ℕ} (t : PermutationTriple n) : t.rot.rotInv.Equivalent t

Up to isomorphism, TauCeti.PermutationTriple.rotInv is a left inverse of TauCeti.PermutationTriple.rot.

theorem TauCeti.PermutationTriple.equivalent_rot_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.rot.Equivalent t

Up to isomorphism, TauCeti.PermutationTriple.rotInv is a right inverse of TauCeti.PermutationTriple.rot.

Invariants

The monodromy group, and with it connectedness, is the subgroup generated by all three components, so it does not see their order; the Euler characteristic, the genus and the geometry type are symmetric functions of the three components' conjugacy classes.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.monodromyGroup = t.monodromyGroup

Exchanging 0 and 1 does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.monodromyGroup = t.monodromyGroup

Exchanging 1 and ∞ does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.monodromyGroup = t.monodromyGroup

Exchanging 0 and ∞ does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_rot {n : ℕ} (t : PermutationTriple n) : t.rot.monodromyGroup = t.monodromyGroup

Rotating 0 → 1 → ∞ → 0 does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.monodromyGroup = t.monodromyGroup

Rotating 0 → ∞ → 1 → 0 does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_swap01_iff {n : ℕ} (t : PermutationTriple n) : t.swap01.IsConnected ↔ t.IsConnected

Exchanging 0 and 1 does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_swap1Inf_iff {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.IsConnected ↔ t.IsConnected

Exchanging 1 and ∞ does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_swap0Inf_iff {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.IsConnected ↔ t.IsConnected

Exchanging 0 and ∞ does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_rot_iff {n : ℕ} (t : PermutationTriple n) : t.rot.IsConnected ↔ t.IsConnected

Rotating 0 → 1 → ∞ → 0 does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_rotInv_iff {n : ℕ} (t : PermutationTriple n) : t.rotInv.IsConnected ↔ t.IsConnected

Rotating 0 → ∞ → 1 → 0 does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.cycleData = (t.cycleData.2.1, t.cycleData.1, t.cycleData.2.2)

Exchanging 0 and 1 exchanges the cycle partitions at 0 and 1.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.cycleData = (t.cycleData.1, t.cycleData.2.2, t.cycleData.2.1)

Exchanging 1 and ∞ exchanges the cycle partitions at 1 and ∞.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.cycleData = (t.cycleData.2.2, t.cycleData.2.1, t.cycleData.1)

Exchanging 0 and ∞ exchanges their cycle partitions.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_rot {n : ℕ} (t : PermutationTriple n) : t.rot.cycleData = (t.cycleData.2.1, t.cycleData.2.2, t.cycleData.1)

Rotating the branch points rotates the cycle partitions.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.cycleData = (t.cycleData.2.2, t.cycleData.1, t.cycleData.2.1)

Rotating the branch points backwards rotates the cycle partitions backwards.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.cycleCounts = (t.cycleCounts.2.1, t.cycleCounts.1, t.cycleCounts.2.2)

Exchanging 0 and 1 exchanges their cycle counts.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.cycleCounts = (t.cycleCounts.1, t.cycleCounts.2.2, t.cycleCounts.2.1)

Exchanging 1 and ∞ exchanges their cycle counts.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.cycleCounts = (t.cycleCounts.2.2, t.cycleCounts.2.1, t.cycleCounts.1)

Exchanging 0 and ∞ exchanges their cycle counts.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_rot {n : ℕ} (t : PermutationTriple n) : t.rot.cycleCounts = (t.cycleCounts.2.1, t.cycleCounts.2.2, t.cycleCounts.1)

Rotating the branch points rotates their cycle counts.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.cycleCounts = (t.cycleCounts.2.2, t.cycleCounts.1, t.cycleCounts.2.1)

Rotating the branch points backwards rotates their cycle counts backwards.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.orderTriple = (t.orderTriple.2.1, t.orderTriple.1, t.orderTriple.2.2)

Exchanging 0 and 1 exchanges their entries in the order triple.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.orderTriple = (t.orderTriple.1, t.orderTriple.2.2, t.orderTriple.2.1)

Exchanging 1 and ∞ exchanges their entries in the order triple.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.orderTriple = (t.orderTriple.2.2, t.orderTriple.2.1, t.orderTriple.1)

Exchanging 0 and ∞ exchanges their entries in the order triple.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_rot {n : ℕ} (t : PermutationTriple n) : t.rot.orderTriple = (t.orderTriple.2.1, t.orderTriple.2.2, t.orderTriple.1)

Rotating the branch points rotates the order triple.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.orderTriple = (t.orderTriple.2.2, t.orderTriple.1, t.orderTriple.2.1)

Rotating the branch points backwards rotates the order triple backwards.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.eulerChar = t.eulerChar

Exchanging 0 and 1 does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.eulerChar = t.eulerChar

Exchanging 1 and ∞ does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.eulerChar = t.eulerChar

Exchanging 0 and ∞ does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_rot {n : ℕ} (t : PermutationTriple n) : t.rot.eulerChar = t.eulerChar

Rotating 0 → 1 → ∞ → 0 does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.eulerChar = t.eulerChar

Rotating 0 → ∞ → 1 → 0 does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.genus_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.genus = t.genus

Exchanging 0 and 1 does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.genus = t.genus

Exchanging 1 and ∞ does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.genus = t.genus

Exchanging 0 and ∞ does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_rot {n : ℕ} (t : PermutationTriple n) : t.rot.genus = t.genus

Rotating 0 → 1 → ∞ → 0 does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.genus = t.genus

Rotating 0 → ∞ → 1 → 0 does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_swap01 {n : ℕ} (t : PermutationTriple n) : t.swap01.geometryType = t.geometryType

Exchanging 0 and 1 does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.geometryType = t.geometryType

Exchanging 1 and ∞ does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_swap0Inf {n : ℕ} (t : PermutationTriple n) : t.swap0Inf.geometryType = t.geometryType

Exchanging 0 and ∞ does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_rot {n : ℕ} (t : PermutationTriple n) : t.rot.geometryType = t.geometryType

Rotating 0 → 1 → ∞ → 0 does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_rotInv {n : ℕ} (t : PermutationTriple n) : t.rotInv.geometryType = t.geometryType

Rotating 0 → ∞ → 1 → 0 does not change the geometry type.

The symmetric group on the branch points

Number the branch points 0, 1, ∞ as 0, 1, 2 : Fin 3. For ρ : Perm (Fin 3), t.reindexBranchPoints ρ is the one of the six operations whose component over i is conjugate to the old component over ρ i. Reindexing is contravariant, so these operations compose as a right action of Perm (Fin 3), and only up to relabeling; the action is therefore stated on TauCeti.PermutationTriple.IsoClass, as a left action of the opposite group.

theorem TauCeti.PermutationTriple.swap1Inf_swap01_swap1Inf {n : ℕ} (t : PermutationTriple n) : t.swap1Inf.swap01.swap1Inf = t.σ1⁻¹ • t.swap0Inf

The composite swap1Inf ∘ swap01 ∘ swap1Inf is swap0Inf = swap01 ∘ swap1Inf ∘ swap01 up to relabeling by the inverse of the second component: the braid relation of the two exchanges.

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

Reorder the branch points of a permutation triple along ρ : Perm (Fin 3), with 0, 1, 2 numbering 0, 1, ∞: the component of the result over i is conjugate to the component of t over ρ i (TauCeti.PermutationTriple.isConj_component_reindexBranchPoints). A permutation of Fin 3 is determined by its values at 0 and 1, and the six cases are the identity and the five operations swap01, swap1Inf, swap0Inf, rot and rotInv.

Equations

• t.reindexBranchPoints ρ = match ρ 0, ρ 1 with | 1, 0 => t.swap01 | 0, 2 => t.swap1Inf | 2, 1 => t.swap0Inf | 1, 2 => t.rot | 2, 0 => t.rotInv | x, x_1 => t

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_one {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints 1 = t

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_swap_zero_one {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints (Equiv.swap 0 1) = t.swap01

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_swap_one_two {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints (Equiv.swap 1 2) = t.swap1Inf

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_swap_zero_two {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints (Equiv.swap 0 2) = t.swap0Inf

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_finRotate {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints (finRotate 3) = t.rot

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_finRotate_inv {n : ℕ} (t : PermutationTriple n) : t.reindexBranchPoints (finRotate 3)⁻¹ = t.rotInv

theorem TauCeti.PermutationTriple.isConj_component_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) (i : Fin 3) : IsConj ((t.reindexBranchPoints ρ).component i) (t.component (ρ i))

The component over i of the reordered triple is conjugate to the old component over ρ i. This is what names t.reindexBranchPoints ρ after ρ.

@[simp]

theorem TauCeti.PermutationTriple.reindexBranchPoints_smul {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) (τ : Equiv.Perm (Fin n)) : (τ • t).reindexBranchPoints ρ = τ • t.reindexBranchPoints ρ

Reordering the branch points commutes with relabeling the sheets.

theorem TauCeti.PermutationTriple.Equivalent.reindexBranchPoints {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).Equivalent (t'.reindexBranchPoints ρ)

Reordering the branch points preserves isomorphism of triples.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).monodromyGroup = t.monodromyGroup

Reordering the branch points does not change the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_reindexBranchPoints_iff {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).IsConnected ↔ t.IsConnected

Reordering the branch points does not change connectedness.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).eulerChar = t.eulerChar

Reordering the branch points does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.genus_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).genus = t.genus

Reordering the branch points does not change the genus.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : (t.reindexBranchPoints ρ).geometryType = t.geometryType

Reordering the branch points does not change the geometry type.

@[instance_reducible]

instance TauCeti.PermutationTriple.instSMulMulOppositePermFinOfNatNatIsoClass {n : ℕ} : SMul (Equiv.Perm (Fin 3))ᵐᵒᵖ (IsoClass n)

Reordering the branch points of the isomorphism class of a triple: MulOpposite.op ρ sends the class of t to the class of t.reindexBranchPoints ρ.

Equations

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

@[simp]

theorem TauCeti.PermutationTriple.IsoClass.op_smul_mk {n : ℕ} (t : PermutationTriple n) (ρ : Equiv.Perm (Fin 3)) : MulOpposite.op ρ • mk t = mk (t.reindexBranchPoints ρ)

Acting by MulOpposite.op ρ on the class represented by t computes by reindexing that representative along ρ.

@[instance_reducible]

instance TauCeti.PermutationTriple.instMulActionMulOppositePermFinOfNatNatIsoClass {n : ℕ} : MulAction (Equiv.Perm (Fin 3))ᵐᵒᵖ (IsoClass n)

Reordering the branch points is a right action of Perm (Fin 3) on isomorphism classes of triples, written as a left action of the opposite group.

Equations

• TauCeti.PermutationTriple.instMulActionMulOppositePermFinOfNatNatIsoClass = { toSMul := TauCeti.PermutationTriple.instSMulMulOppositePermFinOfNatNatIsoClass, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.PermutationTriple.equivalent_reindexBranchPoints_reindexBranchPoints {n : ℕ} (t : PermutationTriple n) (ρ ρ' : Equiv.Perm (Fin 3)) : ((t.reindexBranchPoints ρ').reindexBranchPoints ρ).Equivalent (t.reindexBranchPoints (ρ' * ρ))

Reordering the branch points twice is reordering along the product, up to isomorphism.

Connected triples and their isomorphism classes

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

Reorder the branch points of a connected triple.

Equations

• t.reindexBranchPoints ρ = ⟨(↑t).reindexBranchPoints ρ, ⋯⟩

@[simp]

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

@[simp]

theorem TauCeti.ConnectedTriple.reindexBranchPoints_one {n : ℕ} (t : ConnectedTriple n) : t.reindexBranchPoints 1 = t

Reordering the branch points along the identity permutation changes nothing.

@[simp]

theorem TauCeti.ConnectedTriple.reindexBranchPoints_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : ConnectedTriple n) (ρ : Equiv.Perm (Fin 3)) : (τ • t).reindexBranchPoints ρ = τ • t.reindexBranchPoints ρ

Reordering the branch points commutes with relabeling the sheets.

@[instance_reducible]

instance TauCeti.ConnectedIsoClass.instSMulMulOppositePermFinOfNatNat {n : ℕ} : SMul (Equiv.Perm (Fin 3))ᵐᵒᵖ (ConnectedIsoClass n)

Reordering the branch points of the isomorphism class of a connected triple: MulOpposite.op ρ sends the class of t to the class of t.reindexBranchPoints ρ.

Equations

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

@[simp]

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

Acting by MulOpposite.op ρ on the class represented by t computes by reindexing that representative along ρ.

@[instance_reducible]

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

Reordering the branch points is a right action of Perm (Fin 3) on isomorphism classes of connected triples, written as a left action of the opposite group; it is the restriction of the action on TauCeti.PermutationTriple.IsoClass to the connected classes.

Equations

• TauCeti.ConnectedIsoClass.instMulActionMulOppositePermFinOfNatNat = { toSMul := TauCeti.ConnectedIsoClass.instSMulMulOppositePermFinOfNatNat, mul_smul := ⋯, one_smul := ⋯ }