Verschiebung #

Let W be an elliptic curve over a field F of exponential characteristic p, and let F_{W/F} : W → W⁽ᵖ⁾ be its relative Frobenius isogeny to the Frobenius twist. This file constructs the Verschiebung V : W⁽ᵖ⁾ → W, the dual of relative Frobenius: the unique isogeny with V ∘ F_{W/F} = [p] (Silverman III.6.1). It proves F_{W/F} ∘ V = [p] on the twist as well, deg V = p, and that V carries the whole separable degree of [p].

The construction is the factorisation theorem. The inseparable degree of [p] is divisible by p: in positive characteristic [p] scales the invariant differential by p = 0, so it is inseparable. Hence [p] factors through the relative Frobenius (Silverman II.2.12). This is the construction of TauCeti.Isogeny.dualFrobeniusIsogeny, the dual of the absolute q-power Frobenius over a finite field, carried out for the relative p-power Frobenius, so it needs no hypothesis on the base field, which may be imperfect. In characteristic zero (p = 1) the Verschiebung is the inverse of the relative Frobenius W → W⁽¹⁾.

Since F_{W/F} is purely inseparable, deg_s [p] = deg_s V, and since V has degree p it is either separable or purely inseparable. These are the facts through which Verschiebung detects supersingularity, the triviality of the geometric p-torsion of W (Silverman V.3.1).

Main definitions #

TauCeti.Isogeny.verschiebungIsogeny: the Verschiebung V : W⁽ᵖ⁾ → W.

Main results #

TauCeti.Isogeny.fieldRange_mulByIntIsogenyOfNeZero_le_fieldRange_relativeFrobeniusIsogeny: [p]^* F(W) ≤ F_{W/F}^* F(W⁽ᵖ⁾).
TauCeti.Isogeny.existsUnique_comp_relativeFrobeniusIsogeny_eq_mulByIntIsogenyOfNeZero: [p] factors through relative Frobenius by a unique isogeny.
TauCeti.Isogeny.verschiebungIsogeny_comp_relativeFrobeniusIsogeny and TauCeti.Isogeny.eq_verschiebungIsogeny_iff_comp_eq: V ∘ F_{W/F} = [p], and this characterises V.
TauCeti.Isogeny.dual_relativeFrobeniusIsogeny: V is the dual of F_{W/F}.
TauCeti.Isogeny.relativeFrobeniusIsogeny_comp_verschiebungIsogeny: F_{W/F} ∘ V = [p] on W⁽ᵖ⁾.
TauCeti.Isogeny.degree_verschiebungIsogeny: deg V = p.
TauCeti.Isogeny.separableDegree_verschiebungIsogeny: deg_s V = deg_s [p].
TauCeti.Isogeny.isSeparable_or_isPurelyInseparable_verschiebungIsogeny: V is separable or purely inseparable.
TauCeti.Isogeny.ofIsogeny_verschiebungIsogeny_comp_ofIsogeny_relativeFrobeniusIsogeny and TauCeti.Isogeny.ofIsogeny_relativeFrobeniusIsogeny_comp_ofIsogeny_verschiebungIsogeny: both composites are p • 1 in the additive groups of endomorphisms.
TauCeti.Isogeny.pointMap_verschiebungIsogeny_pointMap_relativeFrobeniusIsogeny and TauCeti.Isogeny.pointMap_relativeFrobeniusIsogeny_pointMap_verschiebungIsogeny: on points, V (F_{W/F} P) = p • P and F_{W/F} (V Q) = p • Q.

References #

J. Silverman, The Arithmetic of Elliptic Curves, II.2.12, III.6.1, III.6.2 and V.3.1.

source

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

(mulByIntIsogenyOfNeZero W ⋯).fieldPullback.fieldRange ≤ (relativeFrobeniusIsogeny p W).fieldPullback.fieldRange

The function field pulled back by [p] lies inside the one pulled back by relative Frobenius: [p]^* F(W) ≤ F_{W/F}^* F(W⁽ᵖ⁾), the latter being generated by the p-th powers.

source

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

∃! χ : Isogeny (W.map (frobenius F p)) W, χ.comp (relativeFrobeniusIsogeny p W) = mulByIntIsogenyOfNeZero W ⋯

[p] factors through relative Frobenius by a unique isogeny: the Verschiebung (Silverman III.6.1).

source

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

Isogeny (W.map (frobenius F p)) W

The Verschiebung V : W⁽ᵖ⁾ → W, the unique isogeny with V ∘ F_{W/F} = [p]: the dual of the relative Frobenius isogeny (Silverman III.6.1).

Instances For

source

@[simp]

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

(verschiebungIsogeny p W).comp (relativeFrobeniusIsogeny p W) = mulByIntIsogenyOfNeZero W ⋯

Verschiebung composed with relative Frobenius is multiplication by p.

source

theorem TauCeti.Isogeny.eq_verschiebungIsogeny_iff_comp_eq {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {χ : Isogeny (W.map (frobenius F p)) W} :

χ = verschiebungIsogeny p W ↔ χ.comp (relativeFrobeniusIsogeny p W) = mulByIntIsogenyOfNeZero W ⋯

V is the only isogeny χ with χ ∘ F_{W/F} = [p].

source

@[simp]

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

(relativeFrobeniusIsogeny p W).dual = verschiebungIsogeny p W

V is the dual of relative Frobenius: the dual isogeny TauCeti.Isogeny.dual of F_{W/F} is verschiebungIsogeny.

source

@[simp]

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

(verschiebungIsogeny p W).degree = p

Verschiebung has degree p, the degree of relative Frobenius (Silverman III.6.2(e)).

source

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

(relativeFrobeniusIsogeny p W).comp (verschiebungIsogeny p W) = mulByIntIsogenyOfNeZero (W.map (frobenius F p)) ⋯

Relative Frobenius composed with Verschiebung is multiplication by p on the twist (Silverman III.6.2(a)).

Deliberately not @[simp]. Its left-hand side is rewritten by the @[simp] naturality square relativeFrobeniusIsogeny_comp, so it is not in simp-normal form wherever that lemma is in scope.

source