The coordinate pullback of multiplication by n, for every nonzero n

Isogeny/Basic.lean gives the identity coordinate pullback and Isogeny/Frobenius/Basic.lean gives the Frobenius one. This file gives [n]: multiplication by n pulls back to a map W.CoordinateRing →ₐ[F] W.FunctionField wherever ψₙ does not vanish at the generic point.

That non-vanishing is available for every n ≠ 0 once the curve is nonsingular, so this file constructs [n] in every characteristic, [p] in characteristic p included. Two lemmas discharge it and neither subsumes the other: psiFunctionField_ne_zero from (n : F) ≠ 0, which needs no nonsingularity, and psiFunctionField_ne_zero_of_Δ_ne_zero from W.Δ ≠ 0 and n ≠ 0, which needs no hypothesis on the characteristic. mulByIntPullback itself, and everything it is built from, carry neither: they ask for psiFunctionField W n ≠ 0 directly.

The construction is the division-polynomial formula read at the generic point. The coordinate ring W.CoordinateRing is F[X][Y] modulo the Weierstrass relation, so the pair (X, Y) is itself a point of W over the function field W.FunctionField — the generic point. n times it has coordinates φₙ / ψₙ² and ωₙ / ψₙ³ by the division-polynomial formulas, and sending X and Y there is exactly a coordinate pullback.

What is not here

The MapsInfinity condition, and so [n] as an Isogeny W W, are not proved here. Neither criterion Isogeny/Basic.lean offers applies directly: mapsInfinity_of_pow wants a fixed power of every coordinate function to be pulled back, which is the Frobenius shape and not this one, and mapsInfinity_iff_isEquiv_comap_infinityPlace wants the induced map of function fields, which is available only after the pullback below is known injective. That chain — injectivity, the function-field map, then the place comparison — is its own topic and its own file. Note the order of dependence: Isogeny/FunctionField.lean proves transcendence, injectivity and the field pullback for any isogeny, but each of those consumes mapsInfinity, so none of them can be used to establish it.

Every definition here is paired with a _def equation lemma, because a def's body is not exposed across the module boundary even inside a public section: a downstream simp only [mulByIntX] is rejected with Expected a definition with an exposed body. Without them the file cannot be computed with from outside at all.

One fact is the whole content here: equation_mulByInt, that the pair (φₙ/ψₙ², ωₙ/ψₙ³) satisfies the equation of the base-changed curve. It is not a polynomial identity to be checked; it holds because n • P is a point of the curve whenever P is, which is WeierstrassCurve.zsmul_point_eq_smulEval at the generic point.

That the generic point is itself a point of the curve — the other half of the argument — lives in Affine/FunctionField/GenericPoint/Basic.lean as WeierstrassCurve.Affine.equation_genericX_genericY, since it is about W and not about [n].

Main definitions

• TauCeti.Isogeny.mulByIntX, TauCeti.Isogeny.mulByIntY: the rational expressions φₙ/ψₙ² and ωₙ/ψₙ³, the coordinates of [n] at the generic point where ψₙ ≠ 0.
• TauCeti.Isogeny.mulByIntPullback: the coordinate pullback of [n], given ψₙ ≠ 0.
• TauCeti.Isogeny.mulByIntPullbackOfNeZero: its specialisation to n ≠ 0 on an elliptic curve, where the non-vanishing is discharged.

The generic point itself (genericX, genericY) is not defined here; it is WeierstrassCurve.Affine's, in Affine/FunctionField/GenericPoint/Basic.lean.

Main results

• TauCeti.Isogeny.equation_mulByInt: the coordinates of [n] satisfy the equation of W over its function field.
• TauCeti.Isogeny.psiFunctionField_two_mul: ψ_{2n} = preΨ_{2n} · ψ₂ at the generic point.
• TauCeti.Isogeny.psiFunctionField_ne_zero: ψₙ does not vanish at the generic point when (n : F) ≠ 0, needing no nonsingularity.
• TauCeti.Isogeny.psiFunctionField_ne_zero_of_Δ_ne_zero: the same conclusion from W.Δ ≠ 0 and n ≠ 0, with no hypothesis on the characteristic. These are the two discharges of mulByIntPullback's hypothesis; neither subsumes the other.
• TauCeti.Isogeny.phiFunctionField_eq_algebraMap: Φₙ at the generic point is the image of the univariate Φₙ, the companion of psiFunctionField_sq for the numerator.
• TauCeti.Isogeny.mulByIntX_mul_aeval_ΨSq: the coordinate identity [n]*x · ΨSqₙ(x) = Φₙ(x) at the generic point, where ψₙ does not vanish.
• TauCeti.Isogeny.mulByIntPullback_mk: the pullback of an arbitrary class, as evaluation of a bivariate polynomial at (φₙ/ψₙ², ωₙ/ψₙ³), with TauCeti.Isogeny.mulByIntPullback_X and TauCeti.Isogeny.mulByIntPullback_Y its values on the two coordinates.
• TauCeti.Isogeny.tautologicalPoint_mulByIntPullback: the tautological point of [n] is n • the generic point. It lives here, next to the Jacobian-coordinate lemmas it is proved from, which stay private.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4 and the division-polynomial formulas of Exercise 3.7.
• Adapted from the AINTLIB HasseWeil project (Chris Birkbeck), HasseWeil/MulByIntPullback.lean, Apache-2.0, at commit 513e83879e2f8cbc626eb9e04d660e92be16ccba, declarations x_gen, y_gen, W_KE, generic_equation, Φ_ff, ΨSq_ff, ψ_ff, ω_ff, mulByInt_x, mulByInt_y, mulByInt_xHom, mulByInt_weierstrass and mulByInt_coordHom. The source stops at a RingHom out of the coordinate ring and then builds its own function-field pullback, injectivity and transcendence statements by hand; here the ring hom is upgraded to the AlgHom that TauCeti.CoordinatePullback already asks for. The source's function-field pullback, injectivity and transcendence are not ported and not reproved here: they are deferred until MapsInfinity is available, because each of the corresponding general results in Isogeny/FunctionField.lean consumes it. See "What is not here".

noncomputable def TauCeti.Isogeny.psiFunctionField {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The image of the division polynomial ψₙ in the function field, i.e. ψₙ evaluated at the generic point. Its non-vanishing is the hypothesis every construction below carries.

Equations

• TauCeti.Isogeny.psiFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ψ W n))

noncomputable def TauCeti.Isogeny.omegaFunctionField {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The image of the division polynomial ωₙ in the function field.

Equations

• TauCeti.Isogeny.omegaFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ω W n))

noncomputable def TauCeti.Isogeny.phiFunctionField {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The image of the division polynomial φₙ in the function field.

Equations

• TauCeti.Isogeny.phiFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.φ W n))

noncomputable def TauCeti.Isogeny.psicFunctionField {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The image of the complementary division polynomial ψcₙ in the function field. It is the numerator of the pullback of 2y + a₁x + a₃ along [n], by the defining identity ω_spec.

Equations

• TauCeti.Isogeny.psicFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ψc W n))

noncomputable def TauCeti.Isogeny.mulByIntX {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The rational division-polynomial expression φₙ / ψₙ².

This is the x-coordinate of [n] at the generic point exactly when ψₙ does not vanish there; at a zero of ψₙ the quotient is junk, since [n] sends that point to infinity, which has no affine coordinate. Every result about it below therefore carries ψₙ ≠ 0.

Equations

• TauCeti.Isogeny.mulByIntX W n = TauCeti.Isogeny.phiFunctionField W n / TauCeti.Isogeny.psiFunctionField W n ^ 2

noncomputable def TauCeti.Isogeny.mulByIntY {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : W.FunctionField

The rational division-polynomial expression ωₙ / ψₙ³, the y-coordinate of [n] at the generic point under the same proviso as mulByIntX: exactly when ψₙ does not vanish there.

Equations

• TauCeti.Isogeny.mulByIntY W n = TauCeti.Isogeny.omegaFunctionField W n / TauCeti.Isogeny.psiFunctionField W n ^ 3

theorem TauCeti.Isogeny.psiFunctionField_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : psiFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ψ W n))

The defining equation of psiFunctionField.

theorem TauCeti.Isogeny.omegaFunctionField_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : omegaFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ω W n))

The defining equation of omegaFunctionField.

theorem TauCeti.Isogeny.phiFunctionField_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : phiFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.φ W n))

The defining equation of phiFunctionField.

theorem TauCeti.Isogeny.psicFunctionField_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : psicFunctionField W n = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (WeierstrassCurve.ψc W n))

The defining equation of psicFunctionField.

theorem TauCeti.Isogeny.phiFunctionField_eq_algebraMap {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : phiFunctionField W n = (algebraMap (Polynomial F) W.FunctionField) (WeierstrassCurve.Φ W n)

Φₙ at the generic point is the image of the univariate Φₙ.

theorem TauCeti.Isogeny.mulByIntX_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : mulByIntX W n = phiFunctionField W n / psiFunctionField W n ^ 2

The defining equation of mulByIntX: the x-coordinate of [n] is φₙ / ψₙ².

theorem TauCeti.Isogeny.mulByIntY_def {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : mulByIntY W n = omegaFunctionField W n / psiFunctionField W n ^ 3

The defining equation of mulByIntY: the y-coordinate of [n] is ωₙ / ψₙ³.

@[simp]

theorem TauCeti.Isogeny.psiFunctionField_sq {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : psiFunctionField W n ^ 2 = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (WeierstrassCurve.ΨSq W n)))

ψₙ² = ΨSqₙ in the function field: the division polynomial's square is the univariate ΨSq, already known in the coordinate ring as mk_ψ followed by mk_Ψ_sq.

theorem TauCeti.Isogeny.psiFunctionField_two_mul {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : psiFunctionField W (2 * n) = (algebraMap (Polynomial F) W.FunctionField) (WeierstrassCurve.preΨ W (2 * n)) * psiFunctionField W 2

ψ_{2n} = preΨ_{2n} · ψ₂ at the generic point. Ψ at an even argument is C (preΨ) * ψ₂, and ψ and Ψ agree in the coordinate ring, so an even-indexed psiFunctionField splits off its preΨ factor.

@[simp]

theorem TauCeti.Isogeny.aeval_genericX_Φ {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : (Polynomial.aeval W.genericX) (WeierstrassCurve.Φ W n) = phiFunctionField W n

Φₙ at the generic point is φₙ: the univariate division polynomial evaluated at the generic coordinate is its image in the function field.

@[simp]

theorem TauCeti.Isogeny.aeval_genericX_ΨSq {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : (Polynomial.aeval W.genericX) (WeierstrassCurve.ΨSq W n) = psiFunctionField W n ^ 2

ΨSqₙ at the generic point is ψₙ².

theorem TauCeti.Isogeny.mulByIntX_mul_aeval_ΨSq {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) (hn : psiFunctionField W n ≠ 0) : mulByIntX W n * (Polynomial.aeval W.genericX) (WeierstrassCurve.ΨSq W n) = (Polynomial.aeval W.genericX) (WeierstrassCurve.Φ W n)

The coordinate identity at the generic point: [n]*x · ΨSqₙ(x) = Φₙ(x).

theorem TauCeti.Isogeny.equation_mulByInt {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (WeierstrassCurve.baseChange W W.FunctionField).toAffine.Equation (mulByIntX W n) (mulByIntY W n)

The coordinates of [n] satisfy the equation of W over its function field.

This is the fact that makes [n] a coordinate pullback at all, and it is not a polynomial identity: it holds because n • P is again a point of the curve whenever P is. Concretely, zsmul_point_eq_smulEval identifies n • (generic point) with the Jacobian class of (φₙ : ωₙ : ψₙ), that class is nonsingular because it is a point, and ψₙ ≠ 0 lets it be read in affine coordinates — where it becomes exactly this equation.

theorem TauCeti.Isogeny.psiFunctionField_ne_zero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) {n : ℤ} (hn : ↑n ≠ 0) : psiFunctionField W n ≠ 0

ψₙ does not vanish at the generic point when the image of n in F is nonzero.

The hypothesis is on n in F, not on n in ℤ: in characteristic p it excludes n = p. It asks nothing about nonsingularity, which is what keeps it useful where psiFunctionField_ne_zero_of_Δ_ne_zero does not apply; neither of the two subsumes the other. The restriction is inherited from Mathlib.ΨSq_ne_zero, and every non-vanishing lemma in Mathlib's division-polynomial development is conditional the same way — preΨ_ne_zero, ΨSq_ne_zero, Ψ₃_ne_zero, preΨ₄_ne_zero — because each is proved from a leading coefficient ((W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = n ^ 2), exactly what vanishes when p ∣ n.

theorem TauCeti.Isogeny.psiFunctionField_ne_zero_of_Δ_ne_zero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (hΔ : WeierstrassCurve.Δ W ≠ 0) {n : ℤ} (hn : n ≠ 0) : psiFunctionField W n ≠ 0

ψₙ does not vanish at the generic point of a nonsingular curve, for every n ≠ 0 — in every characteristic, p ∣ n included.

This is the characteristic-free discharge of mulByIntPullback's hypothesis, and it is what lets this file construct [p] in characteristic p. It trades the condition on the characteristic for nonsingularity: ΨSq_ne_zero_of_Δ_ne_zero gets ΨSqₙ ≠ 0 from W.Δ ≠ 0 by way of IsCoprime (W.Φ n) (W.ΨSq n) (Silverman, Exercise III.3.7), which reads the non-vanishing off coprimality rather than off a leading coefficient. Δ ≠ 0 is stated as a hypothesis rather than taken as [W.IsElliptic] so that the lemma matches its supplier; mulByIntPullbackOfNeZero supplies it from the instance.

noncomputable def TauCeti.Isogeny.mulByIntPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : CoordinatePullback W W

The coordinate pullback of [n]. The point (φₙ/ψₙ², ωₙ/ψₙ³) over W.FunctionField, which equation_mulByInt says lies on W, defines a pullback through WeierstrassCurve.Affine.CoordinateRing.evalAlgHom.

The hypothesis is the weakest one the construction uses: ψₙ must not vanish at the generic point, which is what makes φₙ/ψₙ² and ωₙ/ψₙ³ defined. Two lemmas discharge it — psiFunctionField_ne_zero and psiFunctionField_ne_zero_of_Δ_ne_zero — and mulByIntPullbackOfNeZero is the packaged form.

Equations

• TauCeti.Isogeny.mulByIntPullback W hn = WeierstrassCurve.Affine.CoordinateRing.evalAlgHom ⋯

@[reducible, inline]

noncomputable abbrev TauCeti.Isogeny.mulByIntPullbackOfNeZero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) : CoordinatePullback W W

The coordinate pullback of [n] for every n ≠ 0, the non-vanishing hypothesis of mulByIntPullback being discharged by psiFunctionField_ne_zero_of_Δ_ne_zero. This is the specialisation to use unless you can supply ψₙ ≠ 0 yourself.

The hypothesis is on n in ℤ, so this does give [p] in characteristic p. Nonsingularity comes from the [W.IsElliptic] instance the definition already carried, which is why taking n ≠ 0 here is a strict weakening of the earlier (n : F) ≠ 0 and costs nothing.

Equations

• TauCeti.Isogeny.mulByIntPullbackOfNeZero W hn = TauCeti.Isogeny.mulByIntPullback W ⋯

@[simp]

theorem TauCeti.Isogeny.mulByIntPullback_mk {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (p : Polynomial (Polynomial F)) : (mulByIntPullback W hn) ((WeierstrassCurve.Affine.CoordinateRing.mk W) p) = Polynomial.evalEval (mulByIntX W n) (mulByIntY W n) (Polynomial.map (Polynomial.mapRingHom (algebraMap F W.FunctionField)) p)

The pullback of [n] on an arbitrary class: the class of a bivariate polynomial p goes to p evaluated at (φₙ/ψₙ², ωₙ/ψₙ³) over the function field. This is the general evaluation rule; mulByIntPullback_X and mulByIntPullback_Y are its two special cases.

@[simp]

theorem TauCeti.Isogeny.mulByIntPullback_X {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntPullback W hn) ((AdjoinRoot.of W.polynomial) Polynomial.X) = mulByIntX W n

The pullback of [n] sends the class of X to φₙ/ψₙ².

Stated with AdjoinRoot.of, not algebraMap F[X] W.CoordinateRing, because AdjoinRoot.algebraMap_eq is itself a simp lemma: a goal mentioning the class of X is already normalised this way by the time this fires.

@[simp]

theorem TauCeti.Isogeny.mulByIntPullback_Y {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntPullback W hn) (AdjoinRoot.root W.polynomial) = mulByIntY W n

The pullback of [n] sends the class of Y to ωₙ/ψₙ³.

@[simp]

theorem TauCeti.Isogeny.tautologicalPoint_mulByIntPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntPullback W hn).tautologicalPoint = n • W.genericPoint

The tautological point of [n] is n times the generic point.