Morphisms of elliptic curves on first Galois cohomology

A morphism f : W₁ → W₂ of elliptic curves over a field K acts G_K-equivariantly on the points over a separable closure (TauCeti.Isogeny.Hom.pointCoeffMap), and hence on first Galois cohomology:

f.pointH1Map : H¹(G_K, E₁(Kˢ)) → H¹(G_K, E₂(Kˢ)).

This map is additive in f, respects identities and composition, and sends multiplication by n on the curve to multiplication by n on cohomology. It commutes with restriction to a field extension L/K along an embedding of separable closures, the morphism being replaced by its base change to L. These are the properties needed to transport classes along an isogeny and back along its dual, for instance between Shafarevich–Tate groups.

Main definitions

• TauCeti.Isogeny.Hom.pointH1Map: the map on H¹(G_K, E(Kˢ)) induced by a morphism over K.

Main results

• TauCeti.Isogeny.Hom.pointH1Map_id, TauCeti.Isogeny.Hom.pointH1Map_comp, TauCeti.Isogeny.Hom.pointH1Map_add, TauCeti.Isogeny.Hom.pointH1Map_natCast: functoriality and additivity.
• TauCeti.Isogeny.Hom.pointCoeffBaseChange_pointCoeffMap: on points over the separable closures, a morphism over K commutes with the coordinate map along an embedding Kˢ → Lˢ.
• TauCeti.Isogeny.Hom.pointRes_pointH1Map: the induced map commutes with restriction.

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.4.
• @sqrt-of-2, Tau Ceti PR #20914, whose map on H¹ induced by a morphism this file follows.

The action on the Galois coefficient modules

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_id {K : Type u_1} [Field K] {W₁ : WeierstrassCurve K} [W₁.IsElliptic] : (id W₁.toAffine).pointCoeffMap = DistribMulActionHom.id (AbsoluteGaloisGroup K)

The identity morphism acts identically on the Galois coefficient module.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_comp {K : Type u_1} [Field K] {W₁ W₂ W₃ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] [W₃.IsElliptic] (g : Hom W₂.toAffine W₃.toAffine) (f : Hom W₁.toAffine W₂.toAffine) : (g.comp f).pointCoeffMap = g.pointCoeffMap.comp f.pointCoeffMap

Composition of morphisms induces composition on Galois coefficient modules.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_add {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f g : Hom W₁.toAffine W₂.toAffine) (P : W₁.PointCoeff) : (f + g).pointCoeffMap P = f.pointCoeffMap P + g.pointCoeffMap P

Addition of morphisms adds their actions on the Galois coefficient module.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_neg {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (P : W₁.PointCoeff) : (-f).pointCoeffMap P = -f.pointCoeffMap P

Negating a morphism negates its action on the Galois coefficient module.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_sub {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f g : Hom W₁.toAffine W₂.toAffine) (P : W₁.PointCoeff) : (f - g).pointCoeffMap P = f.pointCoeffMap P - g.pointCoeffMap P

Subtraction of morphisms subtracts their actions on the Galois coefficient module.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_nsmul {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) (n : ℕ) (P : W₁.PointCoeff) : (n • f).pointCoeffMap P = n • f.pointCoeffMap P

Multiplication of a morphism by a natural number multiplies its action on coefficients.

@[simp]

theorem TauCeti.Isogeny.Hom.pointCoeffMap_zero {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (P : W₁.PointCoeff) : (pointCoeffMap 0) P = 0

The zero morphism acts by zero on the Galois coefficient module.

The map on first cohomology

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

The map H¹(G_K, E₁(Kˢ)) → H¹(G_K, E₂(Kˢ)) induced by a morphism f : W₁ → W₂ over K, through its action on the points over the separable closure.

theorem TauCeti.Isogeny.Hom.pointH1Map_def {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) : f.pointH1Map = ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) W₁.PointCoeff f.pointCoeffMap ⋯

The cohomology map is the coefficient map of the action on points over Kˢ.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_id {K : Type u_1} [Field K] {W₁ : WeierstrassCurve K} [W₁.IsElliptic] : (id W₁.toAffine).pointH1Map = AddMonoidHom.id (ContCohomology.H1 (AbsoluteGaloisGroup K) W₁.PointCoeff)

The identity morphism induces the identity on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_comp {K : Type u_1} [Field K] {W₁ W₂ W₃ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] [W₃.IsElliptic] (g : Hom W₂.toAffine W₃.toAffine) (f : Hom W₁.toAffine W₂.toAffine) : (g.comp f).pointH1Map = g.pointH1Map.comp f.pointH1Map

Composition of morphisms induces composition on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_add {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f g : Hom W₁.toAffine W₂.toAffine) : (f + g).pointH1Map = f.pointH1Map + g.pointH1Map

Addition of morphisms adds their induced maps on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_neg {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f : Hom W₁.toAffine W₂.toAffine) : (-f).pointH1Map = -f.pointH1Map

Negating a morphism negates its induced map on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_sub {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (f g : Hom W₁.toAffine W₂.toAffine) : (f - g).pointH1Map = f.pointH1Map - g.pointH1Map

Subtraction of morphisms subtracts their induced maps on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_zero {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] : pointH1Map 0 = 0

The zero morphism induces zero on first cohomology.

@[simp]

theorem TauCeti.Isogeny.Hom.pointH1Map_natCast {K : Type u_1} [Field K] {W₁ : WeierstrassCurve K} [W₁.IsElliptic] (n : ℕ) (c : ContCohomology.H1 (AbsoluteGaloisGroup K) W₁.PointCoeff) : (↑n).pointH1Map c = n • c

Multiplication by n on the curve induces multiplication by n on first cohomology.

Compatibility with restriction

theorem TauCeti.Isogeny.Hom.pointCoeffBaseChange_pointCoeffMap {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (f : Hom W₁.toAffine W₂.toAffine) (P : W₁.PointCoeff) : (W₂.pointCoeffBaseChange τ) (f.pointCoeffMap P) = (f.map (algebraMap K L)).pointCoeffMap ((W₁.pointCoeffBaseChange τ) P)

A morphism over K commutes with the coordinate map along τ : Kˢ → Lˢ: applying τ to the image of a point under f gives the image under the base change of f to L of the point with τ applied.

theorem TauCeti.Isogeny.Hom.pointRes_pointH1Map {K : Type u_1} [Field K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (f : Hom W₁.toAffine W₂.toAffine) (c : ContCohomology.H1 (AbsoluteGaloisGroup K) W₁.PointCoeff) : (W₂.pointRes τ) (f.pointH1Map c) = (f.map (algebraMap K L)).pointH1Map ((W₁.pointRes τ) c)

The induced map commutes with restriction: restricting f.pointH1Map c along τ is applying the map of the base change of f to L to the restriction of c.