The Fermat cubic X^3 + Y^3 = Z^3 in characteristic two, via a Weierstrass model

Over a field K of characteristic two the Fermat cubic E : X^3+Y^3=Z^3 with origin O = [1:1:0] is isomorphic to the Weierstrass curve

fer :  y^2 + y = x^3 + 1

through x = Z/(X+Y), y = X/(X+Y). Under this isomorphism:

• the affine Fermat points (w,t), w^3+t^3=1, correspond to the points with x ≠ 0 (note w + t ≠ 0 is automatic);
• the three points at infinity [1:α:0], α^3=1, correspond to O and the two points with x = 0.

All group-law statements are proved in this model.

def KasamiCyclicAdditive.FermatCubic.fer (K : Type u_2) [Field K] : WeierstrassCurve K

The Weierstrass model y^2 + y = x^3 + 1 of the Fermat cubic in characteristic two.

Equations

• KasamiCyclicAdditive.FermatCubic.fer K = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 1 }

The Weierstrass coefficients of fer, as simp lemmas.

@[simp]

theorem KasamiCyclicAdditive.FermatCubic.fer_a1 {K : Type u_1} [Field K] : (fer K).a₁ = 0

@[simp]

theorem KasamiCyclicAdditive.FermatCubic.fer_a2 {K : Type u_1} [Field K] : (fer K).a₂ = 0

@[simp]

theorem KasamiCyclicAdditive.FermatCubic.fer_a3 {K : Type u_1} [Field K] : (fer K).a₃ = 1

@[simp]

theorem KasamiCyclicAdditive.FermatCubic.fer_a4 {K : Type u_1} [Field K] : (fer K).a₄ = 0

@[simp]

theorem KasamiCyclicAdditive.FermatCubic.fer_a6 {K : Type u_1} [Field K] : (fer K).a₆ = 1

theorem KasamiCyclicAdditive.FermatCubic.eq_of_nonsingular {K : Type u_1} [Field K] {x y : K} (h : (fer K).toAffine.Nonsingular x y) : y ^ 2 + y = x ^ 3 + 1

The Weierstrass equation of fer in the form y^2 + y = x^3 + 1.

theorem KasamiCyclicAdditive.FermatCubic.some_eq_some {K : Type u_1} [Field K] {x₁ y₁ x₂ y₂ : K} (h₁ : (fer K).toAffine.Nonsingular x₁ y₁) (h₂ : (fer K).toAffine.Nonsingular x₂ y₂) (hx : x₁ = x₂) (hy : y₁ = y₂) : WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ = WeierstrassCurve.Affine.Point.some x₂ y₂ h₂

Two affine points of fer agree once their coordinates do.

theorem KasamiCyclicAdditive.FermatCubic.some_inj {K : Type u_1} [Field K] {x₁ y₁ x₂ y₂ : K} {h₁ : (fer K).toAffine.Nonsingular x₁ y₁} {h₂ : (fer K).toAffine.Nonsingular x₂ y₂} (h : WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ = WeierstrassCurve.Affine.Point.some x₂ y₂ h₂) : x₁ = x₂ ∧ y₁ = y₂

Equal affine points of fer have equal coordinates.

theorem KasamiCyclicAdditive.FermatCubic.nonsingular_of_eq {K : Type u_1} [Field K] [CharP K 2] {x y : K} (h : y ^ 2 + y = x ^ 3 + 1) : (fer K).toAffine.Nonsingular x y

Nonsingularity is automatic on y^2+y = x^3+1 in characteristic two.

theorem KasamiCyclicAdditive.FermatCubic.negY_eq {K : Type u_1} [Field K] [CharP K 2] (x y : K) : (fer K).toAffine.negY x y = y + 1

The negation on fer is (x,y) ↦ (x, y+1).

theorem KasamiCyclicAdditive.FermatCubic.addX_eq {K : Type u_1} [Field K] [CharP K 2] (x₁ x₂ l : K) : (fer K).toAffine.addX x₁ x₂ l = l ^ 2 + x₁ + x₂

Char-two form of addX: l^2 + x₁ + x₂.

theorem KasamiCyclicAdditive.FermatCubic.addY_eq {K : Type u_1} [Field K] [CharP K 2] (x₁ x₂ y₁ l : K) : (fer K).toAffine.addY x₁ x₂ y₁ l = l * ((fer K).toAffine.addX x₁ x₂ l + x₁) + y₁ + 1

Char-two form of addY: l * (addX + x₁) + y₁ + 1.

theorem KasamiCyclicAdditive.FermatCubic.Y_ne_negY {K : Type u_1} [Field K] [CharP K 2] (x y : K) : y ≠ (fer K).toAffine.negY x y

y and negY x y = y + 1 differ, so no affine point of fer is 2-torsion.

theorem KasamiCyclicAdditive.FermatCubic.slope_self {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] (x y : K) : (fer K).toAffine.slope x x y y = x ^ 2

The tangent slope at (x,y) is x^2.

theorem KasamiCyclicAdditive.FermatCubic.slope_ne {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {x₁ x₂ y₁ y₂ : K} (hx : x₁ ≠ x₂) : (fer K).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ + y₂) / (x₁ + x₂)

The secant slope is (y₁ + y₂) / (x₁ + x₂).

theorem KasamiCyclicAdditive.FermatCubic.three_torsion_some_iff {K : Type u_1} [Field K] [CharP K 2] [DecidableEq K] {x y : K} (h : (fer K).toAffine.Nonsingular x y) : 3 • WeierstrassCurve.Affine.Point.some x y h = 0 ↔ x ^ 4 = x

An affine point of fer is 3-torsion exactly when its x-coordinate satisfies x^4 = x.