Documentation

Atlas.EllipticCurves.code.TorsionEndomorphism

The multiplication-by-n endomorphism [n] on the group of points of a Weierstrass curve, packaged as an additive group homomorphism W.Point →+ W.Point.

Instances For
    @[simp]
    theorem WeierstrassCurve.Affine.multiplicationByN_apply {F : Type u} [Field F] [DecidableEq F] (W : Affine F) (n : ) (P : W.Point) :
    (W.multiplicationByN n) P = n P

    Evaluating the multiplication-by-n map at a point P is the same as the integer scalar multiple n • P.

    The n-torsion subgroup E[n] of a Weierstrass curve, defined as the kernel of the multiplication-by-n homomorphism.

    Instances For
      @[simp]
      theorem WeierstrassCurve.Affine.mem_torsionSubgroup {F : Type u} [Field F] [DecidableEq F] (W : Affine F) (n : ) (P : W.Point) :

      A point P lies in E[n] if and only if n • P = 0.

      theorem WeierstrassCurve.Affine.map_mem_torsionSubgroup {F : Type u} [Field F] [DecidableEq F] {W₁ W₂ : Affine F} (φ : W₁.Point →+ W₂.Point) (n : ) (P : W₁.Point) (hP : P W₁.torsionSubgroup n) :
      φ P W₂.torsionSubgroup n

      Any additive group homomorphism between point groups of Weierstrass curves preserves the n-torsion subgroup.

      A Weierstrass curve W over a field of characteristic p is ordinary if its p-torsion E[p] is isomorphic to ℤ/pℤ (cf. Definition 6.2 of Sutherland).

      Instances For

        A Weierstrass curve W over a field of characteristic p is supersingular if its p-torsion E[p] is trivial (cf. Definition 6.2 of Sutherland).

        Instances For
          theorem WeierstrassCurve.Affine.IsSupersingular.torsion_eq_zero {F : Type u} [Field F] [DecidableEq F] {W : Affine F} {p : } [CharP F p] [Fact (Nat.Prime p)] (h : W.IsSupersingular p) (P : W.Point) (hP : p P = 0) :
          P = 0

          For a supersingular curve, any point killed by multiplication by p is the zero point.

          theorem WeierstrassCurve.Affine.isSupersingular_iff {F : Type u} [Field F] [DecidableEq F] {W : Affine F} {p : } [CharP F p] [Fact (Nat.Prime p)] :
          W.IsSupersingular p ∀ (P : W.Point), p P = 0P = 0

          A curve is supersingular if and only if multiplication by p is injective on its group of points.

          theorem WeierstrassCurve.Affine.multiplicationByN_comp_hom {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : Affine F} (α : E₁.Point →+ E₂.Point) (n : ) :

          Multiplication-by-n is natural with respect to additive group homomorphisms between point groups: [n] ∘ α = α ∘ [n] (cf. Proposition 6.5 of Sutherland).

          theorem WeierstrassCurve.Affine.multiplicationByN_comm_hom_apply {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : Affine F} (α : E₁.Point →+ E₂.Point) (n : ) (P : E₁.Point) :
          n α P = α (n P)

          The pointwise version of multiplicationByN_comp_hom: n • (α P) = α (n • P).

          theorem WeierstrassCurve.Affine.Isogeny.zsmul_ne_zero {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : Affine F} (φ : Isogeny E₁ E₂) (n : ) (hn : n 0) :

          A nonzero integer multiple of a (nonzero) isogeny remains a nonzero homomorphism; expresses the torsion-freeness of Hom(E₁, E₂) as a -module.

          theorem WeierstrassCurve.Affine.hom_torsion_free {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : Affine F} (α : E₁.Point →+ E₂.Point) (n : ) (hn : n 0) (h : n α = 0) :
          α = 0

          The -module Hom(E₁, E₂) is torsion-free: if n • α = 0 for some nonzero n, then α = 0.

          The -rank of Hom(E₁, E₂) is at most 4, a classical structural fact for the homomorphism group between two elliptic curves.

          theorem WeierstrassCurve.Affine.Isogeny.right_cancel {F : Type u} [Field F] [DecidableEq F] {E₀ E₁ E₂ : Affine F} (α β : Isogeny E₁ E₂) (γ : Isogeny E₀ E₁) (h : α.toAddMonoidHom.comp γ.toAddMonoidHom = β.toAddMonoidHom.comp γ.toAddMonoidHom) :

          Right-cancellation for isogenies (one half of Lemma 6.6): if α ∘ γ = β ∘ γ with γ an isogeny (hence surjective), then α = β as homomorphisms.

          theorem WeierstrassCurve.Affine.Isogeny.comp_nonzero_of_nonzero {F : Type u} [Field F] [DecidableEq F] {E₀ E₁ E₂ : Affine F} (δ : Isogeny E₁ E₂) (f : E₀.Point →+ E₁.Point) (hf : f 0) :

          An isogeny composed with a nonzero homomorphism is itself nonzero: pre-composition by an isogeny δ reflects nonzeroness of homomorphisms.

          theorem WeierstrassCurve.Affine.Isogeny.left_cancel {F : Type u} [Field F] [DecidableEq F] {E₀ E₁ E₂ : Affine F} (δ : Isogeny E₁ E₂) (α β : Isogeny E₀ E₁) (h : δ.toAddMonoidHom.comp α.toAddMonoidHom = δ.toAddMonoidHom.comp β.toAddMonoidHom) :

          Left-cancellation for isogenies (the other half of Lemma 6.6): if δ ∘ α = δ ∘ β with δ an isogeny, then α = β as homomorphisms.

          noncomputable def EllipticCurve.torsionSubgroup (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] (n : ) :

          The n-torsion subgroup E(K)[n] of an elliptic curve E/k after base change to a field extension K, defined as the torsion subgroup of the projective point group.

          Instances For
            @[simp]
            theorem EllipticCurve.mem_torsionSubgroup (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] (n : ) (P : (E.map (algebraMap k K)).toProjective.Point) :
            P torsionSubgroup k E K n n P = 0

            Membership characterisation: a point P ∈ E(K) lies in E(K)[n] iff n • P = 0.

            noncomputable def EllipticCurve.torsionSubgroup_fintype (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (n : ) (hn : 0 < n) (hcop : n.Coprime (ringChar k)) :
            Fintype (torsionSubgroup k E K n)

            Over an algebraically closed field K, when n is coprime to the characteristic, the n-torsion E(K)[n] is finite — a Fintype instance underlying Theorem 6.1.

            Instances For
              theorem EllipticCurve.torsionSubgroup_card (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (n : ) (hn : 0 < n) (hcop : n.Coprime (ringChar k)) :
              Fintype.card (torsionSubgroup k E K n) = n ^ 2

              Theorem 6.1 (cardinality part): over an algebraically closed field K, if n is coprime to char k, then #E(K)[n] = n².

              theorem addCommGroup_sq_card_killed_by_equiv_prod (G : Type u_1) [AddCommGroup G] [Fintype G] (n : ) (hn : 0 < n) (hcard : Fintype.card G = n ^ 2) (hkill : ∀ (x : G), n x = 0) :

              A finite abelian group of order whose every element is killed by n is isomorphic to (ℤ/nℤ)². Used as a structural step toward Theorem 6.1.

              theorem EllipticCurve.torsion_equiv_zmod_prod (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (n : ) (hn : 0 < n) (hcop : n.Coprime (ringChar k)) :
              Nonempty ((torsionSubgroup k E K n) ≃+ ZMod n × ZMod n)

              Theorem 6.1 (structure part): over an algebraically closed K, when n is coprime to char k, the n-torsion is E(K)[n] ≃ ℤ/nℤ ⊕ ℤ/nℤ.

              theorem EllipticCurve.torsion_p_dichotomy (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (p : ) [CharP k p] [Fact (Nat.Prime p)] :
              Nonempty ((torsionSubgroup k E K p) ≃+ ZMod p) torsionSubgroup k E K p =

              Theorem 6.1 (characteristic-p part): over an alg. closed K, the p-torsion is either ℤ/pℤ (ordinary case) or trivial (supersingular case).

              theorem EllipticCurve.mulByInt_surjective (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (n : ) (hn : n 0) :

              Over an algebraically closed field, multiplication-by-n (for n ≠ 0) is surjective on the group of points of an elliptic curve.

              theorem EllipticCurve.torsion_prime_char_supersingular (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (p : ) [CharP k p] [Fact (Nat.Prime p)] (e : ) (he : 0 < e) (hss : torsionSubgroup k E K p = ) :
              torsionSubgroup k E K (p ^ e) =

              Supersingularity is preserved under powers of p: if E[p] = 0 then E[pᵉ] = 0 for all e ≥ 1.

              theorem EllipticCurve.torsion_prime_char_ordinary (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (p : ) [CharP k p] [Fact (Nat.Prime p)] (e : ) (he : 0 < e) (hord : Nonempty ((torsionSubgroup k E K p) ≃+ ZMod p)) :
              Nonempty ((torsionSubgroup k E K (p ^ e)) ≃+ ZMod (p ^ e))

              Ordinarity propagates to powers of p: if E[p] ≃ ℤ/pℤ then E[pᵉ] ≃ ℤ/pᵉℤ.

              theorem EllipticCurve.finite_subgroup_two_cyclic (k : Type u_1) [Field k] (E : WeierstrassCurve k) [E.IsElliptic] (K : Type u_2) [Field K] [Algebra k K] [IsAlgClosed K] (T : AddSubgroup (E.map (algebraMap k K)).toProjective.Point) [Fintype T] :
              ∃ (m₁ : ) (m₂ : ), 0 < m₁ 0 < m₂ m₁ m₂ Nonempty (T ≃+ ZMod m₁ × ZMod m₂) (¬ringChar k m₁ ¬ringChar k m₂)

              Corollary 6.4 (subgroup form): any finite subgroup of E(K̄) is a direct sum of (at most) two cyclic groups, only one of which can have order divisible by char k.

              theorem EllipticCurve.finite_field_group_structure (k : Type u_1) [Field k] [Fintype k] (E : WeierstrassCurve k) [E.IsElliptic] [Fintype E.toProjective.Point] (p : ) [CharP k p] [Fact (Nat.Prime p)] :
              ∃ (n₂ : ) (n₁ : ), 0 < n₂ 0 < n₁ n₂ n₁ ¬p n₂ Nonempty (E.toProjective.Point ≃+ ZMod n₁ × ZMod n₂)

              Corollary 6.4 (finite field form): for E/𝔽_q of characteristic p, E(𝔽_q) ≃ ℤ/n₁ℤ ⊕ ℤ/n₂ℤ with n₂ ∣ n₁ and p ∤ n₂.

              @[simp]
              theorem Isogeny.degree_comp {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (ψ : Isogeny E₂ E₃) (φ : Isogeny E₁ E₂) :
              (ψ.comp φ).degree = ψ.degree * φ.degree

              The degree of a composition of isogenies is the product of the degrees: deg(ψ ∘ φ) = deg ψ · deg φ.

              theorem Isogeny.degree_eq_of_toAddMonoidHom_eq {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α β : Isogeny E₁ E₂) (h : α.toAddMonoidHom = β.toAddMonoidHom) :

              Two isogenies with the same underlying additive map must have the same degree (since the degree is determined by the kernel/map data).

              theorem Isogeny.kernel_le_torsion {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) :

              The kernel of an isogeny α is contained in the kernel of multiplication-by-deg α; this is a key step toward the construction of the dual isogeny (Theorem 6.7).

              theorem Isogeny.ker_eq_bot_of_degree_one {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : α.degree = 1) :

              A degree-1 isogeny has trivial kernel.

              theorem Isogeny.injective_of_degree_one {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : α.degree = 1) :

              A degree-1 isogeny is injective on points.

              theorem Isogeny.dual_exists_degree_one {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : α.degree = 1) :
              ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree

              Existence of the dual for a degree-1 isogeny: a degree-1 isogeny is an isomorphism and its inverse plays the role of the dual (cf. Theorem 6.7).

              theorem Isogeny.exists_quotient_of_prime_dividing_degree {F : Type u} [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), β.degree = p β.toAddMonoidHom.ker α.toAddMonoidHom.ker

              If p is a prime dividing the degree of an isogeny α : E₁ → E₂ of degree > 1, then there exists an intermediate curve and a degree-p quotient isogeny β : E₁ → E_mid whose kernel is contained in that of α.

              theorem Isogeny.prime_factor_aux {F : Type u} [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

              For any prime divisor p of deg α (with deg α > 1), one can factor α = γ ∘ β with deg β = p and the degrees multiplying to deg α.

              theorem Isogeny.factor_prime {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hdeg : 1 < α.degree) (hcomp : ¬Nat.Prime α.degree) :
              ∃ (E_mid : WeierstrassCurve.Affine F) (β : Isogeny E₁ E_mid) (γ : Isogeny E_mid E₂), 0 < β.degree 0 < γ.degree γ.degree * β.degree = α.degree γ.toAddMonoidHom.comp β.toAddMonoidHom = α.toAddMonoidHom β.degree < α.degree γ.degree < α.degree

              A composite-degree isogeny can be properly factored: if deg α > 1 is not prime, then α = γ ∘ β with both β and γ of degree strictly less than deg α.

              theorem Isogeny.dual_exists_of_comp {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E_mid : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (β : Isogeny E₁ E_mid) (γ : Isogeny E_mid E₂) (hcomp : γ.toAddMonoidHom.comp β.toAddMonoidHom = α.toAddMonoidHom) (hdeg : γ.degree * β.degree = α.degree) (hβ_dual : ∃ (βd : Isogeny E_mid E₁), βd.toAddMonoidHom.comp β.toAddMonoidHom = E₁.multiplicationByN β.degree) (hγ_dual : ∃ (γd : Isogeny E₂ E_mid), γd.toAddMonoidHom.comp γ.toAddMonoidHom = E_mid.multiplicationByN γ.degree) :
              ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree

              Existence of the dual via composition: if α factors as γ ∘ β with duals existing for both β and γ, then a dual exists for α (used in the inductive proof of 6.7).

              Multiplication-by-n is surjective on the points of a Weierstrass curve when n ≠ 0.

              noncomputable def Isogeny.multiplicationByN_isogeny {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (n : ) (hn : n 0) :

              Package multiplication-by-n as an Isogeny E E of degree .

              Instances For

                The underlying additive homomorphism of the packaged multiplication-by-n isogeny is exactly multiplicationByN E n.

                theorem Isogeny.degree_multiplicationByN {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (φ : Isogeny E E) (n : ) (hn : n 0) (h : φ.toAddMonoidHom = E.multiplicationByN n) :
                φ.degree = n.natAbs ^ 2

                Any self-isogeny whose underlying map is multiplicationByN E n has degree .

                theorem Isogeny.factor_through_kernel {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) (ψ : Isogeny E₁ E₃) (hker : φ.toAddMonoidHom.ker ψ.toAddMonoidHom.ker) :
                ∃ (lam : Isogeny E₂ E₃), lam.toAddMonoidHom.comp φ.toAddMonoidHom = ψ.toAddMonoidHom

                Factoring through the kernel: if ker φ ⊆ ker ψ, then ψ factors as λ ∘ φ for some isogeny λ (existence statement).

                theorem Isogeny.dual_exists_prime_degree {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (hp : Nat.Prime α.degree) :
                ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree

                Existence of the dual for a prime-degree isogeny: when deg α is prime, the dual exists, by factoring [deg α] through α.

                theorem Isogeny.dual_exists {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) :
                ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree

                Theorem 6.7 (existence): for every isogeny α : E₁ → E₂ there exists an isogeny α̂ : E₂ → E₁ satisfying α̂ ∘ α = [deg α]. Proven by strong induction on degree.

                theorem Isogeny.dual_unique {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (αd₁ αd₂ : Isogeny E₂ E₁) (h₁ : αd₁.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree) (h₂ : αd₂.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree) :

                Uniqueness of the dual at the homomorphism level (cf. Theorem 6.7): any two isogenies αd₁, αd₂ satisfying the defining equation of the dual agree as homomorphisms.

                theorem Isogeny.dual_exists_unique {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) :
                ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree ∀ (β : Isogeny E₂ E₁), β.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degreeβ.toAddMonoidHom = αd.toAddMonoidHom

                Theorem 6.7 in existence-and-uniqueness form: there is a unique-up-to-toAddMonoidHom isogeny α̂ satisfying α̂ ∘ α = [deg α].

                theorem Isogeny.ext {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} {α β : Isogeny E₁ E₂} (h_hom : α.toAddMonoidHom = β.toAddMonoidHom) (h_deg : α.degree = β.degree) :
                α = β

                Extensionality for Isogeny: two isogenies are equal if their underlying homs and degrees agree.

                theorem Isogeny.ext_iff {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} {α β : Isogeny E₁ E₂} :
                theorem Isogeny.degree_of_dual_property {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (β : Isogeny E₂ E₁) ( : β.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree) :

                Any isogeny β satisfying the dual equation β ∘ α = [deg α] automatically has deg β = deg α — using deg(β ∘ α) = (deg α)².

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

                Definition 6.8: the dual isogeny α̂ of α, obtained by choosing a witness from α.dual_exists.

                Instances For

                  Defining property of the dual isogeny (Definition 6.8): α̂ ∘ α = [deg α].

                  theorem Isogeny.dualIsogeny_comp_apply {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (P : E₁.Point) :

                  Pointwise form of Isogeny.dualIsogeny_comp: α̂(α(P)) = (deg α) • P.

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

                  Uniqueness of the dual at the homomorphism level: any β : E₂ → E₁ with β ∘ α = [deg α] agrees as a hom with α.dualIsogeny.

                  theorem Isogeny.degree_dualIsogeny {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) :

                  The dual isogeny has the same degree as the original (part of Lemma 6.10).

                  theorem Isogeny.dual_exists_unique_isogeny {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) :
                  ∃ (αd : Isogeny E₂ E₁), αd.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degree ∀ (β : Isogeny E₂ E₁), β.toAddMonoidHom.comp α.toAddMonoidHom = E₁.multiplicationByN α.degreeβ = αd

                  Strengthened existence-and-uniqueness of the dual as an Isogeny (not just at the toAddMonoidHom level), using Isogeny.ext and degree_dualIsogeny.

                  The other half of Lemma 6.10: α ∘ α̂ = [deg α] on E₂, obtained by right-cancelling through α.

                  theorem Isogeny.comp_dualIsogeny_apply {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (α : Isogeny E₁ E₂) (Q : E₂.Point) :

                  Pointwise form of α ∘ α̂ = [deg α]: α(α̂(Q)) = (deg α) • Q.

                  The dual of the dual recovers the original (α̂̂ = α, part of Lemma 6.10).

                  Lemma 6.10 (self-duality of [n]): for any n ≠ 0, [n]̂ = [n] as endomorphisms.

                  Lemma 6.11: the dual is additive — (α + β)̂ = α̂ + β̂ for α, β ∈ Hom(E₁, E₂).

                  Pointwise form of Lemma 6.11 (dualIsogeny_add).

                  theorem Isogeny.dualIsogeny_comp_eq {F : Type u} [Field F] [DecidableEq F] {E₁ E₂ E₃ : WeierstrassCurve.Affine F} (α : Isogeny E₂ E₃) (β : Isogeny E₁ E₂) :

                  Lemma 6.12: the dual of a composition is the reversed composition of duals, (α ∘ β)̂ = β̂ ∘ α̂.

                  @[reducible, inline]
                  abbrev EndRing {F : Type u} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) :

                  Definition 6.13: the endomorphism ring End(E) = Hom(E, E) as the additive monoid of endomorphisms of E.Point, with multiplication given by composition.

                  Instances For
                    @[implicit_reducible]

                    Ring structure on EndRing E, inherited from AddMonoid.End.

                    noncomputable def intToEndRingHom {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} :

                    The canonical ring homomorphism ℤ → End(E) sending n to [n].

                    Instances For
                      @[simp]
                      theorem intToEndRingHom_apply {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (n : ) (P : E.Point) :

                      Evaluating intToEndRingHom n at a point P yields n • P.

                      theorem intCast_comm_endomorphism {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (n : ) (α : EndRing E) :
                      n * α = α * n

                      Integers (viewed as endomorphisms via [n]) commute with every endomorphism of E, i.e. [n] lies in the center of End(E).

                      @[simp]
                      theorem EndRing.mul_apply' {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : EndRing E) (P : E.Point) :
                      (α * β) P = α (β P)

                      The product in EndRing E is composition pointwise: (α * β) P = α (β P).

                      @[simp]
                      theorem EndRing.add_apply' {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : EndRing E) (P : E.Point) :
                      (α + β) P = α P + β P

                      The sum in EndRing E is pointwise addition.

                      @[simp]
                      theorem EndRing.one_apply' {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (P : E.Point) :
                      1 P = P

                      The unit 1 : EndRing E is the identity endomorphism.

                      @[simp]
                      theorem EndRing.zero_apply' {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (P : E.Point) :
                      0 P = 0

                      The zero 0 : EndRing E sends every point to the zero point.

                      Auxiliary form of Lemma 6.16: if oneMinusAlpha = [1] - α as homs, then its dual equals [1] - α̂. Used to relate the duals of α and 1 - α.

                      theorem Isogeny.toAddMonoidHom_add_dualIsogeny {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) :

                      Lemma 6.16: α + α̂ = [1 + deg α - deg(1 - α)] as endomorphisms of E.

                      Existence of an isogeny representing [1] - α, used to package the trace construction underlying Definition 6.17.

                      noncomputable def Isogeny.traceAux {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) :

                      Auxiliary trace formula tr α = 1 + deg α - deg(1 - α) parameterised by a specific witness of 1 - α (cf. Definition 6.17).

                      Instances For

                        Rephrasing of Lemma 6.16 in terms of traceAux: α + α̂ = [traceAux α (1-α)].

                        noncomputable def Isogeny.trace {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) :

                        Definition 6.17: the trace of an endomorphism α, defined via the integer such that α + α̂ = [tr α]. Implemented by choosing a witness for 1 - α.

                        Instances For

                          Defining identity for the trace (Definition 6.17): α + α̂ = [tr α].

                          Pointwise form of the trace identity: α(P) + α̂(P) = (tr α) • P.

                          @[reducible, inline]
                          noncomputable abbrev Isogeny.trace' {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) :

                          Convenience abbreviation trace' for Isogeny.trace, used to state Theorem 6.18.

                          Instances For

                            Trace identity restated using trace': α + α̂ = [trace' α].

                            Combined existence statement: a witness oma of 1 - α exists together with the trace identity expressed via 1 + deg α - deg(oma).

                            theorem Isogeny.char_poly_alpha_aux {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) :

                            Auxiliary form of Theorem 6.18 (characteristic polynomial via traceAux): α² - [tr α] α + [deg α] = 0 in End(E).

                            Theorem 6.18 (for α): α satisfies its characteristic equation α² - [tr α] α + [deg α] = 0.

                            Auxiliary form of Theorem 6.18 for the dual: α̂ also satisfies the same characteristic equation, expressed via traceAux.

                            Theorem 6.18 (for α̂): the dual α̂ also satisfies the characteristic equation λ² - (tr α) λ + deg α = 0.

                            def Isogeny.agreeOnTorsion {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) :

                            Two endomorphisms α, β of E agree on n-torsion iff their underlying maps match on E[n]. This is the predicate denoted αₙ = βₙ in Lemma 6.19.

                            Instances For
                              theorem Isogeny.cauchy_interpolation_global_sign {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hn_cop_β : n.Coprime β.degree) (hagree : PE.torsionSubgroup n, α.toAddMonoidHom P = β.toAddMonoidHom P) :

                              Cauchy-style interpolation for endomorphisms: if α and β agree on E[n] for a sufficiently large n coprime to the characteristic and to both degrees, then globally either α = β or α = -β.

                              theorem Isogeny.torsion_inter_kernel_trivial {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_cop : n.Coprime α.degree) (P : E.Point) :
                              P E.torsionSubgroup nα.toAddMonoidHom P = 0P = 0

                              If n is coprime to deg α, then α restricted to E[n] is injective: the only n-torsion point in the kernel of α is 0.

                              theorem Isogeny.exists_non_two_torsion_image {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_sq_gt : n * n > 4) (hn_cop_α : n.Coprime α.degree) :
                              PE.torsionSubgroup n, ¬2 α.toAddMonoidHom P = 0

                              Existence of an n-torsion point whose image under α is not 2-torsion, used in the sign resolution step of Lemma 6.19.

                              theorem Isogeny.agree_on_torsion_implies_pm {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hn_cop_β : n.Coprime β.degree) (hagree : PE.torsionSubgroup n, α.toAddMonoidHom P = β.toAddMonoidHom P) (P : E.Point) :

                              Pointwise version of the global ± dichotomy: under the hypotheses of Lemma 6.19, for every P, either α(P) = β(P) or α(P) = -β(P).

                              theorem Isogeny.sign_resolution {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hpm : ∀ (P : E.Point), α.toAddMonoidHom P = β.toAddMonoidHom P α.toAddMonoidHom P = -β.toAddMonoidHom P) (hagree : PE.torsionSubgroup n, α.toAddMonoidHom P = β.toAddMonoidHom P) :

                              Sign-resolution step in Lemma 6.19: combining the pointwise ± dichotomy with agreement on E[n] and the non-2-torsion image, deduce α = β.

                              theorem Isogeny.torsion_determines_endomorphism_aux {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hn_cop_β : n.Coprime β.degree) (hagree : PE.torsionSubgroup n, α.toAddMonoidHom P = β.toAddMonoidHom P) :

                              Auxiliary form of Lemma 6.19 stated with an unfolded agreement hypothesis: if α and β agree on E[n] for n satisfying the size/coprimality conditions, then α = β.

                              theorem Isogeny.torsion_determines_endomorphism {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hn_cop_β : n.Coprime β.degree) (hagree : α.agreeOnTorsion β n) :

                              Lemma 6.19: for n ≥ 2√m + 1 coprime to the characteristic and to deg α, deg β, if αₙ = βₙ (i.e. α and β agree on E[n]) then α = β.

                              theorem Isogeny.torsion_determines_endomorphism_apply {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α β : Isogeny E E) (n : ) (hn_pos : 0 < n) (hn_size : n * n > 4 * max α.degree β.degree) (hn_cop_char : n.Coprime (ringChar F)) (hn_cop_α : n.Coprime α.degree) (hn_cop_β : n.Coprime β.degree) (hagree : α.agreeOnTorsion β n) (P : E.Point) :

                              Pointwise form of Lemma 6.19: under the same hypotheses, α(P) = β(P) for every point P.