The Kummer map of an elliptic curve and the m-descent sequence

Let W be an elliptic curve over a field K, Kˢ a separable closure, G_K its Galois group, and m a natural number invertible in K. The Kummer sequence

0 ⟶ E(Kˢ)[m] ⟶ E(Kˢ) ⟶ E(Kˢ) ⟶ 0

of discrete G_K-modules is WeierstrassCurve.kummerShortExact. Its degree-zero connecting map, read through the identification WeierstrassCurve.basePointEquivInvariants of H⁰(G_K, E(Kˢ)) with E(K), is the Kummer map E(K) → H¹(G_K, E[m]). This file constructs it, computes it on cocycles, and proves the m-descent exact sequence (Silverman VIII.2, X.4)

0 ⟶ E(K) ⧸ m E(K) ⟶ H¹(G_K, E[m]) ⟶ H¹(G_K, E)[m] ⟶ 0.

The computation is the classical one. Choose Q ∈ E(Kˢ) with m • Q = P; then σ ↦ σ Q - Q takes values in E[m], since P is fixed by G_K, and it is a continuous 1-cocycle, its image in E(Kˢ) being the coboundary of Q. Its class is the Kummer class of P.

The three exactness statements are read off the long exact sequence of continuous cohomology. At E(K) ⧸ m E(K) it is exactness at H⁰(G_K, E(Kˢ)), explicitLongExact_H0C, together with the commuting square WeierstrassCurve.explicitCoeff0_basePointEquivInvariants: multiplication by m on the invariants is multiplication by m on E(K). At H¹(G_K, E[m]) it is exactness at the node where δ⁰ lands, explicitLongExact_H1A. At H¹(G_K, E) it is exactness at the middle node, explicitLongExact_H1B, together with the fact that multiplication by m on coefficients induces multiplication by m on H¹.

The construction follows that of the Kummer map of the multiplicative group, TauCeti.kummerMap. That map is surjective by Hilbert 90; here the cokernel H¹(G_K, E)[m] is the m-torsion of the Weil–Châtelet group H¹(G_K, E), which is not zero in general. Over a number field, local conditions cut the m-Selmer group out of the middle term H¹(G_K, E[m]) and the m-torsion of the Shafarevich–Tate group out of the right-hand term H¹(G_K, E)[m].

Main definitions

• WeierstrassCurve.kummerCocycle: the cocycle σ ↦ σ Q - Q attached to an mth division point.
• WeierstrassCurve.kummerMap: the Kummer map E(K) → H¹(G_K, E[m]).
• WeierstrassCurve.kummerClassMap: the induced map on E(K) ⧸ m E(K).
• WeierstrassCurve.torsionCoeffInclH1: the map H¹(G_K, E[m]) → H¹(G_K, E)[m].

Main results

• WeierstrassCurve.kummerMap_eq_H1pi: the Kummer class of P is the class of σ ↦ σ Q - Q, for any Q with m • Q = P.
• WeierstrassCurve.ker_kummerMap: the kernel of the Kummer map is m E(K), with WeierstrassCurve.kummerMap_eq_zero_iff the pointwise form.
• WeierstrassCurve.kummerClassMap_injective: E(K) ⧸ m E(K) injects into H¹(G_K, E[m]).
• WeierstrassCurve.range_kummerMap: the image of the Kummer map is the kernel of H¹(G_K, E[m]) → H¹(G_K, E).
• WeierstrassCurve.range_explicitCoeff1_torsionCoeffIncl: the image of H¹(G_K, E[m]) → H¹(G_K, E) is the m-torsion of H¹(G_K, E).
• WeierstrassCurve.exact_kummerClassMap_torsionCoeffInclH1, WeierstrassCurve.torsionCoeffInclH1_surjective: the m-descent sequence, with WeierstrassCurve.kummerClassMap_injective, as exactness of E(K) ⧸ m E(K) → H¹(G_K, E[m]) → H¹(G_K, E)[m] and surjectivity on the right.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.2 and X.4.

The map H¹(G_K, E[m]) → H¹(G_K, E)[m]

noncomputable def WeierstrassCurve.torsionCoeffInclH1 {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) →+ ↥(AddSubgroup.torsionBy (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff) ↑m)

The map H¹(G_K, E[m]) → H¹(G_K, E)[m], the last map of the m-descent sequence: the map induced by the inclusion E(Kˢ)[m] → E(Kˢ), which lands in the m-torsion because m kills E(Kˢ)[m]. It is surjective (WeierstrassCurve.torsionCoeffInclH1_surjective), with kernel the image of the Kummer map (WeierstrassCurve.exact_kummerClassMap_torsionCoeffInclH1).

@[simp]

theorem WeierstrassCurve.coe_torsionCoeffInclH1 {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : ↑((W.torsionCoeffInclH1 m) c) = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯) c

theorem WeierstrassCurve.range_explicitCoeff1_torsionCoeffIncl {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) [W.IsElliptic] (hm : IsUnit ↑m) : (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯).range = AddSubgroup.torsionBy (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff) ↑m

The image of H¹(G_K, E[m]) → H¹(G_K, E) is the m-torsion of H¹(G_K, E), the last exactness statement of the m-descent sequence.

theorem WeierstrassCurve.torsionCoeffInclH1_surjective {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) [W.IsElliptic] (hm : IsUnit ↑m) : Function.Surjective ⇑(W.torsionCoeffInclH1 m)

H¹(G_K, E[m]) → H¹(G_K, E)[m] is surjective, the right end of the m-descent sequence.

The Kummer cocycle

theorem WeierstrassCurve.smul_sub_mem_torsionCoeff {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} {m : ℕ} {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) (σ : TauCeti.AbsoluteGaloisGroup K) : σ • Q - Q ∈ AddSubgroup.torsionBy W.PointCoeff ↑m

The Kummer difference is m-torsion: if m • Q is the image of a point of E(K), then σ Q - Q is killed by m, because G_K fixes m • Q.

noncomputable def WeierstrassCurve.kummerCocycle {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} {m : ℕ} {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) : TauCeti.AbsoluteGaloisGroup K → W.TorsionCoeff m

The Kummer cocycle σ ↦ σ Q - Q attached to a point Q of E(Kˢ) with m • Q in E(K).

@[simp]

theorem WeierstrassCurve.coe_kummerCocycle {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} {m : ℕ} {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) (σ : TauCeti.AbsoluteGaloisGroup K) : ↑(kummerCocycle hQ σ) = σ • Q - Q

theorem WeierstrassCurve.kummerCocycle_mem_Z1 {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} {m : ℕ} {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) : kummerCocycle hQ ∈ TauCeti.ContCohomology.Z1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)

The Kummer cocycle is a continuous 1-cocycle: its image in E(Kˢ) is the coboundary of Q.

The Kummer map

noncomputable def WeierstrassCurve.kummerMap {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : W.toAffine.Point →+ TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)

The Kummer map E(K) → H¹(G_K, E[m]): the degree-zero connecting homomorphism of the Kummer sequence of W, read on E(K) through its identification with the invariants of E(Kˢ).

@[simp]

theorem WeierstrassCurve.kummerMap_apply {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (P : W.toAffine.Point) : (W.kummerMap m hm) P = (W.kummerShortExact m hm).explicitDelta0 (W.basePointEquivInvariants P)

The Kummer map is the degree-zero connecting homomorphism of the Kummer sequence, read on P through the identification of E(K) with the invariants of E(Kˢ).

theorem WeierstrassCurve.explicitCoeff0_basePointEquivInvariants {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (P : W.toAffine.Point) : (TauCeti.ContCohomology.explicitCoeff0 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff (W.kummerShortExact m hm).projDistribMulActionHom) (W.basePointEquivInvariants P) = W.basePointEquivInvariants (m • P)

Multiplication by m on the invariants of E(Kˢ) is multiplication by m on E(K). This is the commuting square that turns exactness of the long exact sequence at H⁰(G_K, E(Kˢ)) into the computation of the kernel of the Kummer map.

theorem WeierstrassCurve.ker_kummerMap {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : (W.kummerMap m hm).ker = (nsmulAddMonoidHom m).range

The kernel of the Kummer map is m E(K).

theorem WeierstrassCurve.kummerMap_eq_H1pi {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} [W.IsElliptic] {m : ℕ} (hm : IsUnit ↑m) {P : W.toAffine.Point} {Q : W.PointCoeff} (hQ : m • Q = W.basePointCoeff P) : (W.kummerMap m hm) P = (TauCeti.ContCohomology.H1pi (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) ⟨kummerCocycle hQ, ⋯⟩

The Kummer class of P is represented by σ ↦ σ Q - Q, for any Q ∈ E(Kˢ) with m • Q = P (Silverman X.4). Such a Q exists because E(Kˢ) is divisible by m.

theorem WeierstrassCurve.kummerMap_eq_zero_iff {K : Type u_1} [Field K] [DecidableEq K] {W : WeierstrassCurve K} [W.IsElliptic] {m : ℕ} (hm : IsUnit ↑m) {P : W.toAffine.Point} : (W.kummerMap m hm) P = 0 ↔ ∃ (Q : W.toAffine.Point), m • Q = P

A point has trivial Kummer class exactly when it is divisible by m in E(K).

The Kummer map on E(K) ⧸ m E(K)

noncomputable def WeierstrassCurve.kummerClassMap {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : W.toAffine.Point ⧸ (nsmulAddMonoidHom m).range →+ TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)

The Kummer map on E(K) ⧸ m E(K), the first map of the m-descent sequence. It is injective (WeierstrassCurve.kummerClassMap_injective).

@[simp]

theorem WeierstrassCurve.kummerClassMap_mk {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (P : W.toAffine.Point) : (W.kummerClassMap m hm) ↑P = (W.kummerMap m hm) P

The quotient Kummer map agrees with kummerMap on representatives.

theorem WeierstrassCurve.kummerClassMap_injective {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : Function.Injective ⇑(W.kummerClassMap m hm)

E(K) ⧸ m E(K) injects into H¹(G_K, E[m]), the kernel of the Kummer map being exactly m E(K).

Exactness at H¹(G_K, E[m])

theorem WeierstrassCurve.range_kummerMap {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : (W.kummerMap m hm).range = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯).ker

The image of the Kummer map is the kernel of H¹(G_K, E[m]) → H¹(G_K, E).

theorem WeierstrassCurve.exact_kummerClassMap_torsionCoeffInclH1 {K : Type u_1} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : Function.Exact ⇑(W.kummerClassMap m hm) ⇑(W.torsionCoeffInclH1 m)

The m-descent sequence is exact at H¹(G_K, E[m]): the kernel of H¹(G_K, E[m]) → H¹(G_K, E)[m] is the image of E(K) ⧸ m E(K) under the Kummer map. Together with WeierstrassCurve.kummerClassMap_injective and WeierstrassCurve.torsionCoeffInclH1_surjective this is the short exact sequence 0 → E(K) ⧸ m E(K) → H¹(G_K, E[m]) → H¹(G_K, E)[m] → 0.