Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.Hom.Cokernel

The torsion correction to an isogeny's cokernel #

Let f : E₁ → E₂ be a nonzero morphism of elliptic curves. Its dual shows that f reflects torsion: the inverse image of E₂(F)tors is exactly E₁(F)tors. Consequently the cokernel on points and the cokernel modulo torsion satisfy

#coker(f) · #E₁(F)tors = #coker(f_free) · #E₂(F)tors · #ker(f).

Here the cokernel modulo torsion is expressed as the index of the image in E₂(F)/E₂(F)tors; the map from E₁(F) has the same image as the induced map from its quotient by torsion. This avoids choosing bases or splittings of the Mordell–Weil groups.

The kernel is finite for every nonzero morphism. When the source torsion is finite (in particular, when the source is finitely generated), division gives the rational cokernel/kernel ratio #coker(f) / #ker(f). When the target is finitely generated, the cokernel is finite too: its image contains deg(f) · E₂(F).

Since f̂ ∘ f is multiplication by deg f, the cokernel/kernel ratios of f and f̂ multiply to that of [deg f] on E₁(F). In cross-multiplied form,

#coker([deg f]) · #ker(f) · #ker(f̂) = #coker(f̂) · #coker(f) · #E₁(F)[deg f].

This holds over every field, again with no finiteness hypothesis; when the six quantities are finite it is the ratio identity. Over a local field, at a place prime to deg f, the ratio for [deg f] is 1, so the ratios of f and f̂ are inverse.

This is the torsion factor in the kernel/cokernel proof of Cassels' isogeny invariance of the BSD quotient. The regulator, period, local, and Tate–Shafarevich factors are not treated here. No characteristic-zero or separability hypothesis is needed.

Main results #

References #

source
@[simp]
theorem TauCeti.Isogeny.Hom.comap_torsion_pointMapHom {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (hf : f ≠ 0) :
AddSubgroup.comap f.pointMapHom (AddCommGroup.torsion W₂.Point) = AddCommGroup.torsion W₁.Point

A nonzero morphism of elliptic curves has exactly the torsion points as the inverse image of the target's torsion subgroup.

source
theorem TauCeti.Isogeny.Hom.ker_pointMapHom_le_torsion {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (hf : f ≠ 0) :
f.pointMapHom.ker ≤ AddCommGroup.torsion W₁.Point

Every point in the kernel of a nonzero morphism is torsion.

source
theorem TauCeti.Isogeny.Hom.finite_ker_pointMapHom {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (hf : f ≠ 0) :
Finite ↥f.pointMapHom.ker

The kernel on points of a nonzero morphism is finite, as its fibre over zero.

source
theorem TauCeti.Isogeny.Hom.finiteIndex_range_pointMapHom {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) [AddGroup.FG W₂.Point] (hf : f ≠ 0) :
f.pointMapHom.range.FiniteIndex

The cokernel on rational points is finite if the target group is finitely generated: the image contains all deg(f)-multiples, by the dual identity.

source
theorem TauCeti.Isogeny.Hom.index_range_mul_card_torsion {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (hf : f ≠ 0) :
f.pointMapHom.range.index * Nat.card ↥(AddCommGroup.torsion W₁.Point) = (AddSubgroup.map (QuotientAddGroup.mk' (AddCommGroup.torsion W₂.Point)) f.pointMapHom.range).index * Nat.card ↥(AddCommGroup.torsion W₂.Point) * Nat.card ↥f.pointMapHom.ker

The correction between the full cokernel index and the image index modulo torsion. The cross-multiplied identity needs no finite-generation or finiteness hypothesis.

source
theorem TauCeti.Isogeny.Hom.index_range_div_card_ker {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) [Finite ↥(AddCommGroup.torsion W₁.Point)] (hf : f ≠ 0) :
↑f.pointMapHom.range.index / ↑(Nat.card ↥f.pointMapHom.ker) = ↑(AddSubgroup.map (QuotientAddGroup.mk' (AddCommGroup.torsion W₂.Point)) f.pointMapHom.range).index * ↑(Nat.card ↥(AddCommGroup.torsion W₂.Point)) / ↑(Nat.card ↥(AddCommGroup.torsion W₁.Point))

The rational cokernel/kernel ratio #coker(f) / #ker(f) equals the image index modulo torsion times the ratio of target to source torsion orders. Only the source torsion subgroup needs to be finite; in particular, finite generation of the source suffices. If the target is finitely generated, finiteIndex_range_pointMapHom makes the cokernel index a positive integer.

source
theorem TauCeti.Isogeny.Hom.index_range_nsmul_mul_card_ker_mul_card_ker_dual {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) :
(nsmulAddMonoidHom f.degree).range.index * (Nat.card ↥f.pointMapHom.ker * Nat.card ↥f.dual.pointMapHom.ker) = f.dual.pointMapHom.range.index * f.pointMapHom.range.index * Nat.card ↥(nsmulAddMonoidHom f.degree).ker

The cokernel/kernel ratios of a morphism and of its dual multiply to that of multiplication by the degree: on the points over any field, #coker([deg f]) · #ker(f) · #ker(f̂) = #coker(f̂) · #coker(f) · #E₁(F)[deg f]. No finiteness is required: infinite orders and indices are read as 0. When all of them are finite, dividing out gives the identity of ratios.