The relative Frobenius isogeny

When p > 1 (equivalently, when F has positive characteristic), raising to the p-th power is a ring endomorphism of F but not an F-algebra map, so it does not turn a Weierstrass curve into an endomorphism of itself unless F is a prime field. When p = 1, the characteristic-zero case, this map is the identity. In either case it gives a map to the Frobenius twist W⁽ᵖ⁾, whose a-invariants are the p-th powers of those of W: Mathlib's W.map (frobenius F p), with WeierstrassCurve.map_a₁ and its siblings for the coefficient description and WeierstrassCurve.map_map for iteration. The relative Frobenius F_{W/F} : W → W⁽ᵖ⁾ is then an honest F-morphism, the one that reads (x, y) ↦ (xᵖ, yᵖ) on points.

Contravariantly, that is the F-algebra map out of the coordinate ring of the twist sending the two coordinates of W⁽ᵖ⁾ to the p-th powers of the coordinates of W. It is well defined because the Weierstrass polynomial of the twist is the image of that of W under the coefficient Frobenius, so substituting p-th powers into it produces the p-th power of the Weierstrass polynomial of W, which vanishes on the coordinate ring. The resulting map lands in W.CoordinateRing, not merely in W.FunctionField: relative Frobenius is a morphism of affine curves.

Over a finite field the q-power map is already an F-algebra map, and TauCeti.Isogeny.frobeniusIsogeny is the resulting self-isogeny. The construction here is the one that survives over an arbitrary — in particular imperfect — base, at the cost of a moving target.

That coordinate-ring map is an input from Affine/RelativeFrobenius.lean, which declares it as CoordinateRing.relativeFrobenius together with its factorisation relativeFrobenius_comp_map of the p-power map of W.CoordinateRing into Mathlib's semilinear base-change map followed by an F-linear one; the pointedness of the isogeny below and its pure inseparability are both read off that factorisation.

Main definitions

• TauCeti.Isogeny.relativeFrobeniusPullback: the coordinate-ring map read into W.FunctionField, a TauCeti.CoordinatePullback.
• TauCeti.Isogeny.relativeFrobeniusIsogeny: the relative Frobenius isogeny W → W.map (frobenius F p).
• TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny: the n-fold relative Frobenius W → W.map (iterateFrobenius F p n).

Main results

• TauCeti.Isogeny.isPurelyInseparable_relativeFrobeniusIsogeny: the relative Frobenius is purely inseparable (Silverman II.2.11(b)); every element of F(W) has its p-th power in the pulled-back copy of F(W⁽ᵖ⁾).
• TauCeti.Isogeny.degree_relativeFrobeniusIsogeny: its degree is p (Silverman II.2.11(c)), with TauCeti.Isogeny.separableDegree_relativeFrobeniusIsogeny and TauCeti.Isogeny.inseparableDegree_relativeFrobeniusIsogeny splitting that as 1 · p.
• TauCeti.Isogeny.degree_iterateRelativeFrobeniusIsogeny: the n-fold iterate has degree p ^ n and is purely inseparable.
• TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_map and TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_map: coefficient Frobenius followed by the relative pullback is the power map on the whole function field.
• TauCeti.Isogeny.fieldRange_relativeFrobeniusIsogeny and TauCeti.Isogeny.fieldRange_iterateRelativeFrobeniusIsogeny: the pulled-back copy of F(W⁽ᵖ⁾) is F(F(W)ᵖ), the subfield generated over the constants by the p-th powers, and likewise with p ^ n for the iterate; with fieldRange_relativeFrobeniusIsogeny_le_iff and fieldRange_iterateRelativeFrobeniusIsogeny_le_iff as the universal properties, fieldRange_iterateRelativeFrobeniusIsogeny_antitone for the resulting tower, and fieldPullback_relativeFrobeniusIsogeny_genericX, fieldPullback_relativeFrobeniusIsogeny_genericY and their iterates for the values at the generic point.

The degree is the shared tower comparison WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq_pow, applied to the pullback: over the copy of F(xᵖ) inside F(W), that copy sits below F(x) with relative degree p and below the pulled-back F(W⁽ᵖ⁾) with relative degree 2, while [F(W) : F(x)] = 2. The finite-field WeierstrassCurve.Affine.finrank_fieldRange_frobeniusAlgHom is the same lemma applied to the q-power map. Likewise the pulled-back function field is the shared WeierstrassCurve.Affine.fieldRange_eq_adjoin_range_pow, applied to the one-step and the iterated pullback at their values xᵖ, yᵖ and x ^ (p ^ n), y ^ (p ^ n) at the generic point.

No result here needs W to be elliptic, matching the isogeny API it extends; Mathlib's WeierstrassCurve.instIsEllipticMap supplies (W.map (frobenius F p)).IsElliptic for a consumer that does want it.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.11, whose N.B. is the reason this file exists: over an imperfect F, parts (b) and (c) (pure inseparability and degree p) survive unchanged, but part (a), the identification φ* F(W⁽ᵖ⁾) = F(W)ᵖ, does not: the pulled-back copy also contains the constants, which need not be p-th powers. The form valid over every base is φ* F(W⁽ᵖ⁾) = F(F(W)ᵖ), proved here as TauCeti.Isogeny.fieldRange_relativeFrobeniusIsogeny; the containment F(W)ᵖ ⊆ φ* F(W⁽ᵖ⁾) (TauCeti.Isogeny.pow_mem_fieldRange_relativeFrobeniusIsogeny) is all pure inseparability needs. Over a finite, hence perfect, base there is no gap, and Isogeny/Frobenius/Basic.lean identifies the pullback with the q-power map outright (fieldPullback_frobeniusIsogeny).

Provenance

Not a port. The pinned sources of this roadmap build only the absolute q-power Frobenius of a curve over a finite field (AINTLIB's HasseWeil/FrobeniusIsogeny.lean, already migrated as TauCeti.Isogeny.frobeniusIsogeny and WeierstrassCurve.Affine.finrank_fieldRange_frobeniusAlgHom); the relative Frobenius over an arbitrary base, and the twist it maps to, appear in none of them. The degree computation reuses the migrated tower argument of TauCeti/AlgebraicGeometry/EllipticCurve/Affine/FunctionField/PowerTower.lean, which carries the AINTLIB credit for it, and whose ratFuncAdjoinXPowRange API rests on TauCeti.RatFunc.finrank_adjoin_X_pow from TauCeti/FieldTheory/RatFunc/PowerTower.lean.

The relative Frobenius isogeny

noncomputable def TauCeti.Isogeny.relativeFrobeniusPullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : CoordinatePullback W (W.map (frobenius F p))

The relative Frobenius pullback: CoordinateRing.relativeFrobenius read into the function field of W.

Equations

• TauCeti.Isogeny.relativeFrobeniusPullback p W = (IsScalarTower.toAlgHom F W.CoordinateRing W.FunctionField).comp (WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius p W)

@[simp]

theorem TauCeti.Isogeny.relativeFrobeniusPullback_apply {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (z : (W.map (frobenius F p)).CoordinateRing) : (relativeFrobeniusPullback p W) z = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.relativeFrobenius p W) z)

The relative Frobenius pullback is the coordinate-ring map followed by the embedding of W.CoordinateRing in its fraction field.

theorem TauCeti.Isogeny.mapsInfinity_relativeFrobeniusPullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusPullback p W).MapsInfinity

The relative Frobenius maps the point at infinity to the point at infinity. Every element of W.CoordinateRing is a p-th root of an element pulled back from the twist, hence integral over the pulled-back coordinate ring.

noncomputable def TauCeti.Isogeny.relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : Isogeny W (W.map (frobenius F p))

The relative Frobenius isogeny F_{W/F} : W → W⁽ᵖ⁾.

Equations

• TauCeti.Isogeny.relativeFrobeniusIsogeny p W = { pullback := TauCeti.Isogeny.relativeFrobeniusPullback p W, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.relativeFrobeniusIsogeny_pullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).pullback = relativeFrobeniusPullback p W

The relative Frobenius isogeny's pullback is relativeFrobeniusPullback.

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_coordinateRingMap {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (z : W.CoordinateRing) : (relativeFrobeniusIsogeny p W).fieldPullback ((algebraMap (W.map (frobenius F p)).CoordinateRing (W.map (frobenius F p)).FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.map W (frobenius F p)) z)) = (algebraMap W.CoordinateRing W.FunctionField) z ^ p

The function-field pullback of a base-changed coordinate function is its p-th power.

Deliberately not @[simp]. Its left-hand side is already dismantled by the @[simp] chain Isogeny.fieldPullback_algebraMap, relativeFrobeniusIsogeny_pullback, relativeFrobeniusPullback_apply and CoordinateRing.relativeFrobenius_map, so tagging it fails simpNF; it is stated because it is the field-level form the pure-inseparability argument below quotes.

theorem TauCeti.Isogeny.pow_mem_fieldRange_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (z : W.FunctionField) : z ^ p ∈ (relativeFrobeniusIsogeny p W).fieldPullback.fieldRange

F(W)ᵖ lies in the pulled-back copy of F(W⁽ᵖ⁾). A quotient of two coordinate functions has its p-th power the quotient of two pullbacks.

instance TauCeti.Isogeny.isPurelyInseparable_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : IsPurelyInseparable (↥(relativeFrobeniusIsogeny p W).fieldPullback.fieldRange) W.FunctionField

The relative Frobenius isogeny is purely inseparable (Silverman II.2.11(b)).

The degree

@[simp]

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_X {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).fieldPullback ((algebraMap (Polynomial F) (W.map (frobenius F p)).FunctionField) Polynomial.X) = (algebraMap (Polynomial F) W.FunctionField) Polynomial.X ^ p

The relative Frobenius pullback sends the affine coordinate of the twist to xᵖ.

@[simp]

theorem TauCeti.Isogeny.degree_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).degree = p

The relative Frobenius isogeny has degree p (Silverman II.2.11(c)). This is the tower comparison WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq_pow, whose only input is the value of the pullback at the affine coordinate: both F(x) and the pulled-back F(W⁽ᵖ⁾) sit between F(xᵖ) and F(W), of relative degrees p and 2 over it, and [F(W) : F(x)] = 2 as well, so the two towers give 2 · deg = p · 2.

theorem TauCeti.Isogeny.separableDegree_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).separableDegree = 1

The relative Frobenius isogeny has separable degree one, as pure inseparability requires.

Deliberately not @[simp]. The isPurelyInseparable_relativeFrobeniusIsogeny instance already lets the @[simp] lemma separableDegree_eq_one_of_isPurelyInseparable close this goal, so tagging it fails simpNF with simp can prove this; it is stated as the named specialisation a consumer quotes, exactly as separableDegree_frobeniusIsogeny is for the absolute Frobenius.

theorem TauCeti.Isogeny.inseparableDegree_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).inseparableDegree = p

The relative Frobenius isogeny carries its whole degree p in the inseparable part.

Deliberately not @[simp]. Its left-hand side is already rewritten to p by the @[simp] pair inseparableDegree_eq_degree_of_isPurelyInseparable and degree_relativeFrobeniusIsogeny, so tagging it fails simpNF; it is stated for the same reason as separableDegree_relativeFrobeniusIsogeny above.

The image of the pullback

@[simp]

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_genericX {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).fieldPullback (W.map (frobenius F p)).genericX = W.genericX ^ p

The relative Frobenius pullback sends the generic x-coordinate of the twist to xᵖ.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_genericY {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).fieldPullback (W.map (frobenius F p)).genericY = W.genericY ^ p

The relative Frobenius pullback sends the generic y-coordinate of the twist to yᵖ.

theorem TauCeti.Isogeny.fieldRange_relativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : (relativeFrobeniusIsogeny p W).fieldPullback.fieldRange = IntermediateField.adjoin F (Set.range fun (z : W.FunctionField) => z ^ p)

The pulled-back copy of F(W⁽ᵖ⁾) is F(F(W)ᵖ), the subfield generated over the constants by the p-th powers (Silverman II.2.11(a), in the form valid over every base field: over a perfect F the constants are themselves p-th powers and this is F(W)ᵖ). This is WeierstrassCurve.Affine.fieldRange_eq_adjoin_range_pow at the values xᵖ, yᵖ of the pullback at the generic point.

@[simp]

theorem TauCeti.Isogeny.fieldRange_relativeFrobeniusIsogeny_le_iff {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) {N : IntermediateField F W.FunctionField} : (relativeFrobeniusIsogeny p W).fieldPullback.fieldRange ≤ N ↔ ∀ (z : W.FunctionField), z ^ p ∈ N

The universal property of the pulled-back F(W⁽ᵖ⁾): it lies inside an intermediate field exactly when every p-th power does.

Iterated relative Frobenius

noncomputable def TauCeti.Isogeny.iterateRelativeFrobeniusPullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : CoordinatePullback W (W.map (iterateFrobenius F p n))

The iterated relative Frobenius pullback. It reads the coordinate-ring map CoordinateRing.iterateRelativeFrobenius into W.FunctionField.

Equations

• TauCeti.Isogeny.iterateRelativeFrobeniusPullback p W n = (IsScalarTower.toAlgHom F W.CoordinateRing W.FunctionField).comp (WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius p W n)

@[simp]

theorem TauCeti.Isogeny.iterateRelativeFrobeniusPullback_apply {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) (z : (W.map (iterateFrobenius F p n)).CoordinateRing) : (iterateRelativeFrobeniusPullback p W n) z = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.iterateRelativeFrobenius p W n) z)

The iterated relative Frobenius pullback is the coordinate-ring map followed by the canonical embedding into the function field.

theorem TauCeti.Isogeny.mapsInfinity_iterateRelativeFrobeniusPullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusPullback p W n).MapsInfinity

The iterated relative Frobenius maps infinity to infinity. Every element of W.CoordinateRing has its p ^ n-th power in the pulled-back coordinate ring and is therefore integral over that ring.

noncomputable def TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : Isogeny W (W.map (iterateFrobenius F p n))

The n-fold relative Frobenius isogeny W → W.map (iterateFrobenius F p n).

Equations

• TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny p W n = { pullback := TauCeti.Isogeny.iterateRelativeFrobeniusPullback p W n, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_pullback {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).pullback = iterateRelativeFrobeniusPullback p W n

The iterated relative Frobenius isogeny's pullback is iterateRelativeFrobeniusPullback.

@[simp]

theorem TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_one {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : iterateRelativeFrobeniusIsogeny p W 1 = ⋯ ▸ relativeFrobeniusIsogeny p W

The first iterated relative Frobenius is the one-step relative Frobenius, after identifying their target curves via iterateFrobenius_one.

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_coordinateRingMap {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) (z : W.CoordinateRing) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback ((algebraMap (W.map (iterateFrobenius F p n)).CoordinateRing (W.map (iterateFrobenius F p n)).FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.map W (iterateFrobenius F p n)) z)) = (algebraMap W.CoordinateRing W.FunctionField) z ^ p ^ n

The function-field pullback of a base-changed coordinate function is its p ^ n-th power.

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_comp_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : have this := ⋯; (iterateRelativeFrobeniusIsogeny p W n).fieldPullback.comp (WeierstrassCurve.Affine.FunctionField.map W (iterateFrobenius F p n)) = iterateFrobenius W.FunctionField p n

The coefficient Frobenius followed by the iterated relative Frobenius pullback is iterated Frobenius on the function field, as an equality of ring homomorphisms.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) (z : W.FunctionField) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback ((WeierstrassCurve.Affine.FunctionField.map W (iterateFrobenius F p n)) z) = z ^ p ^ n

The coefficient Frobenius followed by the iterated relative Frobenius pullback is the p ^ n-power map on the function field, including its rational functions.

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_comp_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : have this := ⋯; (relativeFrobeniusIsogeny p W).fieldPullback.comp (WeierstrassCurve.Affine.FunctionField.map W (frobenius F p)) = frobenius W.FunctionField p

The coefficient Frobenius followed by relative Frobenius is Frobenius on the function field, as an equality of ring homomorphisms.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_relativeFrobeniusIsogeny_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (z : W.FunctionField) : (relativeFrobeniusIsogeny p W).fieldPullback ((WeierstrassCurve.Affine.FunctionField.map W (frobenius F p)) z) = z ^ p

The coefficient Frobenius followed by relative Frobenius is the p-power map on the function field.

theorem TauCeti.Isogeny.pow_mem_fieldRange_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) (z : W.FunctionField) : z ^ p ^ n ∈ (iterateRelativeFrobeniusIsogeny p W n).fieldPullback.fieldRange

Every p ^ n-th power in F(W) lies in the pulled-back function field of the n-th Frobenius twist.

instance TauCeti.Isogeny.isPurelyInseparable_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : IsPurelyInseparable (↥(iterateRelativeFrobeniusIsogeny p W n).fieldPullback.fieldRange) W.FunctionField

Every iterated relative Frobenius is purely inseparable.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_X {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback ((algebraMap (Polynomial F) (W.map (iterateFrobenius F p n)).FunctionField) Polynomial.X) = (algebraMap (Polynomial F) W.FunctionField) Polynomial.X ^ p ^ n

The iterated relative Frobenius pullback sends the affine coordinate of the twist to x ^ (p ^ n).

@[simp]

theorem TauCeti.Isogeny.degree_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).degree = p ^ n

The n-fold relative Frobenius has degree p ^ n.

@[simp]

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_genericX {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback (W.map (iterateFrobenius F p n)).genericX = W.genericX ^ p ^ n

The iterated relative Frobenius pullback sends the generic x-coordinate of the twist to x ^ (p ^ n).

@[simp]

theorem TauCeti.Isogeny.fieldPullback_iterateRelativeFrobeniusIsogeny_genericY {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback (W.map (iterateFrobenius F p n)).genericY = W.genericY ^ p ^ n

The iterated relative Frobenius pullback sends the generic y-coordinate of the twist to y ^ (p ^ n).

theorem TauCeti.Isogeny.fieldRange_iterateRelativeFrobeniusIsogeny {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback.fieldRange = IntermediateField.adjoin F (Set.range fun (z : W.FunctionField) => z ^ p ^ n)

The pulled-back copy of F(W⁽ᵖⁿ⁾) is F(F(W)^(pⁿ)), the subfield generated over the constants by the p ^ n-th powers: the iterate of fieldRange_relativeFrobeniusIsogeny, read off WeierstrassCurve.Affine.fieldRange_eq_adjoin_range_pow in the same way.

@[simp]

theorem TauCeti.Isogeny.fieldRange_iterateRelativeFrobeniusIsogeny_le_iff {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) (n : ℕ) {N : IntermediateField F W.FunctionField} : (iterateRelativeFrobeniusIsogeny p W n).fieldPullback.fieldRange ≤ N ↔ ∀ (z : W.FunctionField), z ^ p ^ n ∈ N

The universal property of the pulled-back F(W⁽ᵖⁿ⁾): it lies inside an intermediate field exactly when every p ^ n-th power does.

theorem TauCeti.Isogeny.fieldRange_iterateRelativeFrobeniusIsogeny_antitone {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) : Antitone fun (n : ℕ) => (iterateRelativeFrobeniusIsogeny p W n).fieldPullback.fieldRange

The pulled-back copies of the twists decrease along the Frobenius tower: for m ≤ n, the pulled-back F(W⁽ᵖⁿ⁾) lies inside the pulled-back F(W⁽ᵖᵐ⁾), as every p ^ n-th power is a p ^ m-th power.