The factorisation of an isogeny through a Frobenius power

Every isogeny φ : W₁ → W₂ over a field F of exponential characteristic p factors as φ = φ_sep ∘ F^r, where F^r : W₁ → W₁⁽ᵖʳ⁾ is the r-fold relative Frobenius and φ_sep is a separable isogeny (Silverman II.2.12). The power p ^ r is determined by φ: it is the inseparable degree of φ, so for p > 1 the exponent r is determined as well. The factor φ_sep is unique, and its degree is the separable degree of φ. In characteristic zero p = 1, every r has p ^ r = 1, the inseparable degree of φ, and the statement says that every isogeny is separable.

Main results

• TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq_iff: φ factors through F^n, by a unique isogeny, exactly when p ^ n divides its inseparable degree; with TauCeti.Isogeny.fieldRange_le_fieldRange_iterateRelativeFrobeniusIsogeny_iff as its subfield-criterion form.
• TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq: the factorisation theorem, that φ factors through F^r by a unique isogeny when p ^ r is its inseparable degree.
• TauCeti.Isogeny.isSeparable_of_comp_iterateRelativeFrobeniusIsogeny_eq and TauCeti.Isogeny.inseparableDegree_eq_pow_of_comp_iterateRelativeFrobeniusIsogeny_eq: a factor of φ through F^r is separable exactly when p ^ r is the inseparable degree of φ, the two directions of the equivalence isSeparable_iff_inseparableDegree_eq_pow_of_comp_iterateRelativeFrobeniusIsogeny_eq.
• TauCeti.Isogeny.separableDegree_eq_of_comp_iterateRelativeFrobeniusIsogeny_eq and TauCeti.Isogeny.degree_eq_separableDegree_of_comp_iterateRelativeFrobeniusIsogeny_eq: a factor through F^r has the separable degree of φ, which is its degree when it is separable.
• TauCeti.Isogeny.exists_isSeparable_comp_iterateRelativeFrobeniusIsogeny_eq: every isogeny is a separable isogeny after a Frobenius power (Silverman II.2.12).

References

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

theorem TauCeti.Isogeny.fieldRange_le_fieldRange_iterateRelativeFrobeniusIsogeny_iff {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) {n : ℕ} : φ.fieldPullback.fieldRange ≤ (iterateRelativeFrobeniusIsogeny p W₁ n).fieldPullback.fieldRange ↔ p ^ n ∣ φ.inseparableDegree

The pulled-back function field of W₂ lies in that of the n-th Frobenius twist of W₁ exactly when p ^ n divides the inseparable degree of φ: the subfield-criterion form of existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq_iff.

theorem TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq_iff {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) {n : ℕ} : (∃! χ : Isogeny (W₁.map (iterateFrobenius F p n)) W₂, χ.comp (iterateRelativeFrobeniusIsogeny p W₁ n) = φ) ↔ p ^ n ∣ φ.inseparableDegree

φ factors through the n-fold relative Frobenius exactly when p ^ n divides its inseparable degree, and then by a unique isogeny.

theorem TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) {r : ℕ} (hr : φ.inseparableDegree = p ^ r) : ∃! χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂, χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ

The factorisation theorem for isogenies (Silverman II.2.12): when p ^ r is the inseparable degree of φ : W₁ → W₂, it factors through the r-fold relative Frobenius F^r : W₁ → W₁⁽ᵖʳ⁾ as φ = χ ∘ F^r for a unique isogeny χ : W₁⁽ᵖʳ⁾ → W₂. The factor is separable (isSeparable_of_comp_iterateRelativeFrobeniusIsogeny_eq), of degree the separable degree of φ (degree_eq_separableDegree_of_comp_iterateRelativeFrobeniusIsogeny_eq).

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

A factor through a Frobenius power has the separable degree of the composite: deg_s χ = deg_s φ when φ = χ ∘ F^r.

theorem TauCeti.Isogeny.isSeparable_of_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] {p : ℕ} [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} {φ : Isogeny W₁ W₂} {r : ℕ} {χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂} (hr : φ.inseparableDegree = p ^ r) (hχ : χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ) : Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) (W₁.map (iterateFrobenius F p r)).FunctionField

A factor of φ through F^r is separable when p ^ r is the inseparable degree of φ.

theorem TauCeti.Isogeny.inseparableDegree_eq_pow_of_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] {p : ℕ} [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} {φ : Isogeny W₁ W₂} {r : ℕ} {χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂} [Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) (W₁.map (iterateFrobenius F p r)).FunctionField] (hχ : χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ) : φ.inseparableDegree = p ^ r

If φ has a separable factor through F^r, then p ^ r is its inseparable degree: the power p ^ r in a factorisation φ = φ_sep ∘ F^r with φ_sep separable is determined by φ, and with it the exponent r when p > 1.

theorem TauCeti.Isogeny.isSeparable_iff_inseparableDegree_eq_pow_of_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] {p : ℕ} [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} {φ : Isogeny W₁ W₂} {r : ℕ} {χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂} (hχ : χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ) : Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) (W₁.map (iterateFrobenius F p r)).FunctionField ↔ φ.inseparableDegree = p ^ r

A factor of φ through F^r is separable exactly when p ^ r is the inseparable degree of φ: a factorisation φ = φ_sep ∘ F^r with φ_sep separable has p ^ r the inseparable degree of φ, which determines r when p > 1, and the factor through that F^r is separable.

theorem TauCeti.Isogeny.degree_eq_separableDegree_of_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] {p : ℕ} [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} {φ : Isogeny W₁ W₂} {r : ℕ} {χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂} [Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) (W₁.map (iterateFrobenius F p r)).FunctionField] (hχ : χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ) : χ.degree = φ.separableDegree

The separable factor of φ through F^r has degree the separable degree of φ (Silverman II.2.12): deg φ_sep = deg_s φ.

theorem TauCeti.Isogeny.exists_isSeparable_comp_iterateRelativeFrobeniusIsogeny_eq {F : Type u_1} [Field F] (p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : ∃ (r : ℕ) (χ : Isogeny (W₁.map (iterateFrobenius F p r)) W₂), Algebra.IsSeparable (↥χ.fieldPullback.fieldRange) (W₁.map (iterateFrobenius F p r)).FunctionField ∧ χ.comp (iterateRelativeFrobeniusIsogeny p W₁ r) = φ

Every isogeny is a separable isogeny after a Frobenius power (Silverman II.2.12): φ = φ_sep ∘ F^r with φ_sep : W₁⁽ᵖʳ⁾ → W₂ separable, where p ^ r is the inseparable degree of φ (inseparableDegree_eq_pow_of_comp_iterateRelativeFrobeniusIsogeny_eq) and φ_sep is unique (existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq).