Frobenius fixed points and finite extensions

Let W be an elliptic curve over a finite field F with q elements, and let E/F be a finite extension of degree n embedded in a field K. The points of W over E map bijectively onto the points over K fixed by the nth iterate of the q-power Frobenius. Thus the fixed-point model for points over 𝔽_{qⁿ} has the same count as base change to any chosen such extension.

If K is separably closed, this identifies #W(E) with deg (1 - π ^ n). No algebraicity assumption on K/F is needed. The extension degree is automatically positive, so the zero iterate, whose fixed locus need not be finite, never occurs.

Main results

• TauCeti.Isogeny.Hom.pow_ofIsogeny_baseChangeFrobenius_pointMap_eq_self_iff_mem_range_map: the fixed points are precisely the images of the points over the finite extension.
• TauCeti.Isogeny.Hom.ncard_fixedPoints_pow_ofIsogeny_baseChangeFrobenius_eq_pointCount: the fixed-point count agrees with the chosen-extension count.
• TauCeti.Isogeny.Hom.degree_one_sub_pow_ofIsogeny_baseChangeFrobenius_eq_pointCount: over separably closed constants the degree is the chosen-extension count.

References

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

theorem TauCeti.Isogeny.Hom.pow_ofIsogeny_baseChangeFrobenius_pointMap_eq_self_iff_mem_range_map {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Finite F] [Field E] [Finite E] [Field K] [Algebra F E] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [DecidableEq E] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (P : (WeierstrassCurve.toAffine (W.baseChange K)).Point) : (ofIsogeny (baseChangeFrobenius K W) ^ Module.finrank F E).pointMap P = P ↔ P ∈ Set.range ⇑(WeierstrassCurve.Affine.Point.map (IsScalarTower.toAlgHom F E K))

The points fixed by Frobenius to the extension degree are exactly the points coming from that finite extension. This holds in any ambient field containing the extension.

theorem TauCeti.Isogeny.Hom.ncard_fixedPoints_pow_ofIsogeny_baseChangeFrobenius_eq_pointCount {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Finite F] [Field E] [Finite E] [Field K] [Algebra F E] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : {P : (WeierstrassCurve.toAffine (W.baseChange K)).Point | (ofIsogeny (baseChangeFrobenius K W) ^ Module.finrank F E).pointMap P = P}.ncard = WeierstrassCurve.pointCount (W.baseChange E)

The number of points fixed by the extension-degree iterate of Frobenius is the point count of the base change to that extension. The point at infinity is included on both sides.

theorem TauCeti.Isogeny.Hom.degree_one_sub_pow_ofIsogeny_baseChangeFrobenius_eq_pointCount {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Finite F] [Field E] [Finite E] [Field K] [Algebra F E] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [IsSepClosed K] : (1 - ofIsogeny (baseChangeFrobenius K W) ^ Module.finrank F E).degree = WeierstrassCurve.pointCount (W.baseChange E)

Over a separably closed ambient field, the degree of 1 - π ^ [E:F] is #W(E). This compares the intrinsic isogeny degree with a chosen finite-extension model.