Holomorphic descent to the coarse Fuchsian quotient

A function on the coarse quotient of the upper half-plane by a properly discontinuous projective subgroup is holomorphic if and only if its pullback to the upper half-plane is holomorphic. This includes elliptic orbits: in the chart at a point with stabilizer order m, the pullback is the composition with u ↦ u ^ m, and holomorphy descends through this power map.

The local statement Subgroup.differentiableOn_comp_stabilizerBallQuotientChart_symm needs holomorphy of the pullback only on the chosen stabilizer ball. The global criterion Subgroup.mdifferentiable_iff_comp_quotientMk and the unique descent theorem Subgroup.existsUnique_mdifferentiable_quotientMk apply to functions valued in any complex Banach space. They use the ordinary orbit quotient, without choosing representatives to define the descended function. For maps into a complex manifold, Subgroup.mdifferentiableAt_of_eventually_mdifferentiableAt_comp_quotientMk checks holomorphy at an orbit, elliptic or not, from holomorphy of the pullback near one of its points, by reading the map in a chart of the target.

The elliptic descent argument uses TauCeti.differentiableOn_descendPow and follows Farkas–Kra, Riemann Surfaces, Chapter I §§4–5, and Miranda, Algebraic Curves and Riemann Surfaces, Chapter III §§3–4.

theorem Subgroup.differentiableOn_comp_stabilizerBallQuotientChart_symm (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (hopen : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {F : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane → E} (hF : MDiff[Metric.ball z ε] (F ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane))) : DifferentiableOn ℂ (F ∘ ↑(stabilizerBallQuotientChart hε hopen).symm) (stabilizerBallQuotientChart hε hopen).target

In a stabilizer-ball chart, a function on the coarse quotient is holomorphic whenever its pullback is holomorphic on the ball. This holds also when the stabilizer is nontrivial.

@[simp]

theorem Subgroup.mdifferentiable_iff_comp_quotientMk (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] {F : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane → E} : MDiff F ↔ MDiff (F ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane))

Holomorphy on the full coarse quotient can be checked after pullback to the upper half-plane, including at elliptic orbits.

theorem Subgroup.mdifferentiableAt_of_eventually_mdifferentiableAt_comp_quotientMk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_3} [TopologicalSpace H'] {I' : ModelWithCorners ℂ E' H'} {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 1 M'] {F : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane → M'} {z : UpperHalfPlane} (hF : ∀ᶠ (w : UpperHalfPlane) in nhds z, MDiffAt (F ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane)) w) : MDiffAt F ⟦z⟧

Holomorphic descent of maps into a manifold. A map from the coarse quotient to a complex manifold is holomorphic at the orbit of z as soon as its pullback along the orbit projection is holomorphic near z. This holds also at elliptic orbits; at a free orbit holomorphy of the pullback at z alone suffices (Subgroup.mdifferentiableAt_of_comp_quotientMk).

theorem Subgroup.existsUnique_mdifferentiable_quotientMk (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] (f : UpperHalfPlane → E) (hinv : ∀ (g : ↥Γ) (z : UpperHalfPlane), f (g • z) = f z) (hf : MDiff f) : ∃! F : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane → E, MDiff F ∧ F ∘ Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) = f

Every invariant holomorphic function on the upper half-plane descends uniquely to a holomorphic function on the coarse quotient, with no freeness assumption.