The Frobenius isogeny

Over a finite field F with q = Nat.card F elements, raising to the q-th power is an F-algebra endomorphism of any F-algebra (FiniteField.frobeniusAlgHom). Composing it with the embedding of the coordinate ring into the function field gives a coordinate pullback, and that pullback maps infinity to infinity, so it is an isogeny of W with itself. It is purely inseparable of degree q.

The declarations take [Finite F] rather than [Fintype F], matching Affine/FunctionField/FrobeniusTower.lean, and state the exponent as Nat.card F: a Fintype instance is chosen enumeration data, and neither the definitions nor the statements should depend on it. The instance Mathlib's map needs is installed locally where it is required.

Main definitions

• TauCeti.Isogeny.frobeniusPullback: the coordinate pullback x ↦ x ^ q.
• TauCeti.Isogeny.frobeniusIsogeny: the same map packaged as an Isogeny W W.

Main results

• AlgHom.comp_fieldPullback_frobeniusIsogeny: an algebra homomorphism between function fields commutes with the Frobenius pullbacks.

• TauCeti.Isogeny.fieldPullback_frobeniusIsogeny: the induced map of function fields is the q-power map FiniteField.frobeniusAlgHom F W.FunctionField.

• TauCeti.Isogeny.fieldPullback_frobeniusIsogeny_apply: the same result pointwise, with no choice of a Fintype instance exposed in its statement.

• TauCeti.Isogeny.isPurelyInseparable_frobeniusIsogeny: the induced function-field extension is purely inseparable.

• TauCeti.Isogeny.degree_frobeniusIsogeny: the Frobenius isogeny has degree q.

• TauCeti.Isogeny.frobeniusIsogeny_ne_id: the Frobenius isogeny is not the identity.

• TauCeti.Isogeny.separableDegree_frobeniusIsogeny and TauCeti.Isogeny.inseparableDegree_frobeniusIsogeny: its separable and inseparable degrees are 1 and q, respectively.

The MapsInfinity condition says that each x of the coordinate ring is integral over the pulled-back copy. It holds because x is a q-th root of its own pullback, so IsIntegral.of_pow reduces it to integrality of an element the pullback already produces. That is what "Frobenius fixes the point at infinity" amounts to here.

Pure inseparability follows because every function x has its q-th power in the image of the pullback, and q is a power of the exponential characteristic of F. The degree is the field-theoretic WeierstrassCurve.Affine.finrank_fieldRange_frobeniusAlgHom, [K(W) : K(W)^q] = q, transported along the identification of fieldPullback with the q-power map on K(W). That identification is Isogeny.fieldPullback_unique: both maps restrict to x ↦ x ^ q on the coordinate ring, and only one extension to the fraction field exists.

This is the frobeniusIsogeny seed of TauCetiRoadmap/EllipticCurves/README.md §Layer 1, where it is described as "f ↦ f ^ q out of the coordinate ring into the function field … whose MapsInfinity is the integrality of the coordinates over their q-th powers". The seed follows Silverman, The Arithmetic of Elliptic Curves, II.2.11: part (a) identifies the pullback image with the q-th powers, part (b) proves pure inseparability, and part (c) computes the degree. The roadmap's Suggested.lean states the pullback and degree with sorry; the formal proofs here are original.

References

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

noncomputable def TauCeti.Isogeny.frobeniusPullback {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : CoordinatePullback W W

The Frobenius coordinate pullback: an element of the coordinate ring is sent to its q-th power, viewed in the function field, where q = Nat.card F.

Equations

• TauCeti.Isogeny.frobeniusPullback W = (IsScalarTower.toAlgHom F W.CoordinateRing W.FunctionField).comp (FiniteField.frobeniusAlgHom F W.CoordinateRing)

@[simp]

theorem TauCeti.Isogeny.frobeniusPullback_apply {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) (x : W.CoordinateRing) : (frobeniusPullback W) x = (algebraMap W.CoordinateRing W.FunctionField) (x ^ Nat.card F)

The Frobenius pullback raises to the q-th power.

theorem TauCeti.Isogeny.mapsInfinity_frobeniusPullback {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusPullback W).MapsInfinity

Frobenius maps the point at infinity to itself. An element of the coordinate ring is a q-th root of its own pullback, so it is integral over the pulled-back copy.

noncomputable def TauCeti.Isogeny.frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : Isogeny W W

The Frobenius isogeny of a Weierstrass curve over a finite field.

Equations

• TauCeti.Isogeny.frobeniusIsogeny W = { pullback := TauCeti.Isogeny.frobeniusPullback W, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.frobeniusIsogeny_pullback {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).pullback = frobeniusPullback W

The Frobenius isogeny's pullback is the q-th power map.

theorem TauCeti.Isogeny.fieldPullback_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).fieldPullback = FiniteField.frobeniusAlgHom F W.FunctionField

The function field pullback of the Frobenius isogeny is the q-power map on the function field (Silverman II.2.11(a)): the two maps agree on the coordinate ring, and an isogeny's fieldPullback is the only such extension.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_frobeniusIsogeny_apply {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) (x : W.FunctionField) : (frobeniusIsogeny W).fieldPullback x = x ^ Nat.card F

The function-field pullback raises every element to the q-th power (Silverman II.2.11(a)). Unlike fieldPullback_frobeniusIsogeny, this consumer-facing pointwise form depends only on [Finite F] and Nat.card F; the locally chosen enumeration of F does not occur in its statement.

instance TauCeti.Isogeny.isPurelyInseparable_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : IsPurelyInseparable (↥(frobeniusIsogeny W).fieldPullback.fieldRange) W.FunctionField

The Frobenius isogeny is purely inseparable (Silverman II.2.11(b)). This is the field-generic pure-inseparability of the q-power map, transported across the identification of that map with the function-field pullback.

@[simp]

theorem TauCeti.Isogeny.degree_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).degree = Nat.card F

The Frobenius isogeny has degree q (Silverman II.2.11(c)). Its function-field pullback is the q-power map, so the extension the degree measures is K(W) over its subfield of q-th powers.

@[simp]

theorem TauCeti.Isogeny.frobeniusIsogeny_ne_id {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : frobeniusIsogeny W ≠ id W

Frobenius is not the identity: its degree is the size of the field, not one.

theorem TauCeti.Isogeny.separableDegree_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).separableDegree = 1

The Frobenius isogeny has separable degree one, as pure inseparability in Silverman II.2.11(b) requires.

theorem TauCeti.Isogeny.inseparableDegree_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).inseparableDegree = Nat.card F

The Frobenius isogeny has inseparable degree q, combining Silverman II.2.11(b,c).

theorem AlgHom.comp_fieldPullback_frobeniusIsogeny {F : Type u_1} [Field F] [_root_.Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} (σ : W₁.FunctionField →ₐ[F] W₂.FunctionField) : σ.comp (TauCeti.Isogeny.frobeniusIsogeny W₁).fieldPullback = (TauCeti.Isogeny.frobeniusIsogeny W₂).fieldPullback.comp σ

An algebra homomorphism between function fields commutes with the Frobenius pullbacks.