Smoothness of the projective Weierstrass model

If the discriminant of a Weierstrass curve W over a commutative ring R is a unit, the projective Weierstrass model W.projModel is smooth of relative dimension one over Spec R.

The proof is chart by chart. On the standard affine chart Xᵢ ≠ 0, presented as R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1), the Jacobian minor of the two relations with respect to the variables Xⱼ and Xᵢ (for j ≠ i) is the partial derivative ∂W/∂Xⱼ; inverting it gives a standard smooth algebra of relative dimension 3 - 2 = 1. The two partial derivatives ∂W/∂Xⱼ, j ≠ i, generate the unit ideal of the chart ring: at a point with residue field k, the image of the point is a nonzero solution of the projective equation over k, hence nonsingular since the discriminant is a unit in k, and Euler's relation 3W = Σ Xⱼ ∂W/∂Xⱼ with Xᵢ = 1 shows that some ∂W/∂Xⱼ with j ≠ i is nonzero there.

Main results

• WeierstrassCurve.Projective.isStandardSmoothOfRelativeDimension_localizationAway_pderiv: the chart Xᵢ ≠ 0 is standard smooth of relative dimension one where ∂W/∂Xⱼ is invertible, j ≠ i; no ellipticity is needed.
• WeierstrassCurve.Projective.span_range_mk_pderiv_eq_top: for an elliptic curve, these partial derivatives generate the unit ideal of the chart.
• WeierstrassCurve.smoothOfRelativeDimension_one_projModelOver: the projective model of an elliptic Weierstrass curve is smooth of relative dimension one over the base.
• WeierstrassCurve.smooth_projModelOver: the projective model of an elliptic Weierstrass curve is smooth over the base.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.
• P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, II.1.
• Stacks Project, Tag 00T7.

Provenance

smooth_projModelOver is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve/: the unnamed instance Smooth universalCurveπ in PointsDictionary.lean and its universe-polymorphic counterpart Smooth (projModelπ universalWeierstrassLocU) in GroupLawAxioms.lean, which treat only the universal Weierstrass curve over ℤ[a₁, a₂, a₃, a₄, a₆][Δ⁻¹]. Here the instance is stated for every elliptic Weierstrass curve over every commutative ring.

theorem WeierstrassCurve.Projective.isStandardSmoothOfRelativeDimension_localizationAway_pderiv {R : Type u} [CommRing R] (W' : Projective R) {i j : Fin 3} (hji : j ≠ i) : Algebra.IsStandardSmoothOfRelativeDimension 1 R (Localization.Away ((Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) ((MvPolynomial.pderiv j) W'.polynomial)))

The standard affine chart Xᵢ ≠ 0 of the projective Weierstrass cubic becomes standard smooth of relative dimension one after inverting the partial derivative ∂W/∂Xⱼ, for j ≠ i.

theorem WeierstrassCurve.Projective.span_range_mk_pderiv_eq_top {R : Type u} [CommRing R] (W' : Projective R) (i : Fin 3) [WeierstrassCurve.IsElliptic W'] : Ideal.span (Set.range fun (j : { j : Fin 3 // j ≠ i }) => (Ideal.Quotient.mk (Ideal.span (Set.range (W'.chartRelation i)))) ((MvPolynomial.pderiv ↑j) W'.polynomial)) = ⊤

On the standard affine chart Xᵢ ≠ 0 of an elliptic Weierstrass cubic, the partial derivatives ∂W/∂Xⱼ with j ≠ i generate the unit ideal.

theorem WeierstrassCurve.Projective.locally_isStandardSmoothOfRelativeDimension_algebraMap {R : Type u} [CommRing R] (W' : Projective R) (i : Fin 3) [WeierstrassCurve.IsElliptic W'] : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension 1) (algebraMap R (W'.ChartRing i))

The standard affine chart Xᵢ ≠ 0 of an elliptic Weierstrass cubic is, locally on the chart, standard smooth of relative dimension one over the base.

instance WeierstrassCurve.smoothOfRelativeDimension_one_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : AlgebraicGeometry.SmoothOfRelativeDimension 1 W.projModelOver

If the discriminant is a unit, the projective Weierstrass model is smooth of relative dimension one over the base.

instance WeierstrassCurve.smooth_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : AlgebraicGeometry.Smooth W.projModelOver

If the discriminant is a unit, the projective Weierstrass model is smooth over the base.