Multiplication by n is n times the identity

[n] is built from the division polynomials, while the additive group of morphisms is built from tautological points; this file says the two agree, so that results about the additive structure apply to [n] and results about [n] are available additively.

Read additively, the degree of [n] says that the degree scales quadratically, deg (n • f) = n² · deg f, for every morphism and not just for a multiplication: that is the homogeneity half of the statement that the degree is a quadratic form on Hom W₁ W₂, the form whose non-negativity gives the Hasse bound. The other half, that the associated pairing is additive, is not proved here.

Main results

• TauCeti.Isogeny.ofIsogeny_mulByIntIsogeny: [n] = n • id in Hom W W.
• TauCeti.Isogeny.Hom.degree_zsmul and TauCeti.Isogeny.Hom.degree_nsmul: deg (n • f) = n² · deg f, the degree's homogeneity, for an integer and a natural scalar.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4 for the identification of [n] with n • id, III.6 for the degree as a quadratic form, of which Hom.degree_zsmul is the homogeneity.

@[simp]

theorem TauCeti.Isogeny.ofIsogeny_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : Hom.ofIsogeny (mulByIntIsogeny W hn) = n • Hom.id W

[n] is n times the identity in the additive group of morphisms. The division-polynomial construction of [n] and the additive structure on Hom therefore describe the same map.

@[simp]

theorem TauCeti.Isogeny.Hom.degree_zsmul {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (n : ℤ) (f : Hom W₁ W₂) : (n • f).degree = n.natAbs ^ 2 * f.degree

The degree scales quadratically: deg (n • f) = n² · deg f.

This is the homogeneity half of the degree being a quadratic form on Hom W₁ W₂. It holds with no hypothesis on n or f: at n = 0 and at f = 0 both sides are 0, which is what the value Hom.degree 0 = 0 is stipulated for.

@[simp]

theorem TauCeti.Isogeny.Hom.degree_nsmul {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (n : ℕ) (f : Hom W₁ W₂) : (n • f).degree = n ^ 2 * f.degree

The degree scales quadratically for a natural multiple: deg (n • f) = n² · deg f.

theorem TauCeti.Isogeny.Hom.zsmul_id_injective {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] : Function.Injective fun (n : ℤ) => n • id W₁

Integer multiples of the identity endomorphism are distinct. In particular, the endomorphism ring of an elliptic curve has characteristic zero, independently of the characteristic of its base field.