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 W⟮F⟯ in affine coordinates is an inductive, consisting of the unique point at infinity 𝓞 and nonsingular affine points (x, y). Then W⟮F⟯ 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 between W⟮F⟯ and the ideal class group of the affine coordinate ring F[W] := F[X, Y] / ⟨W(X, Y)⟩ of W. 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 integral 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 W⟮F⟯ 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 W⟮F⟯ in affine coordinates forms an abelian group under addition.

Notations

• W⟮K⟯: the group of nonsingular points on W base changed to K.

References

• [J Silverman, The Arithmetic of Elliptic Curves][silverman2009]
• 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

• WeierstrassCurve.Affine.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

• WeierstrassCurve.Affine.FunctionField = FractionRing WeierstrassCurve.Affine.CoordinateRing

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

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebra = Ideal.Quotient.algebra R

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

Equations

• WeierstrassCurve.Affine.CoordinateRing.instAlgebraPolynomial = Ideal.Quotient.algebra (Polynomial R)

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

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

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.CoordinateRing.mk {R : Type r} [CommRing R] (W' : Affine R) : Polynomial (Polynomial R) →+* 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) 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]

theorem WeierstrassCurve.Affine.CoordinateRing.smul {R : Type r} [CommRing R] {W' : Affine R} (x : Polynomial R) (y : 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 : 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) : CoordinateRing →+* CoordinateRing

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

Equations

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

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 (WeierstrassCurve.map W' 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 : 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 CoordinateRing

Ideals in the affine coordinate ring

noncomputable def WeierstrassCurve.Affine.CoordinateRing.XClass {R : Type r} [CommRing R] (W' : Affine R) (x : R) : 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) : 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 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 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 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) : (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 CoordinateRing) 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 (XYIdeal' ⋯) * ClassGroup.mk (XYIdeal' h) = 1

@[deprecated WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul (since := "2025-02-01")]

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

Alias of WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul.

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 (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) = ClassGroup.mk (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 : 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 : 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

def WeierstrassCurve.Affine.«term_⟮_⟯».«delab_app.WeierstrassCurve.Affine.Point» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def WeierstrassCurve.Affine.«term_⟮_⟯» : Lean.TrailingParserDescr

For an algebraic extension S of a ring R, the type of nonsingular S-points on a Weierstrass curve W over R in affine coordinates.

Equations

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

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 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 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 h).neg = WeierstrassCurve.Affine.Point.some ⋯

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 h = some ⋯

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 := ⋯ }

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

• WeierstrassCurve.Affine.Point.zero.add x✝ = x✝
• x✝.add WeierstrassCurve.Affine.Point.zero = x✝
• (WeierstrassCurve.Affine.Point.some h₁).add (WeierstrassCurve.Affine.Point.some h₂) = if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else WeierstrassCurve.Affine.Point.some ⋯

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 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 h₁ + some h₂ = some ⋯

@[deprecated WeierstrassCurve.Affine.Point.add_some (since := "2025-02-28")]

theorem WeierstrassCurve.Affine.Point.add_of_imp {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 h₁ + some h₂ = some ⋯

Alias of WeierstrassCurve.Affine.Point.add_some.

@[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 h₁ + some 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 h₁ + some 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 h₁ + some h₂ = some ⋯

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 h₁ + some h₂ = -some ⋯

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 h₁ + some h₁ = some ⋯

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 h₁ + some h₁ = -some ⋯

@[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 h₁ + some h₂ = some ⋯

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 h₁ + some h₂ = -some ⋯

Group law in affine coordinates

noncomputable def WeierstrassCurve.Affine.Point.toClass {F : Type u} [Field F] {W : Affine F} [DecidableEq F] : W.Point →+ Additive (ClassGroup 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 h => Additive.ofMul (ClassGroup.mk (CoordinateRing.XYIdeal' h))

@[deprecated WeierstrassCurve.Affine.Point.toClass (since := "2025-02-01")]

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

Alias of WeierstrassCurve.Affine.Point.toClass.

---

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

• @WeierstrassCurve.Affine.Point.toClassFun = @WeierstrassCurve.Affine.Point.toClass

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 h) = ClassGroup.mk (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 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) : Point (WeierstrassCurve.baseChange W' F) →+ Point (WeierstrassCurve.baseChange W' K)

The group homomorphism from W⟮F⟯ to W⟮K⟯ 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.

@[deprecated WeierstrassCurve.Affine.Point.map (since := "2025-02-01")]

def WeierstrassCurve.Affine.Point.mapFun {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) : Point (WeierstrassCurve.baseChange W' F) →+ Point (WeierstrassCurve.baseChange W' K)

Alias of WeierstrassCurve.Affine.Point.map.

---

The group homomorphism from W⟮F⟯ to W⟮K⟯ 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

• @WeierstrassCurve.Affine.Point.mapFun = @WeierstrassCurve.Affine.Point.map

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 : (WeierstrassCurve.baseChange W' F).toAffine.Nonsingular x y) : (map f) (some h) = some ⋯

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 : Point (WeierstrassCurve.baseChange W' F)) : (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 : Point (WeierstrassCurve.baseChange W' F)) : (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] : Point (WeierstrassCurve.baseChange W' F) →+ Point (WeierstrassCurve.baseChange W' K)

The group homomorphism from W⟮F⟯ to W⟮K⟯ 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 : Point (WeierstrassCurve.baseChange W' F)) : (map f) ((baseChange F K) P) = (baseChange F L) P