Documentation

Atlas.EllipticCurves.code.EndomorphismNorm

The involution of a positive-definite involution algebra sends 0 to 0.

The structure map ℚ → A of a nontrivial positive-definite involution algebra is injective. Used to identify with its image inside A.

The norm map of a nontrivial PD-involution algebra sends 0 to 0.

The norm of any element of a nontrivial PD-involution algebra is nonnegative.

The norm of an element vanishes iff the element itself is zero. Encodes positive-definiteness of the norm form.

A nontrivial PD-involution algebra has no zero divisors: if a * b = 0 then a = 0 or b = 0. Proved using positive-definiteness of the norm.

The norm is invariant under the involution: N(â) = N(a).

Multiplicativity of the norm: N(a * b) = N(a) * N(b).

Every nonzero element of a nontrivial PD-involution algebra is a unit. The inverse is explicitly N(a)⁻¹ • â.

A nontrivial PD-involution algebra has no zero divisors.

A nontrivial PD-involution algebra is an integral domain.

Explicit two-sided inverse for a nonzero element a: (N(a))⁻¹ • â is both a left and right inverse of a.

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

The rational endomorphism algebra End⁰(E) = End(E) ⊗_ℤ ℚ of an elliptic curve E, an abbreviation for EndomorphismAlgebra E.

Instances For
    noncomputable def WeierstrassCurve.Affine.End0.dual {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :

    The Rosati dual / canonical involution of an element of End⁰(E), obtained from the PD-involution algebra structure on the endomorphism algebra.

    Instances For
      noncomputable def WeierstrassCurve.Affine.End0.N {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :

      The reduced norm N : End⁰(E) → ℚ of an endomorphism, obtained from the PD-involution algebra structure on End⁰(E). Geometrically this is the degree of an isogeny (extended ℚ-linearly).

      Instances For
        theorem WeierstrassCurve.Affine.End0.N_spec {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
        (algebraMap E.End0) (N E α) = α * dual E α

        Defining property of the norm: N(α) = α · α^† after embedding ℚ into End⁰(E).

        The endomorphism algebra End⁰(E) is nontrivial (contains both 0 and 1).

        Nonnegativity of the endomorphism norm: N(α) ≥ 0 for all α ∈ End⁰(E).

        theorem WeierstrassCurve.Affine.EndAlgebra.norm_eq_zero_iff {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
        End0.N E α = 0 α = 0

        Positive-definiteness of the norm: N(α) = 0 iff α = 0.

        theorem WeierstrassCurve.Affine.EndAlgebra.norm_dual {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
        End0.N E (End0.dual E α) = End0.N E α

        The norm is invariant under the Rosati dual: N(α^†) = N(α).

        theorem WeierstrassCurve.Affine.EndAlgebra.norm_mul {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α β : E.End0) :
        End0.N E (α * β) = End0.N E α * End0.N E β

        Multiplicativity of the norm on End⁰(E): N(α · β) = N(α) · N(β).

        theorem WeierstrassCurve.Affine.EndAlgebra.norm_properties {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (α β : E.End0) :
        0 End0.N E α (End0.N E α = 0 α = 0) End0.N E (End0.dual E α) = End0.N E α End0.N E (α * β) = End0.N E α * End0.N E β

        Bundled statement of the main norm properties on End⁰(E): nonnegativity, positive-definiteness, invariance under dual, multiplicativity.

        theorem WeierstrassCurve.Affine.EndAlgebra.isUnit_of_ne_zero {F : Type u} [Field F] [DecidableEq F] (E : Affine F) (a : E.End0) (ha : a 0) :

        Every nonzero element of End⁰(E) is invertible, making End⁰(E) a division algebra over .

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

        The reduced trace T : End⁰(E) → ℚ of an endomorphism, obtained from the PD-involution structure on End⁰(E).

        Instances For

          Defining property of the trace map: T(a) mapped into A equals a + â.

          The involution is ℚ-linear in the scalar action: (r • a)^† = r • a^†.

          The trace is invariant under the involution: T(â) = T(a).

          Additivity of the trace: T(a + b) = T(a) + T(b).

          ℚ-linearity of the trace: T(r • a) = r * T(a).

          Characteristic polynomial relation: every element satisfies a² - T(a) • a + N(a) • 1 = 0.

          The trace of algebraMap q is 2q, matching the formula T(q · 1) = 2q for the reduced trace of a scalar.

          The trace of â · a is strictly positive for any nonzero a, since â · a = N(a) · 1 and T(N(a) · 1) = 2 N(a) > 0.

          theorem WeierstrassCurve.Affine.EndAlgebra.trace_rationality {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
          End0.T E α = 1 + End0.N E α - End0.N E (1 - α)

          Rationality formula for the trace on End⁰(E): T(α) = 1 + N(α) - N(1 - α), expressing the trace as a polynomial in norms.

          theorem WeierstrassCurve.Affine.EndAlgebra.trace_dual {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
          End0.T E (End0.dual E α) = End0.T E α

          The trace is invariant under the Rosati dual: T(α^†) = T(α).

          theorem WeierstrassCurve.Affine.EndAlgebra.trace_add {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α β : E.End0) :
          End0.T E (α + β) = End0.T E α + End0.T E β

          Additivity of the trace on End⁰(E): T(α + β) = T(α) + T(β).

          theorem WeierstrassCurve.Affine.EndAlgebra.trace_smul {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (r : ) (α : E.End0) :
          End0.T E (r α) = r * End0.T E α

          ℚ-linearity of the trace on End⁰(E): T(r • α) = r · T(α).

          theorem WeierstrassCurve.Affine.EndAlgebra.trace_dual_and_linear {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) :
          (∀ (α : E.End0), End0.T E (End0.dual E α) = End0.T E α) (∀ (α : E.End0), End0.T E α = 1 + End0.N E α - End0.N E (1 - α)) (∀ (α β : E.End0), End0.T E (α + β) = End0.T E α + End0.T E β) ∀ (r : ) (α : E.End0), End0.T E (r α) = r * End0.T E α

          Bundled package: the trace on End⁰(E) is dual-invariant, ℚ-rational via T(α) = 1 + N(α) - N(1 - α), additive, and ℚ-linear in the scalar action.

          theorem WeierstrassCurve.Affine.EndAlgebra.char_poly {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
          α ^ 2 - End0.T E α α + End0.N E α 1 = 0

          Every endomorphism α satisfies its characteristic equation in End⁰(E): α² - T(α) • α + N(α) • 1 = 0.

          theorem WeierstrassCurve.Affine.EndAlgebra.char_poly_dual {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
          End0.dual E α ^ 2 - End0.T E α End0.dual E α + End0.N E α 1 = 0

          The dual α^† also satisfies α's characteristic polynomial: (α^†)² - T(α) • α^† + N(α) • 1 = 0.

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

          The characteristic polynomial of an endomorphism α, as the polynomial X² - T(α) X + N(α) ∈ ℚ[X].

          Instances For

            α is a root of its own characteristic polynomial under the ℚ-algebra evaluation Polynomial ℚ → End⁰(E).

            The Rosati dual α^† is also a root of α's characteristic polynomial.

            Both α and its Rosati dual α^† are roots of the characteristic polynomial X² - T(α) X + N(α).

            theorem WeierstrassCurve.Affine.EndAlgebra.rosati_fixed_iff_rational {F : Type u₂} [Field F] [DecidableEq F] (E : Affine F) (α : E.End0) :
            End0.dual E α = α ∃ (r : ), α = r 1

            The Rosati-fixed elements of End⁰(E) are exactly the rational multiples of the identity: α^† = α iff α = r • 1 for some r ∈ ℚ.