Degree polarisation for separable isogenies #
For separable isogenies φ, ψ : W₁ → W₂ over a separably closed field, the symmetric
cross-composite
φ̂ ∘ ψ + ψ̂ ∘ φ
is the polarisation of the degree. More precisely, if the sum φ + ψ is represented by a
separable isogeny χ, then
φ̂ ∘ ψ + ψ̂ ∘ φ = [deg χ − deg φ − deg ψ].
This is the separable part of the quadraticity of the degree on the group of morphisms (Silverman III.6.3). The cross-composite is additive in either variable whenever the relevant sum is again a separable isogeny. These identities isolate the algebraic step used to construct the bilinear degree pairing once the dual is available for arbitrary, possibly inseparable, isogenies.
Main results #
TauCeti.Isogeny.ofIsogeny_dual_comp_add_dual_comp_eq_polar_degree: the symmetric cross-composite is multiplication by the degree polarisation.TauCeti.Isogeny.ofIsogeny_dual_comp_add_dual_comp_add_rightandTauCeti.Isogeny.ofIsogeny_dual_comp_add_dual_comp_add_left: the cross-composite is additive in each variable on separable sums.TauCeti.Isogeny.polar_degree_add_right_of_isSeparableandTauCeti.Isogeny.polar_degree_add_left_of_isSeparable: the resulting numerical polarisation is additive on separable sums.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, III.6.2–3.
The symmetric dual composite is the polarisation of the degree. If the separable
isogeny χ represents the sum φ + ψ, then
φ̂ ∘ ψ + ψ̂ ∘ φ = [deg χ − deg φ − deg ψ] (Silverman III.6.3).
The symmetric dual composite is additive in the right variable on separable isogenies:
if η = ψ + ρ, then
φ̂ ∘ η + η̂ ∘ φ = (φ̂ ∘ ψ + ψ̂ ∘ φ) + (φ̂ ∘ ρ + ρ̂ ∘ φ).
The symmetric dual composite is additive in the left variable on separable isogenies.
This is the left-variable form of
ofIsogeny_dual_comp_add_dual_comp_add_right.
The numerical degree polarisation is additive in the right variable whenever all four sums involved are represented by separable isogenies. This is the integer-valued consequence of the two cross-composite identities above.
The numerical degree polarisation is additive in the left variable whenever all four sums involved are represented by separable isogenies.