toAffineLift — Mathlib

English

The natural lift from a nonsingular projective point to an affine point coincides with the standard affine image: toAffineLift ⟨hP⟩ = toAffine W P.

Русский

Естественное восхождение ненонсигурной проектной точки к аффинной точке совпадает с обычным аффинным отображением: toAffineLift ⟨hP⟩ = toAffine W P.

LaTeX

$$$\\mathrm{toAffineLift}(\\langle h_P \\rangle) = \\mathrm{toAffine}(W, P)$$$

Lean4

/-- The natural map from a nonsingular projective point on a Weierstrass curve `W` to its
corresponding nonsingular point in affine coordinates.

If `hP` is the nonsingular condition underlying a nonsingular projective point `P` on `W`, then
`toAffineLift ⟨hP⟩` is definitionally equivalent to `toAffine W P`. -/
noncomputable def toAffineLift (P : W.Point) : W.toAffine.Point :=
  P.point.lift _ fun _ _ => toAffine_of_equiv

Похожие утверждения