Separability of an isogeny and its dual #
An isogeny and its dual are both separable exactly when their common degree is nonzero in the base field. Thus an isogeny of degree prime to the characteristic and its dual both admit the separable Kummer sequences. For a separable isogeny, this also characterizes separability of its dual; separability of the original alone does not suffice in positive characteristic.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, III.6.2 and III.6.4.
theorem
TauCeti.Isogeny.isSeparable_dual_and_self_iff
{F : Type u_1}
[Field F]
{W₁ W₂ : WeierstrassCurve.Affine F}
[WeierstrassCurve.IsElliptic W₁]
[WeierstrassCurve.IsElliptic W₂]
(φ : Isogeny W₁ W₂)
:
Algebra.IsSeparable (↥φ.dual.fieldPullback.fieldRange) W₂.FunctionField ∧ Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField ↔ ↑φ.degree ≠ 0
An isogeny and its dual are both separable exactly when the degree is nonzero in the base field.
theorem
TauCeti.Isogeny.isSeparable_dual_of_degree_ne_zero
{F : Type u_1}
[Field F]
{W₁ W₂ : WeierstrassCurve.Affine F}
[WeierstrassCurve.IsElliptic W₁]
[WeierstrassCurve.IsElliptic W₂]
(φ : Isogeny W₁ W₂)
(h : ↑φ.degree ≠ 0)
:
The dual of an isogeny whose degree is nonzero in the base field is separable.
@[simp]
theorem
TauCeti.Isogeny.isSeparable_dual_iff
{F : Type u_1}
[Field F]
{W₁ W₂ : WeierstrassCurve.Affine F}
[WeierstrassCurve.IsElliptic W₁]
[WeierstrassCurve.IsElliptic W₂]
(φ : Isogeny W₁ W₂)
[Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField]
:
For a separable isogeny, its dual is separable exactly when the degree is nonzero in the base field.