Meromorphic functions on the compactified quotient of a Fuchsian group

Let Γ ≤ PSL(2, ℝ) be discrete, and let F be a function on the compactified quotient Subgroup.CompactifiedQuotient Γ, whose pullback to the upper half-plane is f z = F (ofQuotient ⟦z⟧). This file decides when F is meromorphic, and computes its orders, in terms of f alone, at both kinds of points of the compactified quotient.

At the orbit of z ∈ ℍ the compactified quotient is the coarse quotient Γ \ ℍ, so meromorphic descent applies: F is meromorphic at the orbit of z exactly when f is meromorphic at z, and ord_z f = m * ord_[z] F for the order m of the stabilizer of z.

At an adjoined cusp, read in the q-coordinate chart of any normalized cusp datum D representing it, F is the cusp extension TauCeti.Subgroup.CuspDatum.cuspExtension D f on a punctured disc around q = 0 (Subgroup.CompactifiedQuotient.comp_cuspChart_symm_eventuallyEq). Hence F is meromorphic at the cusp exactly when the cusp extension is meromorphic at 0, with the same order. The q-expansion criteria for invariant functions holomorphic sufficiently high turn exponential growth of rate 2πk / w in the scaling coordinate into meromorphy at the cusp with a pole of order at most k, and exponential decay of rate 2πn / w into a zero of order at least n.

Main declarations

• Subgroup.CompactifiedQuotient.meromorphicAt_ofQuotient_mk_iff and Subgroup.CompactifiedQuotient.meromorphicOrderAt_comp_ofQuotient_mk: meromorphy and the order formula at the orbit of a point of the upper half-plane.
• Subgroup.CompactifiedQuotient.meromorphicAt_ofCusp_iff and Subgroup.CompactifiedQuotient.meromorphicOrderAt_ofCusp: meromorphy and order at a cusp, in the q-coordinate of any cusp datum representing it.
• Subgroup.CompactifiedQuotient.neg_le_meromorphicOrderAt_ofCusp and Subgroup.CompactifiedQuotient.natCast_le_meromorphicOrderAt_ofCusp: growth bounds the pole order and decay bounds the zero order at a cusp.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §§2.4–2.5.
• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §19.

Points of the coarse quotient

theorem Subgroup.CompactifiedQuotient.meromorphicAt_ofQuotient_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Γ.CompactifiedQuotient → E} {p : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane} : TauCeti.RiemannSurface.MeromorphicAt F (ofQuotient p) ↔ TauCeti.RiemannSurface.MeromorphicAt (F ∘ ofQuotient) p

A function on the compactified quotient is meromorphic at a point of the coarse quotient exactly when its restriction to the coarse quotient is.

theorem Subgroup.CompactifiedQuotient.meromorphicOrderAt_ofQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (F : Γ.CompactifiedQuotient → E) (p : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) : TauCeti.RiemannSurface.meromorphicOrderAt F (ofQuotient p) = TauCeti.RiemannSurface.meromorphicOrderAt (F ∘ ofQuotient) p

The order of a function on the compactified quotient at a point of the coarse quotient is the order of its restriction to the coarse quotient.

theorem Subgroup.CompactifiedQuotient.meromorphicAt_ofQuotient_mk_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Γ.CompactifiedQuotient → E} [CompleteSpace E] {z : UpperHalfPlane} : TauCeti.RiemannSurface.MeromorphicAt F (ofQuotient ⟦z⟧) ↔ TauCeti.RiemannSurface.MeromorphicAt (F ∘ ofQuotient ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane)) z

Meromorphy at the orbit of a point of the upper half-plane. A function on the compactified quotient is meromorphic at the orbit of z exactly when its pullback to the upper half-plane is meromorphic at z, including at elliptic points.

theorem Subgroup.CompactifiedQuotient.meromorphicOrderAt_comp_ofQuotient_mk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (F : Γ.CompactifiedQuotient → E) (z : UpperHalfPlane) : TauCeti.RiemannSurface.meromorphicOrderAt (F ∘ ofQuotient ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane)) z = ↑(Nat.card ↥(MulAction.stabilizer (↥Γ) z)) * TauCeti.RiemannSurface.meromorphicOrderAt F (ofQuotient ⟦z⟧)

The elliptic order formula on the compactified quotient. Pulling a function on the compactified quotient back to the upper half-plane multiplies its order at the orbit of z by the order m of the stabilizer of z: ord_z (F ∘ π) = m * ord_[z] F.

Cusps

theorem Subgroup.CompactifiedQuotient.comp_cuspChart_symm_eventuallyEq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (D : Γ.CuspDatum) {A : ℝ} (hA : D.width ≤ A) (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) : F ∘ ↑(cuspChart D hA).symm =ᶠ[nhdsWithin 0 {0}ᶜ] TauCeti.Subgroup.CuspDatum.cuspExtension D f

A function on the compactified quotient read in a cusp chart. If f is the pullback of F to the upper half-plane, then near q = 0, away from 0, the representative of F in the cusp chart of the cusp datum D is the cusp extension of f at D.

theorem Subgroup.CompactifiedQuotient.meromorphicAt_ofCusp_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (D : Γ.CuspDatum) (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) : TauCeti.RiemannSurface.MeromorphicAt F (ofCusp D.cuspOrbit) ↔ MeromorphicAt (TauCeti.Subgroup.CuspDatum.cuspExtension D f) 0

Meromorphy at a cusp. A function on the compactified quotient is meromorphic at the cusp orbit of a cusp datum D exactly when the cusp extension at D of its pullback f to the upper half-plane is meromorphic at q = 0. Any cusp datum representing the cusp orbit may be used.

theorem Subgroup.CompactifiedQuotient.meromorphicOrderAt_ofCusp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (D : Γ.CuspDatum) (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) : TauCeti.RiemannSurface.meromorphicOrderAt F (ofCusp D.cuspOrbit) = meromorphicOrderAt (TauCeti.Subgroup.CuspDatum.cuspExtension D f) 0

The order at a cusp. The order of a function on the compactified quotient at the cusp orbit of a cusp datum D is the order at q = 0 of the cusp extension at D of its pullback f to the upper half-plane. Any cusp datum representing the cusp orbit may be used.

theorem Subgroup.CompactifiedQuotient.meromorphicAt_ofCusp_of_isBigO {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) (D : Γ.CuspDatum) (k : ℤ) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : TauCeti.RiemannSurface.MeromorphicAt F (ofCusp D.cuspOrbit)

Meromorphic extension across a cusp. If the pullback f of a function on the compactified quotient is holomorphic at sufficiently large normalized heights and grows at most like exp (2πky / w) in the scaling coordinate of a cusp datum of width w, then the function is meromorphic at that cusp.

theorem Subgroup.CompactifiedQuotient.neg_le_meromorphicOrderAt_ofCusp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) (D : Γ.CuspDatum) (k : ℤ) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : ↑(-k) ≤ TauCeti.RiemannSurface.meromorphicOrderAt F (ofCusp D.cuspOrbit)

Growth bounds the pole order at a cusp. If the pullback f of a function on the compactified quotient is holomorphic sufficiently high and grows at most like exp (2πky / w) in the scaling coordinate of a cusp datum of width w, then the order of the function at that cusp is at least -k.

theorem Subgroup.CompactifiedQuotient.natCast_le_meromorphicOrderAt_ofCusp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {F : Γ.CompactifiedQuotient → ℂ} {f : UpperHalfPlane → ℂ} (hF : ∀ (z : UpperHalfPlane), F (ofQuotient ⟦z⟧) = f z) (D : Γ.CuspDatum) (n : ℕ) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hdecay : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-2 * Real.pi * ↑n * z.im / D.width)) : ↑↑n ≤ TauCeti.RiemannSurface.meromorphicOrderAt F (ofCusp D.cuspOrbit)

Decay bounds the zero order at a cusp. If the pullback f of a function on the compactified quotient is holomorphic sufficiently high and decays at least like exp (-2πny / w) in the scaling coordinate of a cusp datum of width w, then the function vanishes to order at least n at that cusp.