Theorems · Definition · algebraic geometry

WeierstrassCurve.Jacobian.Point.toAffineLift

{F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → W.Point → W.toAffine.Point

The natural map from a nonsingular Jacobian point on a Weierstrass curve W to its corresponding nonsingular point in affine coordinates. If hP is the nonsingular condition underlying a nonsingular Jacobian point P on W, then toAffineLift ⟨hP⟩ is definitionally equivalent to toAffine W P.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

8 results in Mathlib

Foundations

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

Assumes

Field