Documentation

TauCeti.NumberTheory.EllipticDivisibilitySequence.Universal

The universal normalised elliptic divisibility sequence #

A normalised EDS over a commutative ring R is determined by three parameters b, c, d : R. Taking those parameters to be three indeterminates gives the universal normEDS family

universalNormEDS : ℤ → MvPolynomial NormEDSParam ℤ,

of which every sequence of the form normEDS b c d is a specialization: it is universalNormEDS followed by the evaluation sending the indeterminates to b, c, d (normEDS_eq_aeval), and likewise for preNormEDS and for the two complement sequences (preNormEDS_eq_aeval, complEDS₂_eq_aeval, complEDS_eq_aeval).

Note the claim is about the constructed function normEDS, not about elliptic divisibility sequences in the abstract: the pinned Mathlib does not know that normEDS b c d satisfies IsEllipticDvdSequence — it records proving so as a TODO — so nothing here says every EDS arises this way, only that every normEDS b c d does.

The point is that an identity between the terms of a sequence of the form normEDS b c d need only be proved once, over MvPolynomial NormEDSParam ℤ, and then specialises to every ring and every choice of parameters. Working universally also buys an integral domain to work in, which the parameters' ring need not be.

Main definitions #

Main results #

Implementation notes #

The constructors of NormEDSParam are uppercase because they name indeterminates rather than elements, matching WeierstrassCurve.Coeff in TauCeti/AlgebraicGeometry/EllipticCurve/Universal.lean, which plays the same role for the universal Weierstrass curve.

Only normEDS gets a named universal object. The three companion sequences are stated against preNormEDS (X B) (X C) (X D) and its analogues written out, since naming each one would add three definitions whose only use is to be unfolded — the sequences are already determined by the parameters, and it is the specialization statement that consumers need, not a new name for its left-hand side. Those three carry an explicit X (R := ℤ): with the coefficient ring appearing only under aeval, elaboration has nothing to pin it to and reports a stuck CommSemiring instance otherwise.

Provenance #

Ported from D. K. Angdinata's LutzNagell/EllipticDivisibilitySequence.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main at 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), declarations Param, universalNormEDS, normEDS_eq_aeval, compl₂EDS_eq_aeval and complEDS_eq_aeval. Param is spelt NormEDSParam here — a root-level Param says nothing about elliptic divisibility sequences and makes its namespace equally generic; that rename is an adaptation made in this repository, not upstream's name. That file's header reads Authors: David Kurniadi Angdinata; following this repository's convention for adapted material the upstream authorship is credited here rather than in the copyright header. J. Xu is acknowledged for the surrounding LutzNagell development — he authors Universal.lean and co-authors DivisionPolynomialOmega.lean at the same revision — as context for this port, not as an author of the declarations above.

The same declarations sit in Mathlib PR #13057 (open, last updated 2024-07-31), the upstreaming of that AINTLIB file, so they are portable under this project's rule and deduplicate when it lands. compl₂EDS is spelt complEDS₂ here, following Mathlib's subsequent rename of the elliptic-net API (addMulSub → IsEllipticNet.atom, net → IsEllipticNet.rel, rel₄ → IsEllipticNet.atomRel, IsEllSequence → IsEllipticSequence, compl₂EDS → complEDS₂), which #13057 predates.

preNormEDS_eq_aeval is new: the source states the principle for normEDS and the two complements but not for preNormEDS, although Mathlib's map_preNormEDS makes it the same one-line proof and consumers reaching for the pre-normalised sequence would otherwise have to redo it.

universalNormEDS_ne_zero is not here, and the reason is the import direction rather than a gap. It rests on normEDS 2 3 2 = id, which is normEDS_two_three_two_eq_id; that in turn needs normEDS to be an elliptic sequence, isEllipticSequence_normEDS, which is proved in NormEDS.lean — downstream of this file, since NormEDS.lean imports it and not the other way round. So the nonvanishing lemma is stated there, beside the identity it is one line from. (The identity also uses IsEllipticSequence.ext from Ext.lean, but that file imports neither this one nor NormEDS.lean, so it is not what fixes the direction.)

source
inductive NormEDSParam :
Type

A three-element index type for the parameters b, c, d of a normalised elliptic divisibility sequence. It indexes the variables of MvPolynomial NormEDSParam ℤ = ℤ[B, C, D], the ring the universal normalised EDS is defined over; the constructors are uppercase as names of indeterminates.

Instances For
    source
    noncomputable def NormEDSParam.universalNormEDS :
    ℤ → MvPolynomial NormEDSParam ℤ

    The universal normEDS: normEDS over ℤ[B, C, D], at the three indeterminates. Every sequence of the form normEDS b c d is one of its specializations (normEDS_eq_aeval), so an identity between such terms can be proved here once and read off for every ring and every choice of parameters.

    Equations
    Instances For
      source
      @[simp]
      theorem NormEDSParam.universalNormEDS_def :
      universalNormEDS = normEDS (MvPolynomial.X B) (MvPolynomial.X C) (MvPolynomial.X D)

      The defining equation of universalNormEDS: normEDS at the three indeterminates. It is the stable name for that expansion, so downstream proofs rewrite with a lemma rather than unfolding a definition; it does not hide the representation, and its right-hand side is that representation.

      It is stated at the level of functions, not pointwise. Downstream modules cannot see the body, so a rewrite under a function-valued argument — invarNum, IsEllipticNet — needs this form; the pointwise one is congrFun universalNormEDS_def n, and @[simp] rewrites the head constant, so applied occurrences reach the same normal form either way.

      source
      theorem NormEDSParam.normEDS_eq_aeval {R : Type u_1} [CommRing R] (b c d : R) :
      normEDS b c d = fun (n : ℤ) => (MvPolynomial.aeval fun (t : NormEDSParam) => rec b c d t) (universalNormEDS n)

      Every sequence of the form normEDS b c d is a specialization of the universal one.

      source
      theorem NormEDSParam.preNormEDS_eq_aeval {R : Type u_1} [CommRing R] (b c d : R) :
      preNormEDS b c d = fun (n : ℤ) => (MvPolynomial.aeval fun (t : NormEDSParam) => rec b c d t) (preNormEDS (MvPolynomial.X B) (MvPolynomial.X C) (MvPolynomial.X D) n)

      The pre-normalised sequence of a normalised EDS is likewise a specialization.

      source
      theorem NormEDSParam.complEDS₂_eq_aeval {R : Type u_1} [CommRing R] (b c d : R) :
      complEDS₂ b c d = fun (n : ℤ) => (MvPolynomial.aeval fun (t : NormEDSParam) => rec b c d t) (complEDS₂ (MvPolynomial.X B) (MvPolynomial.X C) (MvPolynomial.X D) n)

      The second complement sequence of a normalised EDS is likewise a specialization.

      source
      theorem NormEDSParam.complEDS_eq_aeval {R : Type u_1} [CommRing R] (b c d : R) :
      complEDS b c d = fun (k n : ℤ) => (MvPolynomial.aeval fun (t : NormEDSParam) => rec b c d t) (complEDS (MvPolynomial.X B) (MvPolynomial.X C) (MvPolynomial.X D) k n)

      The complement sequence of a normalised EDS is likewise a specialization, in both arguments.