Elliptic points and cusps of a group tiled by a doubled triangle

Let P be a convex hyperbolic triangle whose angles at the ends of side 0 are acute, and let Γ ≤ PSL(2, ℝ) contain the side-pairing maps of its double ConvexPolygon.doubleTriangleSidePairing, with locally finite translates of the double whose interiors are pairwise disjoint: the double is a locally finite fundamental polygon for Γ. This is how a hyperbolic triangle group, generated by the side-pairing maps, acts on its tessellation by triangles and their mirror images.

The vertex cycles of the double are {P 0}, {P 1} and {P 2, P 2'}, so they correspond to the vertices of P, and no side of the double is paired with itself. Hence the elliptic orbits of Γ are exactly the orbits of the finite vertices of P, and the cusp orbits of Γ are exactly the orbits of its ideal vertices, distinct vertices giving distinct orbits. At a vertex with angle π / m, the stabilizer has order m. In terms of a typed triple p, q, r of TriangleOrder parameters realised as the angles of P, the group has one elliptic orbit for each elliptic entry, of the stated order, and one cusp for each cusp entry. These are the elliptic orders and the cusp count in the orbifold signature of a triangle group.

Main declarations

• ConvexPolygon.doubleTriangleEllipticOrbitEquiv: the finite vertices of P are in bijection with the elliptic orbits of Γ, each vertex going to its orbit.
• ConvexPolygon.doubleTriangleCuspOrbitEquiv: the ideal vertices of P are in bijection with the cusp orbits of Γ, each vertex going to its orbit.
• ConvexPolygon.natCard_stabilizer_of_doubleTriangle: at a vertex of P with angle π / m, the stabilizer in Γ has order m.
• ConvexPolygon.natCard_ellipticOrbits_of_doubleTriangle and ConvexPolygon.natCard_cuspOrbit_of_doubleTriangle: the numbers of elliptic orbits and of cusps are the numbers of elliptic and of cusp entries of the typed triple.
• ConvexPolygon.natCard_stabilizer_of_doubleTriangle_of_eq_elliptic: at a vertex whose entry is elliptic of order m, the stabilizer has order m.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §10.6 (triangle groups and their fundamental polygons).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §4.3 (the signature of a Fuchsian group).

Elliptic points

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleEllipticOrbitEquiv {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • (P.doubleTriangle h₀ h₁).carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) : { i : Fin 3 // (P.vertex i).isLeft = true } ≃ ↑Γ.ellipticOrbits

The elliptic orbits of a group tiled by a doubled triangle. Let Γ contain the side-pairing maps of the double of P, with translates of the double covering ℍ and having pairwise disjoint interiors. Sending a finite vertex of P to its orbit identifies the finite vertices of P with the elliptic orbits of Γ.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.coe_doubleTriangleEllipticOrbitEquiv_apply {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • (P.doubleTriangle h₀ h₁).carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) (i : { i : Fin 3 // (P.vertex i).isLeft = true }) : ↑((doubleTriangleEllipticOrbitEquiv hmap hcover hdisj) i) = Quotient.mk'' ((P.vertex ↑i).getLeft ⋯)

The elliptic-orbit bijection sends a finite vertex of P to its orbit.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_stabilizer_of_doubleTriangle {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) {i : Fin 3} {z : UpperHalfPlane} (hz : P.vertex i = Sum.inl z) {m : ℕ} (hm : m ≠ 0) (hP : P.interiorAngle i = Real.pi / ↑m) : Nat.card ↥(MulAction.stabilizer (↥Γ) z) = m

The elliptic orders of a group tiled by a doubled triangle. At a finite vertex of P with angle π / m, the stabilizer in Γ has order m.

Cusps

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.doubleTriangleCuspOrbitEquiv {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • (P.doubleTriangle h₀ h₁).carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) : { i : Fin 3 // (P.vertex i).isRight = true } ≃ Γ.CuspOrbit

The cusps of a group tiled by a doubled triangle. Let Γ contain the side-pairing maps of the double of P, with locally finite translates of the double having pairwise disjoint interiors. Sending an ideal vertex of P to its orbit identifies the ideal vertices of P with the cusp orbits of Γ.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.coe_doubleTriangleCuspOrbitEquiv_apply {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • (P.doubleTriangle h₀ h₁).carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) (i : { i : Fin 3 // (P.vertex i).isRight = true }) : ↑((doubleTriangleCuspOrbitEquiv hmap hlf hdisj) i) = Quotient.mk'' ((P.vertex ↑i).getRight ⋯)

The cusp bijection sends an ideal vertex of P to its orbit.

Typed triangle parameters

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_ellipticOrbits_of_doubleTriangle {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • (P.doubleTriangle h₀ h₁).carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) : Nat.card ↑Γ.ellipticOrbits = {i : Fin (Nat.succ 0).succ.succ | ![p, q, r] i ≠ TriangleOrder.cusp}.card

The number of elliptic orbits of a triangle group. If P has angles given by the typed triple p, q, r, a group tiled by the double of P has one elliptic orbit for each elliptic entry of the triple.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_cuspOrbit_of_doubleTriangle {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • (P.doubleTriangle h₀ h₁).carrier) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) : Nat.card Γ.CuspOrbit = {i : Fin (Nat.succ 0).succ.succ | ![p, q, r] i = TriangleOrder.cusp}.card

The number of cusps of a triangle group. If P has angles given by the typed triple p, q, r, a group tiled by the double of P has one cusp orbit for each cusp entry of the triple.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.natCard_stabilizer_of_doubleTriangle_of_eq_elliptic {P : ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2} {h₁ : P.interiorAngle 1 < Real.pi / 2} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {p q r : TriangleOrder} (hp : P.interiorAngle 0 = p.angle) (hq : P.interiorAngle 1 = q.angle) (hr : P.interiorAngle 2 = r.angle) (hmap : ∀ (i : Fin 4), (P.doubleTriangleSidePairing h₀ h₁).map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior (P.doubleTriangle h₀ h₁).carrier) (interior (P.doubleTriangle h₀ h₁).carrier)) {i : Fin 3} {z : UpperHalfPlane} (hz : P.vertex i = Sum.inl z) {m : ℕ} {hm : 2 ≤ m} (hi : ![p, q, r] i = TriangleOrder.elliptic m hm) : Nat.card ↥(MulAction.stabilizer (↥Γ) z) = m

The elliptic orders of a triangle group. If P has angles given by the typed triple p, q, r, then at a vertex of P whose entry is elliptic of order m, the stabilizer in a group tiled by the double of P has order m.