Integral modular forms of the Weierstrass coordinate-change action

A polynomial f ∈ ℤ[a₁, a₂, a₃, a₄, a₆] in the coefficients of the universal Weierstrass curve is an integral modular form of weight k (WeierstrassCurve.IsIntegralModularForm) when f(C • W) = u⁻ᵏ f(W) for every Weierstrass curve W and every admissible change of variables C = (u, r, s, t) over every commutative ring. These are the weight-k invariants of the Weierstrass Hopf algebroid, the integral modular forms of level one of Deligne's formulaire. The invariants c₄, c₆ and Δ of the universal curve are such forms, of weights 4, 6 and 12.

The weight of a coefficient aᵢ is i (WeierstrassCurve.coefficientWeight): the scaling C = (u, 0, 0, 0) sends aᵢ to u⁻ⁱ aᵢ. Since the definition quantifies over all coefficient rings, it can be tested on the scaling by a unit u with u⁻¹ = 2 over ℚ[a₁, ⋯, a₆], which multiplies every monomial of weight n by 2ⁿ: an integral modular form of weight k is weighted homogeneous of weight k. Over ℤ alone the only units are ±1, which separate weights only modulo 2, so this quantification is essential.

On the subring ℤ[c₄, c₆, Δ] every change of variables acts through its u alone, so there the weight-k modular forms are exactly the weighted homogeneous elements of weight k (WeierstrassCurve.isIntegralModularForm_iff_of_mem_adjoin).

After inverting 6, every Weierstrass equation is carried by a change of variables (1/6, r, s, t) to the short equation y² = x³ - 27c₄x - 54c₆. Hence an integral modular form f of weight k satisfies 6ᵏ f = f(0, 0, 0, -27c₄, -54c₆), a polynomial in c₄ and c₆. Conversely, since the universal curve and change of variables are defined together over the torsion-free ring ℤ[u, u⁻¹, r, s, t][a₁, ⋯, a₆], the transformation law of n • f for a nonzero integer n implies that of f. Together these describe the integral modular forms of weight k as the weighted homogeneous f of weight k with 6ⁿ f ∈ ℤ[c₄, c₆] for some n (WeierstrassCurve.isIntegralModularForm_iff_exists_six_pow_mul_mem_adjoin).

By Deligne's theorem every integral modular form lies in ℤ[c₄, c₆, Δ] (WeierstrassCurve.IsIntegralModularForm.mem_adjoin). Together with the description of the modular forms in ℤ[c₄, c₆, Δ] above, this determines the ring of integral modular forms of level one: an integral modular form of weight k is exactly a weighted homogeneous element of weight k of ℤ[c₄, c₆, Δ] (WeierstrassCurve.isIntegralModularForm_iff), and this subring is presented by the single relation c₄³ - c₆² = 1728Δ (WeierstrassCurve.adjoinC₄C₆ΔEquiv).

Deligne's theorem follows from the description after inverting 6, because ℤ[c₄, c₆, Δ] is saturated with respect to 6: every element of it is α(c₄, Δ) + c₆ β(c₄, Δ), and reducing modulo 6 on the curve with a₁ = x and a₆ = -y over (ℤ/6)[x, y], whose invariants are the monomials x⁴, -x⁶ and x⁶y, shows that if this element is divisible by 6 then so are α and β.

Main definitions

• WeierstrassCurve.IsIntegralModularForm: the predicate of being an integral modular form of weight k.
• TauCeti.WeierstrassCurve.integralModularFormSubmodule: the ℤ-submodule of integral modular forms of weight k, forming a graded monoid across weights.

Main results

• WeierstrassCurve.IsIntegralModularForm.add, .smul, .mul, .pow: integral modular forms of a fixed weight form a ℤ-module, and weights add under multiplication.
• WeierstrassCurve.isIntegralModularForm_c₄, isIntegralModularForm_c₆, isIntegralModularForm_Δ: the invariants c₄, c₆ and Δ of the universal curve are integral modular forms of weights 4, 6 and 12.
• WeierstrassCurve.IsIntegralModularForm.isWeightedHomogeneous: an integral modular form of weight k is weighted homogeneous of weight k; in particular a nonzero integral modular form has a unique weight (WeierstrassCurve.IsIntegralModularForm.inj_right).
• WeierstrassCurve.isIntegralModularForm_iff_of_mem_adjoin: an element of ℤ[c₄, c₆, Δ] is an integral modular form of weight k exactly when it is weighted homogeneous of weight k.
• WeierstrassCurve.isIntegralModularForm_iff_universal: the transformation law need only be checked for the universal curve and change of variables over ℤ[u, u⁻¹, r, s, t][a₁, ⋯, a₆].
• WeierstrassCurve.isIntegralModularForm_iff_forall_isElliptic: the transformation law need only be checked on elliptic curves, still over every commutative ring.
• WeierstrassCurve.isIntegralModularForm_smul_iff: for a nonzero integer n, n • f is an integral modular form of weight k exactly when f is.
• WeierstrassCurve.IsIntegralModularForm.six_pow_mul_eq_specialize_shortCurve: an integral modular form f of weight k satisfies 6ᵏ f = f(0, 0, 0, -27c₄, -54c₆).
• WeierstrassCurve.isIntegralModularForm_iff_exists_six_pow_mul_mem_adjoin: the integral modular forms of weight k are the weighted homogeneous f of weight k with 6ⁿ f ∈ ℤ[c₄, c₆] for some n.
• WeierstrassCurve.IsIntegralModularForm.mem_adjoin: Deligne's theorem, every integral modular form lies in ℤ[c₄, c₆, Δ].
• WeierstrassCurve.isIntegralModularForm_iff: the integral modular forms of weight k are the weighted homogeneous elements of weight k of ℤ[c₄, c₆, Δ].

References

• P. Deligne, Courbes elliptiques : formulaire d'après J. Tate, in Modular functions of one variable IV, Lecture Notes in Math. 476, Springer, 1975.
• T. Bauer, Computation of the homotopy of the spectrum tmf, in Groups, homotopy and configuration spaces, Geom. Topol. Monogr. 13 (2008), §3.

def WeierstrassCurve.IsIntegralModularForm (k : ℕ) (f : MvPolynomial Coeff ℤ) : Prop

A polynomial f in the coefficients of the universal Weierstrass curve is an integral modular form of weight k if f(C • W) = u⁻ᵏ f(W) for every Weierstrass curve W and every change of variables C = (u, r, s, t) over every commutative ring R (in Type). Here f(W) is the specialization W.specialize f.

theorem WeierstrassCurve.isIntegralModularForm_def {k : ℕ} {f : MvPolynomial Coeff ℤ} : IsIntegralModularForm k f ↔ ∀ (R : Type) [inst : CommRing R] (W : WeierstrassCurve R) (C : VariableChange R), (C • W).specialize f = ↑C.u⁻¹ ^ k * W.specialize f

theorem WeierstrassCurve.IsIntegralModularForm.specialize_smul {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) {R : Type} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).specialize f = ↑C.u⁻¹ ^ k * W.specialize f

The transformation law of an integral modular form of weight k under a change of variables.

theorem WeierstrassCurve.IsIntegralModularForm.add {k : ℕ} {f g : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) (hg : IsIntegralModularForm k g) : IsIntegralModularForm k (f + g)

theorem WeierstrassCurve.IsIntegralModularForm.neg {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) : IsIntegralModularForm k (-f)

theorem WeierstrassCurve.IsIntegralModularForm.sub {k : ℕ} {f g : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) (hg : IsIntegralModularForm k g) : IsIntegralModularForm k (f - g)

theorem WeierstrassCurve.IsIntegralModularForm.smul {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) (n : ℤ) : IsIntegralModularForm k (n • f)

theorem WeierstrassCurve.IsIntegralModularForm.mul {k l : ℕ} {f g : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) (hg : IsIntegralModularForm l g) : IsIntegralModularForm (k + l) (f * g)

The product of integral modular forms of weights k and l has weight k + l.

theorem WeierstrassCurve.IsIntegralModularForm.pow {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) (n : ℕ) : IsIntegralModularForm (k * n) (f ^ n)

The n-th power of an integral modular form of weight k has weight k * n.

theorem WeierstrassCurve.isIntegralModularForm_iff_universal {k : ℕ} {f : MvPolynomial Coeff ℤ} : IsIntegralModularForm k f ↔ (specialize ((TauCeti.WeierstrassChange.ChangeRing.universalChange ℤ).map (algebraMap TauCeti.WeierstrassChange.Universal.CoordinateRing (MvPolynomial Coeff TauCeti.WeierstrassChange.Universal.CoordinateRing)) • Universal.curve.map (MvPolynomial.map (Int.castRingHom TauCeti.WeierstrassChange.Universal.CoordinateRing)))) f = ↑((TauCeti.WeierstrassChange.ChangeRing.universalChange ℤ).map (algebraMap TauCeti.WeierstrassChange.Universal.CoordinateRing (MvPolynomial Coeff TauCeti.WeierstrassChange.Universal.CoordinateRing))).u⁻¹ ^ k * (specialize (Universal.curve.map (MvPolynomial.map (Int.castRingHom TauCeti.WeierstrassChange.Universal.CoordinateRing)))) f

The universal transformation law. It suffices to check the transformation law of an integral modular form once, for the universal Weierstrass curve and the universal change of variables over Γ = ℤ[u, u⁻¹, r, s, t][a₁, ⋯, a₆], the polynomial ring in the Weierstrass coefficients over the coordinate ring TauCeti.WeierstrassChange.Universal.CoordinateRing of the changes of variables: every pair (W, C) is a specialization of that one.

theorem WeierstrassCurve.isIntegralModularForm_iff_forall_isElliptic {k : ℕ} {f : MvPolynomial Coeff ℤ} : IsIntegralModularForm k f ↔ ∀ (R : Type) [inst : CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (C : VariableChange R), (C • W).specialize f = ↑C.u⁻¹ ^ k * W.specialize f

A coefficient polynomial satisfies the modular transformation law on all cubics if and only if it satisfies it on elliptic curves over every commutative ring. The reverse direction extends across the discriminant in the universal coefficient/change-of-variables domain.

theorem WeierstrassCurve.isIntegralModularForm_smul_iff {k : ℕ} {f : MvPolynomial Coeff ℤ} {n : ℤ} (hn : n ≠ 0) : IsIntegralModularForm k (n • f) ↔ IsIntegralModularForm k f

Multiplying by a nonzero integer neither creates nor destroys integral modular forms.

@[simp]

theorem WeierstrassCurve.isIntegralModularForm_zero (k : ℕ) : IsIntegralModularForm k 0

@[simp]

theorem WeierstrassCurve.isIntegralModularForm_intCast (n : ℤ) : IsIntegralModularForm 0 ↑n

Every integer is an integral modular form of weight 0. This is the simp normal form of isIntegralModularForm_C.

theorem WeierstrassCurve.isIntegralModularForm_C (n : ℤ) : IsIntegralModularForm 0 (MvPolynomial.C n)

Every integer constant is an integral modular form of weight 0.

@[simp]

theorem WeierstrassCurve.isIntegralModularForm_one : IsIntegralModularForm 0 1

theorem WeierstrassCurve.isIntegralModularForm_c₄ : IsIntegralModularForm 4 (c₄ Universal.curve)

The invariant c₄ of the universal curve is an integral modular form of weight 4.

theorem WeierstrassCurve.isIntegralModularForm_c₆ : IsIntegralModularForm 6 (c₆ Universal.curve)

The invariant c₆ of the universal curve is an integral modular form of weight 6.

theorem WeierstrassCurve.isIntegralModularForm_Δ : IsIntegralModularForm 12 (Δ Universal.curve)

The discriminant Δ of the universal curve is an integral modular form of weight 12.

theorem WeierstrassCurve.IsIntegralModularForm.isWeightedHomogeneous {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) : MvPolynomial.IsWeightedHomogeneous coefficientWeight f k

The weight of an integral modular form. An integral modular form of weight k is weighted homogeneous of weight k for the weights coefficientWeight.

theorem WeierstrassCurve.IsIntegralModularForm.inj_right {k l : ℕ} {f : MvPolynomial Coeff ℤ} (hf : f ≠ 0) (hk : IsIntegralModularForm k f) (hl : IsIntegralModularForm l f) : k = l

A nonzero integral modular form has a unique weight.

theorem WeierstrassCurve.isIntegralModularForm_iff_of_mem_adjoin {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : f ∈ ℤ[c₄ Universal.curve, c₆ Universal.curve, Δ Universal.curve]) : IsIntegralModularForm k f ↔ MvPolynomial.IsWeightedHomogeneous coefficientWeight f k

On the subring ℤ[c₄, c₆, Δ], being an integral modular form of weight k is weighted homogeneity of weight k: there a change of variables (u, r, s, t) acts as the scaling (u, 0, 0, 0).

theorem WeierstrassCurve.IsIntegralModularForm.six_pow_mul_eq_specialize_shortCurve {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) : 6 ^ k * f = (shortCurve (-27 * c₄ Universal.curve) (-54 * c₆ Universal.curve)).specialize f

Integral modular forms after inverting 6. If f is an integral modular form of weight k, then 6ᵏ f is the value of f at the short Weierstrass equation y² = x³ - 27c₄x - 54c₆ of the universal curve. Over ℤ[1/6] every Weierstrass equation is carried to this one by the change of variables (1/6, r, s, t) for suitable r, s, t.

theorem WeierstrassCurve.IsIntegralModularForm.six_pow_mul_mem_adjoin {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) : 6 ^ k * f ∈ ℤ[c₄ Universal.curve, c₆ Universal.curve]

After inverting 6, an integral modular form is a polynomial in c₄ and c₆: if f has weight k then 6ᵏ f lies in the subring ℤ[c₄, c₆].

theorem WeierstrassCurve.isIntegralModularForm_iff_exists_six_pow_mul_mem_adjoin {k : ℕ} {f : MvPolynomial Coeff ℤ} : IsIntegralModularForm k f ↔ MvPolynomial.IsWeightedHomogeneous coefficientWeight f k ∧ ∃ (n : ℕ), 6 ^ n * f ∈ ℤ[c₄ Universal.curve, c₆ Universal.curve]

Integral modular forms after inverting 6. A polynomial in the Weierstrass coefficients is an integral modular form of weight k exactly when it is weighted homogeneous of weight k and becomes a polynomial in c₄ and c₆ after multiplication by a power of 6. This describes the modular forms without reference to changes of variables; Deligne's theorem refines the second condition to membership in ℤ[c₄, c₆, Δ].

Deligne's theorem

theorem WeierstrassCurve.IsIntegralModularForm.mem_adjoin {k : ℕ} {f : MvPolynomial Coeff ℤ} (hf : IsIntegralModularForm k f) : f ∈ ℤ[c₄ Universal.curve, c₆ Universal.curve, Δ Universal.curve]

Deligne's theorem. Every integral modular form lies in the subring ℤ[c₄, c₆, Δ].

theorem WeierstrassCurve.isIntegralModularForm_iff {k : ℕ} {f : MvPolynomial Coeff ℤ} : IsIntegralModularForm k f ↔ f ∈ ℤ[c₄ Universal.curve, c₆ Universal.curve, Δ Universal.curve] ∧ MvPolynomial.IsWeightedHomogeneous coefficientWeight f k

The ring of integral modular forms. A polynomial in the coefficients of the universal Weierstrass curve is an integral modular form of weight k exactly when it lies in ℤ[c₄, c₆, Δ] and is weighted homogeneous of weight k.

def TauCeti.WeierstrassCurve.integralModularFormSubmodule (k : ℕ) : Submodule ℤ (MvPolynomial WeierstrassCurve.Coeff ℤ)

The ℤ-submodule of ℤ[a₁, a₂, a₃, a₄, a₆] consisting of integral modular forms of weight k for the Weierstrass coordinate-change action.

@[simp]

theorem TauCeti.WeierstrassCurve.mem_integralModularFormSubmodule {k : ℕ} {f : MvPolynomial WeierstrassCurve.Coeff ℤ} : f ∈ integralModularFormSubmodule k ↔ WeierstrassCurve.IsIntegralModularForm k f

instance TauCeti.WeierstrassCurve.instGradedMonoidNatMvPolynomialCoeffIntSubmoduleIntegralModularFormSubmodule : SetLike.GradedMonoid integralModularFormSubmodule