The Frobenius on torsion

Let W be an elliptic curve over a finite field F with q elements, and K an extension of F. The base-changed q-power Frobenius π of W⁄K (TauCeti.Isogeny.baseChangeFrobenius) acts on the points of W over K as the q-power map on coordinates. When K is algebraic over F, that map is the Frobenius automorphism σ of K over F, so on N-torsion π acts as the Galois automorphism σ.

When moreover K is separably closed and N is invertible in K, the Weil pairing is Galois-equivariant, and σ raises roots of unity to the q-th power, so π scales the Weil pairing by q. Hence the determinant of the action of π on E[N] is q = deg π modulo N, although π is inseparable (the Frobenius case of Silverman III.8.6). This is the determinant of the Frobenius matrix in the Weil-pairing proof of the Hasse bound. The isogeny 1 - π, and r π - s when the characteristic does not divide s, are separable, so they are covered by TauCeti.Isogeny.Hom.det_torsionLinearMap_ofIsogeny.

Main results

• TauCeti.Isogeny.Hom.pointMap_ofIsogeny_baseChangeFrobenius: π acts on points as the q-power map on coordinates.
• TauCeti.Isogeny.Hom.torsionLinearMap_ofIsogeny_baseChangeFrobenius_apply: over an algebraic extension, π acts on N-torsion as the Frobenius automorphism.
• TauCeti.Isogeny.Hom.det_torsionLinearMap_ofIsogeny_baseChangeFrobenius: the determinant of the action of π on E[N] is q.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.8.1 and III.8.6.

@[simp]

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

The Frobenius acts on points as the q-power map on coordinates: π (x, y) = (x ^ q, y ^ q).

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_ofIsogeny_baseChangeFrobenius_apply {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Fintype F] [Algebra.IsAlgebraic F K] (N : ℕ) (P : ↥(AddSubgroup.torsionBy (WeierstrassCurve.toAffine (W.baseChange K)).Point ↑N)) : ((ofIsogeny (baseChangeFrobenius K W)).torsionLinearMap N) P = (Multiplicative.toAdd ((WeierstrassCurve.torsionGaloisAction W ↑N) (FiniteField.frobeniusAlgEquivOfAlgebraic F K))) P

Over an algebraic extension, the Frobenius acts on N-torsion as the Frobenius automorphism FiniteField.frobeniusAlgEquivOfAlgebraic F K.

theorem TauCeti.Isogeny.Hom.det_torsionLinearMap_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [Finite F] [Algebra.IsAlgebraic F K] [IsSepClosed K] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) : LinearMap.det ((ofIsogeny (baseChangeFrobenius K W)).torsionLinearMap N) = ↑(Nat.card F)

The determinant of the action of the Frobenius on E[N] is q = #F, over a separably closed algebraic extension K of the finite base F in which N is invertible.