Finiteness of local isogeny cokernels

For a nonzero morphism f : E₁ → E₂ over a finite extension K of ℚ_p, the quotient E₂(K) / f E₁(K) is finite, including when p divides the degree. This makes its order an honest finite local Kummer index, as needed in isogeny descent and the local factors of Cassels' isogeny formula.

The argument uses the Kummer injection into H¹(G_K, E₁[f]). The geometric kernel is finite, and the absolute Galois group of a finite extension of ℚ_p is topologically finitely generated, so this degree-one cohomology group is finite. No reduction hypothesis is required. The cohomological argument is also stated for a separable isogeny over any field whose absolute Galois group is topologically finitely generated.

Main results

• TauCeti.Isogeny.Hom.finite_kerCoeff: a nonzero morphism has finite geometric kernel.
• TauCeti.Isogeny.finiteIndex_range_pointMapHom_of_isTopologicallyFinitelyGenerated: the cokernel of a separable isogeny is finite when the absolute Galois group is topologically finitely generated.
• TauCeti.Isogeny.Hom.finiteIndex_range_pointMapHom_of_module_finite_padic: the local cokernel of any nonzero morphism over a finite extension of ℚ_p is finite.

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.4.1), for topological finite generation of local absolute Galois groups.
• J. W. S. Cassels, Arithmetic on curves of genus 1. VIII. On conjectures of Birch and Swinnerton-Dyer, J. Reine Angew. Math. 217 (1965), 180–199.

theorem TauCeti.Isogeny.Hom.finite_kerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (hf : f ≠ 0) : Finite f.KerCoeff

The geometric kernel of a nonzero morphism is finite, read in the discrete Galois coefficient module.

theorem TauCeti.Isogeny.Hom.finite_H1_kerCoeff_of_isTopologicallyFinitelyGenerated {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (hf : f ≠ 0) (hK : IsTopologicallyFinitelyGenerated (AbsoluteGaloisGroup K)) : Finite (ContCohomology.H1 (AbsoluteGaloisGroup K) f.KerCoeff)

The first cohomology of the geometric kernel of a nonzero morphism is finite when the absolute Galois group is topologically finitely generated.

theorem TauCeti.Isogeny.finiteIndex_range_pointMapHom_of_isTopologicallyFinitelyGenerated {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (φ : Isogeny W₁.toAffine W₂.toAffine) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.toAffine.FunctionField] [DecidableEq K] (hK : IsTopologicallyFinitelyGenerated (AbsoluteGaloisGroup K)) : (Hom.ofIsogeny φ).pointMapHom.range.FiniteIndex

The Kummer injection makes the cokernel of a separable isogeny finite over a field with topologically finitely generated absolute Galois group.

theorem TauCeti.Isogeny.Hom.finiteIndex_range_pointMapHom_of_isTopologicallyFinitelyGenerated {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] [DecidableEq K] [CharZero K] (f : Hom W₁.toAffine W₂.toAffine) (hf : f ≠ 0) (hK : IsTopologicallyFinitelyGenerated (AbsoluteGaloisGroup K)) : f.pointMapHom.range.FiniteIndex

A nonzero morphism in characteristic zero has finite cokernel when the absolute Galois group is topologically finitely generated.

theorem TauCeti.Isogeny.Hom.finiteIndex_range_pointMapHom_of_module_finite_padic (p : ℕ) [Fact (Nat.Prime p)] {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) [DecidableEq K] (hf : f ≠ 0) : f.pointMapHom.range.FiniteIndex

The local Kummer cokernel E₂(K) / f E₁(K) is finite for every nonzero morphism over a finite compatible extension of ℚ_p, even when p divides its degree.