Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Affine.FunctionField.GenericPoint.Basic

The generic point of an affine Weierstrass curve #

The coordinate ring W.CoordinateRing is R[X][Y] modulo the Weierstrass relation, so the classes of X and Y in the function field are a pair satisfying that relation over W.FunctionField. They are the generic point: a point of W base-changed to its own function field.

What is proved here is that the pair is a point (equation_genericX_genericY), that evaluating a bivariate polynomial at it is reduction modulo the Weierstrass relation (evalEval_genericX_genericY), and that on an elliptic curve over a nontrivial base ring the resulting solution is nonsingular, cutting out a point genericPoint of W⁄F(W). The coordinate-ring image also lies in the subalgebra generated by the two coordinates (algebraMap_mem_adjoin_genericX_genericY).

Over a field the generic x-coordinate is transcendental, and on an elliptic curve the partial derivative W_Y = 2Y + a₁X + a₃ is nonzero at the generic point (evalEval_polynomialY_genericX_genericY_ne_zero); in characteristic two the latter holds because Δ ≠ 0 rules out a₁ = a₃ = 0.

The word "generic" is the usual geometric one, but no specialisation property is established: nothing below says that a statement about this point transfers to the points of W, and no consumer may rely on that.

Main definitions #

Main results #

References #

Provenance #

The generic coordinates and their equation are adapted from the AINTLIB HasseWeil project (Chris Birkbeck), Apache-2.0, HasseWeil/MulByIntPullback.lean at commit 513e83879e2f8cbc626eb9e04d660e92be16ccba, declarations x_gen, y_gen, W_KE, and generic_equation. Its transcendence statement is reproved here as transcendental_genericX. The bundled genericPoint and its coordinate-accessor API are not ported from that source.

map_genericPoint_injective adapts the statement of that project's HasseWeil/GapSpines.lean declaration emb_le_card_kernel, same commit and license, which assigns a point to each embedding and shows the assignment injective. The proof differs: the source works with points over AlgebraicClosure K(E) and with an isogeny carrying its own point map, while here the point is the image of the generic point and injectivity comes from CoordinateRing.algHom_ext and IsFractionRing.ringHom_ext.

source
noncomputable def WeierstrassCurve.Affine.genericX {R : Type u_1} [CommRing R] (W : Affine R) :
W.FunctionField

The generic x-coordinate: the class of X in the function field.

Equations
Instances For
    source
    noncomputable def WeierstrassCurve.Affine.genericY {R : Type u_1} [CommRing R] (W : Affine R) :
    W.FunctionField

    The generic y-coordinate: the class of Y in the function field.

    Equations
    Instances For
      source
      theorem WeierstrassCurve.Affine.genericX_def {R : Type u_1} [CommRing R] (W : Affine R) :
      W.genericX = (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) (Polynomial.C Polynomial.X))

      The generic coordinate x is the image of the coordinate-ring class of X in the function field.

      source
      theorem WeierstrassCurve.Affine.genericY_def {R : Type u_1} [CommRing R] (W : Affine R) :
      W.genericY = (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) Polynomial.X)

      The generic coordinate y is the image of the coordinate-ring class of Y in the function field.

      source
      theorem WeierstrassCurve.Affine.genericX_eq_algebraMap {R : Type u_1} [CommRing R] (W : Affine R) :
      W.genericX = (algebraMap (Polynomial R) W.FunctionField) Polynomial.X

      The generic coordinate x is the image of polynomial X under the induced map from R[X] to the function field.

      source
      theorem WeierstrassCurve.Affine.FunctionField.ringHom_ext {R : Type u_1} [CommRing R] {W : Affine R} {S : Type u_2} [Semiring S] {f g : W.FunctionField →+* S} (hc : ∀ (a : R), f ((algebraMap R W.FunctionField) a) = g ((algebraMap R W.FunctionField) a)) (hx : f W.genericX = g W.genericX) (hy : f W.genericY = g W.genericY) :
      f = g

      Ring homomorphisms out of the function field are determined by the constants and the generic coordinates. The function field is a localization of the coordinate ring, which is generated over R by the classes of x and y.

      source
      theorem WeierstrassCurve.Affine.evalEval_genericX_genericY {R : Type u_1} [CommRing R] (W : Affine R) (p : Polynomial (Polynomial R)) :
      Polynomial.evalEval W.genericX W.genericY (Polynomial.map (Polynomial.mapRingHom (algebraMap R W.FunctionField)) p) = (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) p)

      Evaluating at the generic point is reduction modulo the Weierstrass relation. A bivariate polynomial over R, pushed to the function field and evaluated at (genericX, genericY), is the image of its class in the coordinate ring.

      This is the workhorse: it converts any polynomial expression at the generic point into the image of a coordinate-ring element, where the ring's own API applies.

      source
      theorem WeierstrassCurve.Affine.equation_genericX_genericY {R : Type u_1} [CommRing R] (W : Affine R) :
      (toAffine (W.baseChange W.FunctionField)).Equation W.genericX W.genericY

      The generic coordinate functions satisfy the equation of the curve. (X, Y) satisfies the equation of W base-changed to the function field, because the Weierstrass polynomial is precisely what the coordinate ring quotients out.

      source
      @[simp]
      theorem WeierstrassCurve.Affine.aeval_genericY_polynomial {R : Type u_1} [CommRing R] (W : Affine R) :
      (Polynomial.aeval W.genericY) W.polynomial = 0

      The generic y-coordinate is a root of the Weierstrass polynomial.

      This is AINTLIB's root_aeval_polynomial_map of projects/HasseWeil/HasseWeil/Ramification.lean at revision 513e83879e2f, Apache-2.0, stated over R[X] rather than over a fraction field.

      source
      theorem WeierstrassCurve.Affine.isIntegral_genericY {R : Type u_1} [CommRing R] (W : Affine R) (L : Type u_2) [CommRing L] [Algebra (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] :
      IsIntegral L W.genericY

      The generic y-coordinate is integral over any commutative R[X]-algebra L mapping compatibly to the function field. L need not embed: no injectivity is assumed.

      source
      theorem WeierstrassCurve.Affine.algebraMap_eq_aeval_genericX {R : Type u_1} [CommRing R] (W : Affine R) (p : Polynomial R) :
      (algebraMap (Polynomial R) W.FunctionField) p = (Polynomial.aeval W.genericX) p

      The image of R[X] in the function field consists of the polynomials in the generic x-coordinate.

      source
      theorem WeierstrassCurve.Affine.algebraMap_smul_eq_mul {R : Type u_1} [CommRing R] (W : Affine R) (r : Polynomial R) (z : W.CoordinateRing) :
      (algebraMap W.CoordinateRing W.FunctionField) (r • z) = (algebraMap (Polynomial R) W.FunctionField) r * (algebraMap W.CoordinateRing W.FunctionField) z

      Scalars pass through the inclusion of the coordinate ring into the function field. An R[X]-scalar acting on R[W] becomes multiplication by its image in R(W).

      source
      theorem WeierstrassCurve.Affine.algebraMap_mem_adjoin_genericX_genericY {R : Type u_1} [CommRing R] (W : Affine R) (z : W.CoordinateRing) :
      (algebraMap W.CoordinateRing W.FunctionField) z ∈ R[W.genericX, W.genericY]

      The coordinate ring, read inside the function field, lies in the subalgebra generated by the generic point. Every affine function of W is a polynomial in x and y over R, so its image lies in the R-subalgebra R[x, y] of R(W). The proof uses that R[W] is free of rank two over R[X] with basis {1, y}.

      source
      theorem WeierstrassCurve.Affine.nonsingular_genericX_genericY {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W] :
      (toAffine (W.baseChange W.FunctionField)).Nonsingular W.genericX W.genericY

      The generic coordinates are nonsingular, so they define an affine point of the base-changed curve.

      Beyond the ambient [CommRing R] this needs [W.IsElliptic], which turns the equation into nonsingularity, and [Nontrivial R], which is what supplies Nontrivial W.FunctionField to equation_iff_nonsingular.

      source
      noncomputable def WeierstrassCurve.Affine.genericPoint {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W] :
      (toAffine (W.baseChange W.FunctionField)).Point

      The generic point of W: the tautological point of W with coordinates in its own function field.

      Equations
      Instances For
        source
        theorem WeierstrassCurve.Affine.genericPoint_eq_some {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W] :
        W.genericPoint = Point.some W.genericX W.genericY ⋯

        The generic point is the affine point whose coordinates are genericX W and genericY W.

        source
        @[simp]
        theorem WeierstrassCurve.Affine.xCoord_genericPoint {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W] :
        W.genericPoint.xCoord = W.genericX
        source
        @[simp]
        theorem WeierstrassCurve.Affine.yCoord_genericPoint {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W] :
        W.genericPoint.yCoord = W.genericY
        source
        theorem WeierstrassCurve.Affine.transcendental_genericX {F : Type u_2} [Field F] (W : Affine F) :
        Transcendental F W.genericX

        The coordinate function x is transcendental over the base field.

        source
        theorem WeierstrassCurve.Affine.algebraMap_mk_C_C {F : Type u_2} [Field F] (W : Affine F) (c : F) :
        (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.mk W) (Polynomial.C (Polynomial.C c))) = (algebraMap F W.FunctionField) c

        A constant of the function field is the class of the constant polynomial C (C c).

        source
        @[simp]
        theorem WeierstrassCurve.Affine.algebraMap_XClass {F : Type u_2} [Field F] (W : Affine F) (x : F) :
        (algebraMap W.CoordinateRing W.FunctionField) (CoordinateRing.XClass W x) = W.genericX - (algebraMap F W.FunctionField) x

        The class of X - x in the function field is genericX - x.

        source
        @[simp]
        theorem WeierstrassCurve.Affine.algebraMap_YClass {F : Type u_2} [Field F] (W : Affine F) (y : F) :
        (algebraMap W.CoordinateRing W.FunctionField) (CoordinateRing.YClass W (Polynomial.C y)) = W.genericY - (algebraMap F W.FunctionField) y

        The class of Y - y in the function field is genericY - y.

        source
        theorem WeierstrassCurve.Affine.genericX_ne_algebraMap {F : Type u_2} [Field F] (W : Affine F) (x₁ : F) :
        W.genericX ≠ (algebraMap F W.FunctionField) x₁

        The coordinate function x takes no constant value, being transcendental.

        source
        @[simp]
        theorem WeierstrassCurve.Affine.evalEval_polynomialY_genericX_genericY_ne_zero {F : Type u_2} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] :
        Polynomial.evalEval W.genericX W.genericY (toAffine (W.baseChange W.FunctionField)).polynomialY ≠ 0

        The partial derivative W_Y is nonzero at the generic point of an elliptic curve.

        source
        theorem WeierstrassCurve.Affine.map_genericPoint_injective {F : Type u_2} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {Ω : Type u_3} [Field Ω] [Algebra F Ω] [DecidableEq Ω] :
        Function.Injective fun (σ : W.FunctionField →ₐ[F] Ω) => (Point.map σ) W.genericPoint

        An F-embedding of the function field into a field extension is determined by the image of the generic point. The generic point's two coordinates generate the function field over F, so an embedding is recoverable from the point it induces.

        source
        theorem WeierstrassCurve.Affine.eq_of_baseChange_eq_sub_map_genericPoint {F : Type u_2} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq F] {Ω : Type u_3} [Field Ω] [Algebra F Ω] [DecidableEq Ω] {ι : Type u_4} (e : ι → W.FunctionField →ₐ[F] Ω) (σ₀ : W.FunctionField →ₐ[F] Ω) {f : ι → (toAffine (W.baseChange F)).Point} (hf : ∀ (i : ι), (Point.baseChange F Ω) (f i) = (Point.map (e i)) W.genericPoint - (Point.map σ₀) W.genericPoint) {i j : ι} (h : f i = f j) :
        e i = e j

        An embedding is determined by the rational point it displaces the generic point by. If each index i carries a rational point whose base change is e i's displacement of the generic point from a fixed embedding σ₀, then that point determines e i.

        This is the injectivity step shared by the embedding counts of the isogenies whose kernels are counted this way: they differ in why the displacement is rational, not in this step.