Points of the projective Weierstrass model

Let W be a Weierstrass curve over a commutative ring R, let g : R →+* S be a ring homomorphism and let P be a solution of the projective Weierstrass equation of W.map g with a unit coordinate Pᵢ. Then P gives an S-point of the projective Weierstrass model projModel W, through the standard affine chart D₊(Xᵢ) at which Xₖ / Xᵢ = Pₖ / Pᵢ, lying over Spec g. When S is a local ring, every S-point of projModel W lying over Spec g arises in this way.

Over a local ring R, this file identifies the sections of the structure morphism projModel W ⟶ Spec R of the projective Weierstrass model with the projective point classes [X : Y : Z] of solutions of the projective Weierstrass equation with unimodular coordinates (WeierstrassCurve.Projective.UnimodularLift), that is, with one coordinate a unit. No ellipticity is needed. A section factors through the standard affine chart D₊(Xᵢ) containing the image of the closed point, and its homogeneous coordinates are its values on the fractions Xⱼ / Xᵢ. The zero section [0 : 1 : 0] corresponds to the class of (0, 1, 0), and a solution (x, y) of the affine equation to the section through the chart D₊(Z) at which X / Z = x and Y / Z = y.

When R = K is a field and W is elliptic, the unimodular classes are Mathlib's nonsingular projective points, so the sections are identified with the points W.toAffine.Point of W, the zero section corresponding to the point at infinity.

Main definitions

• WeierstrassCurve.projModelPoint W g hP hi: the point Spec S ⟶ projModel W with homogeneous coordinates P, through the chart D₊(Xᵢ).
• WeierstrassCurve.chartRingEval W h: evaluation at a solution (x, y) of the affine Weierstrass equation, the R-algebra map R[X, Y, Z] ⧸ (W, Z - 1) → R with X ↦ x, Y ↦ y and Z ↦ 1 on the coordinate ring of the chart D₊(Z).
• WeierstrassCurve.projModelPointsEquivUnimodular W: over a local ring, the equivalence between the sections of projModel W ⟶ Spec R and the unimodular projective point classes.
• WeierstrassCurve.projModelPointsEquiv W: over a field, for elliptic W, the equivalence between the sections of projModel W ⟶ Spec K and W.toAffine.Point.

Main results

• WeierstrassCurve.projModelPoint_projModelOver: the point with homogeneous coordinates P lies over Spec g.
• WeierstrassCurve.projModelPoint_eq_of_isUnit and WeierstrassCurve.projModelPoint_smul: the point does not depend on the chart used to define it, nor on rescaling P by a unit.
• WeierstrassCurve.projModelPoint_mem_basicOpen_iff: the point lies on the chart D₊(Xⱼ) over a prime x of S exactly when Pⱼ ∉ x.
• WeierstrassCurve.projModelPoint_eq_projModelPoint_iff: two such points are equal exactly when they lie over the same ring homomorphism and their homogeneous coordinates differ by a unit.
• WeierstrassCurve.SpecMap_projModelPoint: the point is natural in the ring S.
• WeierstrassCurve.chartι_eq_projModelPoint: the chart D₊(Xᵢ) is the point with homogeneous coordinates the universal point of the chart ring.
• WeierstrassCurve.projModelPointsEquivUnimodular_projModelZero: the zero section corresponds to the class of (0, 1, 0).
• WeierstrassCurve.projModelPointsEquivUnimodular_projModelPoint: the section with homogeneous coordinates P corresponds to the class of P.
• WeierstrassCurve.projModelPointsEquivUnimodular_symm_mk: the class of a representative P with unit coordinate Pᵢ corresponds to the section through the chart D₊(Xᵢ) at which Xₖ / Xᵢ = Pₖ / Pᵢ.
• WeierstrassCurve.projModelPointsEquivUnimodular_symm_mk_some: the class of (x, y, 1) corresponds to Spec of chartRingEval at (x, y), followed by the inclusion of the chart D₊(Z).
• WeierstrassCurve.SpecMap_chartι: a point Spec α of the chart D₊(Xᵢ) is the point with homogeneous coordinates the image under α of the universal point of the chart ring.
• WeierstrassCurve.exists_eq_projModelPoint: a point of the projective model with values in a local ring S, lying over Spec g, is the point with homogeneous coordinates P, for some solution P of the projective Weierstrass equation of W.map g with a unit coordinate.
• WeierstrassCurve.projModelPointsEquiv_projModelZero: the zero section corresponds to 0.
• WeierstrassCurve.projModelPointsEquiv_symm_some: the affine point (x, y) corresponds to Spec of chartRingEval at (x, y), followed by the inclusion of the chart D₊(Z).
• WeierstrassCurve.projModelPointsEquiv_projModelPoint: the section with homogeneous coordinates P corresponds to the point WeierstrassCurve.Projective.Point.toAffine W P.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.

Provenance

SpecMap_chartι is adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/AdditionSpecPoints.lean: it corresponds to chartPointTriple with ChartPointTriple.equation, ChartPointTriple.self_eq_one and ChartPointTriple.eq_chartHom (stated with chartAwayHomOfTriple, file AdditionChartHom.lean). There a ring homomorphism out of the chart ring A_(Xₖ), compatible with the R-algebra structures, is the chart homomorphism chartAwayHomOfTriple of its own coordinate triple; here the statement is an equality of points of the projective model, for any ring homomorphism out of ChartRing i. exists_eq_projModelPoint is not stated in the source, which factors a point with values in a field through a chart (specPoint_factors_through_chart, file WeierstrassModel.lean) and reads off that the chart homomorphism is compatible with the R-algebra structures (chartHom_compat_of_specPoint, file AdditionSpecPoints.lean); here the point has values in any local ring S, over any ring homomorphism g : R →+* S.

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/WeierstrassModel.lean, declarations specPoint_factors_through_chart, chartSolutionsEquiv, chartHomEquiv, chartPointOfHom_factors_iff, projModel_points and projModelPointsEquivEll (with _zero and _some), and file AdditionSpecPoints.lean, declaration Dictionary.eq_toAffine, as projModelPointsEquiv_projModelPoint. Here the chart arguments are carried out over a local ring R with unit coordinates in place of nonzero ones, the model is the Proj of WeierstrassCurve.Projective.CoordinateRing, the charts are read through WeierstrassCurve.Projective.awayEquivChartRing, and the field statement is deduced through Mathlib's nonsingular projective points WeierstrassCurve.Projective.Point and their equivalence with W.toAffine.Point, in place of AINTLIB's split into the chart D₊(Z) and the point at infinity. The point projModelPoint of a solution with a unit coordinate over an arbitrary ring homomorphism g : R →+* S corresponds to AINTLIB's chartHomOfTriple (file AdditionChartHom.lean) followed by the chart inclusion; here it evaluates the homogeneous coordinate ring at P in place of the source's dehomogenised chart ring.

noncomputable def WeierstrassCurve.chartRingEval {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) : W.toProjective.ChartRing 2 →ₐ[R] R

Evaluation at a solution (x, y) of the affine Weierstrass equation on the coordinate ring R[X, Y, Z] ⧸ (W, Z - 1) of the standard affine chart D₊(Z): the R-algebra map with X ↦ x, Y ↦ y and Z ↦ 1.

Equations

• W.chartRingEval h = Ideal.Quotient.liftₐ (Ideal.span (Set.range (W.toProjective.chartRelation 2))) (MvPolynomial.aeval ![x, y, 1]) ⋯

@[simp]

theorem WeierstrassCurve.chartRingEval_mk {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) (p : MvPolynomial (Fin 3) R) : (W.chartRingEval h) ((Ideal.Quotient.mk (Ideal.span (Set.range (W.toProjective.chartRelation 2)))) p) = (MvPolynomial.eval ![x, y, 1]) p

chartRingEval sends the class of a polynomial p to its value p(x, y, 1).

noncomputable def WeierstrassCurve.projModelPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W.toProjective.map g).Equation P) {i : Fin 3} (hi : IsUnit (P i)) : AlgebraicGeometry.Spec ↧S ⟶ W.projModel

The point of the projective model with homogeneous coordinates P. For a ring homomorphism g : R →+* S and a solution P of the projective Weierstrass equation of W.map g whose coordinate Pᵢ is a unit, this is the morphism Spec S ⟶ projModel W through the standard affine chart D₊(Xᵢ) at which Xₖ / Xᵢ = Pₖ / Pᵢ: Spec of Projective.awayEvalHom, followed by the inclusion of D₊(Xᵢ). It lies over Spec g (projModelPoint_projModelOver).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.projModelPoint_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W.toProjective.map g).Equation P) {i : Fin 3} (hi : IsUnit (P i)) : CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP hi) W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom g)

The point projModelPoint W g hP hi of the projective model lies over the morphism Spec S ⟶ Spec R induced by g.

@[simp]

theorem WeierstrassCurve.projModelPoint_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] (g : R →+* S) {P : Fin 3 → S} (hP : (W.toProjective.map g).Equation P) {i : Fin 3} (hi : IsUnit (P i)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP hi) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g)) h

The point projModelPoint W g hP hi of the projective model lies over the morphism Spec S ⟶ Spec R induced by g.

theorem WeierstrassCurve.projModelPoint_eq_of_isUnit {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i j : Fin 3} (hi : IsUnit (P i)) (hj : IsUnit (P j)) : W.projModelPoint g hP hi = W.projModelPoint g hP hj

The point projModelPoint W g hP hi does not depend on the unit coordinate Pᵢ through whose chart it is defined.

theorem WeierstrassCurve.projModelPoint_smul {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} (u : Sˣ) (hi : IsUnit (P i)) : W.projModelPoint g ⋯ ⋯ = W.projModelPoint g hP hi

Rescaling the homogeneous coordinates by a unit u does not change the point projModelPoint W g hP hi.

@[simp]

theorem WeierstrassCurve.SpecMap_projModelPoint {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} {T : Type u} [CommRing T] (ψ : S →+* T) (hi : IsUnit (P i)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ψ)) (W.projModelPoint g hP hi) = W.projModelPoint (ψ.comp g) ⋯ ⋯

The point projModelPoint W g hP hi is natural in the ring S: composing it with Spec ψ for a ring homomorphism ψ : S →+* T gives the point with homogeneous coordinates ψ ∘ P, along ψ.comp g.

@[simp]

theorem WeierstrassCurve.SpecMap_projModelPoint_assoc {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} {T : Type u} [CommRing T] (ψ : S →+* T) (hi : IsUnit (P i)) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ψ)) (CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP hi) h) = CategoryTheory.CategoryStruct.comp (W.projModelPoint (ψ.comp g) ⋯ ⋯) h

The point projModelPoint W g hP hi is natural in the ring S: composing it with Spec ψ for a ring homomorphism ψ : S →+* T gives the point with homogeneous coordinates ψ ∘ P, along ψ.comp g.

theorem WeierstrassCurve.projModelPoint_mem_basicOpen_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} (hi : IsUnit (P i)) (x : ↥(AlgebraicGeometry.Spec ↧S)) (j : Fin 3) : (W.projModelPoint g hP hi) x ∈ AlgebraicGeometry.Proj.basicOpen W.toProjective.grading (W.toProjective.coord j) ↔ P j ∉ x.asIdeal

The point projModelPoint W g hP hi with homogeneous coordinates P sends a point x of Spec S into the standard chart D₊(Xⱼ) exactly when the coordinate Pⱼ does not lie in the prime ideal x.

theorem WeierstrassCurve.projModelPoint_eq_projModelPoint_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} {g' : R →+* S} {Q : Fin 3 → S} {hQ : (W.toProjective.map g').Equation Q} {j : Fin 3} {hi : IsUnit (P i)} {hj : IsUnit (Q j)} : W.projModelPoint g hP hi = W.projModelPoint g' hQ hj ↔ g = g' ∧ ∃ (u : Sˣ), P = u • Q

Two points of the projective model, with homogeneous coordinates P along g and Q along g', are equal exactly when g = g' and P is a unit multiple of Q.

theorem WeierstrassCurve.chartι_eq_projModelPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) (i : Fin 3) : W.chartι i = W.projModelPoint (algebraMap R (W.toProjective.ChartRing i)) ⋯ ⋯

The standard affine chart D₊(Xᵢ) of the projective model is the point with homogeneous coordinates the universal point chartPoint i of the chart ring R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1).

theorem WeierstrassCurve.SpecMap_chartι {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : CommRingCat} {i : Fin 3} (α : ↧(W.toProjective.ChartRing i) ⟶ A) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map α) (W.chartι i) = W.projModelPoint ((CommRingCat.Hom.hom α).comp (algebraMap R ↑↧(W.toProjective.ChartRing i))) ⋯ ⋯

A point Spec α of the standard affine chart D₊(Xᵢ) of the projective model is the point with homogeneous coordinates the image under α of the universal point chartPoint i of the chart ring, along the composite R → ChartRing i → A. The case α = 𝟙 gives chartι_eq_projModelPoint.

theorem WeierstrassCurve.exists_eq_projModelPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] [IsLocalRing S] {g : R →+* S} {x : AlgebraicGeometry.Spec ↧S ⟶ W.projModel} (hx : CategoryTheory.CategoryStruct.comp x W.projModelOver = AlgebraicGeometry.Spec.map (CommRingCat.ofHom g)) : ∃ (P : Fin 3 → S) (hP : (W.toProjective.map g).Equation P) (i : Fin 3) (hi : IsUnit (P i)), x = W.projModelPoint g hP hi

A point of the projective Weierstrass model with values in a local ring is given by homogeneous coordinates: for a local ring S, a ring homomorphism g : R →+* S and x : Spec S ⟶ projModel W over Spec g, x is the point with homogeneous coordinates P for some solution P of the projective Weierstrass equation of W.map g with a unit coordinate. Such a P is unique up to a unit (projModelPoint_eq_projModelPoint_iff). For a ring S that is not local, a point through the chart D₊(Xᵢ) is described by SpecMap_chartι.

noncomputable def WeierstrassCurve.projModelPointsEquivUnimodular {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsLocalRing R] : { g : AlgebraicGeometry.Spec ↧R ⟶ W.projModel // CategoryTheory.CategoryStruct.comp g W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R) } ≃ { P : Projective.PointClass R // W.toProjective.UnimodularLift P }

Over a local ring R, the sections of the structure morphism projModel W ⟶ Spec R of the projective Weierstrass model correspond to the projective point classes [X : Y : Z] of solutions of the projective Weierstrass equation with unimodular coordinates, that is, with one coordinate a unit. The class of a representative P with unit coordinate Pᵢ corresponds to the section through the chart D₊(Xᵢ) at which Xₖ / Xᵢ = Pₖ / Pᵢ (projModelPointsEquivUnimodular_symm_mk). The zero section [0 : 1 : 0] corresponds to the class of (0, 1, 0) (projModelPointsEquivUnimodular_projModelZero), and the section through the chart D₊(Z) at which X / Z = x and Y / Z = y to the class of (x, y, 1) (projModelPointsEquivUnimodular_symm_mk_some). No ellipticity is assumed.

Equations

• W.projModelPointsEquivUnimodular = (Equiv.ofBijective (WeierstrassCurve.sectionOfClass✝ W) ⋯).symm

@[simp]

theorem WeierstrassCurve.projModelPointsEquivUnimodular_projModelZero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsLocalRing R] : W.projModelPointsEquivUnimodular ⟨W.projModelZero, ⋯⟩ = ⟨⟦![0, 1, 0]⟧, ⋯⟩

The zero section [0 : 1 : 0] of the projective model corresponds to the class of (0, 1, 0).

@[simp]

theorem WeierstrassCurve.projModelPointsEquivUnimodular_projModelPoint {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsLocalRing R] {P : Fin 3 → R} (hP : (W.toProjective.map (RingHom.id R)).Equation P) {i : Fin 3} (hi : IsUnit (P i)) : ↑(W.projModelPointsEquivUnimodular ⟨W.projModelPoint (RingHom.id R) hP hi, ⋯⟩) = ⟦P⟧

The section projModelPoint W (RingHom.id R) hP hi with homogeneous coordinates P, a solution of the projective Weierstrass equation with a unit coordinate Pᵢ, corresponds to the class of P.

theorem WeierstrassCurve.projModelPointsEquivUnimodular_symm_mk {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsLocalRing R] {P : Fin 3 → R} (hP : W.toProjective.UnimodularLift ⟦P⟧) {i : Fin 3} (hi : IsUnit (P i)) (α : W.toProjective.ChartRing i →ₐ[R] R) (hα : ∀ (k : Fin 3), α ((Ideal.Quotient.mk (Ideal.span (Set.range (W.toProjective.chartRelation i)))) (MvPolynomial.X k)) = P k * ↑hi.unit⁻¹) : ↑(W.projModelPointsEquivUnimodular.symm ⟨⟦P⟧, hP⟩) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((↑α).comp ↑(W.toProjective.awayEquivChartRing i)))) (AlgebraicGeometry.Proj.awayι W.toProjective.grading (W.toProjective.coord i) ⋯ ⋯)

The class of a unimodular representative P with unit coordinate Pᵢ corresponds to the section through the chart D₊(Xᵢ) at which Xₖ / Xᵢ = Pₖ / Pᵢ: Spec of any R-algebra map α : R[X₀, X₁, X₂] ⧸ (W, Xᵢ - 1) → R with α(Xₖ) = Pₖ / Pᵢ, read on A_(Xᵢ) through awayEquivChartRing, followed by the inclusion of D₊(Xᵢ).

theorem WeierstrassCurve.projModelPointsEquivUnimodular_symm_mk_some {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsLocalRing R] {x y : R} (h : W.toAffine.Equation x y) : ↑(W.projModelPointsEquivUnimodular.symm ⟨⟦![x, y, 1]⟧, ⋯⟩) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((↑(W.chartRingEval h)).comp ↑(W.toProjective.awayEquivChartRing 2)))) (AlgebraicGeometry.Proj.awayι W.toProjective.grading (W.toProjective.coord 2) ⋯ ⋯)

The class of (x, y, 1) corresponds to the section through the chart D₊(Z) at which X / Z = x and Y / Z = y: Spec of the evaluation chartRingEval at (x, y) on R[X, Y, Z] ⧸ (W, Z - 1), read on A_(Z) through awayEquivChartRing, followed by the inclusion of D₊(Z).

noncomputable def WeierstrassCurve.projModelPointsEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : { g : AlgebraicGeometry.Spec ↧K ⟶ W.projModel // CategoryTheory.CategoryStruct.comp g W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧K) } ≃ W.toAffine.Point

Over a field K, the sections of the structure morphism projModel W ⟶ Spec K of the projective Weierstrass model of an elliptic Weierstrass curve W correspond to the points W.toAffine.Point: the zero section [0 : 1 : 0] corresponds to 0 (projModelPointsEquiv_projModelZero), and the section through the chart D₊(Z) at which X / Z = x and Y / Z = y corresponds to the affine point (x, y) (projModelPointsEquiv_symm_some).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.projModelPointsEquiv_projModelZero {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : W.projModelPointsEquiv ⟨W.projModelZero, ⋯⟩ = 0

The zero section [0 : 1 : 0] of the projective model corresponds to the point at infinity.

theorem WeierstrassCurve.projModelPointsEquiv_symm_some {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {x y : K} (h : W.toAffine.Nonsingular x y) : ↑(W.projModelPointsEquiv.symm (Affine.Point.some x y h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((↑(W.chartRingEval ⋯)).comp ↑(W.toProjective.awayEquivChartRing 2)))) (AlgebraicGeometry.Proj.awayι W.toProjective.grading (W.toProjective.coord 2) ⋯ ⋯)

The affine point (x, y) corresponds to the section through the chart D₊(Z) at which X / Z = x and Y / Z = y: Spec of the evaluation chartRingEval at (x, y) on K[X, Y, Z] ⧸ (W, Z - 1), read on A_(Z) through awayEquivChartRing, followed by the inclusion of D₊(Z).

@[simp]

theorem WeierstrassCurve.projModelPointsEquiv_projModelPoint {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {P : Fin 3 → K} (hP : (W.toProjective.map (RingHom.id K)).Equation P) {i : Fin 3} (hi : IsUnit (P i)) : W.projModelPointsEquiv ⟨W.projModelPoint (RingHom.id K) hP hi, ⋯⟩ = Projective.Point.toAffine W.toProjective P

For a solution P of the projective Weierstrass equation with a unit coordinate Pᵢ, the section projModelPoint W (RingHom.id K) hP hi with homogeneous coordinates P corresponds to the point WeierstrassCurve.Projective.Point.toAffine W P of W: the point at infinity if P₂ = 0, and the affine point (P₀ / P₂, P₁ / P₂) otherwise. Unlike projModelPointsEquiv_symm_some, which describes the section of an affine point through the chart D₊(Z), it applies to a section read through any chart D₊(Xᵢ).