Documentation

TauCeti.Analysis.Complex.Fuchsian.LevelOne.ModularInvariant

The modular invariant on the level-one quotient #

The normalized modular invariant j = E₄³ / Δ is holomorphic on the upper half-plane and invariant under the effective level-one group, the image of PSL(2, ℤ) in PSL(2, ℝ). It therefore descends through the orbit projection to a holomorphic function TauCeti.ModularGroup.jQuotient on the coarse level-one quotient.

The local multiplicities of the descended function are determined by those of j and the stabilizer orders: pulling back to the upper half-plane multiplies the local multiplicity at the orbit of z by the order of the stabilizer of z. At the elliptic point ρ the stabilizer has order 3 and j vanishes to order 3; at i the stabilizer has order 2 and j - 1728 vanishes to order 2. So the descended function is unramified at both elliptic orbits, and at every other orbit its local multiplicity equals that of j upstairs.

The descent uses the ordinary orbit quotient, without choosing representatives. Everything here concerns the uncompactified quotient; the behaviour of j at the cusp is not treated.

Main results #

References #

source
@[simp]
theorem TauCeti.ModularForm.localMultiplicity_j_ρ :
RiemannSurface.localMultiplicity j UpperHalfPlane.ρ = 3

The modular invariant has ramification index 3 at the elliptic point ρ.

source
@[simp]
theorem TauCeti.ModularForm.localMultiplicity_j_I :
RiemannSurface.localMultiplicity j UpperHalfPlane.I = 2

The modular invariant has ramification index 2 at the elliptic point i.

source
@[simp]
theorem TauCeti.ModularGroup.j_smul_psl2zToPSL2RRange (g : ↥psl2zToPSL2R.range) (z : UpperHalfPlane) :
ModularForm.j (g • z) = ModularForm.j z

The modular invariant is invariant under the effective level-one group.

source
noncomputable def TauCeti.ModularGroup.jQuotient :
MulAction.orbitRel.Quotient (↥psl2zToPSL2R.range) UpperHalfPlane → ℂ

The modular invariant on the coarse level-one quotient: the function on the orbit space of the effective level-one group whose pullback along the orbit projection is the modular invariant j.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ModularGroup.jQuotient_mk (z : UpperHalfPlane) :
    jQuotient ⟦z⟧ = ModularForm.j z

    The descended modular invariant takes the value j z at the orbit of z.

    source
    @[simp]
    theorem TauCeti.ModularGroup.jQuotient_comp_quotientMk :
    jQuotient ∘ Quotient.mk (MulAction.orbitRel (↥psl2zToPSL2R.range) UpperHalfPlane) = ModularForm.j

    The pullback of the descended modular invariant along the orbit projection is j.

    source
    theorem TauCeti.ModularGroup.mdifferentiable_jQuotient :
    MDiff jQuotient

    The modular invariant on the coarse level-one quotient is holomorphic, including at the two elliptic orbits.

    source
    theorem TauCeti.ModularGroup.localMultiplicity_j_eq_card_stabilizer_mul_localMultiplicity_jQuotient (z : UpperHalfPlane) :
    RiemannSurface.localMultiplicity ModularForm.j z = Nat.card ↥(MulAction.stabilizer (↥psl2zToPSL2R.range) z) * RiemannSurface.localMultiplicity jQuotient ⟦z⟧

    The ramification formula for j. The local multiplicity of j at z is the order of the stabilizer of z in the effective level-one group times the local multiplicity of its descent at the orbit of z.

    source
    @[simp]
    theorem TauCeti.ModularGroup.localMultiplicity_jQuotient_ρ :
    RiemannSurface.localMultiplicity jQuotient ⟦UpperHalfPlane.ρ⟧ = 1

    The descended modular invariant is unramified at the orbit of ρ.

    source
    @[simp]
    theorem TauCeti.ModularGroup.localMultiplicity_jQuotient_I :
    RiemannSurface.localMultiplicity jQuotient ⟦UpperHalfPlane.I⟧ = 1

    The descended modular invariant is unramified at the orbit of i.

    source
    theorem TauCeti.ModularGroup.localMultiplicity_jQuotient_eq_localMultiplicity_j_of_stabilizer_eq_bot {z : UpperHalfPlane} (hz : MulAction.stabilizer (↥psl2zToPSL2R.range) z = ⊥) :
    RiemannSurface.localMultiplicity jQuotient ⟦z⟧ = RiemannSurface.localMultiplicity ModularForm.j z

    At an orbit with trivial stabilizer, the descended modular invariant has the same local multiplicity as j. By stabilizer_psl2zToPSL2RRange_eq_bot_iff these are exactly the orbits other than those of i and ρ.