Elliptic meridians and their lifts

For a finite point stabilizer of order m, choose its positive generator by requiring its rotation in the disc coordinate to be exp (2πi/m). A counterclockwise meridian in the local quotient coordinate u = w^m lifts from w to this generator applied to w, not its inverse. More generally, n signed turns end at the nth power of the positive generator.

The explicit lifts stay at constant hyperbolic distance from the fixed point. Consequently they stay in any invariant disc containing their starting point, and the quotient-chart formula applies throughout the path. These lifts are unique, including at the fixed point where they are constant. Reversing the meridian inverts its endpoint transformation. These conventions specify the elliptic peripheral elements used alongside cusp meridians in oriented quotient presentations. The comparison with finite vertex-cycle transformations of side-paired polygons is in TauCeti.Analysis.Complex.Fuchsian.Elliptic.Polygon.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 8.
• Svetlana Katok, Fuchsian Groups, §§2.4 and 4.3.
• Otto Forster, Lectures on Riemann Surfaces, §4 (the local power-map model).

noncomputable def Subgroup.ellipticMeridianLift (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) : Path τ (Γ.positiveStabilizerGenerator z ^ n • τ)

The lift of n signed turns about an elliptic orbit. Its disc coordinate rotates through 2πn/m, where m is the stabilizer order.

@[simp]

theorem Subgroup.discCoordinate_ellipticMeridianLift (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : z.discCoordinate ((Γ.ellipticMeridianLift z n τ) t) = z.discCoordinate τ * Complex.exp (↑(2 * Real.pi * ↑n * ↑t / ↑(Nat.card ↥(MulAction.stabilizer (↥Γ) z))) * Complex.I)

The lift in the disc coordinate is a constant-speed circular arc.

@[simp]

theorem Subgroup.dist_ellipticMeridianLift (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : dist ((Γ.ellipticMeridianLift z n τ) t) z = dist τ z

An elliptic meridian lift stays at constant distance from the fixed point.

theorem Subgroup.discCoordinate_ellipticMeridianLift_pow (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : z.discCoordinate ((Γ.ellipticMeridianLift z n τ) t) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z) = z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z) * Complex.exp (↑(2 * Real.pi * ↑n * ↑t) * Complex.I)

The local power-map projection of an elliptic lift is the circular loop with n signed turns. Positive turns are counterclockwise in the quotient coordinate.

noncomputable def Subgroup.ellipticMeridian (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) : Path (z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)) (z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z))

The meridian in the local quotient coordinate, defined as the power-map projection of its explicit lift. At the fixed point itself this degenerates to the constant zero path.

theorem Subgroup.ellipticMeridian_apply (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : (Γ.ellipticMeridian z n τ) t = z.discCoordinate ((Γ.ellipticMeridianLift z n τ) t) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

Evaluation of the local elliptic meridian as the projection of the lift.

@[simp]

theorem Subgroup.ellipticMeridian_eq_exp (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : (Γ.ellipticMeridian z n τ) t = z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z) * Complex.exp (↑(2 * Real.pi * ↑n * ↑t) * Complex.I)

Away from the fixed point, the elliptic meridian is the circular loop with n signed turns around zero. The formula also holds at the fixed point, where both sides vanish.

theorem Subgroup.stabilizerBallQuotientChart_ellipticMeridianLift (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {ε : ℝ} (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBall z ε).orbitRelQuotientMap) (n : ℤ) {τ : UpperHalfPlane} (hτ : dist τ z < ε) (t : ↑unitInterval) : ↑(stabilizerBallQuotientChart hε hopen) ⟦(Γ.ellipticMeridianLift z n τ) t⟧ = (Γ.ellipticMeridian z n τ) t

On any precisely invariant disc containing the basepoint, the local quotient chart reads the projected lift as the elliptic meridian for its entire duration.

theorem Subgroup.eq_ellipticMeridianLift_of_pow_eq (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (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 = ⇑(Γ.ellipticMeridianLift z n τ)

The explicit elliptic lift is the unique continuous lift of the local meridian with the specified starting point, including the constant lift at the fixed point.

theorem Subgroup.ellipticMeridian_lift_endpoint (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (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 = Γ.positiveStabilizerGenerator z ^ n • τ

A continuous lift of an elliptic meridian ends at the corresponding signed power of the positive stabilizer generator, including when the lift is constant at the fixed point.

theorem Subgroup.ellipticMeridianLift_neg_apply (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) (t : ↑unitInterval) : (Γ.ellipticMeridianLift z (-n) τ) t = Γ.positiveStabilizerGenerator z ^ (-n) • (Γ.ellipticMeridianLift z n τ).symm t

Negating the turns reverses the lifted path and translates it back by the inverse endpoint transformation.

@[simp]

theorem Subgroup.ellipticMeridian_neg (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (n : ℤ) (τ : UpperHalfPlane) : Γ.ellipticMeridian z (-n) τ = (Γ.ellipticMeridian z n τ).symm

Reversing the meridian negates its turns, hence inverts its endpoint generator.

@[simp]

theorem Subgroup.ellipticMeridian_zero (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] (τ : UpperHalfPlane) : Γ.ellipticMeridian z 0 τ = Path.refl (z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z))

The zero-turn elliptic meridian is constant.