Documentation

TauCeti.Analysis.Complex.Fuchsian.LevelOne.Extension

The modular invariant on the compactified level-one quotient #

The descended modular invariant extends meromorphically to the compact Riemann surface obtained by adjoining the unique modular cusp. Its order at that cusp is exactly -1: in the normalized width-one chart it is q⁻¹ times the analytic cusp function of q j, whose value at zero is 1. On the coarse quotient the extension agrees with jQuotient, and its local multiplicities agree with those already computed there.

jCompactified is complex-valued, using value zero at the pole as a representative of its meromorphic germ. Meromorphy and order depend only on punctured neighbourhoods, so this assigned value does not remove the pole. The target surface is the constructed compactified orbit quotient; no identification with the Riemann sphere is used.

References #

source
noncomputable def TauCeti.ModularGroup.jCompactified :
psl2zToPSL2R.range.CompactifiedQuotient → ℂ

The modular invariant on the compactified effective level-one quotient. At its unique pole the assigned value is zero; its meromorphic germ there is independent of this value.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ModularGroup.jCompactified_ofQuotient (p : MulAction.orbitRel.Quotient (↥psl2zToPSL2R.range) UpperHalfPlane) :
    jCompactified (Subgroup.CompactifiedQuotient.ofQuotient p) = jQuotient p
    source
    @[simp]
    theorem TauCeti.ModularGroup.jCompactified_ofCusp (C : psl2zToPSL2R.range.CuspOrbit) :
    jCompactified (Subgroup.CompactifiedQuotient.ofCusp C) = 0
    source
    @[simp]
    theorem TauCeti.ModularGroup.jCompactified_comp_ofQuotient :
    jCompactified ∘ Subgroup.CompactifiedQuotient.ofQuotient = jQuotient

    The compactified function restricts to the descended modular invariant.

    source
    theorem TauCeti.ModularGroup.meromorphicAt_jCompactified (x : psl2zToPSL2R.range.CompactifiedQuotient) :
    RiemannSurface.MeromorphicAt jCompactified x

    The extended modular invariant is meromorphic at every point of the constructed compact level-one surface, including its cusp.

    source
    @[simp]
    theorem TauCeti.ModularGroup.meromorphicOrderAt_jCompactified_ofCusp (C : psl2zToPSL2R.range.CuspOrbit) :
    RiemannSurface.meromorphicOrderAt jCompactified (Subgroup.CompactifiedQuotient.ofCusp C) = -1

    The extended modular invariant has a simple pole at the unique modular cusp. The order is computed in the normalized identity-scaling, width-one q-coordinate.

    source
    @[simp]
    theorem TauCeti.ModularGroup.meromorphicOrderAt_jCompactified_nonneg_iff (x : psl2zToPSL2R.range.CompactifiedQuotient) :
    0 ≤ RiemannSurface.meromorphicOrderAt jCompactified x ↔ x ≠ Subgroup.CompactifiedQuotient.ofCusp cuspOrbitInfty

    The unique cusp is the only pole of the modular invariant on the compactified surface.