The projective Weierstrass polynomial is prime

For a Weierstrass curve W' over an integral domain R, the homogeneous Weierstrass polynomial

Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³)

is a prime element of R[X, Y, Z], so the homogeneous coordinate ring WeierstrassCurve.Projective.CoordinateRing W' is an integral domain. No ellipticity hypothesis is needed.

Main results

• WeierstrassCurve.Projective.prime_polynomial: over an integral domain, the Weierstrass polynomial in projective coordinates is prime.
• WeierstrassCurve.Projective.instIsDomainCoordinateRing: over an integral domain, the homogeneous coordinate ring of a Weierstrass curve is an integral domain.

References

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

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/ForMathlib/WeierstrassProjectivePrime.lean, declarations WeierstrassCurve.projective_polynomial_prime and ModularCurves.instIsDomainProjCoordRing, which treat Weierstrass curves over a field; here the base is any integral domain, and the coordinate ring is WeierstrassCurve.Projective.CoordinateRing.

theorem WeierstrassCurve.Projective.prime_polynomial {R : Type u_1} [CommRing R] (W' : Projective R) [IsDomain R] : Prime W'.polynomial

Over an integral domain, the Weierstrass polynomial Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³) in projective coordinates is prime in R[X, Y, Z]. Its irreducibility follows by Prime.irreducible; compare WeierstrassCurve.Affine.irreducible_polynomial for the affine Weierstrass polynomial.

instance WeierstrassCurve.Projective.instIsDomainCoordinateRing {R : Type u_1} [CommRing R] (W' : Projective R) [IsDomain R] : IsDomain W'.CoordinateRing

Over an integral domain, the homogeneous coordinate ring of a Weierstrass curve is an integral domain; compare the corresponding instance on the affine coordinate ring WeierstrassCurve.Affine.CoordinateRing.