Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Affine.InvariantDifferential

The invariant differential of an elliptic curve #

For an elliptic curve E over a field F this file constructs the invariant differential ω = dx / (2y + a₁x + a₃) inside the module of Kähler differentials Ω[K(E)/F] of the function field, and proves that ω is a basis: Ω[K(E)/F] is a one-dimensional K(E)-vector space, so every differential of K(E) is c • ω for a unique c ∈ K(E).

The imported function-field API proves that x is a separating element of K(E)/F. The general separating-element API then says that dx is a basis of the Kähler differentials; rescaling it by W_Y⁻¹ gives the invariant-differential basis.

Main definitions #

Main results #

References #

Silverman's III.1.5 says more than anything proved here: that div ω = 0, so that ω is regular and nonvanishing at every point. This file proves that ω is a basis of Ω[K(E)/F], which does not imply that — a nonzero rational differential may have both zeros and poles. The divisor statement needs a pointwise regularity and nonvanishing theory not developed here.

Provenance #

Ported from the AINTLIB HasseWeil project (Chris Birkbeck), Apache-2.0, at commit 513e83879e2f: HasseWeil/InvariantDifferential.lean (D_x_ne_zero, denom_ne_zero, invariantDifferential and invariantDifferential_ne_zero) and HasseWeil/FormalGroupCorrespondence.lean (kaehler_rank_one, the one-dimensionality, proved there by the same span-of-dx argument).

The denominator 2y + a₁x + a₃ #

source
noncomputable def WeierstrassCurve.Affine.invariantDifferentialDenom {F : Type u_1} [Field F] (E : Affine F) :
E.FunctionField

The denominator 2y + a₁x + a₃ of the invariant differential, as an element of K(E). It is the value at the generic point of the partial derivative W_Y = polynomialY, which is invariantDifferentialDenom_eq_evalEval_polynomialY; invariantDifferentialDenom_ne_zero shows it is nonzero when E is elliptic. The converse fails: y² = x³ over ℚ is singular, yet its W_Y = 2y is nonzero.

Equations
Instances For
    source
    theorem WeierstrassCurve.Affine.invariantDifferentialDenom_def {F : Type u_1} [Field F] (E : Affine F) :
    E.invariantDifferentialDenom = 2 * E.genericY + (algebraMap F E.FunctionField) E.a₁ * E.genericX + (algebraMap F E.FunctionField) E.a₃

    The defining formula for invariantDifferentialDenom.

    source
    theorem WeierstrassCurve.Affine.invariantDifferentialDenom_eq_evalEval_polynomialY {F : Type u_1} [Field F] (E : Affine F) :
    E.invariantDifferentialDenom = Polynomial.evalEval E.genericX E.genericY (toAffine (E.baseChange E.FunctionField)).polynomialY

    The denominator is W_Y at the generic point. This is the reading that makes it the denominator of ω = dx / W_Y.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.invariantDifferentialDenom_ne_zero {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] :
    E.invariantDifferentialDenom ≠ 0

    The denominator of the invariant differential is nonzero. It is the image of W_Y in K(E), and W_Y is a nonzero polynomial of degree below deg W, so it survives both F[X][Y] → F[E] and F[E] → K(E).

    The invariant differential #

    source
    noncomputable def WeierstrassCurve.Affine.invariantDifferential {F : Type u_1} [Field F] (E : Affine F) :
    Ω[E.FunctionField⁄F]

    The invariant differential ω = dx / (2y + a₁x + a₃), as an element of Ω[K(E)/F].

    Equations
    Instances For
      source
      theorem WeierstrassCurve.Affine.invariantDifferential_def {F : Type u_1} [Field F] (E : Affine F) :
      E.invariantDifferential = E.invariantDifferentialDenom⁻¹ • (KaehlerDifferential.D F E.FunctionField) E.genericX

      The defining formula for invariantDifferential. The definition body is not exposed, so this equation lemma is how a consumer in another module computes with it. Not @[simp]: the point of naming invariantDifferentialDenom is that the nonvanishing results can be stated over it, which unfolding everywhere would defeat.

      source
      @[simp]
      theorem WeierstrassCurve.Affine.invariantDifferential_ne_zero {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] :
      E.invariantDifferential ≠ 0

      The invariant differential is nonzero as an element of Ω[K(E)/F]. It is the product of an inverse of the nonzero denominator with dx, both nonzero.

      source
      theorem WeierstrassCurve.Affine.span_invariantDifferential_eq_top {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] :
      E.FunctionField ∙ E.invariantDifferential = ⊤

      The invariant differential spans Ω[K(E)/F]: it differs from dx by an invertible scalar.

      source
      noncomputable def WeierstrassCurve.Affine.invariantDifferentialBasis {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] :
      Module.Basis Unit E.FunctionField Ω[E.FunctionField⁄F]

      ω is a basis of Ω[K(E)/F], the module being one-dimensional and ω nonzero.

      Equations
      Instances For
        source
        @[simp]
        theorem WeierstrassCurve.Affine.invariantDifferentialBasis_apply {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] (i : Unit) :
        E.invariantDifferentialBasis i = E.invariantDifferential

        The unique Unit-indexed vector of invariantDifferentialBasis is the invariant differential ω.

        source
        theorem WeierstrassCurve.Affine.existsUnique_smul_invariantDifferential {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] (η : Ω[E.FunctionField⁄F]) :
        ∃! c : E.FunctionField, c • E.invariantDifferential = η

        Every differential of K(E) is c • ω for a unique c ∈ K(E). This is the form the differential calculus of isogenies consumes: the pullback coefficient of an isogeny φ is the scalar attached to φ^*ω by this statement.

        source
        @[simp]
        theorem WeierstrassCurve.Affine.zsmul_invariantDifferential_eq_zero_iff {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] (n : ℤ) :
        n • E.invariantDifferential = 0 ↔ ↑n = 0

        An integer multiple of ω vanishes exactly when the integer does in the base field.