@[reducible, inline]

noncomputable abbrev DualIsogeny.dualIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : Isogeny E₂ E₁

The dual isogeny α̂ : E₂ → E₁ associated to an isogeny α : E₁ → E₂.

theorem DualIsogeny.dualIsogeny_comp {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : (dualIsogeny α).toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN ↑α.degree

Composing the dual isogeny α̂ after α yields multiplication by deg α on E₁.

theorem DualIsogeny.dualIsogeny_unique {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (β : Isogeny E₂ E₁) (hβ : β.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN ↑α.degree) : β = dualIsogeny α

Uniqueness of the dual isogeny: any β : E₂ → E₁ with β ∘ α = [deg α] on E₁ must equal α̂.

theorem DualIsogeny.comp_dualIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : α.toAddMonoidHom.comp (dualIsogeny α).toAddMonoidHom = E₂.multiplicationByN ↑α.degree

Composing α after its dual α̂ yields multiplication by deg α on E₂.

theorem DualIsogeny.degree_dualIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : (dualIsogeny α).degree = α.degree

The dual isogeny has the same degree as the original isogeny.

theorem DualIsogeny.dualIsogeny_dualIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : (dualIsogeny (dualIsogeny α)).toAddMonoidHom = α.toAddMonoidHom

The dual of the dual recovers the original isogeny as an additive map (involutivity).

theorem DualIsogeny.multiplicationByN_self_dual {F : Type u_1} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (n : ℤ) (hn : n ≠ 0) : (Isogeny.multiplicationByN_isogeny E n hn).dualIsogeny.toAddMonoidHom = E.multiplicationByN n

The multiplication-by-n isogeny is self-dual: its dual is again multiplication by n.

inductive DualIsogenyExt.IsogenyOrZero {F : Type u_1} [Field F] [DecidableEq F] (E₁ E₂ : WeierstrassCurve.Affine F) : Type u_1

An isogeny E₁ → E₂ or the zero map (which is not an isogeny, but is needed to make the set of "isogenies-or-zero" into a monoid).

• zero {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyOrZero E₁ E₂
• ofIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : IsogenyOrZero E₁ E₂

def DualIsogenyExt.IsogenyOrZero.toAddMonoidHom {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyOrZero E₁ E₂ → E₁.Point →+ E₂.Point

Converts an IsogenyOrZero to the underlying additive group homomorphism.

def DualIsogenyExt.IsogenyOrZero.deg {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyOrZero E₁ E₂ → ℕ

The degree of an IsogenyOrZero (zero for the zero map, the degree of the isogeny otherwise).

noncomputable def DualIsogenyExt.IsogenyOrZero.dual {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : IsogenyOrZero E₁ E₂ → IsogenyOrZero E₂ E₁

The dual of an IsogenyOrZero: zero stays zero, an isogeny is sent to its dual.

@[simp]

theorem DualIsogenyExt.IsogenyOrZero.dual_zero {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : zero.dual = zero

The dual of the zero map is the zero map.

@[simp]

theorem DualIsogenyExt.IsogenyOrZero.deg_zero {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} : zero.deg = 0

The degree of the zero map is 0.

@[simp]

theorem DualIsogenyExt.IsogenyOrZero.dual_ofIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : (ofIsogeny α).dual = ofIsogeny α.dualIsogeny

The dual of ofIsogeny α is ofIsogeny α̂.

@[simp]

theorem DualIsogenyExt.IsogenyOrZero.deg_ofIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) : (ofIsogeny α).deg = α.degree

The degree of ofIsogeny α equals the degree of α.

theorem IsogenyDecomposition.isogeny_prime_factor {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : 1 < α.degree) (p : ℕ) (hp : Nat.Prime p) (hdvd : p ∣ α.degree) : ∃ (E_mid : WeierstrassCurve.Affine F) (β : Isogeny E₁ E_mid) (γ : Isogeny E_mid E₂), β.degree = p ∧ 0 < γ.degree ∧ γ.degree * β.degree = α.degree ∧ γ.toAddMonoidHom.comp β.toAddMonoidHom = α.toAddMonoidHom

If an isogeny α has degree > 1 and p is a prime dividing deg α, then α factors through an intermediate curve as α = γ ∘ β with β of degree p.

theorem IsogenyDecomposition.isogeny_prime_degree_decomposition {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : 1 < α.degree) : ∃ (chain : IsogenyChain E₁ E₂), chain.allPrimeDegree ∧ chain.compose = α.toAddMonoidHom

Any isogeny α of degree > 1 decomposes as a chain of isogenies, each of prime degree, whose composition equals α.