[n] maps infinity to infinity

Isogeny/MulByInt/Basic.lean builds the coordinate pullback of [n] and records that the MapsInfinity condition — and so [n] as an Isogeny W W — is not proved there. This file proves it, for every n with ψₙ nonvanishing at the generic point.

The argument

CoordinatePullback.mapsInfinity_iff_isIntegralElem_genericX reduces pointedness to a single integral witness, so all that is [n]-specific is the generic x-coordinate: [n]*x · ΨSqₙ(x) = Φₙ(x) makes it a root of Φₙ − C ([n]*x) * ΨSqₙ, monic by monic_Φ_sub_C_mul_ΨSq, with [n]*x the pullback of the class of X.

Main results

• TauCeti.Isogeny.mapsInfinity_mulByIntPullback: the pullback of [n] maps infinity to infinity.
• TauCeti.Isogeny.mulByIntIsogeny: [n] as an Isogeny W W.
• TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_genericX and TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_genericY: the pullback of [n] sends the generic coordinates to [n]*x and [n]*y.
• TauCeti.Isogeny.mulByIntX_sub_algebraMap_ne_zero: [n]*x is not a constant — the transcendence of the generic coordinate, carried across the pullback.
• TauCeti.Isogeny.map_mulByIntIsogeny_genericPoint: the function-field map of [n] carries the generic point to n • the generic point.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.

Provenance

The integral witness is adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0) pinned at 513e83879e2f8cbc626eb9e04d660e92be16ccba, HasseWeil/MulByIntPullback.lean, declaration mulByInt_x_transcendental, which builds the same polynomial Φₙ.map (algebraMap F S) − C c * ΨSqₙ.map (algebraMap F S) and the same root step, there to contradict transcendence of the generic x-coordinate rather than to establish MapsInfinity. Its monicity half is already in this repository as monic_Φ_sub_C_mul_ΨSq, itself ported from that project's NagellLutz.

The MapsInfinity packaging is not from that source and has no counterpart in it: its Isogeny carries a function-field AlgHom obtained by localizing an injective coordinate homomorphism, with no pointedness field, so it never needs the y-coordinate step or the reduction to the two coordinates.

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

The pullback of [n] maps infinity to infinity, so [n] is an isogeny.

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

Multiplication by n as an isogeny, for every n whose division polynomial does not vanish at the generic point.

Equations

• TauCeti.Isogeny.mulByIntIsogeny W hn = { pullback := TauCeti.Isogeny.mulByIntPullback W hn, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.mulByIntIsogeny_pullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).pullback = mulByIntPullback W hn

@[simp]

theorem TauCeti.Isogeny.map_mulByIntIsogeny_genericPoint {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (WeierstrassCurve.Affine.Point.map (mulByIntIsogeny W hn).fieldPullback) W.genericPoint = n • W.genericPoint

The function-field map of [n] carries the generic point to its n-th multiple.

@[reducible, inline]

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

Multiplication by n as an isogeny, for every n ≠ 0, the non-vanishing hypothesis discharged by psiFunctionField_ne_zero_of_Δ_ne_zero as in mulByIntPullbackOfNeZero.

Equations

• TauCeti.Isogeny.mulByIntIsogenyOfNeZero W hn = TauCeti.Isogeny.mulByIntIsogeny W ⋯

@[simp]

theorem TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_genericX {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).fieldPullback W.genericX = mulByIntX W n

The pullback of [n] sends the generic x to [n]*x.

Not the same statement as fieldPullback_mulByIntIsogeny_X, which the degree tower needs and which lands in F(x) as a quotient of RatFunc F; this is the mulByIntX form, which is what a computation in F(W) wants, as in mulByIntX_sub_algebraMap_ne_zero below and in the place and Wronskian computations downstream.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_genericY {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).fieldPullback W.genericY = mulByIntY W n

The pullback of [n] sends the generic y to [n]*y, the companion of fieldPullback_mulByIntIsogeny_genericX for the second coordinate.

theorem TauCeti.Isogeny.mulByIntX_sub_algebraMap_ne_zero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (x : F) : mulByIntX W n - (algebraMap F W.FunctionField) x ≠ 0

[n]*x is not a constant: it is the image of the generic coordinate under an injective map, and the generic coordinate is not a constant.