The presentation of ℤ[c₄, c₆, Δ]

For any Weierstrass curve W over a commutative ring R whose invariants c₄ and c₆ are algebraically independent over ℤ, the invariants c₄, c₆ and Δ satisfy exactly one relation, c₄³ - c₆² = 1728Δ (WeierstrassCurve.c_relation): the kernel of the evaluation ℤ[C₄, C₆, D] → R, C₄, C₆, D ↦ W.c₄, W.c₆, W.Δ, is the principal ideal generated by C₄³ - C₆² - 1728D (WeierstrassCurve.ker_aeval_c₄_c₆_Δ), so ℤ[W.c₄, W.c₆, W.Δ] is isomorphic to ℤ[C₄, C₆, D]/(C₄³ - C₆² - 1728D) (WeierstrassCurve.adjoinC₄C₆ΔEquiv).

Applying this to the universal Weierstrass equation over ℤ[a₁, a₂, a₃, a₄, a₆] via WeierstrassCurve.Universal.algebraicIndependent_c₄_c₆ presents the ring of integral modular forms of level one; the same theorem applies to the Tate curve over ℤ⟦q⟧.

The proof has two steps. Modulo the relation, 1728D is congruent to C₄³ - C₆², so some 1728ⁿ-multiple of every polynomial is congruent to a polynomial in C₄ and C₆ alone; if the original polynomial lies in the kernel, that polynomial in C₄ and C₆ vanishes by the algebraic independence of W.c₄ and W.c₆. Second, the relation is coprime to every nonzero integer, since it takes the value 1 at (C₄, C₆, D) = (1, 0, 0); so the power of 1728 can be cancelled.

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.

theorem WeierstrassCurve.ker_aeval_c₄_c₆_Δ {R : Type u_1} [CommRing R] [Algebra ℤ R] (W : WeierstrassCurve R) (hind : AlgebraicIndependent ℤ ![W.c₄, W.c₆]) : RingHom.ker (MvPolynomial.aeval ![W.c₄, W.c₆, W.Δ]) = Ideal.span {MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2 - 1728 * MvPolynomial.X 2}

For any Weierstrass curve W whose invariants c₄ and c₆ are algebraically independent over ℤ, the kernel of the evaluation ℤ[C₄, C₆, D] → R at W.c₄, W.c₆, W.Δ is generated by C₄³ - C₆² - 1728D.

noncomputable def WeierstrassCurve.adjoinC₄C₆ΔEquiv {R : Type u_1} [CommRing R] [Algebra ℤ R] (W : WeierstrassCurve R) (hind : AlgebraicIndependent ℤ ![W.c₄, W.c₆]) : (MvPolynomial (Fin 3) ℤ ⧸ Ideal.span {MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2 - 1728 * MvPolynomial.X 2}) ≃ₐ[ℤ] ↥ℤ[W.c₄, W.c₆, W.Δ]

For any Weierstrass curve W whose invariants c₄ and c₆ are algebraically independent over ℤ, the subring ℤ[W.c₄, W.c₆, W.Δ] of R is presented by c₄³ - c₆² = 1728Δ.

@[simp]

theorem WeierstrassCurve.adjoinC₄C₆ΔEquiv_mk {R : Type u_1} [CommRing R] [Algebra ℤ R] (W : WeierstrassCurve R) (hind : AlgebraicIndependent ℤ ![W.c₄, W.c₆]) (P : MvPolynomial (Fin 3) ℤ) : ↑((W.adjoinC₄C₆ΔEquiv hind) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2 - 1728 * MvPolynomial.X 2})) P)) = (MvPolynomial.aeval ![W.c₄, W.c₆, W.Δ]) P

The presentation W.adjoinC₄C₆ΔEquiv sends the class of P to P(W.c₄, W.c₆, W.Δ).