Dividing and exact orders of permutation triples

A permutation triple t of degree n can be attached to three natural numbers a, b, c in three ways, which sources on triangle groups and dessins tend to conflate:

• dividing orders: t.σ0 ^ a = 1, t.σ1 ^ b = 1 and t.σinf ^ c = 1. This is the hypothesis under which t is a permutation representation of the triangle group Δ(a, b, c) (TauCeti.TriangleGroup.toPerm), whose image is then the whole monodromy group of t (TauCeti.TriangleGroup.range_toPerm);
• exact orders: t.orderTriple = (a, b, c), the abc datum of a three-point cover.
• surjective monodromy: the triangle group representation has range equal to the monodromy group of t.

Exact orders are dividing orders, and a triple has dividing orders (a, b, c) exactly when its order triple divides (a, b, c) componentwise. Exact orders can also be read off one component at a time, and a first order of one is the repeated form (1, m, m): a monodromy of order one is the identity, so the product relation makes the other two inverse.

The file then records necessary conditions for a connected triple of degree n with given orders to exist. Each entry of the order triple is the least common multiple of a partition of n. A permutation whose order divides a ≠ 0 has cycles of length at most a, so it has at least n / a cycles; summing over the three components bounds the Euler characteristic from below:

n * (1 / a + 1 / b + 1 / c - 1) ≤ χ(t).

For a connected triple χ(t) ≤ 2, so n * (1 / a + 1 / b + 1 / c - 1) ≤ 2. When 1 / a + 1 / b + 1 / c > 1 (the spherical case) this bounds the degree n; in the Euclidean and hyperbolic cases it is no condition at all. None of these conditions is claimed to be sufficient.

Main results

• TauCeti.PermutationTriple.hasDividingOrders_iff_orderTriple_dvd: dividing orders are multiples of the order triple.
• TauCeti.PermutationTriple.HasExactOrders.hasDividingOrders: exact orders are dividing orders.
• TauCeti.PermutationTriple.orderOf_σ1_eq_orderOf_σinf_of_σ0_eq_one and TauCeti.PermutationTriple.second_eq_third_of_hasExactOrders_one: a first monodromy of order one is the identity, so an exact signature (1, b, c) is the repeated form (1, m, m).
• TauCeti.PermutationTriple.hasSurjectiveMonodromy_iff: the dividing relations automatically give a representation surjective onto the monodromy group.
• TauCeti.PermutationTriple.exists_partition_lcm_eq_orderTriple: each component order is the least common multiple of a partition of the degree; by Equiv.Perm.exists_orderOf_eq_iff these are exactly the orders of the permutations of n points.
• TauCeti.PermutationTriple.natCast_mul_inv_add_inv_add_inv_sub_one_le_eulerChar: the lower bound on the Euler characteristic by dividing orders.
• TauCeti.PermutationTriple.IsConnected.natCast_mul_inv_add_inv_add_inv_sub_one_le_two: the resulting constraint on a connected triple.
• TauCeti.PermutationTriple.IsConnected.natCast_le_of_one_lt_inv_add_inv_add_inv: the degree bound in the spherical case.

References

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

Dividing and exact orders

def TauCeti.PermutationTriple.HasDividingOrders {n : ℕ} (t : PermutationTriple n) (a b c : ℕ) : Prop

The component orders of t divide (a, b, c).

Equations

• t.HasDividingOrders a b c = (t.σ0 ^ a = 1 ∧ t.σ1 ^ b = 1 ∧ t.σinf ^ c = 1)

def TauCeti.PermutationTriple.HasExactOrders {n : ℕ} (t : PermutationTriple n) (a b c : ℕ) : Prop

The component orders of t are exactly (a, b, c).

Equations

• t.HasExactOrders a b c = (t.orderTriple = (a, b, c))

def TauCeti.PermutationTriple.HasSurjectiveMonodromy {n : ℕ} (t : PermutationTriple n) (a b c : ℕ) : Prop

The triangle group representation of t has image its monodromy group. The witnessing power relations are part of this condition, since the representation requires them.

Equations

• t.HasSurjectiveMonodromy a b c = ∃ (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1), (TauCeti.TriangleGroup.toPerm t ha hb hc).range = t.monodromyGroup

@[simp]

theorem TauCeti.PermutationTriple.hasDividingOrders_iff {n a b c : ℕ} (t : PermutationTriple n) : t.HasDividingOrders a b c ↔ t.σ0 ^ a = 1 ∧ t.σ1 ^ b = 1 ∧ t.σinf ^ c = 1

Dividing orders are the three power relations.

@[simp]

theorem TauCeti.PermutationTriple.hasExactOrders_iff {n a b c : ℕ} (t : PermutationTriple n) : t.HasExactOrders a b c ↔ t.orderTriple = (a, b, c)

Exact orders agree with the order triple.

theorem TauCeti.PermutationTriple.hasDividingOrders_iff_orderTriple_dvd {n a b c : ℕ} (t : PermutationTriple n) : t.HasDividingOrders a b c ↔ t.orderTriple.1 ∣ a ∧ t.orderTriple.2.1 ∣ b ∧ t.orderTriple.2.2 ∣ c

Dividing orders are precisely the multiples of the component orders.

theorem TauCeti.PermutationTriple.HasExactOrders.hasDividingOrders {n a b c : ℕ} (t : PermutationTriple n) (h : t.HasExactOrders a b c) : t.HasDividingOrders a b c

A triple with exact orders (a, b, c) has dividing orders (a, b, c). In particular every triple has dividing orders its own order triple.

theorem TauCeti.PermutationTriple.hasDividingOrders_orderTriple {n : ℕ} (t : PermutationTriple n) : t.HasDividingOrders t.orderTriple.1 t.orderTriple.2.1 t.orderTriple.2.2

Every triple has dividing orders given by its own order triple.

@[simp]

theorem TauCeti.PermutationTriple.hasSurjectiveMonodromy_iff {n a b c : ℕ} (t : PermutationTriple n) : t.HasSurjectiveMonodromy a b c ↔ t.HasDividingOrders a b c

Surjectivity onto the monodromy group follows from the dividing relations.

theorem TauCeti.PermutationTriple.exists_partition_lcm_eq_orderTriple {n : ℕ} (t : PermutationTriple n) : (∃ (p : n.Partition), p.parts.lcm = t.orderTriple.1) ∧ (∃ (p : n.Partition), p.parts.lcm = t.orderTriple.2.1) ∧ ∃ (p : n.Partition), p.parts.lcm = t.orderTriple.2.2

Each component order of a degree-n triple is the least common multiple of a partition of n.

theorem TauCeti.PermutationTriple.exists_partition_lcm_eq_of_orderTriple_eq {n a b c : ℕ} (t : PermutationTriple n) (h : t.HasExactOrders a b c) : (∃ (p : n.Partition), p.parts.lcm = a) ∧ (∃ (p : n.Partition), p.parts.lcm = b) ∧ ∃ (p : n.Partition), p.parts.lcm = c

Each prescribed exact order is the least common multiple of a partition of the degree.

theorem TauCeti.PermutationTriple.orderOf_σ1_eq_orderOf_σinf_of_σ0_eq_one {n : ℕ} (t : PermutationTriple n) (h : t.σ0 = 1) : orderOf t.σ1 = orderOf t.σinf

A trivial first monodromy makes the other two inverse, by the product relation σinf * σ1 * σ0 = 1, so the second and third entries of the order triple agree.

theorem TauCeti.PermutationTriple.second_eq_third_of_hasExactOrders_one {n b c : ℕ} (t : PermutationTriple n) (h : t.HasExactOrders 1 b c) : b = c

An exact signature (1, b, c) is the repeated form (1, m, m): its second and third orders agree, since a first monodromy of order one is the identity and the other two are inverse.

The Euler characteristic bound

theorem TauCeti.PermutationTriple.natCast_mul_inv_add_inv_add_inv_sub_one_le_eulerChar {n a b c : ℕ} (t : PermutationTriple n) (h : t.HasDividingOrders a b c) : ↑n * ((↑a)⁻¹ + (↑b)⁻¹ + (↑c)⁻¹ - 1) ≤ ↑t.eulerChar

The Euler characteristic is bounded below by dividing orders. If the components of a degree-n triple have orders dividing a, b and c, then n * (1 / a + 1 / b + 1 / c - 1) ≤ χ(t). A zero order imposes no condition and contributes no term, since (0 : ℚ)⁻¹ = 0.

theorem TauCeti.PermutationTriple.IsConnected.natCast_mul_inv_add_inv_add_inv_sub_one_le_two {n a b c : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) (h : t.HasDividingOrders a b c) : ↑n * ((↑a)⁻¹ + (↑b)⁻¹ + (↑c)⁻¹ - 1) ≤ 2

The orbifold constraint on a connected triple. If the components of a connected degree-n triple have orders dividing a, b and c, then n * (1 / a + 1 / b + 1 / c - 1) ≤ 2.

theorem TauCeti.PermutationTriple.IsConnected.natCast_le_of_one_lt_inv_add_inv_add_inv {n a b c : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) (h : t.HasDividingOrders a b c) (habc : 1 < (↑a)⁻¹ + (↑b)⁻¹ + (↑c)⁻¹) : ↑n ≤ 2 / ((↑a)⁻¹ + (↑b)⁻¹ + (↑c)⁻¹ - 1)

The degree bound in the spherical case. If 1 / a + 1 / b + 1 / c > 1 and the components of a connected degree-n triple have orders dividing a, b and c, then n ≤ 2 / (1 / a + 1 / b + 1 / c - 1).