Nonsingular points and the group law in affine coordinates

Let W be a Weierstrass curve over a field F given by a Weierstrass equation W(X, Y) = 0 in affine coordinates. The type of nonsingular points in affine coordinates is an inductive, consisting of the unique point at infinity 𝓞 and nonsingular affine points (x, y). It can be endowed with a group law, with 𝓞 as the identity nonsingular point, which is uniquely determined by the formulae in Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean.

With this description, there is an addition-preserving injection from the nonsingular points to the ideal class group of the affine coordinate ring F[W] := F[X, Y] / ⟨W(X, Y)⟩. This is given by mapping 𝓞 to the trivial ideal class and a nonsingular affine point (x, y) to the ideal class of the invertible ideal ⟨X - x, Y - y⟩. Proving that this is well-defined and preserves addition reduces to equalities of ideals checked in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul and in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal via explicit ideal computations. Now F[W] is a free rank two F[X]-algebra with basis {1, Y}, so every element of F[W] is of the form p + qY for some p, q in F[X], and there is an algebra norm N : F[W] → F[X]. Injectivity can then be shown by computing the degree of such a norm N(p + qY) in two different ways, which is done in WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis and in the auxiliary lemmas in the proof of WeierstrassCurve.Affine.Point.instAddCommGroup.

This file defines the group law on nonsingular points in affine coordinates.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing: the affine coordinate ring F[W].
• WeierstrassCurve.Affine.CoordinateRing.basis: the power basis of F[W] over F[X].
• WeierstrassCurve.Affine.Point: a nonsingular point in affine coordinates.
• WeierstrassCurve.Affine.Point.neg: the negation of a nonsingular point in affine coordinates.
• WeierstrassCurve.Affine.Point.add: the addition of a nonsingular point in affine coordinates.

Main statements

• WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing: the affine coordinate ring of a Weierstrass curve is an integral domain.
• WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis: the degree of the norm of an element in the affine coordinate ring in terms of its power basis.
• WeierstrassCurve.Affine.Point.instAddCommGroup: the type of nonsingular points in affine coordinates forms an abelian group under addition.

References

• J Silverman, The Arithmetic of Elliptic Curves
• https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.6/LIPIcs.ITP.2023.6.pdf

Tags

elliptic curve, affine, point, group law, class group

The affine coordinate ring

@[reducible, inline]

abbrev WeierstrassCurve.Affine.CoordinateRing {R : Type r} [CommRing R] (W' : Affine R) : Type r

The affine coordinate ring R[W] := R[X, Y] / ⟨W(X, Y)⟩ of a Weierstrass curve W.

Equations

• W'.CoordinateRing = AdjoinRoot W'.polynomial

@[reducible, inline]

abbrev WeierstrassCurve.Affine.FunctionField {R : Type r} [CommRing R] (W' : Affine R) : Type r

The function field R(W) := Frac(R[W]) of a Weierstrass curve W.

Equations

• W'.FunctionField = FractionRing W'.CoordinateRing

@[instance_reducible]

noncomputable instance WeierstrassCurve.Affine.CoordinateRing.instAlgebra {R : Type r} [CommRing R] {W' : Affine R} : Algebra R W'.CoordinateRing

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebra = inferInstance

@[instance_reducible]

noncomputable instance WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial {R : Type r} [CommRing R] {W' : Affine R} : Algebra (Polynomial R) W'.CoordinateRing

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial = inferInstance

instance WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial {R : Type r} [CommRing R] {W' : Affine R} : IsScalarTower R (Polynomial R) W'.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instSubsingleton {R : Type r} [CommRing R] {W' : Affine R} [Subsingleton R] : Subsingleton W'.CoordinateRing

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.CoordinateRing.mk {R : Type r} [CommRing R] (W' : Affine R) : Polynomial (Polynomial R) →+* W'.CoordinateRing

The natural ring homomorphism mapping R[X][Y] to R[W].

Equations

• WeierstrassCurve.Affine.CoordinateRing.mk W' = AdjoinRoot.mk W'.polynomial

noncomputable def WeierstrassCurve.Affine.CoordinateRing.basis {R : Type r} [CommRing R] (W' : Affine R) : Module.Basis (Fin 2) (Polynomial R) W'.CoordinateRing

The power basis {1, Y} for R[W] over R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.basis W' = ⋯.by_cases (fun (x : Subsingleton R) => default) fun (x : Nontrivial R) => (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)

theorem WeierstrassCurve.Affine.CoordinateRing.basis_apply {R : Type r} [CommRing R] {W' : Affine R} (n : Fin 2) : (CoordinateRing.basis W') n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.basis_zero {R : Type r} [CommRing R] {W' : Affine R} : (CoordinateRing.basis W') 0 = 1

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.basis_one {R : Type r} [CommRing R] {W' : Affine R} : (CoordinateRing.basis W') 1 = (mk W') Polynomial.X

theorem WeierstrassCurve.Affine.CoordinateRing.coe_basis {R : Type r} [CommRing R] {W' : Affine R} : ⇑(CoordinateRing.basis W') = ![1, (mk W') Polynomial.X]

instance WeierstrassCurve.Affine.CoordinateRing.instFreePolynomial {R : Type r} [CommRing R] {W' : Affine R} : Module.Free (Polynomial R) W'.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instFree {R : Type r} [CommRing R] {W' : Affine R} : Module.Free R W'.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instNontrivial {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] : Nontrivial W'.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instFaithfulSMulPolynomial {R : Type r} [CommRing R] {W' : Affine R} : FaithfulSMul (Polynomial R) W'.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instFaithfulSMul {R : Type r} [CommRing R] {W' : Affine R} : FaithfulSMul R W'.CoordinateRing

theorem WeierstrassCurve.Affine.CoordinateRing.smul {R : Type r} [CommRing R] {W' : Affine R} (x : Polynomial R) (y : W'.CoordinateRing) : x • y = (mk W') (Polynomial.C x) * y

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_eq_zero {R : Type r} [CommRing R] {W' : Affine R} {p q : Polynomial R} (hpq : p • 1 + q • (mk W') Polynomial.X = 0) : p = 0 ∧ q = 0

theorem WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq {R : Type r} [CommRing R] {W' : Affine R} (x : W'.CoordinateRing) : ∃ (p : Polynomial R) (q : Polynomial R), p • 1 + q • (mk W') Polynomial.X = x

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C {R : Type r} [CommRing R] {W' : Affine R} (y p q : Polynomial R) : (p • 1 + q • (mk W') Polynomial.X) * (mk W') (Polynomial.C y) = (p * y) • 1 + (q * y) • (mk W') Polynomial.X

theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y {R : Type r} [CommRing R] {W' : Affine R} (p q : Polynomial R) : (p • 1 + q • (mk W') Polynomial.X) * (mk W') Polynomial.X = (q * (Polynomial.X ^ 3 + Polynomial.C W'.a₂ * Polynomial.X ^ 2 + Polynomial.C W'.a₄ * Polynomial.X + Polynomial.C W'.a₆)) • 1 + (p - q * (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃)) • (mk W') Polynomial.X

noncomputable def WeierstrassCurve.Affine.CoordinateRing.map {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W' : Affine R) (f : R →+* S) : W'.CoordinateRing →+* (W'.map f).CoordinateRing

The ring homomorphism R[W] →+* S[W.map f] induced by a ring homomorphism f : R →+* S.

Equations

• WeierstrassCurve.Affine.CoordinateRing.map W' f = AdjoinRoot.lift ((AdjoinRoot.of (W'.map f).polynomial).comp (Polynomial.mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial) ⋯

theorem WeierstrassCurve.Affine.CoordinateRing.map_mk {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x : Polynomial (Polynomial R)) : (map W' f) ((mk W') x) = (mk (W'.map f)) (Polynomial.map (Polynomial.mapRingHom f) x)

theorem WeierstrassCurve.Affine.CoordinateRing.map_smul {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x : Polynomial R) (y : W'.CoordinateRing) : (map W' f) (x • y) = Polynomial.map f x • (map W' f) y

theorem WeierstrassCurve.Affine.CoordinateRing.map_injective {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} {f : R →+* S} (hf : Function.Injective ⇑f) : Function.Injective ⇑(map W' f)

instance WeierstrassCurve.Affine.CoordinateRing.instIsDomain {R : Type r} [CommRing R] {W' : Affine R} [IsDomain R] : IsDomain W'.CoordinateRing

Ideals in the affine coordinate ring

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XClass {R : Type r} [CommRing R] (W' : Affine R) (x : R) : W'.CoordinateRing

The class of the element X - x in R[W] for some x in R.

Equations

• WeierstrassCurve.Affine.CoordinateRing.XClass W' x = (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C (Polynomial.X - Polynomial.C x))

theorem WeierstrassCurve.Affine.CoordinateRing.XClass_ne_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] (x : R) : XClass W' x ≠ 0

noncomputable def WeierstrassCurve.Affine.CoordinateRing.YClass {R : Type r} [CommRing R] (W' : Affine R) (y : Polynomial R) : W'.CoordinateRing

The class of the element Y - y(X) in R[W] for some y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.YClass W' y = (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.X - Polynomial.C y)

theorem WeierstrassCurve.Affine.CoordinateRing.YClass_ne_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] (y : Polynomial R) : YClass W' y ≠ 0

theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial {R : Type r} [CommRing R] {W' : Affine R} (x y ℓ : R) : (mk W') (Polynomial.C (W'.addPolynomial x y ℓ)) = (mk W') ((Polynomial.X - Polynomial.C (linePolynomial x y ℓ)) * (W'.negPolynomial - Polynomial.C (linePolynomial x y ℓ)))

theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : (mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XIdeal {R : Type r} [CommRing R] (W' : Affine R) (x : R) : Ideal W'.CoordinateRing

The ideal ⟨X - x⟩ of R[W] for some x in R.

Equations

• WeierstrassCurve.Affine.CoordinateRing.XIdeal W' x = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W' x}

noncomputable def WeierstrassCurve.Affine.CoordinateRing.YIdeal {R : Type r} [CommRing R] (W' : Affine R) (y : Polynomial R) : Ideal W'.CoordinateRing

The ideal ⟨Y - y(X)⟩ of R[W] for some y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.YIdeal W' y = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.YClass W' y}

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XYIdeal {R : Type r} [CommRing R] (W' : Affine R) (x : R) (y : Polynomial R) : Ideal W'.CoordinateRing

The ideal ⟨X - x, Y - y(X)⟩ of R[W] for some x in R and y(X) in R[X].

Equations

• WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x y = Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W' x, WeierstrassCurve.Affine.CoordinateRing.YClass W' y}

noncomputable def WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv {R : Type r} [CommRing R] {W' : Affine R} {x : R} {y : Polynomial R} (h : Polynomial.eval x (Polynomial.eval y W'.polynomial) = 0) : (W'.CoordinateRing ⧸ XYIdeal W' x y) ≃ₐ[R] R

The R-algebra isomorphism from R[W] / ⟨X - x, Y - y(X)⟩ to R obtained by evaluation at some y(X) in R[X] and at some x in R provided that W(x, y(x)) = 0.

Equations

• WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv h = ((Ideal.quotientEquivAlgOfEq R ⋯).trans (DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)).trans Polynomial.quotientSpanCXSubCXSubCAlgEquiv

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq {R : Type r} [CommRing R] {W' : Affine R} (x₁ x₂ y₁ ℓ : R) : XYIdeal W' (W'.addX x₁ x₂ ℓ) (Polynomial.C (W'.addY x₁ x₂ y₁ ℓ)) = Ideal.span {(mk W') (W'.negPolynomial - Polynomial.C (linePolynomial x₁ y₁ ℓ))} ⊔ XIdeal W' (W'.addX x₁ x₂ ℓ)

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₁ {R : Type r} [CommRing R] {W' : Affine R} (x y ℓ : R) : XYIdeal W' x (Polynomial.C y) = XYIdeal W' x (linePolynomial x y ℓ)

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂ {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : XYIdeal W x₂ (Polynomial.C y₂) = XYIdeal W x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : XYIdeal W x (Polynomial.C (W.negY x y)) * XYIdeal W x (Polynomial.C y) = XIdeal W x

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (Polynomial.C y₁) * XYIdeal W x₂ (Polynomial.C y₂)) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (Polynomial.C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XYIdeal' {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : (FractionalIdeal (nonZeroDivisors W.CoordinateRing) W.FunctionField)ˣ

The non-zero fractional ideal ⟨X - x, Y - y⟩ of F(W) for some x and y in F.

Equations

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

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : ↑(XYIdeal' h) = ↑(XYIdeal W x (Polynomial.C y))

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul {F : Type u} [Field F] {W : Affine F} {x y : F} (h : W.Nonsingular x y) : (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯) * (ClassGroup.mk W.FunctionField) (XYIdeal' h) = 1

theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : (ClassGroup.mk W.FunctionField) (XYIdeal' h₁) * (ClassGroup.mk W.FunctionField) (XYIdeal' h₂) = (ClassGroup.mk W.FunctionField) (XYIdeal' ⋯)

Norms on the affine coordinate ring

theorem WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis {R : Type r} [CommRing R] {W' : Affine R} (p q : Polynomial R) : (Algebra.norm (Polynomial R)) (p • 1 + q • (mk W') Polynomial.X) = p ^ 2 - p * q * (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W'.a₂ * Polynomial.X ^ 2 + Polynomial.C W'.a₄ * Polynomial.X + Polynomial.C W'.a₆)

theorem WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis {R : Type r} [CommRing R] {W' : Affine R} (p q : Polynomial R) : (AdjoinRoot.of W'.polynomial) ((Algebra.norm (Polynomial R)) (p • 1 + q • (mk W') Polynomial.X)) = (mk W') ((Polynomial.C p + Polynomial.C q * Polynomial.X) * (Polynomial.C p + Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃))))

theorem WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis {R : Type r} [CommRing R] {W' : Affine R} [IsDomain R] (p q : Polynomial R) : ((Algebra.norm (Polynomial R)) (p • 1 + q • (mk W') Polynomial.X)).degree = max (2 • p.degree) (2 • q.degree + 3)

theorem WeierstrassCurve.Affine.CoordinateRing.degree_norm_ne_one {R : Type r} [CommRing R] {W' : Affine R} [IsDomain R] (x : W'.CoordinateRing) : ((Algebra.norm (Polynomial R)) x).degree ≠ 1

theorem WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one {R : Type r} [CommRing R] {W' : Affine R} [IsDomain R] (x : W'.CoordinateRing) : ((Algebra.norm (Polynomial R)) x).natDegree ≠ 1

Nonsingular points in affine coordinates

inductive WeierstrassCurve.Affine.Point {R : Type r} [CommRing R] (W' : Affine R) : Type r

A nonsingular point on a Weierstrass curve W in affine coordinates. This is either the unique point at infinity WeierstrassCurve.Affine.Point.zero or a nonsingular affine point WeierstrassCurve.Affine.Point.some (x, y) satisfying the Weierstrass equation of W.

• zero {R : Type r} [CommRing R] {W' : Affine R} : W'.Point
• some {R : Type r} [CommRing R] {W' : Affine R} (x y : R) (h : W'.Nonsingular x y) : W'.Point

@[instance_reducible]

instance WeierstrassCurve.Affine.instDecidableEqPoint {R✝ : Type u_1} {inst✝ : CommRing R✝} {W'✝ : Affine R✝} [DecidableEq R✝] : DecidableEq W'✝.Point

Equations

• WeierstrassCurve.Affine.instDecidableEqPoint = WeierstrassCurve.Affine.instDecidableEqPoint.decEq

def WeierstrassCurve.Affine.instDecidableEqPoint.decEq {R✝ : Type u_1} {inst✝ : CommRing R✝} {W'✝ : Affine R✝} [DecidableEq R✝] (x✝ x✝¹ : W'✝.Point) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• WeierstrassCurve.Affine.instDecidableEqPoint.decEq WeierstrassCurve.Affine.Point.zero WeierstrassCurve.Affine.Point.zero = isTrue ⋯
• WeierstrassCurve.Affine.instDecidableEqPoint.decEq WeierstrassCurve.Affine.Point.zero (WeierstrassCurve.Affine.Point.some x_2 y h) = isFalse ⋯
• WeierstrassCurve.Affine.instDecidableEqPoint.decEq (WeierstrassCurve.Affine.Point.some x_2 y h) WeierstrassCurve.Affine.Point.zero = isFalse ⋯

def WeierstrassCurve.Affine.nonsingularPointEquivSubtype {R : Type r} [CommRing R] {W' : Affine R} {p : W'.Point → Prop} (p0 : p Point.zero) : { P : W'.Point // p P } ≃ WithZero { xy : R × R // ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h) }

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

Equations

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

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_zero {R : Type r} [CommRing R] {W' : Affine R} {p : W'.Point → Prop} (p0 : p Point.zero) : (nonsingularPointEquivSubtype p0) ⟨Point.zero, p0⟩ = none

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} {h : W'.Nonsingular x y} {p : W'.Point → Prop} (p0 : p Point.zero) (ph : p (Point.some x y h)) : (nonsingularPointEquivSubtype p0) ⟨Point.some x y h, ph⟩ = some ⟨(x, y), ⋯⟩

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_none {R : Type r} [CommRing R] {W' : Affine R} {p : W'.Point → Prop} (p0 : p Point.zero) : (nonsingularPointEquivSubtype p0).symm none = ⟨Point.zero, p0⟩

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} {h : W'.Nonsingular x y} {p : W'.Point → Prop} (p0 : p Point.zero) (ph : p (Point.some x y h)) : (nonsingularPointEquivSubtype p0).symm (some ⟨(x, y), ⋯⟩) = ⟨Point.some x y h, ph⟩

def WeierstrassCurve.Affine.nonsingularPointEquiv {R : Type r} [CommRing R] (W' : Affine R) : W'.Point ≃ WithZero { xy : R × R // W'.Nonsingular xy.1 xy.2 }

The equivalence between the nonsingular points on a Weierstrass curve W in affine coordinates and the set of pairs ⟨x, y⟩ satisfying W.Nonsingular x y with zero.

Equations

• W'.nonsingularPointEquiv = (Equiv.Set.univ W'.Point).symm.trans ((WeierstrassCurve.Affine.nonsingularPointEquivSubtype trivial).trans (Equiv.subtypeEquivProp ⋯).optionCongr)

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquiv_zero {R : Type r} [CommRing R] {W' : Affine R} : W'.nonsingularPointEquiv Point.zero = none

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquiv_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : W'.nonsingularPointEquiv (Point.some x y h) = some ⟨(x, y), h⟩

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquiv_symm_none {R : Type r} [CommRing R] {W' : Affine R} : W'.nonsingularPointEquiv.symm none = Point.zero

@[simp]

theorem WeierstrassCurve.Affine.nonsingularPointEquiv_symm_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : W'.nonsingularPointEquiv.symm (some ⟨(x, y), h⟩) = Point.some x y h

def WeierstrassCurve.Affine.Point.mk {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y) : W'.Point

A point on an elliptic curve W over R.

Equations

• WeierstrassCurve.Affine.Point.mk h = WeierstrassCurve.Affine.Point.some x y ⋯

def WeierstrassCurve.Affine.pointEquivSubtype {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {p : W'.Point → Prop} (p0 : p Point.zero) : { P : W'.Point // p P } ≃ WithZero { xy : R × R // ∃ (h : W'.Equation xy.1 xy.2), p (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.

Equations

• WeierstrassCurve.Affine.pointEquivSubtype p0 = (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0).trans (Equiv.subtypeEquivProp ⋯).optionCongr

@[simp]

theorem WeierstrassCurve.Affine.pointEquivSubtype_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {p : W'.Point → Prop} (p0 : p Point.zero) : (pointEquivSubtype p0) ⟨Point.zero, p0⟩ = none

@[simp]

theorem WeierstrassCurve.Affine.pointEquivSubtype_some {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop} (p0 : p Point.zero) (ph : p (Point.mk h)) : (pointEquivSubtype p0) ⟨Point.mk h, ph⟩ = some ⟨(x, y), ⋯⟩

@[simp]

theorem WeierstrassCurve.Affine.pointEquivSubtype_symm_none {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {p : W'.Point → Prop} (p0 : p Point.zero) : (pointEquivSubtype p0).symm none = ⟨Point.zero, p0⟩

@[simp]

theorem WeierstrassCurve.Affine.pointEquivSubtype_symm_some {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop} (p0 : p Point.zero) (ph : p (Point.mk h)) : (pointEquivSubtype p0).symm (some ⟨(x, y), ⋯⟩) = ⟨Point.mk h, ph⟩

def WeierstrassCurve.Affine.pointEquiv {R : Type r} [CommRing R] (W' : Affine R) [Nontrivial R] [WeierstrassCurve.IsElliptic W'] : W'.Point ≃ WithZero { xy : R × R // W'.Equation xy.1 xy.2 }

The equivalence between the rational points on an elliptic curve E and the set of pairs ⟨x, y⟩ satisfying E.Equation x y with zero.

Equations

• W'.pointEquiv = (Equiv.Set.univ W'.Point).symm.trans ((WeierstrassCurve.Affine.pointEquivSubtype trivial).trans (Equiv.subtypeEquivProp ⋯).optionCongr)

@[simp]

theorem WeierstrassCurve.Affine.pointEquiv_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] : W'.pointEquiv Point.zero = none

@[simp]

theorem WeierstrassCurve.Affine.pointEquiv_some {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y) : W'.pointEquiv (Point.mk h) = some ⟨(x, y), h⟩

@[simp]

theorem WeierstrassCurve.Affine.pointEquiv_symm_none {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] : W'.pointEquiv.symm none = Point.zero

@[simp]

theorem WeierstrassCurve.Affine.pointEquiv_symm_some {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] [WeierstrassCurve.IsElliptic W'] {x y : R} (h : W'.Equation x y) : W'.pointEquiv.symm (some ⟨(x, y), h⟩) = Point.mk h

Group law in affine coordinates

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instInhabited {R : Type r} [CommRing R] {W' : Affine R} : Inhabited W'.Point

Equations

• WeierstrassCurve.Affine.Point.instInhabited = { default := WeierstrassCurve.Affine.Point.zero }

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instZero {R : Type r} [CommRing R] {W' : Affine R} : Zero W'.Point

Equations

• WeierstrassCurve.Affine.Point.instZero = { zero := WeierstrassCurve.Affine.Point.zero }

theorem WeierstrassCurve.Affine.Point.zero_def {R : Type r} [CommRing R] {W' : Affine R} : 0 = zero

theorem WeierstrassCurve.Affine.Point.some_ne_zero {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : some x y h ≠ 0

def WeierstrassCurve.Affine.Point.neg {R : Type r} [CommRing R] {W' : Affine R} : W'.Point → W'.Point

The negation of a nonsingular point on a Weierstrass curve in affine coordinates.

Given a nonsingular point P in affine coordinates, use -P instead of neg P.

Equations

• WeierstrassCurve.Affine.Point.zero.neg = 0
• (WeierstrassCurve.Affine.Point.some x_1 y h).neg = WeierstrassCurve.Affine.Point.some x_1 (W'.negY x_1 y) ⋯

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instNeg {R : Type r} [CommRing R] {W' : Affine R} : Neg W'.Point

Equations

• WeierstrassCurve.Affine.Point.instNeg = { neg := WeierstrassCurve.Affine.Point.neg }

theorem WeierstrassCurve.Affine.Point.neg_def {R : Type r} [CommRing R] {W' : Affine R} (P : W'.Point) : -P = P.neg

@[simp]

theorem WeierstrassCurve.Affine.Point.neg_zero {R : Type r} [CommRing R] {W' : Affine R} : -0 = 0

@[simp]

theorem WeierstrassCurve.Affine.Point.neg_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : -some x y h = some x (W'.negY x y) ⋯

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instInvolutiveNeg {R : Type r} [CommRing R] {W' : Affine R} : InvolutiveNeg W'.Point

Equations

• WeierstrassCurve.Affine.Point.instInvolutiveNeg = { toNeg := WeierstrassCurve.Affine.Point.instNeg, neg_neg := ⋯ }

theorem WeierstrassCurve.Affine.Point.X_eq_iff {F : Type u} [Field F] {W : Affine F} {x₁ y₁ x₂ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} : x₁ = x₂ ↔ some x₁ y₁ h₁ = some x₂ y₂ h₂ ∨ some x₁ y₁ h₁ = -some x₂ y₂ h₂

def WeierstrassCurve.Affine.Point.add {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : W.Point → W.Point → W.Point

The addition of two nonsingular points on a Weierstrass curve in affine coordinates.

Given two nonsingular points P and Q in affine coordinates, use P + Q instead of add P Q.

Equations

• One or more equations did not get rendered due to their size.
• WeierstrassCurve.Affine.Point.zero.add x✝ = x✝
• x✝.add WeierstrassCurve.Affine.Point.zero = x✝

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instAdd {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : Add W.Point

Equations

• WeierstrassCurve.Affine.Point.instAdd = { add := WeierstrassCurve.Affine.Point.add }

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instAddZeroClass {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : AddZeroClass W.Point

Equations

• WeierstrassCurve.Affine.Point.instAddZeroClass = { toZero := WeierstrassCurve.Affine.Point.instZero, toAdd := WeierstrassCurve.Affine.Point.instAdd, zero_add := ⋯, add_zero := ⋯ }

theorem WeierstrassCurve.Affine.Point.add_def {F : Type u} [Field F] {W : Affine F} [DecidableEq F] (P Q : W.Point) : P + Q = P.add Q

theorem WeierstrassCurve.Affine.Point.add_some {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} : some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

@[simp]

theorem WeierstrassCurve.Affine.Point.add_of_Y_eq {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) : some x₁ y₁ h₁ + some x₂ y₂ h₂ = 0

theorem WeierstrassCurve.Affine.Point.add_self_of_Y_eq {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ = W.negY x₁ y₁) : some x₁ y₁ h₁ + some x₁ y₁ h₁ = 0

theorem WeierstrassCurve.Affine.Point.add_of_Y_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ ≠ W.negY x₂ y₂) : some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

theorem WeierstrassCurve.Affine.Point.add_of_Y_ne' {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ ≠ W.negY x₂ y₂) : some x₁ y₁ h₁ + some x₂ y₂ h₂ = -some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁) : some x₁ y₁ h₁ + some x₁ y₁ h₁ = some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.addY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁)) ⋯

theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne' {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ ≠ W.negY x₁ y₁) : some x₁ y₁ h₁ + some x₁ y₁ h₁ = -some (W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) (W.negAddY x₁ x₁ y₁ (W.slope x₁ x₁ y₁ y₁)) ⋯

@[simp]

theorem WeierstrassCurve.Affine.Point.add_of_X_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ ≠ x₂) : some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

theorem WeierstrassCurve.Affine.Point.add_of_X_ne' {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ ≠ x₂) : some x₁ y₁ h₁ + some x₂ y₂ h₂ = -some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

theorem WeierstrassCurve.Affine.Point.isRoot_twoTorsionPolynomial_of_add_self {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x y : F} (h : W.Nonsingular x y) (hP : some x y h + some x y h = 0) : (twoTorsionPolynomial W).toPoly.IsRoot x

A nonzero affine 2-torsion point some x y h of W (that is, P + P = 0) has X-coordinate a root of W.twoTorsionPolynomial.

theorem WeierstrassCurve.Affine.Point.isRoot_twoTorsionPolynomial_iff {F : Type u} [Field F] {W : Affine F} [DecidableEq F] (h2 : NeZero 2) (hΔ : Δ W ≠ 0) (x : F) : (twoTorsionPolynomial W).toPoly.IsRoot x ↔ ∃ (y : F) (h : W.Nonsingular x y), some x y h + some x y h = 0

x is a root of the 2-torsion polynomial of a Weierstrass curve of characteristic different from 2 with nonzero discriminant if and only if it is the X-coordinate of a nonzero affine 2-torsion point.

noncomputable def WeierstrassCurve.Affine.Point.toClass {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : W.Point →+ Additive (ClassGroup W.CoordinateRing)

The group homomorphism mapping a nonsingular affine point (x, y) of a Weierstrass curve W to the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].

Equations

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

@[simp]

theorem WeierstrassCurve.Affine.Point.toClass_apply {F : Type u} [Field F] {W : Affine F} [DecidableEq F] (P : W.Point) : toClass P = match P with | zero => 0 | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

theorem WeierstrassCurve.Affine.Point.toClass_zero {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : toClass 0 = 0

theorem WeierstrassCurve.Affine.Point.toClass_some {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x y : F} (h : W.Nonsingular x y) : toClass (some x y h) = (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

theorem WeierstrassCurve.Affine.Point.toClass_eq_zero {F : Type u} [Field F] {W : Affine F} [DecidableEq F] (P : W.Point) : toClass P = 0 ↔ P = 0

theorem WeierstrassCurve.Affine.Point.toClass_injective {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : Function.Injective ⇑toClass

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instAddCommSemigroup {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : AddCommSemigroup W.Point

Equations

• WeierstrassCurve.Affine.Point.instAddCommSemigroup = { toAdd := WeierstrassCurve.Affine.Point.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[instance_reducible]

instance WeierstrassCurve.Affine.Point.instAddCommGroup {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : AddCommGroup W.Point

Equations

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

Maps and base changes

noncomputable def WeierstrassCurve.Affine.Point.map {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Affine R} [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) : (W'.baseChange F).Point →+ (W'.baseChange K).Point

The group homomorphism on nonsingular points induced by an algebra homomorphism f : F →ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Equations

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

theorem WeierstrassCurve.Affine.Point.map_zero {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Affine R} [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) : (map f) 0 = 0

theorem WeierstrassCurve.Affine.Point.map_some {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Affine R} [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) {x y : F} (h : (W'.baseChange F).Nonsingular x y) : (map f) (some x y h) = some (f x) (f y) ⋯

theorem WeierstrassCurve.Affine.Point.map_id {R : Type r} {F : Type u} [CommRing R] [Field F] {W' : Affine R} [DecidableEq F] [Algebra R F] (P : (W'.baseChange F).Point) : (map (Algebra.ofId F F)) P = P

theorem WeierstrassCurve.Affine.Point.map_map {R : Type r} {S : Type s} {F : Type u} {K : Type v} {L : Type w} [CommRing R] [CommRing S] [Field F] [Field K] [Field L] {W' : Affine R} [DecidableEq F] [DecidableEq K] [DecidableEq L] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [Algebra R L] [Algebra S L] [IsScalarTower R S L] (f : F →ₐ[S] K) (g : K →ₐ[S] L) (P : (W'.baseChange F).Point) : (map g) ((map f) P) = (map (g.comp f)) P

theorem WeierstrassCurve.Affine.Point.map_injective {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Affine R} [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) : Function.Injective ⇑(map f)

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.Point.baseChange {R : Type r} (F : Type u) (K : Type v) [CommRing R] [Field F] [Field K] {W' : Affine R} [DecidableEq F] [DecidableEq K] [Algebra R F] [Algebra R K] [Algebra F K] [IsScalarTower R F K] : (W'.baseChange F).Point →+ (W'.baseChange K).Point

The group homomorphism on nonsingular points induced by the base change from F to K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

Equations

• WeierstrassCurve.Affine.Point.baseChange F K = WeierstrassCurve.Affine.Point.map (Algebra.ofId F K)

theorem WeierstrassCurve.Affine.Point.map_baseChange {R : Type r} {F : Type u} {K : Type v} {L : Type w} [CommRing R] [Field F] [Field K] [Field L] {W' : Affine R} [DecidableEq F] [DecidableEq K] [DecidableEq L] [Algebra R F] [Algebra R K] [Algebra R L] [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalarTower R F L] (f : K →ₐ[F] L) (P : (W'.baseChange F).Point) : (map f) ((baseChange F K) P) = (baseChange F L) P

The x-coordinate map to ℙ¹

We define the map from points on an affine Weierstrass curve over R to the projective line by producing a coordinate vector in Fin 2 → R that represents the projective point.

noncomputable def WeierstrassCurve.Affine.Point.xRep {R : Type r} [CommRing R] {W' : 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.

Equations

• WeierstrassCurve.Affine.Point.zero.xRep = ![1, 0]
• (WeierstrassCurve.Affine.Point.some x_1 y h).xRep = ![x_1, 1]

@[simp]

theorem WeierstrassCurve.Affine.Point.xRep_zero {R : Type r} [CommRing R] {W' : Affine R} : xRep 0 = ![1, 0]

@[simp]

theorem WeierstrassCurve.Affine.Point.xRep_some {R : Type r} [CommRing R] {W' : Affine R} {x y : R} (h : W'.Nonsingular x y) : (some x y h).xRep = ![x, 1]

theorem WeierstrassCurve.Affine.Point.xRep_ne_zero {R : Type r} [CommRing R] {W' : Affine R} [Nontrivial R] (P : W'.Point) : P.xRep ≠ 0

@[simp]

theorem WeierstrassCurve.Affine.Point.xRep_neg {R : Type r} [CommRing R] {W' : Affine R} (P : W'.Point) : (-P).xRep = P.xRep

theorem WeierstrassCurve.Affine.Point.eq_or_eq_neg_of_xRep_eq_xRep {F : Type u} [Field F] {W : Affine F} {P Q : W.Point} (h : P.xRep = Q.xRep) : P = Q ∨ P = -Q

theorem WeierstrassCurve.Affine.Point.xRep_eq_xRep_iff {F : Type u} [Field F] {W : Affine F} {P Q : W.Point} : P.xRep = Q.xRep ↔ P = Q ∨ P = -Q

theorem WeierstrassCurve.Affine.Point.xRep_add_self_of_Y_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x y : F} (h : W.Nonsingular x y) (hn : y ≠ W.negY x y) : (some x y h + some x y h).xRep = ![(x ^ 4 - b₄ W * x ^ 2 - 2 * b₆ W * x - b₈ W) / (4 * x ^ 3 + b₂ W * x ^ 2 + 2 * b₄ W * x + b₆ W), 1]

We give an explicit expression for xRep of P + P when 2*P ≠ 0.

theorem WeierstrassCurve.Affine.Point.xRep_add_self_of_Y_eq {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x y : F} (h : W.Nonsingular x y) (hn : y = W.negY x y) : (some x y h + some x y h).xRep = ![1, 0]

We give an explicit expression for xRep of P + P when P ≠ 0 and 2*P = 0.

theorem WeierstrassCurve.Affine.Point.xRep_add_of_X_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {xP yP xQ yQ : F} (hP : W.Nonsingular xP yP) (hQ : W.Nonsingular xQ yQ) (hn : xP ≠ xQ) : (some xP yP hP + some xQ yQ hQ).xRep = ![((yP - yQ) ^ 2 + W.a₁ * (yP - yQ) * (xP - xQ) - (W.a₂ + xP + xQ) * (xP - xQ) ^ 2) / (xP - xQ) ^ 2, 1]

We give an explicit expression for xRep of P + Q when P ≠ ±Q.

theorem WeierstrassCurve.Affine.Point.xRep_sub_of_X_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {xP yP xQ yQ : F} (hP : W.Nonsingular xP yP) (hQ : W.Nonsingular xQ yQ) (hn : xP ≠ xQ) : (some xP yP hP - some xQ yQ hQ).xRep = ![((yP + yQ + W.a₁ * xQ + W.a₃) ^ 2 + W.a₁ * (yP + yQ + W.a₁ * xQ + W.a₃) * (xP - xQ) - (W.a₂ + xP + xQ) * (xP - xQ) ^ 2) / (xP - xQ) ^ 2, 1]

We give an explicit expression for xRep of P - Q when P ≠ ±Q.

theorem WeierstrassCurve.Affine.finite_preimage_xRep {F : Type u} [Field F] {W : Affine F} (x : F) : {P : W.Point | P.xRep = ![x, 1]}.Finite

theorem WeierstrassCurve.Affine.finite_preimage_xRep0 {F : Type u} [Field F] {W : Affine F} (x : F) : {P : W.Point | P.xRep 0 = x}.Finite