Regular triples and normal subgroups of triangle groups

A permutation triple t of degree n whose components have orders dividing a, b, c is a permutation representation TauCeti.TriangleGroup.toPerm t : Δ(a, b, c) →* Equiv.Perm (Fin n). The preimage of the stabilizer of a sheet i is the point stabilizer of this action.

This file proves the normality criterion: for a connected triple, the point stabilizer is a normal subgroup of Δ(a, b, c) exactly when the triple is regular. In that case the point stabilizer is the kernel of the representation, a normal subgroup whose index is the degree n, the order of the monodromy group.

Conversely the action of Δ(a, b, c) on the cosets of a normal subgroup N of index n is a regular triple, the coset triple of N, and a regular triple is the coset triple of its kernel. So regular triples up to relabeling are the same thing as finite-index normal subgroups of the triangle group, the quotient by the subgroup being the monodromy group of the triple (the image of the representation, TauCeti.TriangleGroup.range_toPerm).

Main definitions

• TauCeti.TriangleGroup.regularIsoClasses: the isomorphism classes of regular triples of degree n with component orders dividing a, b, c.
• TauCeti.TriangleGroup.regularIsoClassEquiv: for n ≠ 0, the bijection between these classes and the normal subgroups of index n of Δ(a, b, c).
• TauCeti.TriangleGroup.automorphismGroupMulEquivQuotientKer: the automorphism group of a regular triple is the opposite of the triangle group modulo the kernel of its representation.

Main results

• TauCeti.TriangleGroup.normal_comap_stabilizer_toPerm_iff: for a connected triple, the point stabilizer of its representation is normal exactly when the triple is regular.
• TauCeti.TriangleGroup.comap_stabilizer_toPerm_eq_ker: when a sheet has trivial monodromy stabilizer (e.g. for a regular triple), its point stabilizer is the kernel of the representation.
• TauCeti.TriangleGroup.index_ker_toPerm: the kernel of the representation has index the order of the monodromy group, and TauCeti.TriangleGroup.index_ker_toPerm_of_isRegular: for a regular triple this is the degree.
• TauCeti.TriangleGroup.isRegular_cosetTriple_iff: the coset triple of a subgroup is regular exactly when the subgroup is normal, and TauCeti.TriangleGroup.ker_toPerm_cosetTriple_of_normal: the kernel of its representation is then the subgroup itself.
• TauCeti.TriangleGroup.equivalent_cosetTriple_ker_toPerm: a regular triple is isomorphic to the coset triple of its kernel.
• TauCeti.TriangleGroup.coe_regularIsoClassEquiv_mk and TauCeti.TriangleGroup.coe_regularIsoClassEquiv_symm_apply: the two directions of TauCeti.TriangleGroup.regularIsoClassEquiv.
• TauCeti.TriangleGroup.kerLift_automorphismGroupMulEquivQuotientKer_apply: the coset that TauCeti.TriangleGroup.automorphismGroupMulEquivQuotientKer assigns to an automorphism τ moves the sheet 0 to τ 0.

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.64 and Proposition 2.66.
• G. A. Jones, D. Singerman, Belyi functions, hypermaps and Galois groups, Bull. London Math. Soc. 28 (1996), 561–590.

theorem TauCeti.TriangleGroup.comap_stabilizer_toPerm_eq_ker {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (i : Fin n) (hi : MulAction.stabilizer (↥t.monodromyGroup) i = ⊥) : Subgroup.comap (toPerm t ha hb hc) (MulAction.stabilizer (Equiv.Perm (Fin n)) i) = (toPerm t ha hb hc).ker

If a sheet has trivial monodromy stabilizer, its point stabilizer under the representation of the triangle group is the kernel of the representation.

theorem TauCeti.TriangleGroup.normal_comap_stabilizer_toPerm_iff {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ht : t.IsConnected) (i : Fin n) : (Subgroup.comap (toPerm t ha hb hc) (MulAction.stabilizer (Equiv.Perm (Fin n)) i)).Normal ↔ t.IsRegular

The normality criterion. For a connected triple, the point stabilizer of a sheet under the representation of the triangle group is a normal subgroup exactly when the triple is regular.

theorem TauCeti.TriangleGroup.index_ker_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).ker.index = Nat.card ↥t.monodromyGroup

The kernel of the representation of a triple has index the order of its monodromy group, the image of the representation.

theorem TauCeti.TriangleGroup.index_ker_toPerm_of_isRegular {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ht : t.IsRegular) : (toPerm t ha hb hc).ker.index = n

The kernel of the representation of a regular triple has index the degree.

Regular triples and normal subgroups of finite index

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

The components of a coset triple have orders dividing a, b, c.

@[simp]

theorem TauCeti.TriangleGroup.isRegular_cosetTriple_iff {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) : (cosetTriple H e).IsRegular ↔ H.Normal

The coset triple of a subgroup is regular exactly when the subgroup is normal.

theorem TauCeti.TriangleGroup.ker_toPerm_cosetTriple_of_normal {a b c n : ℕ} (H : Subgroup (TriangleGroup a b c)) (e : TriangleGroup a b c ⧸ H ≃ Fin n) [H.Normal] {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

The kernel of the representation of the coset triple of a normal subgroup is that subgroup.

theorem TauCeti.TriangleGroup.equivalent_cosetTriple_ker_toPerm {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ht : t.IsRegular) (e : TriangleGroup a b c ⧸ (toPerm t ha hb hc).ker ≃ Fin n) : (cosetTriple (toPerm t ha hb hc).ker e).Equivalent t

A regular triple is the coset triple of its kernel: the action of Δ(a, b, c) on the sheets of a regular triple is its action on the cosets of the kernel of the representation.

def TauCeti.TriangleGroup.regularIsoClasses (a b c n : ℕ) : Set (PermutationTriple.IsoClass n)

The isomorphism classes of regular triples of degree n whose component orders divide a, b and c.

Equations

• TauCeti.TriangleGroup.regularIsoClasses a b c n = TauCeti.PermutationTriple.IsoClass.mk '' {t : TauCeti.PermutationTriple n | t.IsRegular ∧ t.HasDividingOrders a b c}

@[simp]

theorem TauCeti.TriangleGroup.mk_mem_regularIsoClasses_iff {a b c n : ℕ} {t : PermutationTriple n} : PermutationTriple.IsoClass.mk t ∈ regularIsoClasses a b c n ↔ t.IsRegular ∧ t.HasDividingOrders a b c

The class of a triple is in regularIsoClasses a b c n exactly when the triple is regular with component orders dividing a, b, c.

noncomputable def TauCeti.TriangleGroup.regularIsoClassEquiv {a b c n : ℕ} [NeZero n] : ↑(regularIsoClasses a b c n) ≃ { N : Subgroup (TriangleGroup a b c) // N.Normal ∧ N.index = n }

Regular triples are finite-index normal subgroups of the triangle group. For n ≠ 0, the isomorphism classes of regular triples of degree n with component orders dividing a, b, c correspond to the normal subgroups of index n of Δ(a, b, c). A class goes to the kernel of the representation of any of its triples (TauCeti.TriangleGroup.coe_regularIsoClassEquiv_mk), and a normal subgroup N to the class of the coset triple of N, the action of Δ(a, b, c) on Δ(a, b, c) ⧸ N (TauCeti.TriangleGroup.coe_regularIsoClassEquiv_symm_apply).

Equations

• TauCeti.TriangleGroup.regularIsoClassEquiv = (Equiv.ofBijective TauCeti.TriangleGroup.cosetRegularIsoClass✝ ⋯).symm

theorem TauCeti.TriangleGroup.coe_regularIsoClassEquiv_symm_apply {a b c n : ℕ} [NeZero n] (N : { N : Subgroup (TriangleGroup a b c) // N.Normal ∧ N.index = n }) (e : TriangleGroup a b c ⧸ ↑N ≃ Fin n) : ↑(regularIsoClassEquiv.symm N) = PermutationTriple.IsoClass.mk (cosetTriple (↑N) e)

The class of a normal subgroup N of index n is the class of its coset triple, for any numbering e of the cosets.

@[simp]

theorem TauCeti.TriangleGroup.coe_regularIsoClassEquiv_mk {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) [NeZero n] (h : PermutationTriple.IsoClass.mk t ∈ regularIsoClasses a b c n) : ↑(regularIsoClassEquiv ⟨PermutationTriple.IsoClass.mk t, h⟩) = (toPerm t ha hb hc).ker

The normal subgroup of the class of a regular triple t is the kernel of the representation of t.

noncomputable def TauCeti.TriangleGroup.automorphismGroupMulEquivQuotientKer {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ht : t.IsRegular) : ↥t.automorphismGroup ≃* (TriangleGroup a b c ⧸ (toPerm t ha hb hc).ker)ᵐᵒᵖ

The automorphism group of a regular triple is the opposite of the triangle group modulo the kernel of its representation. This kernel is the normal subgroup selected by TauCeti.TriangleGroup.regularIsoClassEquiv, by TauCeti.TriangleGroup.coe_regularIsoClassEquiv_mk. The opposite occurs because automorphisms act on the right of the regular monodromy action. An automorphism τ goes to the coset of the elements moving the sheet 0 to τ 0 (TauCeti.TriangleGroup.kerLift_automorphismGroupMulEquivQuotientKer_apply).

Equations

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

@[simp]

theorem TauCeti.TriangleGroup.kerLift_automorphismGroupMulEquivQuotientKer_apply {a b c n : ℕ} (t : PermutationTriple n) (ha : t.σ0 ^ a = 1) (hb : t.σ1 ^ b = 1) (hc : t.σinf ^ c = 1) (ht : t.IsRegular) (τ : ↥t.automorphismGroup) : ((QuotientGroup.kerLift (toPerm t ha hb hc)) (MulOpposite.unop ((automorphismGroupMulEquivQuotientKer t ha hb hc ht) τ))) ⟨0, ⋯⟩ = ↑τ ⟨0, ⋯⟩

The characteristic property of TauCeti.TriangleGroup.automorphismGroupMulEquivQuotientKer: the coset that an automorphism τ goes to moves the sheet 0 to τ 0.