The Laurent expansion of the coordinate ring at the point at infinity

Let W be a Weierstrass curve over a commutative ring R, with affine coordinate ring R[W] = R[X, Y] ⧸ (W(X, Y)) and coordinate functions x and y. Near the point at infinity [0 : 1 : 0], the parameter is z = -x / y, and w = -1 / y is the power series w(z) = z³ u(z) of WeierstrassCurve.formalW, with u(0) = 1. Inverting these relations gives the Laurent series

x = z / w(z) = z⁻² u(z)⁻¹ and y = -1 / w(z) = -z⁻³ u(z)⁻¹

in R⸨X⸩, the variable of the Laurent series ring standing for z. They satisfy the Weierstrass equation of W, so they define an R-algebra homomorphism R[W] →ₐ[R] R⸨X⸩, the Laurent expansion of a function on the affine curve at the point at infinity.

The order of the Laurent expansion is the order of the pole at infinity. The coordinate ring is free over R on the monomials xⁱyʲ with j ≤ 1 (WeierstrassCurve.Affine.CoordinateRing.basisMonomials), and the expansion of xⁱyʲ is (-1)ʲ z^(-(2i + 3j)) times a power series with constant coefficient 1. The weights 2i + 3j of distinct monomials are distinct, so the expansion of an element vanishes below z^(-n) exactly when the element is an R-linear combination of the monomials of weight at most n. For n = 0, 2, 3, 4, 5, 6 these are the bases 1; 1, x; 1, x, y; 1, x, y, x²; 1, x, y, x², xy; 1, x, y, x², xy, x³ of the functions with a pole of order at most n at infinity. No hypothesis on W or on R is needed: the leading coefficients are ±1, so the argument does not use that R is reduced. Over a field, the bounds for n = 2, 3 are also proved with the valuation at the place at infinity, in TauCeti/AlgebraicGeometry/EllipticCurve/Affine/FunctionField/InfinityPlace/PoleOrder.lean; over a general ring there is no such valuation, and the Laurent expansion takes its place.

Main definitions

• WeierstrassCurve.laurentExpansion: the Laurent expansion R[W] →ₐ[R] R⸨X⸩ at the point at infinity.

Main results

• WeierstrassCurve.laurentExpansion_of_X and WeierstrassCurve.laurentExpansion_root: the expansions of x and y are z⁻² u(z)⁻¹ and -z⁻³ u(z)⁻¹.
• WeierstrassCurve.laurentExpansion_root_mul_formalW and WeierstrassCurve.laurentExpansion_of_X_eq_neg_X_mul_laurentExpansion_root: the expansion of y is -1 / w(z), and that of x is -z times that of y.
• WeierstrassCurve.mem_span_basisMonomials_iff_forall_coeff_laurentExpansion_eq_zero: the expansion of g vanishes below z^(-n) exactly when g is a linear combination of the monomials xⁱyʲ with 2i + 3j ≤ n.
• WeierstrassCurve.laurentExpansion_injective: the Laurent expansion is injective.
• WeierstrassCurve.exists_eq_algebraMap_of_coeff_laurentExpansion_eq_zero_of_neg: a function without a pole at infinity is a constant.
• WeierstrassCurve.exists_eq_of_coeff_laurentExpansion_eq_zero_of_lt_neg_two and WeierstrassCurve.exists_eq_of_coeff_laurentExpansion_eq_zero_of_lt_neg_three: a function with a pole of order at most 2 (resp. 3) at infinity is αx + β (resp. γy + δx + β), where α (resp. -γ) is the coefficient of z⁻² (resp. z⁻³) of its expansion.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, IV.1 (the expansions of x and y in the parameter z) and II.5.8 (the bases of the spaces L(n(O))).
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.1–2.2.

noncomputable def WeierstrassCurve.laurentExpansion {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.toAffine.CoordinateRing →ₐ[R] LaurentSeries R

The Laurent expansion at the point at infinity of a function on the affine Weierstrass curve: the R-algebra homomorphism R[W] →ₐ[R] R⸨X⸩ sending x to z⁻² u(z)⁻¹ = z / w(z) and y to -z⁻³ u(z)⁻¹ = -1 / w(z), where z is the variable of the Laurent series ring and w(z) = z³ u(z) is the w-expansion WeierstrassCurve.formalW of W.

@[simp]

theorem WeierstrassCurve.laurentExpansion_of_X {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.laurentExpansion ((AdjoinRoot.of W.toAffine.polynomial) Polynomial.X) = (HahnSeries.single (-2)) 1 * (HahnSeries.ofPowerSeries ℤ R) (W.formalU.invOfUnit 1)

The Laurent expansion of the coordinate function x is z⁻² u(z)⁻¹.

@[simp]

theorem WeierstrassCurve.laurentExpansion_root {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.laurentExpansion (AdjoinRoot.root W.toAffine.polynomial) = (HahnSeries.single (-3)) (-1) * (HahnSeries.ofPowerSeries ℤ R) (W.formalU.invOfUnit 1)

The Laurent expansion of the coordinate function y is -z⁻³ u(z)⁻¹.

theorem WeierstrassCurve.laurentExpansion_root_mul_formalW {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.laurentExpansion (AdjoinRoot.root W.toAffine.polynomial) * (HahnSeries.ofPowerSeries ℤ R) W.formalW = -1

The Laurent expansion of the coordinate function y is -1 / w(z): its product with the w-expansion is -1.

theorem WeierstrassCurve.laurentExpansion_of_X_eq_neg_X_mul_laurentExpansion_root {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.laurentExpansion ((AdjoinRoot.of W.toAffine.polynomial) Polynomial.X) = -((HahnSeries.ofPowerSeries ℤ R) PowerSeries.X * W.laurentExpansion (AdjoinRoot.root W.toAffine.polynomial))

The Laurent expansion of the coordinate function x is -z times that of y, that is, x = -z y.

The order of the pole at infinity

theorem WeierstrassCurve.mem_span_basisMonomials_iff_forall_coeff_laurentExpansion_eq_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {g : W.toAffine.CoordinateRing} {n : ℕ} : g ∈ Submodule.span R (⇑(Affine.CoordinateRing.basisMonomials W.toAffine) '' {p : ℕ × Fin 2 | 2 * p.1 + 3 * ↑p.2 ≤ n}) ↔ ∀ m < -↑n, (W.laurentExpansion g).coeff m = 0

The pole order at infinity. The Laurent expansion of a function g on the affine Weierstrass curve vanishes below z^(-n) exactly when g is an R-linear combination of the monomials xⁱyʲ, j ≤ 1, of weight 2i + 3j ≤ n.

theorem WeierstrassCurve.laurentExpansion_injective {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Function.Injective ⇑W.laurentExpansion

The Laurent expansion at the point at infinity is injective.

theorem WeierstrassCurve.exists_eq_of_coeff_laurentExpansion_eq_zero_of_lt_neg_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {g : W.toAffine.CoordinateRing} (h : ∀ m < -2, (W.laurentExpansion g).coeff m = 0) : ∃ (β : R), g = (algebraMap R W.toAffine.CoordinateRing) ((W.laurentExpansion g).coeff (-2)) * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) β

A function with a pole of order at most 2 at infinity is αx + β. If the Laurent expansion of g vanishes below z⁻², then g = αx + β for some β, where α is the coefficient of z⁻² of the expansion.

theorem WeierstrassCurve.exists_eq_of_coeff_laurentExpansion_eq_zero_of_lt_neg_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {g : W.toAffine.CoordinateRing} (h : ∀ m < -3, (W.laurentExpansion g).coeff m = 0) : ∃ (δ : R) (β : R), g = (algebraMap R W.toAffine.CoordinateRing) (-(W.laurentExpansion g).coeff (-3)) * AdjoinRoot.root W.toAffine.polynomial + (algebraMap R W.toAffine.CoordinateRing) δ * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) β

A function with a pole of order at most 3 at infinity is γy + δx + β. If the Laurent expansion of g vanishes below z⁻³, then g = γy + δx + β for some δ and β, where -γ is the coefficient of z⁻³ of the expansion.

theorem WeierstrassCurve.exists_eq_algebraMap_of_coeff_laurentExpansion_eq_zero_of_neg {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {g : W.toAffine.CoordinateRing} (h : ∀ m < 0, (W.laurentExpansion g).coeff m = 0) : ∃ (β : R), g = (algebraMap R W.toAffine.CoordinateRing) β

A function with no pole at infinity is constant. If the Laurent expansion of g has no negative powers of z, then g is a constant β.