Frobenius as a group endomorphism of the Fermat cubic, and its kernel

This file supplies the two pieces of infrastructure that the geometric bridging statements of Assembly/GeometricChain.lean need but that no other module provides.

1. Frobenius as an endomorphism. frobPt is the squaring map π on (fer K).toAffine.Point, packaged as an AddMonoidHom. It is obtained from Mathlib's WeierstrassCurve.Affine.Point.map applied to the Frobenius x ↦ x ^ 2, viewed as a ℤ-algebra map (every ring hom is one), together with the transport along ferZ.baseChange K = fer K. The computation rules frobPt_pt and frobPt_ptInf say that π squares the coordinates in both charts of FermatCubic.

2. The kernel dictionary. isKernelPoint_iff identifies KasamiCyclicAdditive.FermatCubicFrobenius.IsKernelPoint of Geometry/FermatCubic/RationalKernel.lean — a condition on homogeneous triples — with the group-theoretic condition π^k P = -P. Combined with KasamiCyclicAdditive.FermatCubicFrobenius.rational_kernel_odd this gives kernel_trivial_odd: for odd n the map 1 + π^k is injective on E(K).

point_repr classifies the points of E(K): every one is the origin, a point at infinity ptInf a, or an affine Fermat point pt w t. This is what lets the two charts of FermatCubic be used exhaustively.

The Frobenius endomorphism

def KasamiCyclicAdditive.PointFrobenius.ferZ : WeierstrassCurve ℤ

The Fermat cubic in Weierstrass form over ℤ; fer K is its base change.

Equations

• KasamiCyclicAdditive.PointFrobenius.ferZ = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 1 }

theorem KasamiCyclicAdditive.PointFrobenius.ferZ_baseChange {K : Type u_1} [Field K] : ferZ.baseChange K = FermatCubic.fer K

fer K is the base change of ferZ along ℤ → K.

def KasamiCyclicAdditive.PointFrobenius.curveCast {K : Type u_1} [Field K] [DecidableEq K] {W W' : WeierstrassCurve K} (h : W = W') : W.toAffine.Point ≃+ W'.toAffine.Point

Transport points along an equality of curves.

Equations

• KasamiCyclicAdditive.PointFrobenius.curveCast h = h ▸ AddEquiv.refl W.toAffine.Point

theorem KasamiCyclicAdditive.PointFrobenius.curveCast_some {K : Type u_1} [Field K] [DecidableEq K] {W W' : WeierstrassCurve K} (h : W = W') {x y : K} (hns : W.toAffine.Nonsingular x y) : (curveCast h) (WeierstrassCurve.Affine.Point.some x y hns) = WeierstrassCurve.Affine.Point.some x y ⋯

curveCast leaves the coordinates of an affine point unchanged.

theorem KasamiCyclicAdditive.PointFrobenius.curveCast_symm_some {K : Type u_1} [Field K] [DecidableEq K] {W W' : WeierstrassCurve K} (h : W = W') {x y : K} (hns : W'.toAffine.Nonsingular x y) : (curveCast h).symm (WeierstrassCurve.Affine.Point.some x y hns) = WeierstrassCurve.Affine.Point.some x y ⋯

The inverse of curveCast likewise leaves the coordinates unchanged.

noncomputable def KasamiCyclicAdditive.PointFrobenius.frobPt (K : Type u_2) [Field K] [DecidableEq K] [CharP K 2] : (FermatCubic.fer K).toAffine.Point →+ (FermatCubic.fer K).toAffine.Point

Frobenius as a group endomorphism of E(K).

Equations

• One or more equations did not get rendered due to their size.

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

π squares both Fermat coordinates.

theorem KasamiCyclicAdditive.PointFrobenius.frobPt_ptInf {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] {a : K} (ha : a ^ 3 = 1) : (frobPt K) (FermatCubic.ptInf a ha) = FermatCubic.ptInf (a ^ 2) ⋯

π squares the parameter of a point at infinity.

theorem KasamiCyclicAdditive.PointFrobenius.frobPt_frobPt {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] (P : (FermatCubic.fer K).toAffine.Point) : (frobPt K) ((frobPt K) P) = -2 • P

The CM relation. fer is defined over 𝔽₂, where it has exactly three points, so its trace of Frobenius is a = 2 + 1 - 3 = 0 and π² + 2 = 0 in the endomorphism ring.

Iterated Frobenius

noncomputable def KasamiCyclicAdditive.PointFrobenius.frobEnd (K : Type u_2) [Field K] [DecidableEq K] [CharP K 2] : AddMonoid.End (FermatCubic.fer K).toAffine.Point

π as an element of the endomorphism monoid, so that π ^ k is available.

Equations

• KasamiCyclicAdditive.PointFrobenius.frobEnd K = KasamiCyclicAdditive.PointFrobenius.frobPt K

theorem KasamiCyclicAdditive.PointFrobenius.frobEnd_pow_pt {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] (k : ℕ) {w t : K} (h : w ^ 3 + t ^ 3 = 1) : (frobEnd K ^ k) (FermatCubic.pt w t h) = FermatCubic.pt (w ^ 2 ^ k) (t ^ 2 ^ k) ⋯

π ^ k raises both Fermat coordinates to the 2 ^ k.

theorem KasamiCyclicAdditive.PointFrobenius.frobEnd_pow_ptInf {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] (k : ℕ) {a : K} (ha : a ^ 3 = 1) : (frobEnd K ^ k) (FermatCubic.ptInf a ha) = FermatCubic.ptInf (a ^ 2 ^ k) ⋯

π ^ k raises the parameter of a point at infinity to the 2 ^ k.

Classification of the points of E(K)

Every point is the origin, a point at infinity, or an affine Fermat point. This is what makes the two charts of FermatCubic exhaustive.

theorem KasamiCyclicAdditive.PointFrobenius.point_repr {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] (P : (FermatCubic.fer K).toAffine.Point) : P = 0 ∨ (∃ (a : K) (ha : a ^ 3 = 1), P = FermatCubic.ptInf a ha) ∨ ∃ (w : K) (t : K) (h : w ^ 3 + t ^ 3 = 1), P = FermatCubic.pt w t h

The two charts of FermatCubic cover E(K).

instance KasamiCyclicAdditive.PointFrobenius.instFinitePoint {K : Type u_1} [Field K] [Finite K] : Finite (FermatCubic.fer K).toAffine.Point

E(K) is finite when K is.

The kernel of 1 + π^k

KasamiCyclicAdditive.FermatCubicFrobenius.IsKernelPoint of Geometry/FermatCubic/RationalKernel.lean is a statement about homogeneous triples; on the affine chart it is exactly π^k P = -P.

theorem KasamiCyclicAdditive.PointFrobenius.isKernelPoint_iff {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] {k : ℕ} {w t : K} (h : w ^ 3 + t ^ 3 = 1) : FermatCubicFrobenius.IsKernelPoint k w t 1 ↔ (frobEnd K ^ k) (FermatCubic.pt w t h) = -FermatCubic.pt w t h

The dictionary. For an affine Fermat point, Geometry/FermatCubic/RationalKernel.lean's triple condition IsKernelPoint k W T 1 is the group-theoretic statement π^k P = -P.

theorem KasamiCyclicAdditive.PointFrobenius.kernel_trivial_odd {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] [Fintype K] {n k : ℕ} (hn : Odd n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) {P : (FermatCubic.fer K).toAffine.Point} (hP : (frobEnd K ^ k) P + P = 0) : P = 0

Trivial rational kernel for odd n. The map 1 + π^k is injective on E(K): its only zero is the origin. This is KasamiCyclicAdditive.FermatCubicFrobenius.rational_kernel_odd transported through the dictionary.