Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.pointEquivSubtype

{R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      [inst_1 : Nontrivial R] →
        [inst_2 : WeierstrassCurve.IsElliptic W'] →
          {p : W'.Point → Prop} →
            p WeierstrassCurve.Affine.Point.zero →
              { P // p P } ≃ WithZero { xy // ∃ (h : W'.Equation xy.1 xy.2), p (WeierstrassCurve.Affine.Point.mk h) }

The equivalence between the points on an elliptic curve W in affine coordinates satisfying a predicate and the set of pairs ⟨x, y⟩ satisfying W.Equation x y with zero.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingNontrivialWeierstrassCurve.IsElliptic