The normalized level-one cusp

The cusp at infinity of the effective modular group has width one in the identity scaling. Its full stabilizer is generated by the image of the translation matrix T. The resulting normalized datum identifies the compactification's cusp coordinate with the usual modular parameter q = exp (2πiτ), allowing modular q-expansions to be read in the surface chart.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §§2.3–2.4.

def TauCeti.ModularGroup.cuspDatumInfty : psl2zToPSL2R.range.CuspDatum

The normalized cusp datum at infinity for the effective level-one modular group: identity scaling, width one, and the image of T as primitive positive generator.

Equations

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

@[simp]

theorem TauCeti.ModularGroup.cuspDatumInfty_cusp : cuspDatumInfty.cusp = OnePoint.infty

@[simp]

theorem TauCeti.ModularGroup.cuspDatumInfty_scaling : cuspDatumInfty.scaling = 1

@[simp]

theorem TauCeti.ModularGroup.cuspDatumInfty_width : cuspDatumInfty.width = 1

@[simp]

theorem TauCeti.ModularGroup.cuspDatumInfty_generator : ↑cuspDatumInfty.generator = psl2zToPSL2R ↑ModularGroup.T

@[simp]

theorem TauCeti.ModularGroup.coordinate_cuspDatumInfty (z : UpperHalfPlane) : Subgroup.CuspDatum.coordinate cuspDatumInfty z = Function.Periodic.qParam 1 ↑z

The surface cusp coordinate for the normalized modular datum is the usual width-one q-parameter.

@[simp]

theorem TauCeti.ModularGroup.cuspExtension_cuspDatumInfty (f : UpperHalfPlane → ℂ) : Subgroup.CuspDatum.cuspExtension cuspDatumInfty f = UpperHalfPlane.cuspFunction 1 f

Reading a function in the normalized modular cusp datum gives its usual width-one cusp function.