Documentation

TauCeti.NumberTheory.ModularForms.LevelOne.GradedRing

E₄ and E₆ freely generate the level-one modular forms #

This file defines the evaluation map ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k sending X₀ ↦ E₄, X₁ ↦ E₆, and proves it is surjective: every modular form of level one is a polynomial in the Eisenstein series E₄ and E₆.

The proof is the classical induction on the weight. Negative-weight pieces vanish. In nonnegative weight below 12 each graded piece has dimension at most one — zero in odd weights and in weight 2, and otherwise spanned by a monomial in E₄, E₆; at weight k ≥ 12, subtracting a multiple of such a monomial leaves a cusp form, which is Δ times a form of weight k − 12 by Mathlib's CuspForm.discriminantEquiv, and Δ = (E₄³ − E₆²)/1728.

Injectivity is a weight-by-weight argument on weighted-homogeneous components (weights 4, 6): any component of a relation splits, by repeated division of its high-X₀ monomials, as a reduced part of X₀-degree below 3 plus the discriminant polynomial times a lower-weight piece; evaluating and inspecting the constant q-coefficient kills the reduced monomial, and induction on the weight — descending through the discriminant factor — finishes.

Main declarations #

References #

source
noncomputable def TauCeti.ModularForm.evalE₄E₆ :
MvPolynomial (Fin 2) ℂ →ₐ[ℂ] DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range)

Evaluation homomorphism sending ℂ[X₀, X₁] to the graded ring of level 1 modular forms via X₀ ↦ E₄ and X₁ ↦ E₆.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ModularForm.evalE₄E₆_X_zero :
    evalE₄E₆ (MvPolynomial.X 0) = (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) ModularForm.E₄
    source
    @[simp]
    theorem TauCeti.ModularForm.evalE₄E₆_X_one :
    evalE₄E₆ (MvPolynomial.X 1) = (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) ModularForm.E₆
    source
    theorem TauCeti.ModularForm.evalE₄E₆_surjective :
    Function.Surjective ⇑evalE₄E₆

    Every modular form of level one is a polynomial in E₄ and E₆: the evaluation homomorphism evalE₄E₆ is surjective.

    source
    theorem TauCeti.ModularForm.evalE₄E₆_injective :
    Function.Injective ⇑evalE₄E₆

    The evaluation homomorphism evalE₄E₆ is injective: E₄ and E₆ are algebraically independent.

    source
    noncomputable def TauCeti.ModularForm.mvPolynomialEquivModularForms :
    MvPolynomial (Fin 2) ℂ ≃ₐ[ℂ] DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range)

    The graded ring of level-1 modular forms is isomorphic to the polynomial ring ℂ[X₀, X₁] via evaluation at E₄ and E₆.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ModularForm.mvPolynomialEquivModularForms_apply (p : MvPolynomial (Fin 2) ℂ) :
      mvPolynomialEquivModularForms p = evalE₄E₆ p
      source
      theorem TauCeti.ModularForm.adjoin_E₄_E₆_eq_top :
      ℂ[(DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) ModularForm.E₄, (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) ModularForm.E₆] = ⊤

      E₄ and E₆ generate the entire graded ring of level 1 modular forms as an ℂ-algebra.

      source
      instance TauCeti.ModularForm.instIsDomainDirectSumIntModularFormRangeSpecialLinearGroupFinOfNatNatGeneralLinearGroupRealMapGL_tauCeti :
      IsDomain (DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range))

      The graded ring of level-1 modular forms is an integral domain, being isomorphic (via mvPolynomialEquivModularForms) to the polynomial ring ℂ[X₀, X₁].