Multiplication by n under base change

Multiplication by n is defined by the same division polynomials over every field, and the division polynomials of W.map f are those of W with f applied to their coefficients (WeierstrassCurve.map_ψ, WeierstrassCurve.map_φ, WeierstrassCurve.map_ω). So carrying the isogeny [n] of W along a homomorphism f : F →+* K of the base field gives the isogeny [n] of W.map f. This is what lets a statement about [n] over F be read over an extension, where more points are available: over an algebraic closure its kernel is the whole geometric n-torsion.

Main results

• TauCeti.Isogeny.map_psiFunctionField, TauCeti.Isogeny.map_phiFunctionField and TauCeti.Isogeny.map_omegaFunctionField: the division polynomials at the generic point are carried to those of W.map f.
• TauCeti.Isogeny.map_mulByIntX and TauCeti.Isogeny.map_mulByIntY: so are the coordinates of [n] at the generic point.
• TauCeti.Isogeny.mulByIntIsogeny_map: the base change of [n] is [n].

References

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

@[simp]

theorem TauCeti.Isogeny.map_psiFunctionField {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) (n : ℤ) : (WeierstrassCurve.Affine.FunctionField.map W f) (psiFunctionField W n) = psiFunctionField (W.map f) n

ψₙ at the generic point is carried to ψₙ of W.map f.

@[simp]

theorem TauCeti.Isogeny.map_phiFunctionField {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) (n : ℤ) : (WeierstrassCurve.Affine.FunctionField.map W f) (phiFunctionField W n) = phiFunctionField (W.map f) n

φₙ at the generic point is carried to φₙ of W.map f.

@[simp]

theorem TauCeti.Isogeny.map_omegaFunctionField {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) (n : ℤ) : (WeierstrassCurve.Affine.FunctionField.map W f) (omegaFunctionField W n) = omegaFunctionField (W.map f) n

ωₙ at the generic point is carried to ωₙ of W.map f.

@[simp]

theorem TauCeti.Isogeny.map_mulByIntX {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) (n : ℤ) : (WeierstrassCurve.Affine.FunctionField.map W f) (mulByIntX W n) = mulByIntX (W.map f) n

The x-coordinate φₙ / ψₙ² of [n] is carried to that of W.map f.

@[simp]

theorem TauCeti.Isogeny.map_mulByIntY {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) (n : ℤ) : (WeierstrassCurve.Affine.FunctionField.map W f) (mulByIntY W n) = mulByIntY (W.map f) n

The y-coordinate ωₙ / ψₙ³ of [n] is carried to that of W.map f.

@[simp]

theorem TauCeti.Isogeny.mulByIntIsogeny_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).map f = mulByIntIsogeny (W.map f) ⋯

The base change of [n] is [n]: carrying multiplication by n on W along f gives multiplication by n on W.map f. The nonvanishing of ψₙ over K is that over F, carried along the injective map FunctionField.map W f.