Documentation

LeanPool.KasamiCyclicAdditive.Geometry.FermatCubic.Infinity

The points at infinity of the Fermat cubic and the diagonal translation formula #

The three points at infinity P_a = [1:a:0], a^3 = 1, of the Fermat cubic correspond in the Weierstrass model fer to the origin (a = 1) and to the two affine points (0,a) with a^2+a+1 = 0. They form the set K0: neg_ptInf shows -P_a = P_{a^2} = pi(P_a), i.e. (1+pi) P_a = O, and three_torsion_ptInf shows K0 ⊆ E[3].

The main result is the diagonal translation formula:

(w,t) + P_a = (a*w, a^{-1}*t)          (a^{-1} = a^2).
source
theorem KasamiCyclicAdditive.FermatCubic.cube_root_rel {K : Type u_1} [Field K] [CharP K 2] {a : K} (ha : a ^ 3 = 1) (ha1 : a ≠ 1) :
a ^ 2 + a + 1 = 0

A cube root of unity other than 1 satisfies a^2 + a + 1 = 0.

source
theorem KasamiCyclicAdditive.FermatCubic.cube_root_of_rel {K : Type u_1} [Field K] [CharP K 2] {a : K} (ha2 : a ^ 2 + a + 1 = 0) :
a ^ 3 = 1

Conversely, a^2 + a + 1 = 0 makes a a cube root of unity.

source
theorem KasamiCyclicAdditive.FermatCubic.inf_nonsingular {K : Type u_1} [Field K] [CharP K 2] {a : K} (ha2 : a ^ 2 + a + 1 = 0) :
(fer K).toAffine.Nonsingular 0 a

(0, a) with a^2 + a + 1 = 0 is a nonsingular point of fer K.

source
def KasamiCyclicAdditive.FermatCubic.ptInf {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] (a : K) (ha : a ^ 3 = 1) :
(fer K).toAffine.Point

The point at infinity P_a = [1:a:0] of the Fermat cubic, a^3 = 1, in the Weierstrass model. For a = 1 this is the origin O = [1:1:0].

Equations
Instances For
    source
    @[simp]
    theorem KasamiCyclicAdditive.FermatCubic.ptInf_one {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] :
    ptInf 1 ⋯ = 0

    P_1 is the origin.

    source
    theorem KasamiCyclicAdditive.FermatCubic.ptInf_ne_one {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {a : K} (ha : a ^ 3 = 1) (ha1 : a ≠ 1) :
    ptInf a ha = WeierstrassCurve.Affine.Point.some 0 a ⋯

    For a ≠ 1 the point at infinity P_a is the affine point (0, a).

    source
    theorem KasamiCyclicAdditive.FermatCubic.three_torsion_ptInf {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {a : K} (ha : a ^ 3 = 1) :
    3 • ptInf a ha = 0

    Every point at infinity is 3-torsion: K0 ⊆ E[3].

    source
    theorem KasamiCyclicAdditive.FermatCubic.pt_congr {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) (hw : w = w') (ht : t = t') :
    pt w t h = pt w' t' h'

    Affine Fermat points with equal coordinates are equal, whatever proof of the Fermat equation each carries.

    source
    theorem KasamiCyclicAdditive.FermatCubic.add_ptInf {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {w t a : K} (h : w ^ 3 + t ^ 3 = 1) (ha : a ^ 3 = 1) :
    pt w t h + ptInf a ha = pt (a * w) (a ^ 2 * t) ⋯

    The diagonal translation formula: (w,t) + P_a = (a*w, a^{-1}*t).