The dual isogeny is additive

Let φ, ψ : W₁ → W₂ be separable isogenies of elliptic curves over a separably closed field, and suppose that their sum in the group of morphisms is again a separable isogeny χ. Then the dual of the sum is the sum of the duals: χ̂ = φ̂ + ψ̂ (Silverman III.6.2(b)).

The proof goes through the Weil pairing. For N invertible in the field, the dual is adjoint to the isogeny (TauCeti.Isogeny.weilPairing_eq_weilPairing_dual), so for S ∈ W₁[N] and T ∈ W₂[N]

e_N(S, χ̂ T) = e_N(χ S, T) = e_N(φ S, T) · e_N(ψ S, T) = e_N(S, φ̂ T) · e_N(S, ψ̂ T)
            = e_N(S, φ̂ T + ψ̂ T).

Nondegeneracy of the pairing gives χ̂ T = φ̂ T + ψ̂ T on W₂[N], and two morphisms agreeing on the ℓ-torsion for every prime ℓ other than the characteristic are equal (TauCeti.Isogeny.Hom.ext_pointMap_of_prime_zsmul_eq_zero).

Additivity of the dual is what makes the degree a quadratic form on the morphisms: writing [m] for the multiplication-by-m endomorphism, f̂ ∘ f = [deg f], so the pairing (f, g) ↦ f̂ ∘ g + ĝ ∘ f = [deg (f + g) − deg f − deg g] is bilinear exactly because the dual is additive (Silverman III.6.3). Silverman proves the additivity by the Picard-group description of the dual; the argument here replaces it with the Weil pairing, whose compatibility with the dual (Silverman III.8.2) is already available.

Main result

• TauCeti.Isogeny.ofIsogeny_dual_add: if χ = φ + ψ as morphisms, then χ̂ = φ̂ + ψ̂.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.2(b), III.6.3 and III.8.2.

theorem TauCeti.Isogeny.ofIsogeny_dual_add {F : Type u_1} [Field F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ ψ χ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] [Algebra.IsSeparable (↥ψ.fieldPullback.fieldRange) W₁.FunctionField] [Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) W₁.FunctionField] (hχ : Hom.ofIsogeny χ = Hom.ofIsogeny φ + Hom.ofIsogeny ψ) : Hom.ofIsogeny χ.dual = Hom.ofIsogeny φ.dual + Hom.ofIsogeny ψ.dual

The dual isogeny is additive (Silverman III.6.2(b)): if the separable isogenies φ and ψ sum, as morphisms, to the separable isogeny χ, then χ̂ = φ̂ + ψ̂.