Local charts at elliptic orbits

Let Γ ≤ PSL(2, ℝ) be a subgroup and z a point of the upper half-plane with finite stabilizer of order m. The orbit space of a small hyperbolic disc about z under that stabilizer maps to an open subset of the coarse orbit quotient Γ \ ℍ as soon as the disc is precisely invariant (Subgroup.eventually_isOpenEmbedding_stabilizerBallQuotientToQuotient). This file packages the local quotient coordinate on that open subset as a chart Subgroup.stabilizerBallQuotientChart, an open partial homeomorphism from Γ \ ℍ to ℂ sending the orbit of a point τ of the disc to discCoordinate z τ ^ m (Subgroup.stabilizerBallQuotientChart_mk). On the free locus m = 1 and the chart is the disc coordinate pushed forward along the orbit projection; at an elliptic point it is the cyclic quotient model u ↦ u ^ m.

Near a point τ whose orbit lies in the source of the chart at z, the chart composed with the orbit projection is discCoordinate z (g • ·) ^ m for a group element g moving τ into the disc, hence holomorphic. Consequently the transition map between the charts at z and z' is the descent through u ↦ u ^ m of a holomorphic function invariant under the m-th roots of unity, and descent preserves holomorphy (TauCeti.differentiableOn_descendPow). These are the local inputs that make the atlas of all such charts a holomorphic atlas on Γ \ ℍ.

The cyclic quotient model follows Farkas–Kra, Riemann Surfaces, Chapter IV §9, and Katok, Fuchsian Groups, §2.4.

Main declarations

• Subgroup.stabilizerBallQuotientChart: the chart at the orbit of z, with Subgroup.stabilizerBallQuotientChart_mk computing it on orbits, Subgroup.mem_stabilizerBallQuotientChart_source_iff describing its source, and Subgroup.stabilizerBallQuotientChart_symm_pow computing its inverse.
• Subgroup.exists_stabilizerBallQuotientChart_quotientMk_eventuallyEq and Subgroup.mdifferentiableAt_stabilizerBallQuotientChart_comp_quotientMk: the chart composed with the orbit projection is locally a power of a disc coordinate, hence holomorphic.
• Subgroup.differentiableOn_stabilizerBallQuotientChart_symm_trans: transition maps between two charts are holomorphic, being descents through u ↦ u ^ m of holomorphic pullbacks to the disc coordinate.

References

• Hershel Farkas and Irwin Kra, Riemann Surfaces, Graduate Texts in Mathematics 71, Springer, second edition, 1992, Chapter IV §9.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.4.

noncomputable def Subgroup.stabilizerBallQuotientChart {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) : OpenPartialHomeomorph (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) ℂ

The chart at the orbit of z. Its source is the image in Γ \ ℍ of the local orbit space of the hyperbolic disc of radius ε about z, assumed to embed openly, and its target is the Euclidean disc of radius tanh (ε / 2) ^ m, where m is the order of the stabilizer of z. It sends the orbit of a point τ of the disc to discCoordinate z τ ^ m (Subgroup.stabilizerBallQuotientChart_mk).

Equations

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

theorem Subgroup.stabilizerBallQuotientChart_source {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) : (stabilizerBallQuotientChart hε hopen).source = Set.range (Γ.stabilizerBallQuotientToQuotient z ε)

theorem Subgroup.stabilizerBallQuotientChart_target {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) : (stabilizerBallQuotientChart hε hopen).target = Metric.ball 0 (Real.tanh (ε / 2) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z))

@[simp]

theorem Subgroup.stabilizerBallQuotientChart_mk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {τ : UpperHalfPlane} (hτ : dist τ z < ε) : ↑(stabilizerBallQuotientChart hε hopen) ⟦τ⟧ = z.discCoordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

In the chart at the orbit of z, the orbit of a point τ of the hyperbolic disc has coordinate the m-th power of its disc coordinate, m the order of the stabilizer of z.

theorem Subgroup.mem_stabilizerBallQuotientChart_source_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {τ : UpperHalfPlane} : ⟦τ⟧ ∈ (stabilizerBallQuotientChart hε hopen).source ↔ ∃ (g : ↥Γ), dist (g • τ) z < ε

The orbit of τ lies in the source of the chart at the orbit of z exactly when some element of Γ moves τ into the hyperbolic disc of radius ε about z.

theorem Subgroup.stabilizerBallQuotientChart_symm_pow {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {w : ℂ} (hw : ‖w‖ < Real.tanh (ε / 2)) : ↑(stabilizerBallQuotientChart hε hopen).symm (w ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)) = ⟦z.discCoordinateHomeomorph.symm (Complex.UnitDisc.mk w ⋯)⟧

The inverse of the chart at the orbit of z sends the m-th power of a point w of the disc of radius tanh (ε / 2) to the orbit of the point with disc coordinate w.

theorem Subgroup.exists_stabilizerBallQuotientChart_quotientMk_eventuallyEq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {τ : UpperHalfPlane} (hτ : ⟦τ⟧ ∈ (stabilizerBallQuotientChart hε hopen).source) : ∃ (g : ↥Γ), (fun (σ : UpperHalfPlane) => ↑(stabilizerBallQuotientChart hε hopen) ⟦σ⟧) =ᶠ[nhds τ] fun (σ : UpperHalfPlane) => z.discCoordinate (g • σ) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

Near a point τ whose orbit lies in the source of the chart at the orbit of z, the chart composed with the orbit projection is discCoordinate z (g • ·) ^ m, where g ∈ Γ moves τ into the hyperbolic disc about z and m is the order of the stabilizer of z.

theorem Subgroup.mdifferentiableAt_stabilizerBallQuotientChart_comp_quotientMk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {τ : UpperHalfPlane} (hτ : ⟦τ⟧ ∈ (stabilizerBallQuotientChart hε hopen).source) : (MDiffAt fun (σ : UpperHalfPlane) => ↑(stabilizerBallQuotientChart hε hopen) ⟦σ⟧) τ

The chart at the orbit of z composed with the orbit projection is holomorphic at every point whose orbit lies in the source of the chart.

theorem Subgroup.differentiableAt_comp_stabilizerBallQuotientChart_symm_pow (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane → E} {w₀ : ℂ} (hw₀ : ‖w₀‖ < Real.tanh (ε / 2)) (hF : MDiffAt (F ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane)) (z.discCoordinateHomeomorph.symm (Complex.UnitDisc.mk w₀ ⋯))) : DifferentiableAt ℂ (fun (w : ℂ) => F (↑(stabilizerBallQuotientChart hε hopen).symm (w ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)))) w₀

Pulling back a function in a stabilizer-ball chart along the power map gives a holomorphic function wherever its pullback to the upper half-plane is holomorphic.

theorem Subgroup.differentiableOn_stabilizerBallQuotientChart_symm_trans {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {z' : UpperHalfPlane} {ε' : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z')] (hε' : 0 < ε') (hopen' : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z' ε')) : DifferentiableOn ℂ (↑((stabilizerBallQuotientChart hε hopen).symm.trans (stabilizerBallQuotientChart hε' hopen'))) ((stabilizerBallQuotientChart hε hopen).symm.trans (stabilizerBallQuotientChart hε' hopen')).source

The transition map between the charts at the orbits of z and z' is holomorphic on its domain: it is the descent through u ↦ u ^ m of its pullback to the disc coordinate at z.

@[simp]

theorem Subgroup.stabilizerBallQuotientChart_trans_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {ε' : ℝ} (hε' : 0 < ε') (hopen' : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε')) {u : ℂ} (hu : u ∈ (stabilizerBallQuotientChart hε hopen).target ∧ ↑(stabilizerBallQuotientChart hε hopen).symm u ∈ (stabilizerBallQuotientChart hε' hopen').source) : ↑(stabilizerBallQuotientChart hε' hopen') (↑(stabilizerBallQuotientChart hε hopen).symm u) = u

The elliptic chart at the orbit of z does not depend on the invariant disc. The charts at the orbit of z built from the invariant discs of radii ε and ε', both positive, agree at every point of the domain of the transition between them, that is at every point u of the target of the first chart whose inverse image belongs to the source of the second, so the two charts define the same local complex structure on the coarse quotient. Being the characteristic computation rule for that independence, it is recorded as a simp lemma.