The point formula for relative Frobenius

The relative Frobenius isogeny from an affine Weierstrass curve to its Frobenius twist is contravariantly defined on coordinate rings. This file records the corresponding formula on its tautological point: its affine coordinates are the corresponding powers of the generic coordinates. The same formulas are supplied for the iterated relative Frobenius. Reducing the tautological point at the place of a point (x, y) then shows that the r-fold relative Frobenius sends (x, y) to (x ^ p ^ r, y ^ p ^ r), the transport of points along the p ^ r-power Frobenius of the field.

These formulas are the point-level interface of relative Frobenius. They let later arguments compare a pullback defined on coordinate rings with the usual coordinate description of Frobenius, without unfolding either the coordinate ring or the tautological point.

Main results

• TauCeti.Isogeny.xCoord_tautologicalPoint_relativeFrobeniusIsogeny and TauCeti.Isogeny.yCoord_tautologicalPoint_relativeFrobeniusIsogeny give the coordinates of relative Frobenius.
• TauCeti.Isogeny.xCoord_tautologicalPoint_iterateRelativeFrobeniusIsogeny and TauCeti.Isogeny.yCoord_tautologicalPoint_iterateRelativeFrobeniusIsogeny give their iterated counterparts.
• TauCeti.Isogeny.pointMap_iterateRelativeFrobeniusIsogeny: the r-fold relative Frobenius acts on points by (x, y) ↦ (x ^ p ^ r, y ^ p ^ r).

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.11.

theorem TauCeti.Isogeny.xCoord_tautologicalPoint_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (relativeFrobeniusIsogeny p W).pullback.tautologicalPoint.xCoord = W.genericX ^ p

Relative Frobenius sends the generic affine x-coordinate to its p-th power.

Deliberately not @[simp]. Its left-hand side is already reduced by the coordinate-pullback and relative-Frobenius simp lemmas; this named form remains the point-level API.

theorem TauCeti.Isogeny.yCoord_tautologicalPoint_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (relativeFrobeniusIsogeny p W).pullback.tautologicalPoint.yCoord = W.genericY ^ p

Relative Frobenius sends the generic affine y-coordinate to its p-th power.

Deliberately not @[simp]. Its left-hand side is already reduced by the coordinate-pullback and relative-Frobenius simp lemmas; this named form remains the point-level API.

theorem TauCeti.Isogeny.xCoord_tautologicalPoint_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).pullback.tautologicalPoint.xCoord = W.genericX ^ p ^ n

The n-fold relative Frobenius sends the generic affine x-coordinate to its p ^ n-th power.

Deliberately not @[simp]. Its left-hand side is already reduced by the coordinate-pullback and iterated-relative-Frobenius simp lemmas; this named form remains the point-level API.

theorem TauCeti.Isogeny.yCoord_tautologicalPoint_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).pullback.tautologicalPoint.yCoord = W.genericY ^ p ^ n

The n-fold relative Frobenius sends the generic affine y-coordinate to its p ^ n-th power.

Deliberately not @[simp]. Its left-hand side is already reduced by the coordinate-pullback and iterated-relative-Frobenius simp lemmas; this named form remains the point-level API.

@[simp]

theorem TauCeti.Isogeny.pointMap_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [DecidableEq F] [WeierstrassCurve.IsElliptic W] (r : ℕ) (P : W.Point) : (Hom.ofIsogeny (iterateRelativeFrobeniusIsogeny p W r)).pointMap P = WeierstrassCurve.Affine.Point.mapAlong (iterateFrobenius F p r) ⋯ P

Relative Frobenius acts on points by raising the coordinates to the p ^ r-th power: the r-fold relative Frobenius W → W⁽ᵖʳ⁾ sends (x, y) to (x ^ p ^ r, y ^ p ^ r), and the point at infinity to the point at infinity (Silverman II.2.11).