Isogenies of Weierstrass curves

An isogeny between affine Weierstrass curves over a field is represented contravariantly by a pullback from the target coordinate ring to the source function field. The pullback is required to send the source point at infinity to the target point at infinity. Algebraically, this means that the source coordinate ring is integral over the image of the target coordinate ring.

This file introduces that data and its identity element. The integrality condition installs the algebra structure induced by the chosen pullback only locally: different pullbacks generally give different algebra structures on the same function field, so registering one globally would create a typeclass diamond.

Main definitions

• TauCeti.CoordinatePullback: the contravariant coordinate-ring map of a morphism.
• TauCeti.CoordinatePullback.MapsInfinity: the integrality condition expressing pointedness.
• TauCeti.Isogeny: a coordinate pullback satisfying MapsInfinity.
• TauCeti.Isogeny.id: the identity isogeny.

Main results

• WeierstrassCurve.Affine.CoordinateRing.algHom_ext: two pullbacks agreeing on the two coordinates are equal.

The coordinate-ring universal property used to build and move pullbacks is stated at its natural generality in Affine/Eval.lean. Isogeny/MulByInt/Basic.lean makes [n] from the division-polynomial point, and Isogeny/BaseChange.lean carries a pullback along a change of base field by carrying its point. The identity and Frobenius pullbacks instead come directly from their underlying ring maps.

This is the opening milestone of Layer 1 of the elliptic-curves roadmap. The definition is the coordinate-ring form of D. Angdinata's function-field definition of an isogeny. The geometric interpretation follows Silverman, The Arithmetic of Elliptic Curves, II.2.4. No ellipticity or normality assumption is needed to state the data.

@[reducible, inline]

abbrev TauCeti.CoordinatePullback {F : Type u_1} [Field F] (W₁ W₂ : WeierstrassCurve.Affine F) : Type u_1

A contravariant pullback from the target coordinate ring to the source function field.

Equations

• TauCeti.CoordinatePullback W₁ W₂ = (W₂.CoordinateRing →ₐ[F] W₁.FunctionField)

def TauCeti.CoordinatePullback.MapsInfinity {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (pullback : CoordinatePullback W₁ W₂) : Prop

The source point at infinity maps to the target point at infinity: every element of the source coordinate ring is integral over the target coordinate ring acting through pullback.

The algebra structure induced by pullback is deliberately local to the definition.

Equations

• pullback.MapsInfinity = ∀ (x : W₁.CoordinateRing), (algebraMap W₁.CoordinateRing W₁.FunctionField) x ∈ integralClosure W₂.CoordinateRing W₁.FunctionField

@[simp]

theorem TauCeti.CoordinatePullback.mapsInfinity_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (pullback : CoordinatePullback W₁ W₂) : pullback.MapsInfinity ↔ ∀ (x : W₁.CoordinateRing), IsIntegral W₂.CoordinateRing ((algebraMap W₁.CoordinateRing W₁.FunctionField) x)

A coordinate pullback maps infinity to infinity exactly when the source coordinate ring is integral over the target coordinate ring acting through the pullback.

theorem TauCeti.CoordinatePullback.mapsInfinity_of_pow {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (pullback : CoordinatePullback W₁ W₂) {n : ℕ} (hn : 0 < n) (h : ∀ (z : W₁.CoordinateRing), ∃ (w : W₂.CoordinateRing), pullback w = (algebraMap W₁.CoordinateRing W₁.FunctionField) z ^ n) : pullback.MapsInfinity

A coordinate pullback maps infinity to infinity if a fixed positive power of every source coordinate function is pulled back from the target.

noncomputable def TauCeti.CoordinatePullback.id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : CoordinatePullback W W

The identity coordinate pullback, embedding a coordinate ring into its fraction field.

Equations

• TauCeti.CoordinatePullback.id W = IsScalarTower.toAlgHom F W.CoordinateRing W.FunctionField

@[simp]

theorem TauCeti.CoordinatePullback.id_apply {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (x : W.CoordinateRing) : (id W) x = (algebraMap W.CoordinateRing W.FunctionField) x

The identity coordinate pullback is the canonical embedding into the function field.

@[simp]

theorem TauCeti.CoordinatePullback.mapsInfinity_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (x : W.CoordinateRing) : IsIntegral W.CoordinateRing ((algebraMap W.CoordinateRing W.FunctionField) x)

The identity coordinate pullback maps infinity to infinity.

structure TauCeti.Isogeny {F : Type u_1} [Field F] (W₁ W₂ : WeierstrassCurve.Affine F) : Type u_1

The pullback data of a nonzero isogeny between affine Weierstrass curves.

The mapsInfinity field is the algebraic form of pointedness. Injectivity and finiteness of the induced extension are the next results in the isogeny development; they are consequences of this condition rather than additional structure fields.

• pullback : CoordinatePullback W₁ W₂

  The contravariant map out of the target coordinate ring.

• mapsInfinity : self.pullback.MapsInfinity

  The source point at infinity maps to the target point at infinity.

theorem TauCeti.Isogeny.ext_iff {F : Type u_1} {inst✝ : Field F} {W₁ W₂ : WeierstrassCurve.Affine F} {x y : Isogeny W₁ W₂} : x = y ↔ x.pullback = y.pullback

theorem TauCeti.Isogeny.ext {F : Type u_1} {inst✝ : Field F} {W₁ W₂ : WeierstrassCurve.Affine F} {x y : Isogeny W₁ W₂} (pullback : x.pullback = y.pullback) : x = y

noncomputable def TauCeti.Isogeny.id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : Isogeny W W

The identity isogeny.

Equations

• TauCeti.Isogeny.id W = { pullback := TauCeti.CoordinatePullback.id W, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.id_pullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).pullback = CoordinatePullback.id W