The endomorphism ring of an elliptic curve

Composition of morphisms of elliptic curves is additive in the outer morphism by construction (TauCeti.Isogeny.Hom.add_comp), the sum of morphisms being computed on their tautological points. This file proves that it is additive in the inner morphism as well, over every field, so that composition is biadditive and the endomorphisms Hom W W of an elliptic curve form a ring (Silverman III.4).

Additivity in the inner morphism is a statement about points: two morphisms are equal once they agree on infinitely many points, so over a separably closed field h ∘ (f + g) = h ∘ f + h ∘ g follows once h acts additively on points (TauCeti.Isogeny.Hom.comp_add_of_pointMap_add). That every morphism acts additively on points is Silverman III.4.8. A separable isogeny over a separably closed field acts through the class-group point map, which is additive by construction (TauCeti.Isogeny.Hom.pointMap_ofIsogeny_eq_toPointHom). Every isogeny factors as a separable one after a Frobenius power F^r : W → W⁽ᵖʳ⁾ (Silverman II.2.12), and F^r sends (x, y) to (x ^ p ^ r, y ^ p ^ r) (TauCeti.Isogeny.pointMap_iterateRelativeFrobeniusIsogeny), which is additive because the Frobenius of the field is a ring homomorphism. Over an arbitrary field, both additivity statements are compared after base change to a separable closure: on points, which embed additively and compatibly with the action of morphisms (TauCeti.Isogeny.Hom.pointMap_map), and on morphisms, along the faithful, additive base change (TauCeti.Isogeny.Hom.map_injective).

Main results

• TauCeti.Isogeny.Hom.pointMap_add: every morphism acts additively on points, over any field (Silverman III.4.8), with pointMap_neg, pointMap_sub, pointMap_nsmul and pointMap_zsmul.
• TauCeti.Isogeny.Hom.comp_add: composition is additive in the inner morphism, over any field.
• TauCeti.Isogeny.Hom.compLeftHom: postcomposition by a morphism, as an additive homomorphism.
• The Ring (Hom W W) and IsDomain (Hom W W) instances.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.11–12 and III.4.

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_add {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (P Q : W₁.Point) : f.pointMap (P + Q) = f.pointMap P + f.pointMap Q

Every morphism of elliptic curves acts additively on points (Silverman III.4.8).

noncomputable def TauCeti.Isogeny.Hom.pointMapHom {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) : W₁.Point →+ W₂.Point

The action of a morphism on points, as a homomorphism of point groups.

Equations

• f.pointMapHom = AddMonoidHom.mk' f.pointMap ⋯

@[simp]

theorem TauCeti.Isogeny.Hom.pointMapHom_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (P : W₁.Point) : f.pointMapHom P = f.pointMap P

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_neg {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (P : W₁.Point) : f.pointMap (-P) = -f.pointMap P

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_sub {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (P Q : W₁.Point) : f.pointMap (P - Q) = f.pointMap P - f.pointMap Q

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_nsmul {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (n : ℕ) (P : W₁.Point) : f.pointMap (n • P) = n • f.pointMap P

Every morphism commutes with natural multiples of points.

@[simp]

theorem TauCeti.Isogeny.Hom.pointMap_zsmul {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [DecidableEq F] (f : Hom W₁ W₂) (n : ℤ) (P : W₁.Point) : f.pointMap (n • P) = n • f.pointMap P

Every morphism commutes with integer multiples of points.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_add {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (f g : Hom W₁ W₂) : h.comp (f + g) = h.comp f + h.comp g

Composition is additive in the inner morphism, over any field.

noncomputable def TauCeti.Isogeny.Hom.compLeftHom {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) : Hom W₁ W₂ →+ Hom W₁ W₃

Postcomposition by h, as a homomorphism of the additive groups of morphisms.

Equations

• h.compLeftHom = AddMonoidHom.mk' h.comp ⋯

@[simp]

theorem TauCeti.Isogeny.Hom.compLeftHom_apply {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (f : Hom W₁ W₂) : h.compLeftHom f = h.comp f

@[simp]

theorem TauCeti.Isogeny.Hom.comp_neg {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (f : Hom W₁ W₂) : h.comp (-f) = -h.comp f

Composition commutes with negation in the inner morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_sub {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (f g : Hom W₁ W₂) : h.comp (f - g) = h.comp f - h.comp g

Composition respects subtraction in the inner morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_zsmul {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (n : ℤ) (f : Hom W₁ W₂) : h.comp (n • f) = n • h.comp f

Composition is ℤ-linear in the inner morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.comp_nsmul {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (h : Hom W₂ W₃) (n : ℕ) (f : Hom W₁ W₂) : h.comp (n • f) = n • h.comp f

Composition is ℕ-linear in the inner morphism, the rule for a natural scalar.

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instRing {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] : Ring (Hom W₁ W₁)

The endomorphisms of an elliptic curve form a ring, with addition the group law on morphisms and multiplication composition (Silverman III.4).

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.Isogeny.Hom.instIsDomain {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] : IsDomain (Hom W₁ W₁)

The endomorphism ring of an elliptic curve is a domain: a composite of isogenies is an isogeny.