The compactified quotient of a Fuchsian group is a Riemann surface #
Let Γ ≤ PSL(2, ℝ) be discrete. This file extends the atlas of the coarse quotient Γ \ ℍ to
its compactification Subgroup.CompactifiedQuotient Γ by the q-coordinate charts
Subgroup.CompactifiedQuotient.cuspChart at the cusp orbits, and proves that the resulting atlas
is holomorphic. The compactified quotient is therefore a Riemann surface, Hausdorff and second
countable by Subgroup.CompactifiedQuotient.instT2Space and
Subgroup.CompactifiedQuotient.instSecondCountableTopology, and the inclusion of the coarse
quotient is a holomorphic open embedding.
The atlas consists of the charts of Γ \ ℍ, transported along the open embedding ofQuotient
(Subgroup.CompactifiedQuotient.ofQuotientChart), together with the cusp charts at every cusp
datum and every height at least its width. Every chart of this atlas is holomorphic when pulled
back to the coarse quotient (Subgroup.CompactifiedQuotient.mdifferentiableAt_comp_ofQuotient):
for a cusp chart this is holomorphic descent at a free orbit, since high horodiscs lie in the free
locus. Consequently the transition map out of a transported chart is holomorphic by the chain rule,
and the transition map out of a cusp chart agrees, near every nonzero point of its source, with
Mathlib's periodic cusp function of a w-periodic function that is holomorphic at the logarithmic
lift of that point, hence is holomorphic there
(Function.Periodic.differentiableAt_cuspFunction); at q = 0 the singularity is removable
because a transition map is continuous.
Main declarations #
Subgroup.CompactifiedQuotient.ofQuotientChart: a chart ofΓ \ ℍregarded as a chart of the compactified quotient.Subgroup.CompactifiedQuotient.instChartedSpace: the atlas, described bySubgroup.CompactifiedQuotient.mem_atlas_iff,Subgroup.CompactifiedQuotient.chartAt_ofQuotientandSubgroup.CompactifiedQuotient.chartAt_ofCusp.Subgroup.CompactifiedQuotient.instIsManifold: the atlas is analytic, so the compactified quotient is a Riemann surface.Subgroup.CompactifiedQuotient.mdifferentiable_ofQuotient: the inclusion of the coarse quotient is holomorphic, andSubgroup.CompactifiedQuotient.mdifferentiableAt_comp_ofQuotient_iff: a map out of the compactified quotient is holomorphic along the coarse quotient exactly when its restriction is.
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, §§18–19.
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, Chapter 4.
Charts of the coarse quotient #
A chart of the coarse quotient Γ \ ℍ, regarded as a chart of the compactified quotient along
the open embedding ofQuotient.
Equations
Instances For
The atlas #
The atlas of the compactified quotient. It consists of the charts of the coarse quotient
Γ \ ℍ, transported along the open embedding ofQuotient, together with the cusp charts at every
cusp datum and every height at least its width. The chart at a point of the coarse quotient is the
transported chart there, and the chart at a cusp orbit is the cusp chart at a chosen cusp datum
representing it, at the height equal to its width.
Equations
- One or more equations did not get rendered due to their size.
A chart of the compactified quotient belongs to the atlas exactly when it is a transported chart of the coarse quotient or a cusp chart.
Holomorphy of the transition maps #
Every chart of the atlas is holomorphic along the coarse quotient: pulled back along the
inclusion ofQuotient, a chart of the compactified quotient is holomorphic at every point of the
coarse quotient in its source.
The transition maps of the atlas are holomorphic.
The compactified quotient of a Fuchsian group is a Riemann surface.
The inclusion of the coarse quotient is holomorphic. Together with
Subgroup.CompactifiedQuotient.isOpenEmbedding_ofQuotient, the coarse quotient is an open
submanifold of the compactified quotient.
A map out of the compactified quotient is holomorphic at a point of the coarse quotient exactly when its restriction to the coarse quotient is: the transported charts of the coarse quotient are charts of the compactified quotient.
At a point of the coarse quotient, a map on the compactification has the same local multiplicity as its restriction. No holomorphy assumption is needed because the charts agree.