Documentation

LeanPool.KasamiCyclicAdditive.Geometry.FermatCubic.Hessian

The Hessian addition formulas for the Fermat cubic in characteristic two #

For two affine Fermat points (w1,t1), (w2,t2) the projectivised Hessian addition formula reads

D  = w1*t1 + w2*t2
Nx = t1^2*w2 + t2^2*w1
Ny = w1^2*t2 + w2^2*t1

(for (w2,t2) = (w^r,t^r) these are exactly D0, N_x, N_y of the unit).

This file records the three polynomial identities behind the formula; they are all consequences of the two Fermat equations and of 2 = 0.

source
def KasamiCyclicAdditive.FermatCubic.hessD {K : Type u_1} [Field K] (w1 t1 w2 t2 : K) :
K

The denominator D0 of the Hessian addition formula.

Equations
Instances For
    source
    def KasamiCyclicAdditive.FermatCubic.hessX {K : Type u_1} [Field K] (w1 t1 w2 t2 : K) :
    K

    The first numerator N_x of the Hessian addition formula.

    Equations
    Instances For
      source
      def KasamiCyclicAdditive.FermatCubic.hessY {K : Type u_1} [Field K] (w1 t1 w2 t2 : K) :
      K

      The second numerator N_y of the Hessian addition formula.

      Equations
      Instances For
        source
        theorem KasamiCyclicAdditive.FermatCubic.hess_cubic {K : Type u_1} [Field K] [CharP K 2] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) :
        hessX w1 t1 w2 t2 ^ 3 + hessY w1 t1 w2 t2 ^ 3 = hessD w1 t1 w2 t2 ^ 3

        The Hessian numerators and denominator again satisfy the Fermat equation: N_x^3 + N_y^3 = D0^3.

        source
        theorem KasamiCyclicAdditive.FermatCubic.hess_addX_aux {K : Type u_1} [Field K] [CharP K 2] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) :
        ((w1 * (w2 + t2) + w2 * (w1 + t1)) ^ 2 * ((w1 + t1) * (w2 + t2)) + (w1 + t1 + (w2 + t2)) ^ 3) * (hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2) = hessD w1 t1 w2 t2 * ((w1 + t1 + (w2 + t2)) ^ 2 * ((w1 + t1) * (w2 + t2)))

        The x-coordinate identity behind the Hessian addition formula.

        source
        theorem KasamiCyclicAdditive.FermatCubic.hess_addY_aux {K : Type u_1} [Field K] [CharP K 2] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) :
        (w1 * (w2 + t2) + w2 * (w1 + t1)) * (hessD w1 t1 w2 t2 * (w1 + t1) + (hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2)) + w1 * (w1 + t1 + (w2 + t2)) * (hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2) + (w1 + t1 + (w2 + t2)) * (w1 + t1) * (hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2) = hessX w1 t1 w2 t2 * (w1 + t1 + (w2 + t2)) * (w1 + t1)

        The y-coordinate identity behind the Hessian addition formula.