The Wronskian identity of an…

TheoremThe Wronskian identity of an isogeny #

if φ^*ω₂ = c ω₁, then

w(x) u₁ = c D(x)² φ^*u₂,

where w is the Wronskian of φ.xRatFunc = N / D and u = 2y + a₁x + a₃ is the denominator of the invariant differential.

TauCeti.Isogeny.aeval_wronskian_xRatFunc_mul_invariantDifferentialDenom.{u_1} {F : Type u_1}
  [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] {φ : TauCeti.Isogeny W₁ W₂} {c : F}
  (hc : φ.pullbackDifferential W₂.invariantDifferential = c • W₁.invariantDifferential) :
  (Polynomial.aeval W₁.genericX) (φ.xRatFunc.denom.wronskian φ.xRatFunc.num) *
      W₁.invariantDifferentialDenom =
    (algebraMap F W₁.FunctionField) c * (Polynomial.aeval W₁.genericX) φ.xRatFunc.denom ^ 2 *
      φ.fieldPullback W₂.invariantDifferentialDenom

Lean

Formalized in Tau Ceti as TauCeti.Isogeny.aeval_wronskian_xRatFunc_mul_invariantDifferentialDenom.

Other forms

The Wronskian identity with y eliminated. Formalized in Tau Ceti as TauCeti.Isogeny.wronskian_xRatFunc_sq_mul_Ψ₂Sq.

TauCeti.Isogeny.wronskian_xRatFunc_sq_mul_Ψ₂Sq.{u_1} {F : Type u_1} [Field F]
  {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] {φ : TauCeti.Isogeny W₁ W₂} {c : F}
  (hc : φ.pullbackDifferential W₂.invariantDifferential = c • W₁.invariantDifferential) :
  φ.xRatFunc.denom.wronskian φ.xRatFunc.num ^ 2 * WeierstrassCurve.Ψ₂Sq W₁ =
    Polynomial.C (c ^ 2) * φ.xRatFunc.denom *
      (Polynomial.C 4 * φ.xRatFunc.num ^ 3 +
            Polynomial.C (WeierstrassCurve.b₂ W₂) * φ.xRatFunc.num ^ 2 * φ.xRatFunc.denom +
          Polynomial.C (2 * WeierstrassCurve.b₄ W₂) * φ.xRatFunc.num * φ.xRatFunc.denom ^ 2 +
        Polynomial.C (WeierstrassCurve.b₆ W₂) * φ.xRatFunc.denom ^ 3)