The point map induced by a ring homomorphism

Mathlib's WeierstrassCurve.Affine.Point.map moves the points of a fixed curve between two field extensions of a base, along an AlgHom in a scalar tower — which covers the q-power Frobenius, Mathlib bundling that as FiniteField.frobeniusAlgHom. This file supplies the other functoriality: an injective ring homomorphism f : R →+* S carries the points of W over R to the points of the curve W.map f over S, with no fields and no tower involved.

Main definitions and results

• WeierstrassCurve.Affine.Point.mapAlong: the map W.Point → (W.map f).Point, over arbitrary commutative rings.
• WeierstrassCurve.Affine.Point.mapAlong_neg, mapAlong_id, mapAlong_mapAlong and mapAlong_injective: the functorial API, over arbitrary commutative rings, mirroring Mathlib's Affine.Point.map_id, map_map and map_injective for the AlgHom version. Both curve equalities — W.map (RingHom.id R) = W and (W.map f).map g = W.map (g.comp f) — hold by definition, so the identity and composition laws are stated with no transport.
• WeierstrassCurve.Affine.Point.mapAlong_eq_map: over a field, when K is an F-algebra, the transport along algebraMap F K is Mathlib's Affine.Point.map. A user holding only a ring homomorphism f : F →+* K writes letI := f.toAlgebra and gets the same statement for f.
• WeierstrassCurve.Affine.Point.mapAlong_iterateFrobenius_some: iterated Frobenius sends (x, y) to (x ^ (p ^ n), y ^ (p ^ n)).
• WeierstrassCurve.Affine.Point.mapAlong_add: over fields the transport is additive.

Affine.Point.map is already an AddMonoidHom, so installing f.toAlgebra locally and rewriting with mapAlong_eq_map gives map_add, map_zero and map_zsmul from Mathlib directly, including when f is a field endomorphism.

What Mathlib lacks, and what this file adds, is the transport over arbitrary commutative rings, where W.Point has no group law to speak of.

The definition needs only injectivity, since that is what Affine.map_nonsingular needs to carry nonsingularity across. Negation and the functorial laws hold over any commutative ring and are proved here at that generality.

This supports the Hasse strand of TauCetiRoadmap/EllipticCurves/README.md, Layer 3: the Silverman V.1 route counts #E(𝔽_q) as the fixed points of Frobenius, which means transporting points along the q-power ring homomorphism and knowing that transport respects the group law and ℤ-multiples. The roadmap's §"What Mathlib already has (consume)" lists Affine.Point and its AddCommGroup as consumed infrastructure whose "infrastructure is load-bearing API here, not an implementation detail"; this is a complement to that API, not a reimplementation of it.

Provenance

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by that roadmap at dev/hasse-weil @ 513e83879e2f), HasseWeil/EC/AffinePointMap.lean, declarations map, map_zero, map_some and map_neg.

The source's mapAddMonoidHom and map_zsmul are not ported; over fields they are Mathlib's Affine.Point.map under f.toAlgebra. The source's map_add corresponds to mapAlong_add, proved through the same bridge.

Changes from the source. The names take an Along suffix (mapAlong), Mathlib having taken Point.map for the AlgHom version. The computation rules are stated in simp-normal form, and negation and the functorial laws are stated over an arbitrary commutative ring rather than a field. The identity, composition and injectivity laws have no counterpart in the source.

noncomputable def WeierstrassCurve.Affine.Point.mapAlong {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) : W.toAffine.Point → (W.map f).toAffine.Point

The points of W map to the points of W.map f along an injective ring homomorphism. Nonsingularity transports by Mathlib's Affine.map_nonsingular, which is what injectivity is for.

Equations

• WeierstrassCurve.Affine.Point.mapAlong f hf WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Point.zero
• WeierstrassCurve.Affine.Point.mapAlong f hf (WeierstrassCurve.Affine.Point.some x_1 y h) = WeierstrassCurve.Affine.Point.some (f x_1) (f y) ⋯

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) : mapAlong f hf 0 = 0

The point map sends the point at infinity to the point at infinity.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_some {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) {x y : R} (h : W.toAffine.Nonsingular x y) : mapAlong f hf (some x y h) = some (f x) (f y) ⋯

The point map sends an affine point to the point with image coordinates.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_neg {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) (P : W.toAffine.Point) : mapAlong f hf (-P) = -mapAlong f hf P

The point map preserves negation, over any commutative ring.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_id {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} (P : W.toAffine.Point) : mapAlong (RingHom.id R) ⋯ P = P

The point map along the identity is the identity. W.map (RingHom.id R) is W by definition, so no transport is needed.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_mapAlong {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) {T : Type u_3} [CommRing T] (g : S →+* T) (hg : Function.Injective ⇑g) (P : W.toAffine.Point) : mapAlong g hg (mapAlong f hf P) = mapAlong (g.comp f) ⋯ P

The point map is functorial in the ring homomorphism. (W.map f).map g is W.map (g.comp f) by definition, so no transport is needed.

theorem WeierstrassCurve.Affine.Point.mapAlong_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {W : WeierstrassCurve R} (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (mapAlong f hf)

The point map is injective.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_eq_map {F : Type u_3} {K : Type u_4} [Field F] [Field K] [DecidableEq F] [DecidableEq K] [Algebra F K] {W : WeierstrassCurve F} (P : W.toAffine.Point) : mapAlong (algebraMap F K) ⋯ P = (map (Algebra.ofId F K)) P

Over a field the transport is Mathlib's Affine.Point.map. For a ring homomorphism f : F →+* K that is not an ambient algebraMap, apply this under letI := f.toAlgebra, where algebraMap F K is f by definition.

@[simp]

theorem WeierstrassCurve.Affine.Point.mapAlong_add {F : Type u_3} {K : Type u_4} [Field F] [Field K] [DecidableEq F] [DecidableEq K] {W : WeierstrassCurve F} (f : F →+* K) (hf : Function.Injective ⇑f) (P Q : W.toAffine.Point) : mapAlong f hf (P + Q) = mapAlong f hf P + mapAlong f hf Q

Over fields the point map is additive, by identifying it with Mathlib's additive Affine.Point.map after installing the algebra structure induced by f.

theorem WeierstrassCurve.Affine.Point.mapAlong_iterateFrobenius_some {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} (p : ℕ) [ExpChar R p] (n : ℕ) (hinj : Function.Injective ⇑(iterateFrobenius R p n)) {x y : R} (h : W.toAffine.Nonsingular x y) : mapAlong (iterateFrobenius R p n) hinj (some x y h) = some (x ^ p ^ n) (y ^ p ^ n) ⋯

The iterated Frobenius sends an affine point (x, y) to (x ^ (p ^ n), y ^ (p ^ n)).

Not a simp lemma: mapAlong_some already rewrites the left-hand side to coordinates expressed using iterateFrobenius; this theorem records their p ^ n-power form.