Elementary values of the polarised degree

The degree on morphisms of elliptic curves is extended by degree 0 = 0 and is homogeneous of degree two. Mathlib's generic QuadraticMap.polar therefore gives the expression

polar degree f g = deg (f + g) - deg f - deg g.

This file records the values at zero and on the diagonal. Bilinearity is the substantive isogeny theorem; the separable case is proved in Isogeny/Dual/Degree.lean from additivity of the dual.

Main results

• TauCeti.Isogeny.Hom.polar_degree_zero_left and TauCeti.Isogeny.Hom.polar_degree_zero_right: zero is orthogonal to every morphism.
• TauCeti.Isogeny.Hom.polar_degree_self: the diagonal is twice the degree.

References

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

@[simp]

theorem TauCeti.Isogeny.Hom.polar_degree_zero_left {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) : QuadraticMap.polar (fun (g : Hom W₁ W₂) => ↑g.degree) 0 f = 0

The degree polarisation vanishes when its left argument is zero.

@[simp]

theorem TauCeti.Isogeny.Hom.polar_degree_zero_right {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) : QuadraticMap.polar (fun (g : Hom W₁ W₂) => ↑g.degree) f 0 = 0

The degree polarisation vanishes when its right argument is zero.

@[simp]

theorem TauCeti.Isogeny.Hom.polar_degree_self {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) : QuadraticMap.polar (fun (g : Hom W₁ W₂) => ↑g.degree) f f = 2 * ↑f.degree

On the diagonal, the degree polarisation is twice the degree.