Examples of permutation triples

This file names the small permutation triples that serve as test cases for the theory of three-point covers, and computes their invariants: connectedness, cycle data, Euler characteristic, genus, orders, geometry type, monodromy group and automorphism group.

• TauCeti.PermutationTriple.cyclicTriple n: for n ≠ 0, the monodromy of z ↦ zⁿ, totally ramified over 0 and ∞ and unramified over 1. For n ≠ 0 it is connected of genus zero, with cyclic monodromy of order n, hence regular, and its automorphism group is that monodromy group; it is spherical in every degree. cyclicTriple 0 is the formal empty triple, which is not connected, and cyclicTriple 1 is the trivial triple, the identity cover of the sphere. Disjoint sums of two such triples are disconnected, with Euler characteristic 4. Relabeling cyclicTriple 4 by swap 0 1 gives the different but isomorphic triple (c[0, 2, 3, 1], 1, c[0, 2, 3, 1]⁻¹).
• TauCeti.PermutationTriple.cyclicPowTriple n k: the triple (r, r ^ k, (r ^ (k + 1))⁻¹) built from cyclic rotation r = finRotate n; its monodromy is generated by r, and it is connected in every nonzero degree.
• TauCeti.PermutationTriple.chebyshevTriple: the monodromy of z ↦ 4z(1 - z), a connected genus-zero triple whose component over 0 is the identity. Being unramified over a point is allowed.
• TauCeti.PermutationTriple.torusTriple: a degree-four triple with cycle data [4], [4], [2, 2]. It is connected of genus one and Euclidean; its automorphism group equals its cyclic monodromy group of order four, so it is regular; and {0, 2} is a nontrivial block, so its monodromy action is imprimitive. Its quotient by this block is the degree-two triple unramified over ∞.
• TauCeti.PermutationTriple.s3Triple: a degree-three genus-zero triple whose monodromy group is the whole symmetric group and whose automorphism group is trivial, so it is not regular.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.1 and §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.

The cyclic triple

def TauCeti.PermutationTriple.cyclicTriple (n : ℕ) : PermutationTriple n

The cyclic triple of degree n: the sheets are rotated cyclically around 0 and in the opposite direction around ∞, and are not permuted around 1. For n ≠ 0 it is the monodromy triple of the cover z ↦ zⁿ of the sphere; cyclicTriple 0 is the formal empty triple.

Equations

• TauCeti.PermutationTriple.cyclicTriple n = { σ0 := finRotate n, σ1 := 1, σinf := (finRotate n)⁻¹, product_eq_one := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.cyclicTriple_σ0 {n : ℕ} : (cyclicTriple n).σ0 = finRotate n

@[simp]

theorem TauCeti.PermutationTriple.cyclicTriple_σ1 {n : ℕ} : (cyclicTriple n).σ1 = 1

@[simp]

theorem TauCeti.PermutationTriple.cyclicTriple_σinf {n : ℕ} : (cyclicTriple n).σinf = (finRotate n)⁻¹

@[simp]

theorem TauCeti.PermutationTriple.cyclicTriple_one : cyclicTriple 1 = 1

The cyclic triple of degree one is the trivial triple.

theorem TauCeti.PermutationTriple.monodromyGroup_cyclicTriple {n : ℕ} : (cyclicTriple n).monodromyGroup = Subgroup.zpowers (finRotate n)

The monodromy group of the cyclic triple is generated by cyclic rotation.

theorem TauCeti.PermutationTriple.card_monodromyGroup_cyclicTriple {n : ℕ} (hn : n ≠ 0) : Nat.card ↥(cyclicTriple n).monodromyGroup = n

The monodromy group of the cyclic triple of degree n ≠ 0 has order n.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_cyclicTriple_iff {n : ℕ} : (cyclicTriple n).IsConnected ↔ n ≠ 0

The cyclic triple is connected exactly when it has at least one sheet.

theorem TauCeti.PermutationTriple.isRegular_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).IsRegular

The cyclic triple of degree n ≠ 0 is regular: its monodromy group has order n.

theorem TauCeti.PermutationTriple.automorphismGroup_cyclicTriple {n : ℕ} : (cyclicTriple n).automorphismGroup = Subgroup.zpowers (finRotate n)

The automorphism group of the cyclic triple is generated by cyclic rotation, so it equals the monodromy group (monodromyGroup_cyclicTriple).

theorem TauCeti.PermutationTriple.cycleData_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).cycleData = ({n}, Multiset.replicate n 1, {n})

The cyclic triple is totally ramified over 0 and ∞ and unramified over 1.

theorem TauCeti.PermutationTriple.cycleCounts_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).cycleCounts = (1, n, 1)

The cyclic triple has one cycle over 0 and over ∞, and n fixed points over 1.

theorem TauCeti.PermutationTriple.eulerChar_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).eulerChar = 2

The cover z ↦ zⁿ is a sphere: its Euler characteristic is 2.

theorem TauCeti.PermutationTriple.genus_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).genus = 0

The cyclic triple of positive degree has genus zero.

theorem TauCeti.PermutationTriple.orderTriple_cyclicTriple {n : ℕ} (hn : n ≠ 0) : (cyclicTriple n).orderTriple = (n, 1, n)

The orders of the components of the cyclic triple are (n, 1, n).

@[simp]

theorem TauCeti.PermutationTriple.geometryType_cyclicTriple {n : ℕ} : (cyclicTriple n).geometryType = GeometryType.spherical

The cyclic triple is spherical in every degree, its component over 1 having order one.

Triples built from powers of cyclic rotation

def TauCeti.PermutationTriple.cyclicPowTriple (n k : ℕ) : PermutationTriple n

The triple (r, r ^ k, (r ^ (k + 1))⁻¹) of degree n, where r = finRotate n is cyclic rotation of Fin n.

Equations

• TauCeti.PermutationTriple.cyclicPowTriple n k = TauCeti.PermutationTriple.ofTwo (finRotate n) (finRotate n ^ k)

@[simp]

theorem TauCeti.PermutationTriple.cyclicPowTriple_σ0 {n k : ℕ} : (cyclicPowTriple n k).σ0 = finRotate n

@[simp]

theorem TauCeti.PermutationTriple.cyclicPowTriple_σ1 {n k : ℕ} : (cyclicPowTriple n k).σ1 = finRotate n ^ k

@[simp]

theorem TauCeti.PermutationTriple.cyclicPowTriple_σinf {n k : ℕ} : (cyclicPowTriple n k).σinf = (finRotate n ^ (k + 1))⁻¹

theorem TauCeti.PermutationTriple.cyclicPowTriple_σinf_of_lt {n k : ℕ} (hk : k < n) : (cyclicPowTriple n k).σinf = finRotate n ^ (n - 1 - k)

For k < n, the component of cyclicPowTriple n k over ∞ is the power r ^ (n - 1 - k) of cyclic rotation r.

theorem TauCeti.PermutationTriple.monodromyGroup_cyclicPowTriple {n k : ℕ} : (cyclicPowTriple n k).monodromyGroup = Subgroup.zpowers (finRotate n)

The monodromy group of cyclicPowTriple n k is the cyclic group generated by rotation.

theorem TauCeti.PermutationTriple.isConnected_cyclicPowTriple {n k : ℕ} (hn : n ≠ 0) : (cyclicPowTriple n k).IsConnected

The triple cyclicPowTriple n k is connected when it has at least one sheet.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_cyclicPowTriple_iff {n k : ℕ} (hn : n ≠ 0) : (cyclicPowTriple n k).cycleData = ({n}, {n}, {n}) ↔ k.Coprime n ∧ (k + 1).Coprime n

In nonzero degree, each component of cyclicPowTriple n k is a single n-cycle exactly when k and k + 1 are coprime to n.

theorem TauCeti.PermutationTriple.cycleData_cyclicPowTriple {n k : ℕ} (hk : k.Coprime n) (hk' : (k + 1).Coprime n) : (cyclicPowTriple n k).cycleData = ({n}, {n}, {n})

Each component of cyclicPowTriple n k is a single n-cycle when k and k + 1 are coprime to n.

A disconnected triple, and an isomorphic pair

theorem TauCeti.PermutationTriple.eulerChar_disjointSum_cyclicTriple {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : ((cyclicTriple m).disjointSum (cyclicTriple n)).eulerChar = 4

The disjoint sum of two cyclic triples of positive degree covers two spheres, so its Euler characteristic is 4.

theorem TauCeti.PermutationTriple.swap_smul_cyclicTriple_four_ne : Equiv.swap 0 1 • cyclicTriple 4 ≠ cyclicTriple 4

Relabeling the sheets of cyclicTriple 4 by a transposition changes the triple.

theorem TauCeti.PermutationTriple.swap_smul_cyclicTriple_four : Equiv.swap 0 1 • cyclicTriple 4 = ofTwo ((↑[0, 2, 3, 1]).formPerm ⋯) 1

Relabeling the sheets of cyclicTriple 4 by the transposition swap 0 1 gives the triple whose component over 0 is the 4-cycle c[0, 2, 3, 1] and which is unramified over 1.

theorem TauCeti.PermutationTriple.equivalent_ofTwo_cyclicTriple_four : (ofTwo ((↑[0, 2, 3, 1]).formPerm ⋯) 1).Equivalent (cyclicTriple 4)

The triple (c[0, 2, 3, 1], 1, c[0, 2, 3, 1]⁻¹) is isomorphic to cyclicTriple 4, the isomorphism being the relabeling by swap 0 1.

A triple unramified over 0

def TauCeti.PermutationTriple.chebyshevTriple : PermutationTriple 2

The monodromy triple of z ↦ 4z(1 - z): the two sheets are exchanged around 1 and ∞ and not around 0.

Equations

• TauCeti.PermutationTriple.chebyshevTriple = { σ0 := 1, σ1 := Equiv.swap 0 1, σinf := Equiv.swap 0 1, product_eq_one := TauCeti.PermutationTriple.chebyshevTriple._proof_1 }

@[simp]

theorem TauCeti.PermutationTriple.chebyshevTriple_σ0 : chebyshevTriple.σ0 = 1

@[simp]

theorem TauCeti.PermutationTriple.chebyshevTriple_σ1 : chebyshevTriple.σ1 = Equiv.swap 0 1

@[simp]

theorem TauCeti.PermutationTriple.chebyshevTriple_σinf : chebyshevTriple.σinf = Equiv.swap 0 1

theorem TauCeti.PermutationTriple.isConnected_chebyshevTriple : chebyshevTriple.IsConnected

The triple of z ↦ 4z(1 - z) is connected.

theorem TauCeti.PermutationTriple.cycleData_chebyshevTriple : chebyshevTriple.cycleData = ({1, 1}, {2}, {2})

The triple of z ↦ 4z(1 - z) has two unramified sheets over 0, and one double point over each of 1 and ∞.

theorem TauCeti.PermutationTriple.eulerChar_chebyshevTriple : chebyshevTriple.eulerChar = 2

The cover z ↦ 4z(1 - z) is a sphere: its Euler characteristic is 2.

theorem TauCeti.PermutationTriple.genus_chebyshevTriple : chebyshevTriple.genus = 0

The triple of z ↦ 4z(1 - z) has genus zero.

theorem TauCeti.PermutationTriple.orderTriple_chebyshevTriple : chebyshevTriple.orderTriple = (1, 2, 2)

The orders of the components of the triple of z ↦ 4z(1 - z) are (1, 2, 2).

The torus triple

def TauCeti.PermutationTriple.torusTriple : PermutationTriple 4

A degree-four triple of genus one: cyclic rotation around both 0 and 1, and hence the square of the inverse rotation around ∞.

Equations

• TauCeti.PermutationTriple.torusTriple = { σ0 := finRotate 4, σ1 := finRotate 4, σinf := (finRotate 4 ^ 2)⁻¹, product_eq_one := TauCeti.PermutationTriple.torusTriple._proof_1 }

@[simp]

theorem TauCeti.PermutationTriple.torusTriple_σ0 : torusTriple.σ0 = finRotate 4

@[simp]

theorem TauCeti.PermutationTriple.torusTriple_σ1 : torusTriple.σ1 = finRotate 4

@[simp]

theorem TauCeti.PermutationTriple.torusTriple_σinf : torusTriple.σinf = (finRotate 4 ^ 2)⁻¹

theorem TauCeti.PermutationTriple.monodromyGroup_torusTriple : torusTriple.monodromyGroup = Subgroup.zpowers (finRotate 4)

The monodromy group of the torus triple is generated by cyclic rotation.

theorem TauCeti.PermutationTriple.card_monodromyGroup_torusTriple : Nat.card ↥torusTriple.monodromyGroup = 4

The monodromy group of the torus triple is cyclic of order four.

theorem TauCeti.PermutationTriple.isConnected_torusTriple : torusTriple.IsConnected

The torus triple is connected.

theorem TauCeti.PermutationTriple.cycleData_torusTriple : torusTriple.cycleData = ({4}, {4}, {2, 2})

The torus triple is totally ramified over 0 and 1, and has two double points over ∞.

theorem TauCeti.PermutationTriple.cycleCounts_torusTriple : torusTriple.cycleCounts = (1, 1, 2)

The torus triple has one cycle over each of 0 and 1, and two over ∞.

theorem TauCeti.PermutationTriple.eulerChar_torusTriple : torusTriple.eulerChar = 0

The torus triple has Euler characteristic zero.

theorem TauCeti.PermutationTriple.genus_torusTriple : torusTriple.genus = 1

The torus triple has genus one.

theorem TauCeti.PermutationTriple.orderTriple_torusTriple : torusTriple.orderTriple = (4, 4, 2)

The orders of the components of the torus triple are (4, 4, 2).

theorem TauCeti.PermutationTriple.geometryType_torusTriple : torusTriple.geometryType = GeometryType.euclidean

The torus triple is Euclidean: 1/4 + 1/4 + 1/2 = 1.

theorem TauCeti.PermutationTriple.automorphismGroup_torusTriple : torusTriple.automorphismGroup = torusTriple.monodromyGroup

The automorphism group of the torus triple is its whole monodromy group.

theorem TauCeti.PermutationTriple.isRegular_torusTriple : torusTriple.IsRegular

The torus triple is regular: its monodromy group has order equal to the degree 4.

theorem TauCeti.PermutationTriple.isBlock_torusTriple : MulAction.IsBlock ↥torusTriple.monodromyGroup {0, 2}

The pair {0, 2} is a block for the monodromy action of the torus triple.

theorem TauCeti.PermutationTriple.not_isPreprimitive_torusTriple : ¬MulAction.IsPreprimitive (↥torusTriple.monodromyGroup) (Fin 4)

The monodromy action of the torus triple is imprimitive.

theorem TauCeti.PermutationTriple.card_orbit_torusTriple : Nat.card ↑(MulAction.orbit ↥torusTriple.monodromyGroup {0, 2}) = 2

The block {0, 2} of the Euclidean genus-one triple has two translates.

theorem TauCeti.PermutationTriple.blockQuotient_torusTriple (e : ↑(MulAction.orbit ↥torusTriple.monodromyGroup {0, 2}) ≃ Fin 2) : torusTriple.blockQuotient {0, 2} e = ofTwo (Equiv.swap 0 1) (Equiv.swap 0 1)

The quotient of the Euclidean genus-one triple torusTriple by its block {0, 2}, for any numbering of the two translates, is the degree-two triple with components (0 1), (0 1), 1: the double cover of the sphere branched over 0 and 1 only.

A triple with symmetric monodromy

def TauCeti.PermutationTriple.s3Triple : PermutationTriple 3

A degree-three triple whose monodromy group is all of S₃: a three-cycle around 0 and a transposition around 1.

Equations

• TauCeti.PermutationTriple.s3Triple = { σ0 := finRotate 3, σ1 := Equiv.swap 0 1, σinf := Equiv.swap 1 2, product_eq_one := TauCeti.PermutationTriple.s3Triple._proof_1 }

@[simp]

theorem TauCeti.PermutationTriple.s3Triple_σ0 : s3Triple.σ0 = finRotate 3

@[simp]

theorem TauCeti.PermutationTriple.s3Triple_σ1 : s3Triple.σ1 = Equiv.swap 0 1

@[simp]

theorem TauCeti.PermutationTriple.s3Triple_σinf : s3Triple.σinf = Equiv.swap 1 2

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_s3Triple : s3Triple.monodromyGroup = ⊤

The monodromy group of s3Triple is the whole symmetric group.

theorem TauCeti.PermutationTriple.isConnected_s3Triple : s3Triple.IsConnected

The triple s3Triple is connected.

theorem TauCeti.PermutationTriple.cycleData_s3Triple : s3Triple.cycleData = ({3}, {2, 1}, {2, 1})

The triple s3Triple is totally ramified over 0, and has one double point and one unramified sheet over each of 1 and ∞.

theorem TauCeti.PermutationTriple.eulerChar_s3Triple : s3Triple.eulerChar = 2

The triple s3Triple has Euler characteristic 2.

theorem TauCeti.PermutationTriple.genus_s3Triple : s3Triple.genus = 0

The triple s3Triple has genus zero.

theorem TauCeti.PermutationTriple.orderTriple_s3Triple : s3Triple.orderTriple = (3, 2, 2)

The orders of the components of s3Triple are (3, 2, 2).

@[simp]

theorem TauCeti.PermutationTriple.automorphismGroup_s3Triple : s3Triple.automorphismGroup = ⊥

The automorphism group of s3Triple is trivial.

theorem TauCeti.PermutationTriple.not_isRegular_s3Triple : ¬s3Triple.IsRegular

The triple s3Triple is not regular: its automorphism group is trivial, of order 1 ≠ 3.