The Kummer sequence of an isogeny and the φ-descent sequence

Let φ : W₁ → W₂ be an isogeny of elliptic curves over a field K, Kˢ a separable closure and G_K its Galois group. The isogeny acts on the points over Kˢ, and this action commutes with G_K because φ is defined over K (TauCeti.Isogeny.Hom.pointCoeffMap). Its kernel E₁(Kˢ)[φ] is therefore a discrete G_K-module (TauCeti.Isogeny.Hom.KerCoeff). When φ is separable it is onto on points over Kˢ, and the Kummer sequence of φ

0 ⟶ E₁(Kˢ)[φ] ⟶ E₁(Kˢ) ⟶ E₂(Kˢ) ⟶ 0

is a short exact sequence of discrete G_K-modules (TauCeti.Isogeny.kummerShortExact). Its degree-zero connecting map, read on E₂(K) through WeierstrassCurve.basePointEquivInvariants, is the Kummer map E₂(K) → H¹(G_K, E₁[φ]), and the long exact sequence of continuous cohomology gives the φ-descent sequence (Silverman X.4)

0 ⟶ E₂(K) ⧸ φ(E₁(K)) ⟶ H¹(G_K, E₁[φ]) ⟶ H¹(G_K, E₁)[φ] ⟶ 0,

where H¹(G_K, E₁)[φ] is the kernel of the map H¹(G_K, E₁) → H¹(G_K, E₂) induced by φ. The Kummer class of P is represented by σ ↦ σ Q - Q for any Q ∈ E₁(Kˢ) with φ Q = P.

This is the descent sequence of WeierstrassCurve.kummerMap with multiplication by m replaced by an arbitrary separable isogeny. Separability is what makes φ onto on points over Kˢ; for [m] it is the invertibility of m in K. Selmer groups attached to φ and to its dual are cut out of the middle term by local conditions, as in WeierstrassCurve.selmerGroup.

Main definitions

• TauCeti.Isogeny.Hom.pointCoeffMap: the G_K-equivariant action E₁(Kˢ) → E₂(Kˢ) of a morphism f : W₁ → W₂ over K.
• TauCeti.Isogeny.Hom.KerCoeff: its kernel E₁(Kˢ)[f], a discrete G_K-module.
• TauCeti.Isogeny.Hom.kummerCocycle: the cocycle σ ↦ σ Q - Q attached to a point Q over Kˢ whose image is rational.
• TauCeti.Isogeny.kummerShortExact: the Kummer sequence of a separable isogeny.
• TauCeti.Isogeny.kummerMap: the Kummer map E₂(K) → H¹(G_K, E₁[φ]).
• TauCeti.Isogeny.kummerClassMap: the induced map on E₂(K) ⧸ φ(E₁(K)).
• TauCeti.Isogeny.quotientRangeEquivRangeKummerMap: the identification of E₂(K) ⧸ φ(E₁(K)) with the image of the Kummer map.
• TauCeti.Isogeny.kerCoeffInclH1: the map H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ].

Main results

• TauCeti.Isogeny.Hom.pointCoeffMap_basePointCoeff: the action over Kˢ extends the action on E₁(K).
• TauCeti.Isogeny.kummerMap_eq_H1pi: the Kummer class of P is the class of σ ↦ σ Q - Q.
• TauCeti.Isogeny.ker_kummerMap: the kernel of the Kummer map is φ(E₁(K)).
• TauCeti.Isogeny.natCard_range_kummerMap: the image of the Kummer map has order [E₂(K) : φ(E₁(K))]; it is trivial over a separably closed field (TauCeti.Isogeny.natCard_range_kummerMap_of_isSepClosed).
• TauCeti.Isogeny.kummerClassMap_injective, TauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1 and TauCeti.Isogeny.kerCoeffInclH1_surjective: the φ-descent sequence.

References

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

The action on the points over a separable closure

@[reducible, inline]

noncomputable abbrev TauCeti.Isogeny.Hom.mapSeparableClosure {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} (f : Hom W₁.toAffine W₂.toAffine) : Hom (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₁ (SeparableClosure K))) (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₂ (SeparableClosure K)))

The base change of a morphism f : W₁ → W₂ to a separable closure Kˢ of K, typed between the base changes W₁⁄Kˢ and W₂⁄Kˢ whose points are the Galois coefficient modules.

noncomputable def TauCeti.Isogeny.Hom.pointCoeffMap {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) : W₁.PointCoeff →+[AbsoluteGaloisGroup K] W₂.PointCoeff

The action of a morphism over K on the points over Kˢ, as a G_K-equivariant homomorphism E₁(Kˢ) → E₂(Kˢ). Equivariance holds because the morphism is defined over K (TauCeti.Isogeny.Hom.pointMap_map_algebraMap_map).

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffEquiv_symm_pointCoeffMap {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (P : W₁.PointCoeff) : W₂.pointCoeffEquiv.symm (f.pointCoeffMap P) = f.mapSeparableClosure.pointMap (W₁.pointCoeffEquiv.symm P)

The action on E₁(Kˢ), read on the points of W₁⁄Kˢ, is the base change of f to Kˢ.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_pointCoeffEquiv {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (P : (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W₁ (SeparableClosure K))).Point) : f.pointCoeffMap (W₁.pointCoeffEquiv P) = W₂.pointCoeffEquiv (f.mapSeparableClosure.pointMap P)

The action on a point of W₁⁄Kˢ, read in W₁.PointCoeff.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_basePointCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] [DecidableEq K] (f : Hom W₁.toAffine W₂.toAffine) (P : W₁.toAffine.Point) : f.pointCoeffMap (W₁.basePointCoeff P) = W₂.basePointCoeff (f.pointMap P)

The action over Kˢ extends the action on rational points: a morphism over K sends the image in E₁(Kˢ) of a point of E₁(K) to the image of its value in E₂(K).

The kernel

@[reducible, inline]

abbrev TauCeti.Isogeny.Hom.KerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) : Type u_1

The kernel E₁(Kˢ)[f] of the action of a morphism f : W₁ → W₂ over K on the points over Kˢ, as a coefficient module of the Galois cohomology of W₁. Its topology is the subspace topology, which is discrete.

theorem TauCeti.Isogeny.Hom.smul_mem_kerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} (σ : AbsoluteGaloisGroup K) {P : W₁.PointCoeff} (hP : P ∈ (↑f.pointCoeffMap).ker) : σ • P ∈ (↑f.pointCoeffMap).ker

The Galois action commutes with f, so it preserves E₁(Kˢ)[f].

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.Hom.instDistribMulActionAbsoluteGaloisGroupKerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} : DistribMulAction (AbsoluteGaloisGroup K) f.KerCoeff

@[simp]

theorem TauCeti.Isogeny.Hom.coe_smul_kerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} (σ : AbsoluteGaloisGroup K) (P : f.KerCoeff) : ↑(σ • P) = σ • ↑P

The Galois action on E₁(Kˢ)[f] is the action on E₁(Kˢ).

instance TauCeti.Isogeny.Hom.KerCoeff.instContinuousSMul {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} : ContinuousSMul (AbsoluteGaloisGroup K) f.KerCoeff

E₁(Kˢ)[f] is a discrete G_K-module: the restriction of the continuous action on E₁(Kˢ) to a stable subgroup is continuous.

def TauCeti.Isogeny.Hom.kerCoeffIncl {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) : f.KerCoeff →+[AbsoluteGaloisGroup K] W₁.PointCoeff

The inclusion E₁(Kˢ)[f] → E₁(Kˢ), as a G_K-equivariant homomorphism.

@[simp]

theorem TauCeti.Isogeny.Hom.kerCoeffIncl_apply {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} (P : f.KerCoeff) : f.kerCoeffIncl P = ↑P

The inclusion E₁(Kˢ)[f] → E₁(Kˢ) forgets membership in the kernel.

The Kummer cocycle

theorem TauCeti.Isogeny.Hom.smul_sub_mem_kerCoeff {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} [DecidableEq K] {P : W₂.toAffine.Point} {Q : W₁.PointCoeff} (hQ : f.pointCoeffMap Q = W₂.basePointCoeff P) (σ : AbsoluteGaloisGroup K) : σ • Q - Q ∈ (↑f.pointCoeffMap).ker

The Kummer difference lies in the kernel: if f Q is the image of a point of E₂(K), then σ Q - Q is killed by f, because G_K fixes f Q.

noncomputable def TauCeti.Isogeny.Hom.kummerCocycle {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} [DecidableEq K] {P : W₂.toAffine.Point} {Q : W₁.PointCoeff} (hQ : f.pointCoeffMap Q = W₂.basePointCoeff P) : AbsoluteGaloisGroup K → f.KerCoeff

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

@[simp]

theorem TauCeti.Isogeny.Hom.coe_kummerCocycle {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} [DecidableEq K] {P : W₂.toAffine.Point} {Q : W₁.PointCoeff} (hQ : f.pointCoeffMap Q = W₂.basePointCoeff P) (σ : AbsoluteGaloisGroup K) : ↑(kummerCocycle hQ σ) = σ • Q - Q

The Kummer cocycle takes the value σ Q - Q at σ.

theorem TauCeti.Isogeny.Hom.kummerCocycle_mem_Z1 {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {f : Hom W₁.toAffine W₂.toAffine} [DecidableEq K] {P : W₂.toAffine.Point} {Q : W₁.PointCoeff} (hQ : f.pointCoeffMap Q = W₂.basePointCoeff P) : kummerCocycle hQ ∈ ContCohomology.Z1 (AbsoluteGaloisGroup K) f.KerCoeff

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

The Kummer sequence of a separable isogeny

theorem TauCeti.Isogeny.pointCoeffMap_ofIsogeny_surjective {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] : Function.Surjective ⇑(Hom.ofIsogeny φ).pointCoeffMap

A separable isogeny is onto on points over Kˢ: it stays separable after base change, and a separable isogeny over a separably closed field is surjective on points.

noncomputable def TauCeti.Isogeny.kummerShortExact {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] : ContCohomology.DiscreteShortExact (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff W₁.PointCoeff W₂.PointCoeff

The Kummer sequence 0 → E₁(Kˢ)[φ] → E₁(Kˢ) → E₂(Kˢ) → 0 of a separable isogeny φ. Exactness on the right is the surjectivity of φ on points over Kˢ.

@[simp]

theorem TauCeti.Isogeny.kummerShortExact_incl {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] : φ.kummerShortExact.incl = (↑(Hom.ofIsogeny φ).pointCoeffMap).ker.subtype

The inclusion of the Kummer sequence is the inclusion of the kernel of φ.

@[simp]

theorem TauCeti.Isogeny.kummerShortExact_proj {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] : φ.kummerShortExact.proj = ↑(Hom.ofIsogeny φ).pointCoeffMap

The projection of the Kummer sequence is the action of φ on E₁(Kˢ).

@[simp]

theorem TauCeti.Isogeny.kummerShortExact_inclDistribMulActionHom {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] : φ.kummerShortExact.inclDistribMulActionHom = (Hom.ofIsogeny φ).kerCoeffIncl

The equivariant inclusion of the Kummer sequence is TauCeti.Isogeny.Hom.kerCoeffIncl.

@[simp]

theorem TauCeti.Isogeny.kummerShortExact_projDistribMulActionHom {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] : φ.kummerShortExact.projDistribMulActionHom = (Hom.ofIsogeny φ).pointCoeffMap

The equivariant projection of the Kummer sequence is TauCeti.Isogeny.Hom.pointCoeffMap.

The Kummer map

noncomputable def TauCeti.Isogeny.kummerMap {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] : W₂.toAffine.Point →+ ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff

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

@[simp]

theorem TauCeti.Isogeny.kummerMap_apply {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] (P : W₂.toAffine.Point) : φ.kummerMap P = φ.kummerShortExact.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 TauCeti.Isogeny.kummerMap_eq_H1pi {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] {P : W₂.toAffine.Point} {Q : W₁.PointCoeff} (hQ : (Hom.ofIsogeny φ).pointCoeffMap Q = W₂.basePointCoeff P) : φ.kummerMap P = (ContCohomology.H1pi (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff) ⟨Hom.kummerCocycle hQ, ⋯⟩

The Kummer class of P is represented by σ ↦ σ Q - Q, for any Q ∈ E₁(Kˢ) with φ Q = P (Silverman X.4). Such a Q exists because φ is onto on points over Kˢ.

theorem TauCeti.Isogeny.explicitCoeff0_basePointEquivInvariants {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] (P : W₁.toAffine.Point) : (ContCohomology.explicitCoeff0 (AbsoluteGaloisGroup K) W₁.PointCoeff φ.kummerShortExact.projDistribMulActionHom) (W₁.basePointEquivInvariants P) = W₂.basePointEquivInvariants ((Hom.ofIsogeny φ).pointMap P)

φ on the invariants of E₁(Kˢ) is φ 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 TauCeti.Isogeny.ker_kummerMap {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] : φ.kummerMap.ker = (Hom.ofIsogeny φ).pointMapHom.range

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

theorem TauCeti.Isogeny.kummerMap_eq_zero_iff {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] {P : W₂.toAffine.Point} : φ.kummerMap P = 0 ↔ ∃ (Q : W₁.toAffine.Point), (Hom.ofIsogeny φ).pointMap Q = P

A point has trivial Kummer class exactly when it lies in φ(E₁(K)).

The φ-descent sequence

noncomputable def TauCeti.Isogeny.kummerClassMap {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] : W₂.toAffine.Point ⧸ (Hom.ofIsogeny φ).pointMapHom.range →+ ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff

The Kummer map on E₂(K) ⧸ φ(E₁(K)), the first map of the φ-descent sequence. It is injective (TauCeti.Isogeny.kummerClassMap_injective).

@[simp]

theorem TauCeti.Isogeny.kummerClassMap_mk {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] (P : W₂.toAffine.Point) : φ.kummerClassMap ↑P = φ.kummerMap P

The quotient Kummer map agrees with TauCeti.Isogeny.kummerMap on representatives.

theorem TauCeti.Isogeny.kummerClassMap_injective {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] : Function.Injective ⇑φ.kummerClassMap

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

noncomputable def TauCeti.Isogeny.quotientRangeEquivRangeKummerMap {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] : W₂.toAffine.Point ⧸ (Hom.ofIsogeny φ).pointMapHom.range ≃+ ↥φ.kummerMap.range

The Kummer image is a copy of the cokernel: the Kummer map of a separable isogeny induces an isomorphism of E₂(K) ⧸ φ(E₁(K)) onto its image in H¹(G_K, E₁[φ]), its kernel being φ(E₁(K)) (TauCeti.Isogeny.ker_kummerMap).

@[simp]

theorem TauCeti.Isogeny.coe_quotientRangeEquivRangeKummerMap_mk {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] (P : W₂.toAffine.Point) : ↑(φ.quotientRangeEquivRangeKummerMap ↑P) = φ.kummerMap P

quotientRangeEquivRangeKummerMap sends the class of P to its Kummer class.

theorem TauCeti.Isogeny.natCard_range_kummerMap {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] : Nat.card ↥φ.kummerMap.range = (Hom.ofIsogeny φ).pointMapHom.range.index

The Kummer image has order the Kummer-cokernel index [E₂(K) : φ(E₁(K))]. As a Nat.card identity it holds without finiteness hypotheses, both sides being 0 when the cokernel is infinite.

theorem TauCeti.Isogeny.finite_range_kummerMap_iff {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] : Finite ↥φ.kummerMap.range ↔ (Hom.ofIsogeny φ).pointMapHom.range.FiniteIndex

The Kummer image is finite exactly when the image of E₁(K) has finite index in E₂(K).

theorem TauCeti.Isogeny.natCard_range_kummerMap_of_isSepClosed {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] [IsSepClosed K] : Nat.card ↥φ.kummerMap.range = 1

Over a separably closed field the Kummer image is trivial, a separable isogeny being onto on points there. At a complex place this is the numerator of the local factor #H¹_φ(K_v) / #E₁(K_v)[φ], which is therefore 1 / deg φ.

theorem TauCeti.Isogeny.range_kummerMap {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] : φ.kummerMap.range = (ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff (Hom.ofIsogeny φ).kerCoeffIncl ⋯).ker

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

theorem TauCeti.Isogeny.range_explicitCoeff1_kerCoeffIncl {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] : (ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff (Hom.ofIsogeny φ).kerCoeffIncl ⋯).range = (ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) W₁.PointCoeff (Hom.ofIsogeny φ).pointCoeffMap ⋯).ker

The image of H¹(G_K, E₁[φ]) → H¹(G_K, E₁) is the kernel of the map H¹(G_K, E₁) → H¹(G_K, E₂) induced by φ, the last exactness statement of the φ-descent sequence.

noncomputable def TauCeti.Isogeny.kerCoeffInclH1 {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] : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff →+ ↥(ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) W₁.PointCoeff (Hom.ofIsogeny φ).pointCoeffMap ⋯).ker

The map H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ], the last map of the φ-descent sequence: the map induced by the inclusion E₁(Kˢ)[φ] → E₁(Kˢ), with values in the kernel H¹(G_K, E₁)[φ] of the map induced by φ. It is surjective (TauCeti.Isogeny.kerCoeffInclH1_surjective), with kernel the image of the Kummer map (TauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1).

@[simp]

theorem TauCeti.Isogeny.coe_kerCoeffInclH1 {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] (c : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff) : ↑(φ.kerCoeffInclH1 c) = (ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff (Hom.ofIsogeny φ).kerCoeffIncl ⋯) c

H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ] is the map induced by the inclusion E₁(Kˢ)[φ] → E₁(Kˢ).

theorem TauCeti.Isogeny.kerCoeffInclH1_surjective {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] : Function.Surjective ⇑φ.kerCoeffInclH1

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

theorem TauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1 {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] : Function.Exact ⇑φ.kummerClassMap ⇑φ.kerCoeffInclH1

The φ-descent sequence is exact at H¹(G_K, E₁[φ]): the kernel of H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ] is the image of E₂(K) ⧸ φ(E₁(K)) under the Kummer map. Together with TauCeti.Isogeny.kummerClassMap_injective and TauCeti.Isogeny.kerCoeffInclH1_surjective this is the short exact sequence 0 → E₂(K) ⧸ φ(E₁(K)) → H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ] → 0.