Factoring multiplication through an isogeny whose kernel counts its degree

The kernel form of the factorisation theorem TauCeti.Isogeny.existsUnique_comp_eq_iff_ker_le applies to [n] with n = deg φ: every point of ker φ is killed by the order of ker φ, which is n, so [n] factors through φ, uniquely. The factor χ : W₂ → W₁ with χ ∘ φ = [deg φ] is the dual of φ (Silverman III.6.1), and its degree is deg φ, by the tower formula and deg [n] = n².

Main results

• TauCeti.Isogeny.existsUnique_comp_eq_mulByIntIsogenyOfNeZero_degree: when #ker φ = deg φ, there is a unique χ with χ ∘ φ = [deg φ].
• TauCeti.Isogeny.degree_eq_of_comp_eq_mulByIntIsogenyOfNeZero_degree: any such χ has degree deg φ.

Provenance

Not ported. The factorisation of [deg φ] and the degree of its factor are the opening construction of the dual isogeny in Silverman III.6.1.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.11 and III.6.1.

theorem TauCeti.Isogeny.existsUnique_comp_eq_mulByIntIsogenyOfNeZero_degree {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} (hφ : Nat.card ↥φ.ker = φ.degree) : ∃! χ : Isogeny W₂ W₁, χ.comp φ = mulByIntIsogenyOfNeZero W₁ ⋯

[deg φ] factors through φ when the kernel of φ has deg φ points. The factor χ : W₂ → W₁ with χ ∘ φ = [deg φ] is unique; it is the dual isogeny of φ (Silverman III.6.1). The kernel of φ is a group of order deg φ, so [deg φ] kills it, and the kernel form of the factorisation theorem applies.

theorem TauCeti.Isogeny.degree_eq_of_comp_eq_mulByIntIsogenyOfNeZero_degree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {χ : Isogeny W₂ W₁} {hn : ↑φ.degree ≠ 0} (h : χ.comp φ = mulByIntIsogenyOfNeZero W₁ hn) : χ.degree = φ.degree

A factor of [deg φ] through φ has the degree of φ: deg χ · deg φ = deg [deg φ], which is (deg φ)². No hypothesis on the kernel of φ is needed.