Iterated Frobenius and its fixed points

For an elliptic curve over a finite field with q elements, the nth power of its Frobenius endomorphism acts on geometric points by raising both coordinates to q ^ n. For positive n, 1 - π ^ n is a nonzero separable isogeny: it pulls the invariant differential back to itself. Over a separably closed extension, its degree therefore counts exactly the points fixed by π ^ n. The fixed locus is finite, so this count can supply the coefficients of the elliptic curve's zeta function without choosing a model of the field with q ^ n elements.

The iteration and coordinate formulas hold over any extension of the finite field. Separably closed constants enter only in the degree count. The positive-iterate restriction is essential: at n = 0 the fixed locus is the whole geometric point group and 1 - π ^ n = 0.

Main results

• TauCeti.Isogeny.Hom.pow_ofIsogeny_baseChangeFrobenius_pointMap: the action is the iterated coordinate Frobenius, with coordinate formulas below.
• TauCeti.Isogeny.Hom.one_sub_pow_ofIsogeny_baseChangeFrobenius_ne_zero and isSeparable_toIsogeny_one_sub_pow_ofIsogeny_baseChangeFrobenius: positive iterates give nonzero separable difference isogenies.
• TauCeti.Isogeny.Hom.ncard_fixedPoints_pow_ofIsogeny_baseChangeFrobenius: the fixed-point count is deg (1 - π ^ n).
• TauCeti.Isogeny.Hom.finite_fixedPoints_pow_ofIsogeny_baseChangeFrobenius: the fixed locus is finite even without a closure hypothesis.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, V.2.3.

@[simp]

theorem TauCeti.Isogeny.Hom.pullbackDifferential_pow_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) (hn : 0 < n) : (ofIsogeny (baseChangeFrobenius K W) ^ n).pullbackDifferential (WeierstrassCurve.toAffine (W.baseChange K)).invariantDifferential = 0

Every positive power of Frobenius kills the invariant differential.

theorem TauCeti.Isogeny.Hom.one_sub_pow_ofIsogeny_baseChangeFrobenius_ne_zero {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) (hn : 0 < n) : 1 - ofIsogeny (baseChangeFrobenius K W) ^ n ≠ 0

The difference between the identity and a positive Frobenius iterate is nonzero.

theorem TauCeti.Isogeny.Hom.isSeparable_toIsogeny_one_sub_pow_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (n : ℕ) (hn : 0 < n) : Algebra.IsSeparable (↥(toIsogeny ⋯).fieldPullback.fieldRange) (WeierstrassCurve.toAffine (W.baseChange K)).FunctionField

The difference between the identity and a positive Frobenius iterate is separable.

theorem TauCeti.Isogeny.Hom.pow_ofIsogeny_baseChangeFrobenius_pointMap {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] [Fintype F] (n : ℕ) (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : (ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P = (WeierstrassCurve.Affine.Point.map (FiniteField.frobeniusAlgHom F K ^ n)) P

Iterated Frobenius on points agrees with mapping by the power of the coordinate Frobenius.

@[simp]

theorem TauCeti.Isogeny.Hom.xCoord_pow_ofIsogeny_baseChangeFrobenius_pointMap {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] (n : ℕ) (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : ((ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P).xCoord = P.xCoord ^ Nat.card F ^ n

The x-coordinate of the nth Frobenius iterate is raised to q ^ n.

@[simp]

theorem TauCeti.Isogeny.Hom.yCoord_pow_ofIsogeny_baseChangeFrobenius_pointMap {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] (n : ℕ) (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : ((ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P).yCoord = P.yCoord ^ Nat.card F ^ n

The y-coordinate of the nth Frobenius iterate is raised to q ^ n.

@[simp]

theorem TauCeti.Isogeny.Hom.pow_ofIsogeny_baseChangeFrobenius_pointMap_eq_self_iff {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] (n : ℕ) (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : (ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P = P ↔ P.xCoord ^ Nat.card F ^ n = P.xCoord ∧ P.yCoord ^ Nat.card F ^ n = P.yCoord

A point is fixed by the nth Frobenius iterate exactly when both its affine coordinates are fixed by q ^ n-powering. This includes the point at infinity.

theorem TauCeti.Isogeny.Hom.finite_fixedPoints_pow_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] (n : ℕ) (hn : 0 < n) : {P : (WeierstrassCurve.toAffine (W.baseChange K)).Point | (ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P = P}.Finite

The points fixed by a positive Frobenius iterate form a finite set over any extension.

theorem TauCeti.Isogeny.Hom.ncard_fixedPoints_pow_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] [IsSepClosed K] (n : ℕ) (hn : 0 < n) : {P : (WeierstrassCurve.toAffine (W.baseChange K)).Point | (ofIsogeny (baseChangeFrobenius K W) ^ n).pointMap P = P}.ncard = (1 - ofIsogeny (baseChangeFrobenius K W) ^ n).degree

Over a separably closed extension, deg (1 - π ^ n) counts the points fixed by π ^ n for every positive n (Silverman V.2.3).