Orders and geometry types of permutation triples

The order triple of a permutation triple records the orders of its monodromies at the ordered branch points 0, 1, and ∞. It is the abc invariant used in the classification of three-point covers. Each entry is also the least common multiple of the corresponding full cycle partition.

The reciprocal sum of the three orders determines whether the associated triangle-group signature is spherical, Euclidean, or hyperbolic. This file defines that trichotomy using exact rational arithmetic and proves that both invariants are unchanged by relabeling the sheets or by inverting all three permutations to change composition convention.

Main declarations

• TauCeti.PermutationTriple.orderTriple: the ordered triple of permutation orders.
• TauCeti.GeometryType: the spherical, Euclidean, and hyperbolic trichotomy.
• TauCeti.GeometryType.ofOrders: the geometry type determined by three orders.
• TauCeti.PermutationTriple.geometryType: the geometry type of a permutation triple.
• TauCeti.PermutationTriple.geometryType_eq_of_sum_eq: equality of reciprocal order sums determines equality of geometry types.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, §2.4.

noncomputable def TauCeti.PermutationTriple.orderTriple {n : ℕ} (t : PermutationTriple n) : ℕ × ℕ × ℕ

The ordered triple of the orders of the monodromies at 0, 1, and ∞.

Equations

• t.orderTriple = (orderOf t.σ0, orderOf t.σ1, orderOf t.σinf)

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_σ0 {n : ℕ} (t : PermutationTriple n) : t.orderTriple.1 = orderOf t.σ0

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_σ1 {n : ℕ} (t : PermutationTriple n) : t.orderTriple.2.1 = orderOf t.σ1

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_σinf {n : ℕ} (t : PermutationTriple n) : t.orderTriple.2.2 = orderOf t.σinf

theorem TauCeti.PermutationTriple.orderTriple_eq_lcm_cycleData {n : ℕ} (t : PermutationTriple n) : t.orderTriple = (t.cycleData.1.lcm, t.cycleData.2.1.lcm, t.cycleData.2.2.lcm)

The entries of the order triple are the least common multiples of the corresponding full cycle partitions.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_one {n : ℕ} : orderTriple 1 = (1, 1, 1)

The trivial triple has order triple (1, 1, 1).

@[simp]

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

Relabeling the sheets does not change the order triple.

@[simp]

theorem TauCeti.PermutationTriple.orderTriple_transport {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).orderTriple = t.orderTriple

Transporting the sheet labels along an equivalence does not change the order triple.

theorem TauCeti.PermutationTriple.orderTriple_inv_components {n : ℕ} (t : PermutationTriple n) : (orderOf t.σ0⁻¹, orderOf t.σ1⁻¹, orderOf t.σinf⁻¹) = t.orderTriple

Inverting all three components does not change their ordered triple of orders.

theorem TauCeti.PermutationTriple.orderTriple_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.orderTriple = t'.orderTriple

Isomorphic permutation triples have the same order triple.

inductive TauCeti.GeometryType : Type

The geometry type determined by the reciprocal sum of three monodromy orders.

• spherical : GeometryType
• euclidean : GeometryType
• hyperbolic : GeometryType

@[instance_reducible]

instance TauCeti.instDecidableEqGeometryType : DecidableEq GeometryType

Equations

• TauCeti.instDecidableEqGeometryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TauCeti.instReprGeometryType : Repr GeometryType

Equations

• TauCeti.instReprGeometryType = { reprPrec := TauCeti.instReprGeometryType.repr }

def TauCeti.instReprGeometryType.repr : GeometryType → ℕ → Std.Format

Equations

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

def TauCeti.GeometryType.ofOrders (abc : ℕ+ × ℕ+ × ℕ+) : GeometryType

Classify three positive orders as spherical, Euclidean, or hyperbolic according as their reciprocal sum is greater than, equal to, or less than one.

Equations

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

@[simp]

theorem TauCeti.GeometryType.ofOrders_eq_spherical_iff (abc : ℕ+ × ℕ+ × ℕ+) : ofOrders abc = spherical ↔ 1 < (↑↑abc.1)⁻¹ + (↑↑abc.2.1)⁻¹ + (↑↑abc.2.2)⁻¹

Three orders have spherical type exactly when their reciprocal sum is greater than one.

@[simp]

theorem TauCeti.GeometryType.ofOrders_eq_euclidean_iff (abc : ℕ+ × ℕ+ × ℕ+) : ofOrders abc = euclidean ↔ (↑↑abc.1)⁻¹ + (↑↑abc.2.1)⁻¹ + (↑↑abc.2.2)⁻¹ = 1

Three orders have Euclidean type exactly when their reciprocal sum is one.

@[simp]

theorem TauCeti.GeometryType.ofOrders_eq_hyperbolic_iff (abc : ℕ+ × ℕ+ × ℕ+) : ofOrders abc = hyperbolic ↔ (↑↑abc.1)⁻¹ + (↑↑abc.2.1)⁻¹ + (↑↑abc.2.2)⁻¹ < 1

Three orders have hyperbolic type exactly when their reciprocal sum is less than one.

noncomputable def TauCeti.PermutationTriple.geometryType {n : ℕ} (t : PermutationTriple n) : GeometryType

The spherical, Euclidean, or hyperbolic geometry type of a permutation triple, determined by the exact rational reciprocal sum of its three component orders.

Equations

• t.geometryType = TauCeti.GeometryType.ofOrders (⟨orderOf t.σ0, ⋯⟩, ⟨orderOf t.σ1, ⋯⟩, ⟨orderOf t.σinf, ⋯⟩)

@[simp]

theorem TauCeti.PermutationTriple.geometryType_eq_spherical_iff {n : ℕ} (t : PermutationTriple n) : t.geometryType = GeometryType.spherical ↔ 1 < (↑(orderOf t.σ0))⁻¹ + (↑(orderOf t.σ1))⁻¹ + (↑(orderOf t.σinf))⁻¹

A permutation triple is spherical exactly when the reciprocal sum of its component orders is greater than one.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_eq_euclidean_iff {n : ℕ} (t : PermutationTriple n) : t.geometryType = GeometryType.euclidean ↔ (↑(orderOf t.σ0))⁻¹ + (↑(orderOf t.σ1))⁻¹ + (↑(orderOf t.σinf))⁻¹ = 1

A permutation triple is Euclidean exactly when the reciprocal sum of its component orders is one.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_eq_hyperbolic_iff {n : ℕ} (t : PermutationTriple n) : t.geometryType = GeometryType.hyperbolic ↔ (↑(orderOf t.σ0))⁻¹ + (↑(orderOf t.σ1))⁻¹ + (↑(orderOf t.σinf))⁻¹ < 1

A permutation triple is hyperbolic exactly when the reciprocal sum of its component orders is less than one.

theorem TauCeti.PermutationTriple.geometryType_eq_of_sum_eq {n : ℕ} {t t' : PermutationTriple n} (h : (↑t.orderTriple.1)⁻¹ + (↑t.orderTriple.2.1)⁻¹ + (↑t.orderTriple.2.2)⁻¹ = (↑t'.orderTriple.1)⁻¹ + (↑t'.orderTriple.2.1)⁻¹ + (↑t'.orderTriple.2.2)⁻¹) : t.geometryType = t'.geometryType

Two permutation triples have the same geometry type if the reciprocal sums of their order triples are equal.

@[simp]

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

Relabeling the sheets does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_transport {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).geometryType = t.geometryType

Transporting the sheet labels along an equivalence does not change the geometry type.

@[simp]

theorem TauCeti.PermutationTriple.geometryType_one {n : ℕ} : geometryType 1 = GeometryType.spherical

The trivial permutation triple has spherical geometry type.

theorem TauCeti.PermutationTriple.geometryType_inv_components {n : ℕ} (t : PermutationTriple n) : GeometryType.ofOrders (⟨orderOf t.σ0⁻¹, ⋯⟩, ⟨orderOf t.σ1⁻¹, ⋯⟩, ⟨orderOf t.σinf⁻¹, ⋯⟩) = t.geometryType

Inverting all three components, as in the opposite composition convention, does not change the geometry type computed from their orders.

theorem TauCeti.PermutationTriple.geometryType_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.geometryType = t'.geometryType

Isomorphic permutation triples have the same geometry type.