Elliptic orbits extracted from a fundamental polygon

For a side-paired convex polygon whose translates cover the upper half-plane and have disjoint interiors, the elliptic orbits are exactly the nontrivial finite vertex cycles together with one orbit for each self-paired side. The latter orbits have order two and are distinct from all vertex orbits. Finite vertex cycles of order one are excluded.

The classification is an equivalence with the actual elliptic-orbit subtype of the coarse quotient. Its characteristic equations recover the orbit representatives and their stabilizer orders, so it supplies both the number and the orders of the elliptic points in an orbifold signature. Discreteness and compactness are not additional hypotheses.

The finite vertex-cycle transformation is also identified with the positive stabilizer generator. Thus a positive meridian lifts to that cycle transformation, with no inversion.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chapters 3–4.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.quotientMk_vertex_ne_selfPairedSideFixedPoint {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (i : { i : Fin n // σ.pair i = i }) : Quotient.mk'' z ≠ Quotient.mk'' (σ.selfPairedSideFixedPoint i)

The fixed point of a self-paired side is not equivalent to a finite vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.injective_quotientMk_selfPairedSideFixedPoint {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Function.Injective fun (i : { i : Fin n // σ.pair i = i }) => Quotient.mk'' (σ.selfPairedSideFixedPoint i)

The fixed points of distinct self-paired sides are not equivalent.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ellipticOrbitEquiv {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : σ.EllipticVertexCycle ⊕ { i : Fin n // σ.pair i = i } ≃ ↑Γ.ellipticOrbits

The elliptic orbits of a fundamental polygon are precisely its nontrivial finite vertex cycles and its self-paired sides. A self-paired side contributes its unique interior fixed point.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ellipticOrbitEquiv_apply_inl_mk {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (j : { i : Fin n // (P.vertex i).isLeft = true ∧ σ.cycleMap i ≠ 1 }) : ↑((σ.ellipticOrbitEquiv hmap hcover hdisj) (Sum.inl (Quotient.mk'' j))) = Quotient.mk'' ((P.vertex ↑j).getLeft ⋯)

The vertex summand is sent to the actual orbit of the finite vertex.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ellipticOrbitEquiv_apply_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (i : { i : Fin n // σ.pair i = i }) : ↑((σ.ellipticOrbitEquiv hmap hcover hdisj) (Sum.inr i)) = Quotient.mk'' (σ.selfPairedSideFixedPoint i)

The side summand is sent to the actual orbit of its unique fixed point.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cardStabilizerOnOrbit_ellipticOrbitEquiv_inl_mk {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (j : { i : Fin n // (P.vertex i).isLeft = true ∧ σ.cycleMap i ≠ 1 }) : cardStabilizerOnOrbit ↑((σ.ellipticOrbitEquiv hmap hcover hdisj) (Sum.inl (Quotient.mk'' j))) = orderOf (σ.cycleMap ↑j)

The stabilizer order on the vertex summand is the order of its cycle transformation.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cardStabilizerOnOrbit_ellipticOrbitEquiv_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (i : { i : Fin n // σ.pair i = i }) : cardStabilizerOnOrbit ↑((σ.ellipticOrbitEquiv hmap hcover hdisj) (Sum.inr i)) = 2

Every side summand has elliptic stabilizer order two.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_ellipticOrbits {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Nat.card ↑Γ.ellipticOrbits = Nat.card σ.EllipticVertexCycle + Nat.card { i : Fin n // σ.pair i = i }

The number of elliptic orbits is the number of nontrivial finite vertex cycles plus the number of self-paired sides. Neither cusp compactness nor discreteness is needed.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.ellipticMeridian_lift_endpoint_eq_cycleMap_zpow_smul {N : ℕ} [NeZero N] {P : ConvexPolygon N} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j : Fin N} {z : UpperHalfPlane} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hz : P.vertex j = Sum.inl z) (hmap : ∀ (i : Fin N), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (n : ℤ) {τ : UpperHalfPlane} {f : ↑unitInterval → UpperHalfPlane} (hf : Continuous f) (h₀ : f 0 = τ) (hq : ∀ (t : ↑unitInterval), z.discCoordinate (f t) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z) = (Γ.ellipticMeridian z n τ) t) : f 1 = σ.cycleMap j ^ n • τ

A positive meridian in the finite vertex quotient lifts to the polygon's cycle transformation. Signed multiple turns give the corresponding signed power of that cycle, including for the constant lift at the fixed point.