Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.MulByInt.Comp

The multiplication isogenies compose: [m] ∘ [n] = [m n] #

On an elliptic curve W, the multiplication isogeny [n] is defined for those n whose division polynomial ψₙ does not vanish at the generic point — by psiFunctionField_ne_zero_of_Δ_ne_zero, every n ≠ 0. For such integers this file proves [m] ∘ [n] = [m n], together with the degenerate cases [1] = id and [-1] = negIsogeny, and that [m] = [n] only if m = n. Each identity carries the ψ-nonvanishing hypotheses it needs; the two composition laws are recorded a second time in the mulByIntIsogenyOfNeZero form, where the hypothesis on the composite index — m n, resp. -n — is discharged from the discriminant instead of assumed.

[0] is not among the isogenies compared: ψ₀ = 0, so mulByIntIsogeny is undefined there, and the distinctness statements range only over the integers at which [·] is defined.

Distinctness rests on the generic point of W having infinite order, as established in MulByInt/GenericPoint.lean.

Main results #

References #

source
@[simp]
theorem TauCeti.Isogeny.mulByIntIsogeny_one {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (h₁ : psiFunctionField W 1 ≠ 0) :
mulByIntIsogeny W h₁ = id W

[1] is the identity isogeny.

source
@[simp]
theorem TauCeti.Isogeny.mulByIntIsogeny_comp_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {m n : ℤ} (hm : psiFunctionField W m ≠ 0) (hn : psiFunctionField W n ≠ 0) (hmn : psiFunctionField W (m * n) ≠ 0) :
(mulByIntIsogeny W hm).comp (mulByIntIsogeny W hn) = mulByIntIsogeny W hmn

Multiplication isogenies compose: [m] ∘ [n] = [m n].

source
@[simp]
theorem TauCeti.Isogeny.mulByIntIsogenyOfNeZero_comp_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) :
(mulByIntIsogenyOfNeZero W hm).comp (mulByIntIsogenyOfNeZero W hn) = mulByIntIsogenyOfNeZero W ⋯

[m] ∘ [n] = [m n] for nonzero m and n, the non-vanishing hypotheses discharged from the discriminant as in mulByIntIsogenyOfNeZero.

source
@[simp]
theorem TauCeti.Isogeny.mulByIntIsogeny_neg_one {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (h : psiFunctionField W (-1) ≠ 0) :
mulByIntIsogeny W h = negIsogeny W

[-1] is the negation isogeny.

source
@[simp]
theorem TauCeti.Isogeny.negIsogeny_comp_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (hneg : psiFunctionField W (-n) ≠ 0) :
(negIsogeny W).comp (mulByIntIsogeny W hn) = mulByIntIsogeny W hneg

[-n] is [n] followed by negation: the case m = -1 of [m] ∘ [n] = [m n], read through [-1] = negIsogeny.

source
@[simp]
theorem TauCeti.Isogeny.negIsogeny_comp_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) :
(negIsogeny W).comp (mulByIntIsogenyOfNeZero W hn) = mulByIntIsogenyOfNeZero W ⋯

[-n] is [n] followed by negation, for nonzero n, the non-vanishing hypotheses discharged from the discriminant as in mulByIntIsogenyOfNeZero.

source
@[simp]
theorem TauCeti.Isogeny.mulByIntIsogeny_inj {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {m n : ℤ} (hm : psiFunctionField W m ≠ 0) (hn : psiFunctionField W n ≠ 0) :
mulByIntIsogeny W hm = mulByIntIsogeny W hn ↔ m = n

The multiplication isogenies are pairwise distinct: [m] = [n] exactly when m = n, for the integers m, n at which [·] is defined.