The affine Fermat chart and the Hessian addition formula

pt w t h is the affine Fermat point (w,t) (w^3+t^3=1) seen inside the Weierstrass model fer. The main results are

• add_pt: if the Hessian denominator D0 is nonzero, then (w1,t1) + (w2,t2) = (N_x/D0, N_y/D0), which is the affine Hessian addition formula used for the chart;
• neg_pt: negation swaps the two affine coordinates;
• three_torsion_pt_iff: an affine Fermat point is 3-torsion iff one of its coordinates vanishes.

theorem KasamiCyclicAdditive.FermatCubic.den_ne_zero {K : Type u_1} [Field K] [CharP K 2] {w t : K} (h : w ^ 3 + t ^ 3 = 1) : w + t ≠ 0

An affine Fermat point has w + t ≠ 0.

theorem KasamiCyclicAdditive.FermatCubic.chart_nonsingular {K : Type u_1} [Field K] [CharP K 2] {w t : K} (h : w ^ 3 + t ^ 3 = 1) : (fer K).toAffine.Nonsingular (w + t)⁻¹ (w * (w + t)⁻¹)

The chart coordinates ((w+t)⁻¹, w * (w+t)⁻¹) of an affine Fermat point are nonsingular on fer K.

def KasamiCyclicAdditive.FermatCubic.pt {K : Type u_1} [Field K] [CharP K 2] (w t : K) (h : w ^ 3 + t ^ 3 = 1) : (fer K).toAffine.Point

The affine Fermat point (w,t) viewed in the Weierstrass model fer.

Equations

• KasamiCyclicAdditive.FermatCubic.pt w t h = WeierstrassCurve.Affine.Point.some (w + t)⁻¹ (w * (w + t)⁻¹) ⋯

theorem KasamiCyclicAdditive.FermatCubic.pt_inj {K : Type u_1} [Field K] [CharP K 2] {w t w' t' : K} {h : w ^ 3 + t ^ 3 = 1} {h' : w' ^ 3 + t' ^ 3 = 1} (he : pt w t h = pt w' t' h') : w = w' ∧ t = t'

pt is injective in its two coordinates.

theorem KasamiCyclicAdditive.FermatCubic.neg_pt {K : Type u_1} [Field K] [CharP K 2] {w t : K} (h : w ^ 3 + t ^ 3 = 1) : -pt w t h = pt t w ⋯

Negation on the Fermat cubic swaps the two affine coordinates.

theorem KasamiCyclicAdditive.FermatCubic.hessD_eq_zero_of_den_eq {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) (hdd : w1 + t1 = w2 + t2) : hessD w1 t1 w2 t2 = 0

If two affine Fermat points have the same x-coordinate in the Weierstrass model, then the Hessian denominator vanishes.

theorem KasamiCyclicAdditive.FermatCubic.hessS_ne_zero {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) (hD : hessD w1 t1 w2 t2 ≠ 0) : hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2 ≠ 0

A nonzero Hessian denominator forces the two Hessian numerators to differ.

theorem KasamiCyclicAdditive.FermatCubic.hess_fermat {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) (hD : hessD w1 t1 w2 t2 ≠ 0) : (hessX w1 t1 w2 t2 / hessD w1 t1 w2 t2) ^ 3 + (hessY w1 t1 w2 t2 / hessD w1 t1 w2 t2) ^ 3 = 1

The Hessian sum of two affine Fermat points is again an affine Fermat point, provided the denominator is nonzero.

theorem KasamiCyclicAdditive.FermatCubic.sum_den_ne_zero {K : Type u_1} [Field K] [CharP K 2] {w1 t1 w2 t2 : K} (hdd : w1 + t1 ≠ w2 + t2) : w1 + t1 + (w2 + t2) ≠ 0

If the two points have distinct w+t, then (w1+t1)+(w2+t2) ≠ 0.

theorem KasamiCyclicAdditive.FermatCubic.x_ne_of_den_ne {K : Type u_1} [Field K] {w1 t1 w2 t2 : K} (hdd : w1 + t1 ≠ w2 + t2) : (w1 + t1)⁻¹ ≠ (w2 + t2)⁻¹

Distinct w+t give distinct Weierstrass x-coordinates.

theorem KasamiCyclicAdditive.FermatCubic.secant_slope {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) (hdd : w1 + t1 ≠ w2 + t2) : (fer K).toAffine.slope (w1 + t1)⁻¹ (w2 + t2)⁻¹ (w1 * (w1 + t1)⁻¹) (w2 * (w2 + t2)⁻¹) = (w1 * (w2 + t2) + w2 * (w1 + t1)) / (w1 + t1 + (w2 + t2))

The secant slope through two affine Fermat points with distinct w+t.

theorem KasamiCyclicAdditive.FermatCubic.addX_secant {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) (hdd : w1 + t1 ≠ w2 + t2) : (fer K).toAffine.addX (w1 + t1)⁻¹ (w2 + t2)⁻¹ ((fer K).toAffine.slope (w1 + t1)⁻¹ (w2 + t2)⁻¹ (w1 * (w1 + t1)⁻¹) (w2 * (w2 + t2)⁻¹)) = ((w1 * (w2 + t2) + w2 * (w1 + t1)) ^ 2 * ((w1 + t1) * (w2 + t2)) + (w1 + t1 + (w2 + t2)) ^ 3) / ((w1 + t1 + (w2 + t2)) ^ 2 * ((w1 + t1) * (w2 + t2)))

The x-coordinate of the sum of two affine Fermat points with distinct w+t.

theorem KasamiCyclicAdditive.FermatCubic.add_pt {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) (hD : hessD w1 t1 w2 t2 ≠ 0) : pt w1 t1 h1 + pt w2 t2 h2 = pt (hessX w1 t1 w2 t2 / hessD w1 t1 w2 t2) (hessY w1 t1 w2 t2 / hessD w1 t1 w2 t2) ⋯

The affine Hessian addition formula. If the denominator D0 = w1*t1 + w2*t2 is nonzero, the sum of the two affine Fermat points is the affine Fermat point (N_x/D0, N_y/D0).

theorem KasamiCyclicAdditive.FermatCubic.add_pt_x_eq_zero {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w1 t1 w2 t2 : K} (h1 : w1 ^ 3 + t1 ^ 3 = 1) (h2 : w2 ^ 3 + t2 ^ 3 = 1) (hdd : w1 + t1 ≠ w2 + t2) (hD : hessD w1 t1 w2 t2 = 0) (hS : hessX w1 t1 w2 t2 + hessY w1 t1 w2 t2 ≠ 0) : (fer K).toAffine.addX (w1 + t1)⁻¹ (w2 + t2)⁻¹ ((fer K).toAffine.slope (w1 + t1)⁻¹ (w2 + t2)⁻¹ (w1 * (w1 + t1)⁻¹) (w2 * (w2 + t2)⁻¹)) = 0

If the Hessian denominator vanishes while the two Hessian numerators differ, and the two points have distinct w+t, then the sum is a point at infinity: its x-coordinate is 0.

theorem KasamiCyclicAdditive.FermatCubic.three_torsion_pt_iff {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w t : K} (h : w ^ 3 + t ^ 3 = 1) : 3 • pt w t h = 0 ↔ w = 0 ∨ t = 0

An affine Fermat point is 3-torsion if and only if one of its two affine coordinates vanishes. (The remaining three points of E[3] are the points at infinity.)