Integrality of the projective Weierstrass model

For a Weierstrass curve W over an integral domain R, the projective Weierstrass model W.projModel is an integral scheme. No ellipticity hypothesis is needed; in particular the projective model of an elliptic curve over a field is integral.

Over an arbitrary commutative ring R, the structure morphism W.projModelOver is therefore geometrically integral: its base change along Spec K ⟶ Spec R, for a field K, is the projective model of W over K.

Main results

• WeierstrassCurve.isIntegral_projModel: over an integral domain, the projective Weierstrass model is an integral scheme.
• WeierstrassCurve.geometricallyIntegral_projModelOver: over any commutative ring, the structure morphism of the projective Weierstrass model is geometrically integral.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1.

Provenance

Both results draw on AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a; the files named below lie in projects/ModularCurves/ModularCurves/EllipticCurve/.

AINTLIB states integrality of the projective model only over a field (ModularCurves.isIntegral_projModel in PointsDictionary.lean and ModularCurves.isIntegral_projModel_u in GroupLawAxioms.lean). Over an integral domain, isIntegral_projModel is assembled from the two inputs adapted from AINTLIB, WeierstrassCurve.Projective.instIsDomainCoordinateRing and AlgebraicGeometry.Proj.isIntegral_of_isDomain.

geometricallyIntegral_projModelOver is adapted from ModularCurves.geometricallyIntegral_universalCurveπ in PointsDictionary.lean and its universe-polymorphic counterpart ModularCurves.geometricallyIntegral_universalCurveπU in GroupLawAxioms.lean, which treat only the universal Weierstrass curve over ℤ[a₁, a₂, a₃, a₄, a₆][Δ⁻¹]. Here the same fibrewise argument applies to every Weierstrass curve over every commutative ring.

instance WeierstrassCurve.isIntegral_projModel {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] : AlgebraicGeometry.IsIntegral W.projModel

Over an integral domain, the projective Weierstrass model is an integral scheme; in particular the projective model of any Weierstrass curve over a field, elliptic or not, is integral. Here IsIntegral is the scheme property AlgebraicGeometry.IsIntegral, not WeierstrassCurve.IsIntegral (integrality of the coefficients over a subring).

instance WeierstrassCurve.geometricallyIntegral_projModelOver {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : AlgebraicGeometry.GeometricallyIntegral W.projModelOver

The structure morphism of the projective Weierstrass model over any commutative ring is geometrically integral: its base change along Spec K ⟶ Spec R, for a field K, is the projective Weierstrass model of W over K, which is an integral scheme. No ellipticity hypothesis is needed.