The Frobenius over an extension of the finite base

Let W be a Weierstrass curve over a finite field F with q elements, and K an extension of F. The q-power Frobenius isogeny of W base-changes along F → K to an isogeny π of W⁄K, TauCeti.Isogeny.baseChangeFrobenius. Its pullback raises the functions defined over F, the generic coordinates in particular, to the q-th power. Over K itself the q-power map is not the identity, and it is this base change that acts on the points of W over K.

Main definitions

• TauCeti.Isogeny.baseChangeFrobenius: the q-power Frobenius of W, as an isogeny of W⁄K.

Main results

• TauCeti.Isogeny.baseChangeFrobenius_pullback: its coordinate pullback is the base change of the q-power Frobenius pullback of W.
• TauCeti.Isogeny.baseChangeFrobenius_def: identifies the base-changed Frobenius with Isogeny.map, allowing scalar-extension results to transfer to W⁄K.
• TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_map: its pullback raises the functions defined over F to the q-th power.
• TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_genericX and TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_genericY: in particular the generic coordinates.

References

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

noncomputable def TauCeti.Isogeny.baseChangeFrobenius {F : Type u_1} (K : Type u_2) [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) : Isogeny (WeierstrassCurve.toAffine (W.baseChange K)) (WeierstrassCurve.toAffine (W.baseChange K))

The Frobenius of W over an extension K of its finite base: the base change of the q-power Frobenius isogeny, read as an isogeny of W⁄K.

Equations

• TauCeti.Isogeny.baseChangeFrobenius K W = (TauCeti.Isogeny.frobeniusIsogeny W).map (algebraMap F K)

theorem TauCeti.Isogeny.baseChangeFrobenius_def {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) : baseChangeFrobenius K W = (frobeniusIsogeny W).map (algebraMap F K)

Identify baseChangeFrobenius K W with the Isogeny.map presentation over W.map (algebraMap F K), so scalar-extension results transfer to W⁄K without unfolding the definition in an importing module.

@[simp]

theorem TauCeti.Isogeny.baseChangeFrobenius_pullback {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) : (baseChangeFrobenius K W).pullback = (frobeniusPullback W).map (algebraMap F K)

The coordinate pullback of baseChangeFrobenius is the base change along F → K of the q-power Frobenius pullback of W.

theorem TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_map {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) (z : W.FunctionField) : (baseChangeFrobenius K W).fieldPullback ((WeierstrassCurve.Affine.FunctionField.map W (algebraMap F K)) z) = (WeierstrassCurve.Affine.FunctionField.map W (algebraMap F K)) z ^ Nat.card F

The pullback of baseChangeFrobenius raises the functions defined over F to the q-th power.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_genericX {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) : (baseChangeFrobenius K W).fieldPullback (WeierstrassCurve.toAffine (W.baseChange K)).genericX = (WeierstrassCurve.toAffine (W.baseChange K)).genericX ^ Nat.card F

The pullback of baseChangeFrobenius raises the generic x-coordinate to the q-th power.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_baseChangeFrobenius_genericY {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) : (baseChangeFrobenius K W).fieldPullback (WeierstrassCurve.toAffine (W.baseChange K)).genericY = (WeierstrassCurve.toAffine (W.baseChange K)).genericY ^ Nat.card F

The pullback of baseChangeFrobenius raises the generic y-coordinate to the q-th power.