Elliptic points on the sides of a fundamental polygon

For a side-paired convex hyperbolic polygon with disjoint translated interiors, an interior point has trivial stabilizer. At a side point other than its finite endpoints, only the two adjacent tiles can occur. Its stabilizer is therefore trivial unless the side is self-paired and the pairing map fixes that point; in that case it is cyclic of order two.

If the translates cover the upper half-plane, every elliptic orbit has a representative at a finite vertex or at such a fixed point of a self-paired side. This supplies the side-point case needed in addition to vertex cycles when extracting elliptic orbits from a fundamental polygon. No claim that all elliptic points are represented by vertices is made.

References

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

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.eq_one_or_eq_map_pair_of_smul_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map (σ.pair i) ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) {z w : UpperHalfPlane} (hz : z ∈ P.carrier) (hw : w ∈ P.side i) (hwp : P.vertex i ≠ Sum.inl w) (hwq : P.vertex (i + 1) ≠ Sum.inl w) (hgz : g • z = w) : g = 1 ∨ g = σ.map (σ.pair i)

A transformation carrying a point of the polygon to a nonendpoint point of side i is one of the two adjacent tile transformations: the identity or the map of the paired side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pair_eq_self_of_map_smul_eq_self {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {i : Fin n} {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) (hfix : σ.map i • z = z) : σ.pair i = i

If a side-pairing map fixes a nonendpoint point of its side, that side is self-paired.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.smul_eq_self_iff_of_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) : g • z = z ↔ g = 1 ∨ g = σ.map i ∧ σ.map i • z = z

At a nonendpoint side point, an element of the acting group fixes the point exactly when it is the identity or the side-pairing map fixing that point.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orderOf_map_of_pair_eq_self {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {i : Fin n} (hi : σ.pair i = i) : orderOf (σ.map i) = 2

A self-paired side has a nonidentity pairing map of order two.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.existsUnique_mem_side_map_smul_eq_self_of_pair_eq_self {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {i : Fin n} (hi : σ.pair i = i) : ∃! z : UpperHalfPlane, z ∈ P.side i ∧ P.vertex i ≠ Sum.inl z ∧ P.vertex (i + 1) ≠ Sum.inl z ∧ σ.map i • z = z

Every self-paired side has exactly one fixed point of its pairing map. It lies on the side away from the finite endpoints. This includes sides with two ideal endpoints.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.selfPairedSideFixedPoint {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : { i : Fin n // σ.pair i = i }) : UpperHalfPlane

The unique fixed point of the involution pairing a side with itself. It is an interior point of that side even when both endpoints are ideal.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.selfPairedSideFixedPoint_spec {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : { i : Fin n // σ.pair i = i }) : σ.selfPairedSideFixedPoint i ∈ P.side ↑i ∧ P.vertex ↑i ≠ Sum.inl (σ.selfPairedSideFixedPoint i) ∧ P.vertex (↑i + 1) ≠ Sum.inl (σ.selfPairedSideFixedPoint i) ∧ σ.map ↑i • σ.selfPairedSideFixedPoint i = σ.selfPairedSideFixedPoint i

The fixed point of a self-paired side lies on the side, avoids its endpoints, and is fixed by the pairing map.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_smul_selfPairedSideFixedPoint {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : { i : Fin n // σ.pair i = i }) : σ.map ↑i • σ.selfPairedSideFixedPoint i = σ.selfPairedSideFixedPoint i

The self-pairing involution fixes its distinguished side point.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.selfPairedSideFixedPoint_eq {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : { i : Fin n // σ.pair i = i }) {z : UpperHalfPlane} (hfix : σ.map ↑i • z = z) : σ.selfPairedSideFixedPoint i = z

Any fixed point of a self-pairing map is its distinguished side fixed point.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.stabilizer_eq_bot_iff_of_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) : MulAction.stabilizer (↥Γ) z = ⊥ ↔ σ.map i • z ≠ z

The stabilizer of a nonendpoint side point is trivial exactly when the side-pairing map does not fix it.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_stabilizer_eq_zpowers_map_of_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) (hfix : σ.map i • z = z) : Subgroup.map Γ.subtype (MulAction.stabilizer (↥Γ) z) = Subgroup.zpowers (σ.map i)

The nontrivial stabilizer of a nonendpoint side point, viewed in PSL(2, ℝ), is generated by its side-pairing involution.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_stabilizer_eq_two_of_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) (hfix : σ.map i • z = z) : Nat.card ↥(MulAction.stabilizer (↥Γ) z) = 2

A nonendpoint side point fixed by its side-pairing map has stabilizer order two.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_orbit_iff_eq_of_mem_side_map_smul_eq_self {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) {i : Fin n} (hmap : σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z w : UpperHalfPlane} (hz : z ∈ P.carrier) (hw : w ∈ P.side i) (hwp : P.vertex i ≠ Sum.inl w) (hwq : P.vertex (i + 1) ≠ Sum.inl w) (hfix : σ.map i • w = w) : w ∈ MulAction.orbit (↥Γ) z ↔ z = w

A nonendpoint fixed point of a self-paired side is the only point of the polygon in its group orbit. Thus it cannot be identified with a vertex or a fixed point of another side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_vertex_or_self_paired_side_of_stabilizer_ne_bot {n : ℕ} [NeZero n] {P : ConvexPolygon n} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (σ : P.SidePairing) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hcover : ⋃ (γ : ↥Γ), ↑γ • P.carrier = Set.univ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {z : UpperHalfPlane} (hz : MulAction.stabilizer (↥Γ) z ≠ ⊥) : ∃ w ∈ MulAction.orbit (↥Γ) z, (∃ (i : Fin n), P.vertex i = Sum.inl w) ∨ ∃ (i : Fin n), w ∈ P.side i ∧ P.vertex i ≠ Sum.inl w ∧ P.vertex (i + 1) ≠ Sum.inl w ∧ σ.pair i = i ∧ σ.map i • w = w ∧ Nat.card ↥(MulAction.stabilizer (↥Γ) w) = 2

In a fundamental polygon whose translates cover the upper half-plane, every point with nontrivial stabilizer is represented either by a finite vertex or by a nonendpoint fixed point of a self-paired side. In the latter case its representative has stabilizer order two.