The modular invariant identifies the level-one surface with the sphere

The normalized modular invariant defines a holomorphic map jSphere from the constructed compactified modular quotient to OnePoint ℂ. It sends the unique cusp to infinity and restricts to jQuotient on the coarse quotient. In the cusp q-coordinate, its reciprocal is q / F(q), where F is the analytic cusp function of q j and F(0) = 1. Thus its only point above infinity has local multiplicity one. The fibre-counting degree theorem gives degree one, and jBiholomorph is the resulting biholomorphism, normalized by the images of the cusp and the two elliptic orbits.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §§2.4–2.5.
• Jean-Pierre Serre, A Course in Arithmetic, Chapter VII, §§3–4.
• Otto Forster, Lectures on Riemann Surfaces, §4, Theorem 4.24.

noncomputable def TauCeti.ModularGroup.jSphere : psl2zToPSL2R.range.CompactifiedQuotient → OnePoint ℂ

The normalized modular invariant as a map from the compactified level-one modular quotient to the Riemann sphere, with its pole assigned the value infinity.

Equations

• TauCeti.ModularGroup.jSphere (Subgroup.CompactifiedQuotient.ofQuotient p) = ↑(TauCeti.ModularGroup.jQuotient p)
• TauCeti.ModularGroup.jSphere (Subgroup.CompactifiedQuotient.ofCusp cusp) = OnePoint.infty

@[simp]

theorem TauCeti.ModularGroup.jSphere_ofQuotient (p : MulAction.orbitRel.Quotient (↥psl2zToPSL2R.range) UpperHalfPlane) : jSphere (Subgroup.CompactifiedQuotient.ofQuotient p) = ↑(jQuotient p)

@[simp]

theorem TauCeti.ModularGroup.jSphere_ofCusp (C : psl2zToPSL2R.range.CuspOrbit) : jSphere (Subgroup.CompactifiedQuotient.ofCusp C) = OnePoint.infty

@[simp]

theorem TauCeti.ModularGroup.jSphere_eq_infty_iff (x : psl2zToPSL2R.range.CompactifiedQuotient) : jSphere x = OnePoint.infty ↔ x = Subgroup.CompactifiedQuotient.ofCusp cuspOrbitInfty

The fibre of infinity consists precisely of the modular cusp.

theorem TauCeti.ModularGroup.mdifferentiable_jSphere : MDiff jSphere

The sphere-valued modular invariant is holomorphic, including at the cusp.

@[simp]

theorem TauCeti.ModularGroup.localMultiplicity_jSphere_ofCusp (C : psl2zToPSL2R.range.CuspOrbit) : RiemannSurface.localMultiplicity jSphere (Subgroup.CompactifiedQuotient.ofCusp C) = 1

The sphere-valued modular invariant has local multiplicity one at the unique cusp.

noncomputable def TauCeti.ModularGroup.jFiniteHolomorphicMap : RiemannSurface.FiniteHolomorphicMap psl2zToPSL2R.range.CompactifiedQuotient (OnePoint ℂ)

The modular invariant, bundled as a finite holomorphic map of compact Riemann surfaces.

Equations

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

@[simp]

theorem TauCeti.ModularGroup.coe_jFiniteHolomorphicMap : ↑jFiniteHolomorphicMap = jSphere

@[simp]

theorem TauCeti.ModularGroup.degree_jSphere : RiemannSurface.degree jSphere = 1

The normalized modular invariant has degree one on the constructed modular surface.

noncomputable def TauCeti.ModularGroup.jBiholomorph : Diffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) psl2zToPSL2R.range.CompactifiedQuotient (OnePoint ℂ) ↑⊤

The normalized modular invariant identifies the compactified level-one modular quotient biholomorphically with the Riemann sphere.

Equations

• TauCeti.ModularGroup.jBiholomorph = TauCeti.RiemannSurface.biholomorphOfDegreeEqOne TauCeti.ModularGroup.jFiniteHolomorphicMap TauCeti.ModularGroup.jBiholomorph._proof_4✝

@[simp]

theorem TauCeti.ModularGroup.coe_jBiholomorph : ⇑jBiholomorph = jSphere

The identifying biholomorphism has the normalized modular invariant as its forward map.

@[simp]

theorem TauCeti.ModularGroup.jBiholomorph_ofQuotient (p : MulAction.orbitRel.Quotient (↥psl2zToPSL2R.range) UpperHalfPlane) : jBiholomorph (Subgroup.CompactifiedQuotient.ofQuotient p) = ↑(jQuotient p)

@[simp]

theorem TauCeti.ModularGroup.jBiholomorph_ofCusp (C : psl2zToPSL2R.range.CuspOrbit) : jBiholomorph (Subgroup.CompactifiedQuotient.ofCusp C) = OnePoint.infty

theorem TauCeti.ModularGroup.jBiholomorph_ρ : jBiholomorph (Subgroup.CompactifiedQuotient.ofQuotient ⟦UpperHalfPlane.ρ⟧) = ↑0

The elliptic orbit of order three maps to zero.

theorem TauCeti.ModularGroup.jBiholomorph_I : jBiholomorph (Subgroup.CompactifiedQuotient.ofQuotient ⟦UpperHalfPlane.I⟧) = ↑1728

The elliptic orbit of order two maps to 1728.