The function field 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. This file identifies its function field with the function field W.toAffine.FunctionField of the affine Weierstrass equation, the fraction field of the affine coordinate ring R[x, y] ⧸ (W(x, y)). No ellipticity hypothesis is needed.

Main definitions

• WeierstrassCurve.projModelFunctionFieldEquiv: the isomorphism W.projModel.functionField ≃+* W.toAffine.FunctionField.

Main results

• WeierstrassCurve.nonempty_basicOpen_coord_two: over a nontrivial ring, the standard affine chart D₊(Z) of the projective model is nonempty.
• WeierstrassCurve.projModelFunctionFieldEquiv_germToFunctionField_awayToSection_mk: the isomorphism sends the rational function p(X, Y, Z) / Zⁿ on the chart D₊(Z) to p(x, y, 1).

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, I.1 and I.2.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/MulByHomDegree.lean, declaration ModularCurves.EllipticCurve.projModelFunctionFieldEquiv, which treats elliptic curves over a field and takes its Z-chart identification coordRingToZSection from ModelVariableChange.lean in the same directory; here the base is any integral domain, no ellipticity is assumed, and the chart identification is built on WeierstrassCurve.Projective.awayEquivChartRing.

instance WeierstrassCurve.nonempty_basicOpen_coord_two {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] : Nonempty ↥↑(AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2))

Over a nontrivial ring, the standard affine chart D₊(Z) of the projective Weierstrass model is nonempty.

noncomputable def WeierstrassCurve.projModelFunctionFieldEquiv {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] : ↑W.projModel.functionField ≃+* W.toAffine.FunctionField

Over an integral domain, the isomorphism between the function field of the projective Weierstrass model and the function field W.toAffine.FunctionField of the affine Weierstrass equation. On the chart D₊(Z) it sends p(X, Y, Z) / Zⁿ to p(x, y, 1), where x and y are the affine coordinates (projModelFunctionFieldEquiv_germToFunctionField_awayToSection_mk).

Equations

• W.projModelFunctionFieldEquiv = IsFractionRing.ringEquivOfRingEquiv (WeierstrassCurve.chartSectionsEquivCoordinateRing✝ W)

@[simp]

theorem WeierstrassCurve.projModelFunctionFieldEquiv_germToFunctionField_awayToSection_mk {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] {n : ℕ} {p : MvPolynomial (Fin 3) R} (hp : (Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) p ∈ W.toProjective.grading (n • 1)) : W.projModelFunctionFieldEquiv ((CategoryTheory.ConcreteCategory.hom (W.projModel.germToFunctionField (AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord 2)))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Proj.awayToSection W.toProjective.grading (W.toProjective.coord 2))) (HomogeneousLocalization.Away.mk W.toProjective.grading ⋯ n ((Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) p) hp))) = (algebraMap W.toAffine.CoordinateRing W.toAffine.FunctionField) ((MvPolynomial.aeval ![(Affine.CoordinateRing.mk W.toAffine) (Polynomial.C Polynomial.X), (Affine.CoordinateRing.mk W.toAffine) Polynomial.X, 1]) p)

On the standard affine chart D₊(Z), projModelFunctionFieldEquiv sends the rational function p(X, Y, Z) / Zⁿ, for p whose class in the homogeneous coordinate ring has degree n, to p(x, y, 1), where x and y are the classes of the affine coordinates in W.toAffine.CoordinateRing.