The oriented triangle groups

For natural numbers a b c, the (oriented, von Dyck) triangle group Δ(a, b, c) is the group presented by three generators x, y, z subject to

x ^ a = 1, y ^ b = 1, z ^ c = 1, z * y * x = 1.

The product relator is written in the display order z * y * x, the same order as the relation σinf * σ1 * σ0 = 1 of TauCeti.PermutationTriple. By the universal property TauCeti.TriangleGroup.lift, a permutation triple whose components have orders dividing a, b, c therefore determines a homomorphism Δ(a, b, c) →* Equiv.Perm (Fin n) sending x, y, z to σ0, σ1, σinf; these finite permutation representations are how triangle groups enter the combinatorics of three-point covers.

The presentation is taken as the definition. No identification with a group of isometries of the sphere, the Euclidean plane or the hyperbolic plane is made here.

A parameter 0 is allowed: the relator x ^ 0 = 1 is trivial, so it imposes no condition on the corresponding generator. In particular Δ(0, 0, 0) is free of rank two, not three, because the product relator determines z from x and y (TauCeti.TriangleGroup.equivFreeGroup).

Main definitions

• TauCeti.triangleRelators a b c: the four relators, in FreeGroup (Fin 3).
• TauCeti.TriangleGroup a b c: the presented group.
• TauCeti.TriangleGroup.x, TauCeti.TriangleGroup.y, TauCeti.TriangleGroup.z: the three distinguished generators.
• TauCeti.TriangleGroup.lift: the universal property, and TauCeti.TriangleGroup.homEquiv, the bijection between homomorphisms out of Δ(a, b, c) and triples of elements satisfying the relations.
• TauCeti.TriangleGroup.rotate: the isomorphism Δ(a, b, c) ≃* Δ(b, c, a) rotating the generators.
• TauCeti.twoGeneratorTriangleRelators and TauCeti.TriangleGroup.equivTwoGenerator: the isomorphism with the two-generator presentation ⟨x, y | x ^ a, y ^ b, (y * x) ^ c⟩.
• TauCeti.TriangleGroup.equivFreeGroup: Δ(0, 0, 0) is the free group on two generators.

Main results

• TauCeti.TriangleGroup.z_eq: the third generator is (y * x)⁻¹.
• TauCeti.TriangleGroup.closure_x_y: the generators x and y alone generate Δ(a, b, c).
• TauCeti.TriangleGroup.hom_ext: a homomorphism out of Δ(a, b, c) is determined by its values on x and y.
• TauCeti.TriangleGroup.range_eq_closure: the range of a homomorphism out of Δ(a, b, c) is generated by the images of x and y.

References

• E. Girondo, G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, LMS Student Texts 79, Cambridge University Press, 2012, Definition 2.28 and the presentation following it.
• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer, 2004.

def TauCeti.triangleRelators (a b c : ℕ) : Set (FreeGroup (Fin 3))

The relators of the (a, b, c) triangle group in FreeGroup (Fin 3): the powers of 0 ^ a, of 1 ^ b, of 2 ^ c and the product relator of 2 * of 1 * of 0.

Equations

• TauCeti.triangleRelators a b c = {FreeGroup.of 0 ^ a, FreeGroup.of 1 ^ b, FreeGroup.of 2 ^ c, FreeGroup.of 2 * FreeGroup.of 1 * FreeGroup.of 0}

@[reducible, inline]

abbrev TauCeti.TriangleGroup (a b c : ℕ) : Type

The oriented triangle group Δ(a, b, c) = ⟨x, y, z | x ^ a, y ^ b, z ^ c, z * y * x⟩.

Equations

• TauCeti.TriangleGroup a b c = PresentedGroup (TauCeti.triangleRelators a b c)

def TauCeti.twoGeneratorTriangleRelators (a b c : ℕ) : Set (FreeGroup (Fin 2))

The relators of the two-generator presentation ⟨x, y | x ^ a, y ^ b, (y * x) ^ c⟩ of the triangle group, in FreeGroup (Fin 2).

Equations

• TauCeti.twoGeneratorTriangleRelators a b c = {FreeGroup.of 0 ^ a, FreeGroup.of 1 ^ b, (FreeGroup.of 1 * FreeGroup.of 0) ^ c}

def TauCeti.TriangleGroup.x (a b c : ℕ) : TriangleGroup a b c

The first distinguished generator of Δ(a, b, c), of order dividing a.

Equations

• TauCeti.TriangleGroup.x a b c = PresentedGroup.of 0

def TauCeti.TriangleGroup.y (a b c : ℕ) : TriangleGroup a b c

The second distinguished generator of Δ(a, b, c), of order dividing b.

Equations

• TauCeti.TriangleGroup.y a b c = PresentedGroup.of 1

def TauCeti.TriangleGroup.z (a b c : ℕ) : TriangleGroup a b c

The third distinguished generator of Δ(a, b, c), of order dividing c; it equals (y * x)⁻¹ (TauCeti.TriangleGroup.z_eq).

Equations

• TauCeti.TriangleGroup.z a b c = PresentedGroup.of 2

@[simp]

theorem TauCeti.TriangleGroup.x_pow (a b c : ℕ) : x a b c ^ a = 1

The first distinguished generator satisfies the first power relation.

@[simp]

theorem TauCeti.TriangleGroup.y_pow (a b c : ℕ) : y a b c ^ b = 1

The second distinguished generator satisfies the second power relation.

@[simp]

theorem TauCeti.TriangleGroup.z_pow (a b c : ℕ) : z a b c ^ c = 1

The third distinguished generator satisfies the third power relation.

@[simp]

theorem TauCeti.TriangleGroup.z_mul_y_mul_x (a b c : ℕ) : z a b c * y a b c * x a b c = 1

The product relation of Δ(a, b, c), in the display order of the presentation.

theorem TauCeti.TriangleGroup.z_eq (a b c : ℕ) : z a b c = (y a b c * x a b c)⁻¹

The third generator is determined by the first two.

@[simp]

theorem TauCeti.TriangleGroup.y_mul_x_pow (a b c : ℕ) : (y a b c * x a b c) ^ c = 1

The product y * x has order dividing c.

theorem TauCeti.TriangleGroup.orderOf_x_dvd (a b c : ℕ) : orderOf (x a b c) ∣ a

The order of the first distinguished generator divides a.

theorem TauCeti.TriangleGroup.orderOf_y_dvd (a b c : ℕ) : orderOf (y a b c) ∣ b

The order of the second distinguished generator divides b.

theorem TauCeti.TriangleGroup.orderOf_z_dvd (a b c : ℕ) : orderOf (z a b c) ∣ c

The order of the third distinguished generator divides c.

@[simp]

theorem TauCeti.TriangleGroup.closure_x_y (a b c : ℕ) : Subgroup.closure {x a b c, y a b c} = ⊤

The generators x and y alone generate Δ(a, b, c).

theorem TauCeti.TriangleGroup.hom_ext (a b c : ℕ) {G : Type u_1} [Group G] {f g : TriangleGroup a b c →* G} (hx : f (x a b c) = g (x a b c)) (hy : f (y a b c) = g (y a b c)) : f = g

A homomorphism out of Δ(a, b, c) is determined by its values on x and y.

theorem TauCeti.TriangleGroup.hom_ext_iff {a b c : ℕ} {G : Type u_1} [Group G] {f g : TriangleGroup a b c →* G} : f = g ↔ f (x a b c) = g (x a b c) ∧ f (y a b c) = g (y a b c)

theorem TauCeti.TriangleGroup.range_eq_closure (a b c : ℕ) {G : Type u_1} [Group G] (f : TriangleGroup a b c →* G) : f.range = Subgroup.closure {f (x a b c), f (y a b c)}

The range of a homomorphism out of Δ(a, b, c) is generated by the images of x and y.

def TauCeti.TriangleGroup.lift {a b c : ℕ} {G : Type u_1} [Group G] (p q r : G) (hp : p ^ a = 1) (hq : q ^ b = 1) (hr : r ^ c = 1) (h : r * q * p = 1) : TriangleGroup a b c →* G

The universal property of the triangle group. Elements p q r of a group with p ^ a = 1, q ^ b = 1, r ^ c = 1 and r * q * p = 1 define a homomorphism out of Δ(a, b, c) sending x, y, z to p, q, r.

Equations

• TauCeti.TriangleGroup.lift p q r hp hq hr h = PresentedGroup.toGroup ⋯

@[simp]

theorem TauCeti.TriangleGroup.lift_x {a b c : ℕ} {G : Type u_1} [Group G] (p q r : G) (hp : p ^ a = 1) (hq : q ^ b = 1) (hr : r ^ c = 1) (h : r * q * p = 1) : (lift p q r hp hq hr h) (x a b c) = p

@[simp]

theorem TauCeti.TriangleGroup.lift_y {a b c : ℕ} {G : Type u_1} [Group G] (p q r : G) (hp : p ^ a = 1) (hq : q ^ b = 1) (hr : r ^ c = 1) (h : r * q * p = 1) : (lift p q r hp hq hr h) (y a b c) = q

@[simp]

theorem TauCeti.TriangleGroup.lift_z {a b c : ℕ} {G : Type u_1} [Group G] (p q r : G) (hp : p ^ a = 1) (hq : q ^ b = 1) (hr : r ^ c = 1) (h : r * q * p = 1) : (lift p q r hp hq hr h) (z a b c) = r

def TauCeti.TriangleGroup.homEquiv {a b c : ℕ} {G : Type u_1} [Group G] : (TriangleGroup a b c →* G) ≃ { g : G × G × G // g.1 ^ a = 1 ∧ g.2.1 ^ b = 1 ∧ g.2.2 ^ c = 1 ∧ g.2.2 * g.2.1 * g.1 = 1 }

Homomorphisms Δ(a, b, c) →* G correspond to triples (p, q, r) of elements of G with p ^ a = 1, q ^ b = 1, r ^ c = 1 and r * q * p = 1, by evaluation at (x, y, z).

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.homEquiv_apply {a b c : ℕ} {G : Type u_1} [Group G] (f : TriangleGroup a b c →* G) : ↑(homEquiv f) = (f (x a b c), f (y a b c), f (z a b c))

@[simp]

theorem TauCeti.TriangleGroup.homEquiv_symm_apply {a b c : ℕ} {G : Type u_1} [Group G] (g : { g : G × G × G // g.1 ^ a = 1 ∧ g.2.1 ^ b = 1 ∧ g.2.2 ^ c = 1 ∧ g.2.2 * g.2.1 * g.1 = 1 }) : homEquiv.symm g = lift (↑g).1 (↑g).2.1 (↑g).2.2 ⋯ ⋯ ⋯ ⋯

def TauCeti.TriangleGroup.rotate {a b c : ℕ} : TriangleGroup a b c ≃* TriangleGroup b c a

The rotation isomorphism Δ(a, b, c) ≃* Δ(b, c, a), sending x, y, z to the generators z, x, y of Δ(b, c, a). The product relator z * y * x of the source becomes the cyclic rotation y * x * z of the product relator of the target.

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.rotate_x {a b c : ℕ} : rotate (x a b c) = z b c a

@[simp]

theorem TauCeti.TriangleGroup.rotate_y {a b c : ℕ} : rotate (y a b c) = x b c a

@[simp]

theorem TauCeti.TriangleGroup.rotate_z {a b c : ℕ} : rotate (z a b c) = y b c a

@[simp]

theorem TauCeti.TriangleGroup.rotate_symm_x {a b c : ℕ} : rotate.symm (x b c a) = y a b c

@[simp]

theorem TauCeti.TriangleGroup.rotate_symm_y {a b c : ℕ} : rotate.symm (y b c a) = z a b c

@[simp]

theorem TauCeti.TriangleGroup.rotate_symm_z {a b c : ℕ} : rotate.symm (z b c a) = x a b c

@[simp]

theorem TauCeti.TriangleGroup.twoGenerator_of_zero_pow {a b c : ℕ} : PresentedGroup.of 0 ^ a = 1

The first generator in the two-generator presentation satisfies its power relation.

@[simp]

theorem TauCeti.TriangleGroup.twoGenerator_of_one_pow {a b c : ℕ} : PresentedGroup.of 1 ^ b = 1

The second generator in the two-generator presentation satisfies its power relation.

@[simp]

theorem TauCeti.TriangleGroup.twoGenerator_mul_pow {a b c : ℕ} : (PresentedGroup.of 1 * PresentedGroup.of 0) ^ c = 1

The product of the second and first generators in the two-generator presentation satisfies its power relation.

def TauCeti.TriangleGroup.equivTwoGenerator {a b c : ℕ} : TriangleGroup a b c ≃* PresentedGroup (twoGeneratorTriangleRelators a b c)

The isomorphism of Δ(a, b, c) with the two-generator presentation ⟨x, y | x ^ a, y ^ b, (y * x) ^ c⟩ obtained by eliminating z = (y * x)⁻¹.

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.equivTwoGenerator_x {a b c : ℕ} : equivTwoGenerator (x a b c) = PresentedGroup.of 0

@[simp]

theorem TauCeti.TriangleGroup.equivTwoGenerator_y {a b c : ℕ} : equivTwoGenerator (y a b c) = PresentedGroup.of 1

@[simp]

theorem TauCeti.TriangleGroup.equivTwoGenerator_z {a b c : ℕ} : equivTwoGenerator (z a b c) = (PresentedGroup.of 1 * PresentedGroup.of 0)⁻¹

@[simp]

theorem TauCeti.TriangleGroup.equivTwoGenerator_symm_of_zero {a b c : ℕ} : equivTwoGenerator.symm (PresentedGroup.of 0) = x a b c

@[simp]

theorem TauCeti.TriangleGroup.equivTwoGenerator_symm_of_one {a b c : ℕ} : equivTwoGenerator.symm (PresentedGroup.of 1) = y a b c

def TauCeti.TriangleGroup.equivFreeGroup : TriangleGroup 0 0 0 ≃* FreeGroup (Fin 2)

The triangle group Δ(0, 0, 0) is the free group on the two generators x and y: every power relator is trivial, and the product relator only determines z = (y * x)⁻¹.

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.equivFreeGroup_x : equivFreeGroup (x 0 0 0) = FreeGroup.of 0

@[simp]

theorem TauCeti.TriangleGroup.equivFreeGroup_y : equivFreeGroup (y 0 0 0) = FreeGroup.of 1

@[simp]

theorem TauCeti.TriangleGroup.equivFreeGroup_z : equivFreeGroup (z 0 0 0) = (FreeGroup.of 1 * FreeGroup.of 0)⁻¹

@[simp]

theorem TauCeti.TriangleGroup.equivFreeGroup_symm_of_zero : equivFreeGroup.symm (FreeGroup.of 0) = x 0 0 0

@[simp]

theorem TauCeti.TriangleGroup.equivFreeGroup_symm_of_one : equivFreeGroup.symm (FreeGroup.of 1) = y 0 0 0