Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.Point.xRep

{R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → W'.Point → Fin 2 → R

This map sends a point P on a Weierstrass curve W' in affine coordinates to a representative of its image on ℙ¹ under the x-coordinate map. We take ![1, 0] for the point at infinity and ![x, 1], where x is the x-coordinate of P, for an affine point. We define it in the general setting of a commutative base ring, even though the definition of points in this setting is not really correct. For Weierstrass curves over fields, this gives the correct notion.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

8 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing