Naturality of relative Frobenius

For an isogeny φ : W₁ → W₂, relative Frobenius satisfies the commuting square F_{W₂/F} ∘ φ = φ⁽ᵖ⁾ ∘ F_{W₁/F}, where φ⁽ᵖ⁾ is the transport of φ along the Frobenius of the ground field. The same identity holds for every iterate. In particular, the twist on the right cannot be omitted over an imperfect field: relative Frobenius has target the Frobenius twist rather than the original curve.

Relative Frobenius also commutes with arbitrary field base change. The two possible target curves are identified by the fact that field homomorphisms commute with Frobenius.

These identities allow compositions involving inseparable isogenies to be compared with their Frobenius-twisted counterparts, as needed when assembling a dual from a separable factor and a Frobenius factor. They hold for all affine Weierstrass curves, with no ellipticity or perfectness assumption, and include exponential characteristic 1.

Main results

• TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_map and TauCeti.Isogeny.relativeFrobeniusIsogeny_map: compatibility with field base change.
• TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_comp: the iterated naturality square.
• TauCeti.Isogeny.relativeFrobeniusIsogeny_comp: the one-step naturality square.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.11–12 and III.6.1.

@[simp]

theorem TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {K : Type u_2} [Field K] (W : WeierstrassCurve.Affine F) (n : ℕ) (f : F →+* K) : have this := ⋯; have e := ⋯; e ▸ (iterateRelativeFrobeniusIsogeny p W n).map f = iterateRelativeFrobeniusIsogeny p (W.map f) n

Iterated relative Frobenius commutes with arbitrary field base change, under the canonical equality between the base change of the twist and the twist of the base change.

@[simp]

theorem TauCeti.Isogeny.relativeFrobeniusIsogeny_map {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {K : Type u_2} [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) : have this := ⋯; have e := ⋯; e ▸ (relativeFrobeniusIsogeny p W).map f = relativeFrobeniusIsogeny p (W.map f)

Relative Frobenius commutes with arbitrary field base change. The target curves are identified by the fact that field homomorphisms commute with Frobenius.

@[simp]

theorem TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny_comp {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (n : ℕ) : (iterateRelativeFrobeniusIsogeny p W₂ n).comp φ = (φ.map (iterateFrobenius F p n)).comp (iterateRelativeFrobeniusIsogeny p W₁ n)

Iterated relative Frobenius is natural in the isogeny: its square commutes with the isogeny obtained by applying the iterated Frobenius to the coefficients.

@[simp]

theorem TauCeti.Isogeny.relativeFrobeniusIsogeny_comp {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (relativeFrobeniusIsogeny p W₂).comp φ = (φ.map (frobenius F p)).comp (relativeFrobeniusIsogeny p W₁)

Relative Frobenius is natural in the isogeny. Over an imperfect field the isogeny on the right is Frobenius-twisted, rather than the original isogeny.