The Frobenius acts on points as the q-power map

Let W be an elliptic curve over a finite field F with q elements, and K an extension of F. The q-power Frobenius isogeny of W base-changes to an isogeny π of W⁄K, whose pullback raises the functions defined over F to the q-th power. Every point P of W over K has a place of degree one of the function field of W⁄K (WeierstrassCurve.Affine.pointEquivDegreeOnePlace). The tautological point of π is π evaluated at the generic point, and its reduction at the place of P (WeierstrassCurve.Affine.reductionOfDegreeEqOne) is π evaluated at P. This file computes that reduction: it is

π (x, y) = (x ^ q, y ^ q),

the image of P under the point map induced by the q-power Frobenius of K over F. So the points of W over K fixed by π are those with coordinates in F, and π commutes with every point map induced by a field map over F. On the torsion of W over a separable closure of F, π is therefore the Galois Frobenius of F, which is the form in which it enters the count of the points of W over F and the Hasse bound. The comparison with the class-group point map TauCeti.Isogeny.toPointHom is not made here.

Main results

• TauCeti.Isogeny.reductionOfDegreeEqOne_tautologicalPoint_baseChangeFrobenius: at the place of P, the tautological point of the base-changed Frobenius TauCeti.Isogeny.baseChangeFrobenius reduces to the image of P under Point.map (FiniteField.frobeniusAlgHom F K), the q-power map on coordinates.

References

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

theorem TauCeti.Isogeny.reductionOfDegreeEqOne_tautologicalPoint_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [Field K] [Algebra F K] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : ((WeierstrassCurve.toAffine (W.baseChange K)).reductionOfDegreeEqOne ⋯) (baseChangeFrobenius K W).pullback.tautologicalPoint = (WeierstrassCurve.Affine.Point.equivBaseChangeSelf (W.baseChange K)) ((WeierstrassCurve.Affine.Point.map (FiniteField.frobeniusAlgHom F K)) P)

The Frobenius acts on points as the q-power map on coordinates: at the place of a point P of W over K, the tautological point of the base-changed Frobenius π reduces to π (x, y) = (x ^ q, y ^ q), the image of P under the q-power Frobenius of K over F.