Galois descent of isogenies

An isogeny between curves defined over F, after base change to a Galois extension K/F, descends uniquely to F exactly when its function-field pullback is Galois equivariant. Equivalently, the isogeny is fixed by every coefficient conjugation.

Pointedness is preserved and reflected by change of the coefficient field: a coordinate pullback satisfies MapsInfinity exactly when its base change does. Equivalently, the pulled-back target x-coordinate has a pole at the source's point at infinity before base change exactly when it does afterwards.

The extension need not be finite. In particular the criterion applies to a separable closure of an imperfect field, the descent step used in constructing the dual of a separable isogeny over its field of definition. Neither ellipticity nor separability of the isogeny is needed here.

Main results

• TauCeti.Isogeny.existsUnique_map_eq_iff_galoisEquivariant: the function-field criterion.
• TauCeti.Isogeny.existsUnique_map_eq_iff_galoisFixed: the coefficient-conjugation criterion.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2 and III.6.

theorem TauCeti.Isogeny.existsUnique_map_eq_iff_galoisEquivariant {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W₁ W₂ : WeierstrassCurve F) [IsGalois F K] (φ : Isogeny (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₁ K)) (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₂ K))) : (∃! ψ : Isogeny W₁.toAffine W₂.toAffine, ψ.map (algebraMap F K) = φ) ↔ ∀ (σ : Gal(K/F)) (z : (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₂ K)).FunctionField), (W₁.functionFieldGaloisAction σ) (φ.fieldPullback z) = φ.fieldPullback ((W₂.functionFieldGaloisAction σ) z)

An isogeny after a Galois extension descends uniquely precisely when its function-field pullback is equivariant.

theorem TauCeti.Isogeny.existsUnique_map_eq_iff_galoisFixed {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W₁ W₂ : WeierstrassCurve F) [IsGalois F K] (φ : Isogeny (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₁ K)) (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₂ K))) : (∃! ψ : Isogeny W₁.toAffine W₂.toAffine, ψ.map (algebraMap F K) = φ) ↔ ∀ (σ : Gal(K/F)), galoisConj W₁ W₂ φ σ = φ

An isogeny between base-changed ground-field curves descends uniquely exactly when every coefficient Galois conjugation fixes it. The extension may be infinite, as for a separable closure; no perfectness hypothesis on the ground field is imposed.