Permutation triples as permutation representations of triangle groups

A permutation triple t of degree n whose components satisfy t.σ0 ^ a = 1, t.σ1 ^ b = 1 and t.σinf ^ c = 1 is the same thing as a homomorphism Δ(a, b, c) →* Equiv.Perm (Fin n): the product relation σinf * σ1 * σ0 = 1 of the triple is the product relator z * y * x of the triangle group, so the universal property TauCeti.TriangleGroup.lift sends x, y, z to σ0, σ1, σinf. This file records that dictionary.

• TauCeti.TriangleGroup.toPerm: the permutation representation of Δ(a, b, c) attached to a triple whose component orders divide a, b, c. Its range is the monodromy group of the triple (TauCeti.TriangleGroup.range_toPerm), so the triple is connected exactly when the representation is transitive on a nonempty set of sheets (TauCeti.TriangleGroup.isConnected_iff_isPretransitive_range_toPerm).
• TauCeti.TriangleGroup.permutationTripleEquiv: every permutation representation of Δ(a, b, c) on Fin n arises in this way from exactly one such triple.
• Relabeling the sheets of a triple conjugates its representation (TauCeti.TriangleGroup.toPerm_smul), and two representations give isomorphic triples exactly when they are conjugate (TauCeti.TriangleGroup.equivalent_permutationTripleEquiv_iff). Together with the connectedness criterion, isomorphism classes of connected triples with component orders dividing (a, b, c) therefore correspond to conjugacy classes of transitive permutation representations of Δ(a, b, c) of degree n ≠ 0.
• TauCeti.TriangleGroup.isConnected_permutationTripleEquiv_toPermHom_iff: the same criterion phrased for an action of Δ(a, b, c) on Fin n: the triple of the action is connected exactly when the action is pretransitive and n ≠ 0.
• TauCeti.TriangleGroup.cosetTriple: the triple of the action of Δ(a, b, c) on the cosets of a subgroup H, read through an enumeration of the cosets. It is connected, its sheet e 1 has point stabiliser H (TauCeti.TriangleGroup.comap_stabilizer_toPerm_cosetTriple), its isomorphism class does not depend on the enumeration (TauCeti.TriangleGroup.equivalent_cosetTriple), and every connected triple is isomorphic to the coset triple of any of its point stabilisers (TauCeti.TriangleGroup.equivalent_cosetTriple_of_comap_stabilizer_eq).

References

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

The representation of a triple

def TauCeti.TriangleGroup.toPerm {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : TriangleGroup a b c →* Equiv.Perm (Fin n)

The permutation representation of Δ(a, b, c) on the sheets of a permutation triple whose components have orders dividing a, b, c: it sends x, y, z to σ0, σ1, σinf.

Equations

• TauCeti.TriangleGroup.toPerm t ha hb hc = TauCeti.TriangleGroup.lift t.σ0 t.σ1 t.σinf ha hb hc ⋯

@[simp]

theorem TauCeti.TriangleGroup.toPerm_x {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : (toPerm t ha hb hc) (x a b c) = t.σ0

@[simp]

theorem TauCeti.TriangleGroup.toPerm_y {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : (toPerm t ha hb hc) (y a b c) = t.σ1

@[simp]

theorem TauCeti.TriangleGroup.toPerm_z {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : (toPerm t ha hb hc) (z a b c) = t.σinf

@[simp]

theorem TauCeti.TriangleGroup.range_toPerm {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : (toPerm t ha hb hc).range = t.monodromyGroup

The image of the permutation representation of a triple is its monodromy group.

theorem TauCeti.TriangleGroup.isConnected_iff_isPretransitive_range_toPerm {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : t.IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥(toPerm t ha hb hc).range) (Fin n)

A triple is connected exactly when it has a sheet and its permutation representation of the triangle group is transitive on the sheets.

theorem TauCeti.TriangleGroup.toPerm_smul {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (τ : Equiv.Perm (Fin n)) : toPerm (τ • t) ⋯ ⋯ ⋯ = (MulEquiv.toMonoidHom (MulAut.conj τ)).comp (toPerm t ha hb hc)

Relabeling the sheets of a triple by τ conjugates its permutation representation by τ.

Every representation comes from a triple

def TauCeti.TriangleGroup.permutationTripleEquiv {a b c n : ℕ} : (TriangleGroup a b c →* Equiv.Perm (Fin n)) ≃ { t : PermutationTriple n // t.σ0 ^ a = 1 ∧ t.σ1 ^ b = 1 ∧ t.σinf ^ c = 1 }

Permutation representations of Δ(a, b, c) on Fin n correspond to permutation triples of degree n whose components have orders dividing a, b, c: a representation ρ gives the triple (ρ x, ρ y, ρ z), and the inverse is TauCeti.TriangleGroup.toPerm.

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_apply_σ0 {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).σ0 = ρ (x a b c)

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_apply_σ1 {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).σ1 = ρ (y a b c)

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_apply_σinf {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).σinf = ρ (z a b c)

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_symm_apply {a b c n : ℕ} (t : { t : PermutationTriple n // t.σ0 ^ a = 1 ∧ t.σ1 ^ b = 1 ∧ t.σinf ^ c = 1 }) : permutationTripleEquiv.symm t = toPerm ↑t ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TriangleGroup.toPerm_permutationTripleEquiv {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) {ha : (↑(permutationTripleEquiv ρ)).σ0 ^ a = 1} {hb : (↑(permutationTripleEquiv ρ)).σ1 ^ b = 1} {hc : (↑(permutationTripleEquiv ρ)).σinf ^ c = 1} : toPerm (↑(permutationTripleEquiv ρ)) ha hb hc = ρ

The permutation representation of the triple of ρ is ρ itself.

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_toPerm {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) : ↑(permutationTripleEquiv (toPerm t ha hb hc)) = t

The triple of the representation of t is t itself.

@[simp]

theorem TauCeti.TriangleGroup.monodromyGroup_permutationTripleEquiv {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).monodromyGroup = ρ.range

The monodromy group of the triple of a representation is the image of the representation.

theorem TauCeti.TriangleGroup.isConnected_permutationTripleEquiv_iff {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥ρ.range) (Fin n)

The triple of a representation is connected exactly when the representation is transitive on a nonempty set of sheets.

@[simp]

theorem TauCeti.TriangleGroup.permutationTripleEquiv_conj {a b c n : ℕ} (ρ : TriangleGroup a b c →* Equiv.Perm (Fin n)) (τ : Equiv.Perm (Fin n)) : ↑(permutationTripleEquiv ((↑(MulAut.conj τ)).comp ρ)) = τ • ↑(permutationTripleEquiv ρ)

Conjugating a representation by τ relabels the sheets of its triple by τ.

theorem TauCeti.TriangleGroup.equivalent_permutationTripleEquiv_iff {a b c n : ℕ} (ρ ρ' : TriangleGroup a b c →* Equiv.Perm (Fin n)) : (↑(permutationTripleEquiv ρ)).Equivalent ↑(permutationTripleEquiv ρ') ↔ ∃ (τ : Equiv.Perm (Fin n)), (↑(MulAut.conj τ)).comp ρ = ρ'

Classification up to relabeling. Two permutation representations of Δ(a, b, c) give isomorphic triples exactly when they are conjugate by a permutation of the sheets.

Actions of the triangle group

theorem TauCeti.TriangleGroup.isConnected_permutationTripleEquiv_toPermHom_iff {a b c n : ℕ} [MulAction (TriangleGroup a b c) (Fin n)] : (↑(permutationTripleEquiv (MulAction.toPermHom (TriangleGroup a b c) (Fin n)))).IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (TriangleGroup a b c) (Fin n)

An action of Δ(a, b, c) on the n sheets gives a connected triple exactly when the action is pretransitive and there is at least one sheet.

The action on the cosets of a subgroup

theorem TauCeti.TriangleGroup.ker_toPerm_eq_of_equivalent {a b c n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ha' : t'.σ0 ^ a = 1) (hb' : t'.σ1 ^ b = 1) (hc' : t'.σinf ^ c = 1) : (toPerm t ha hb hc).ker = (toPerm t' ha' hb' hc').ker

Relabeling one triple into another does not change the kernel of its representation.

noncomputable def TauCeti.TriangleGroup.cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : PermutationTriple n

The permutation triple of the action of Δ(a, b, c) on the cosets of a subgroup H, the cosets being numbered by e: its components are the permutations of the cosets by x, y and z.

Equations

• TauCeti.TriangleGroup.cosetTriple H e = ↑(TauCeti.TriangleGroup.permutationTripleEquiv e.permutationRepresentation)

@[simp]

theorem TauCeti.TriangleGroup.cosetTriple_σ0 {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σ0 = e.permutationRepresentation (x a b c)

@[simp]

theorem TauCeti.TriangleGroup.cosetTriple_σ1 {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σ1 = e.permutationRepresentation (y a b c)

@[simp]

theorem TauCeti.TriangleGroup.cosetTriple_σinf {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σinf = e.permutationRepresentation (z a b c)

theorem TauCeti.TriangleGroup.cosetTriple_σ0_pow {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σ0 ^ a = 1

theorem TauCeti.TriangleGroup.cosetTriple_σ1_pow {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σ1 ^ b = 1

theorem TauCeti.TriangleGroup.cosetTriple_σinf_pow {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).σinf ^ c = 1

@[simp]

theorem TauCeti.TriangleGroup.toPerm_cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) {ha : (cosetTriple H e).σ0 ^ a = 1} {hb : (cosetTriple H e).σ1 ^ b = 1} {hc : (cosetTriple H e).σinf ^ c = 1} : toPerm (cosetTriple H e) ha hb hc = e.permutationRepresentation

The representation of a coset triple is the action on the cosets.

theorem TauCeti.TriangleGroup.isConnected_cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).IsConnected

A coset triple is connected: Δ(a, b, c) acts transitively on the nonempty set of cosets.

theorem TauCeti.TriangleGroup.comap_stabilizer_toPerm_cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) {ha : (cosetTriple H e).σ0 ^ a = 1} {hb : (cosetTriple H e).σ1 ^ b = 1} {hc : (cosetTriple H e).σinf ^ c = 1} : Subgroup.comap (toPerm (cosetTriple H e) ha hb hc) (MulAction.stabilizer (Equiv.Perm (Fin n)) (e ↑1)) = H

The sheet e 1 of the coset triple of H has point stabiliser H.

theorem TauCeti.TriangleGroup.ker_toPerm_cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) {ha : (cosetTriple H e).σ0 ^ a = 1} {hb : (cosetTriple H e).σ1 ^ b = 1} {hc : (cosetTriple H e).σinf ^ c = 1} : (toPerm (cosetTriple H e) ha hb hc).ker = H.normalCore

The kernel of the representation of the coset triple of H is the normal core of H.

theorem TauCeti.TriangleGroup.equivalent_cosetTriple {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e e' : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).Equivalent (cosetTriple H e')

The isomorphism class of a coset triple does not depend on the numbering of the cosets.

theorem TauCeti.TriangleGroup.equivalent_cosetTriple_of_comap_stabilizer_eq {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) {t : PermutationTriple n} (ht : t.IsConnected) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (i : Fin n) (hH : Subgroup.comap (toPerm t ha hb hc) (MulAction.stabilizer (Equiv.Perm (Fin n)) i) = H) : (cosetTriple H e).Equivalent t

Every connected triple is a coset triple. If H is the stabiliser of a sheet i of a connected triple t under its representation, then t is isomorphic to the coset triple of H, however its cosets are numbered.