WeierstrassCurve.Affine.equation_add'
theorem WeierstrassCurve.Affine.equation_add' :
∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
W.equation x₁ y₁ →
W.equation x₂ y₂ →
(x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) →
W.equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY' x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
This theorem states that for any field `F` and any Weierstrass curve `W` defined over that field, if you have two points `(x₁, y₁)` and `(x₂, y₂)` on the curve such that `x₁` is not equal to `x₂` or `y₁` is not equal to the negation of `y₂` after applying the curve's `negY` function to `x₂` and `y₂`, then the sum of these two points, computed as `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))` and `(W.addY' x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))`, before applying the final negation that maps $Y$ to $-Y - a_1X - a_3$, also lies on the Weierstrass curve. The `slope` function is used to determine the slope of the line between the given two points.
More concisely: Given a Weierstrass curve `W` over a field `F` and two distinct points `(x₁, y₁)` and `(x₂, y₂)` on the curve such that `x₁ ≠ x₂` or `y₁ ≠ -(W.negY x₂ y₂)`, the sum of these points `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY' x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))` lies on the Weierstrass curve.
|
WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero
theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {x y : R},
W.equation x y → W.Δ ≠ 0 → W.nonsingular x y
This theorem states that for any commutative ring `R`, if `W` is a Weierstrass curve over `R` and `(x, y)` is a point on `W` satisfying the curve's equation, then as long as the discriminant of the Weierstrass curve is non-zero, the curve `W` is nonsingular at the point `(x, y)`. In other words, having a non-zero discriminant guarantees the absence of singular points on a Weierstrass curve. In the context of algebraic geometry, a nonsingular point on a curve is a point where the curve doesn't cross itself or have a cusp.
More concisely: If `R` is a commutative ring, `W` is a Weierstrass curve over `R` with non-zero discriminant, and `(x, y)` is a point on `W` satisfying its equation, then `(x, y)` is a nonsingular point on `W`.
|
WeierstrassCurve.Affine.polynomial_eq
theorem WeierstrassCurve.Affine.polynomial_eq :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R),
W.polynomial =
{ a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly
The theorem `WeierstrassCurve.Affine.polynomial_eq` states that for any Weierstrass curve `W` defined over a commutative ring `R`, its defining polynomial is equal to the cubic polynomial generated by transforming a cubic polynomial with coefficients `a = 0`, `b = 1`, `c` being the polynomial generated from a cubic polynomial with coefficients `a = 0`, `b = 0`, `c = W.a₁`, `d = W.a₃`, and `d` being the polynomial generated from a cubic polynomial with coefficients `a = -1`, `b = -W.a₂`, `c = -W.a₄`, `d = -W.a₆`. In other words, this theorem provides the relationship between the defining polynomial of a Weierstrass curve and a specific cubic polynomial in the affine coordinates of the curve.
More concisely: The defining polynomial of a Weierstrass curve over a commutative ring is equivalent to a specific cubic polynomial formed from transforming polynomials with coefficients from the Weierstrass curve's parameters.
|
Mathlib.AlgebraicGeometry.EllipticCurve.Affine._auxLemma.1
theorem Mathlib.AlgebraicGeometry.EllipticCurve.Affine._auxLemma.1 :
∀ {R : Type u} [inst : Semiring R], 0 = Polynomial.C 0
The theorem `Mathlib.AlgebraicGeometry.EllipticCurve.Affine._auxLemma.1` states that for any type `R` that is a semiring, the constant polynomial with value `0` (denoted as `Polynomial.C 0`) is equal to `0`. In mathematical terms, it expresses that the constant polynomial mapping that assigns to every `0` in `R` the zero polynomial, is equivalent to the zero element in the ring of polynomials over `R`.
More concisely: For any semiring `R`, the constant polynomial `Polynomial.C 0` equals the zero element in the ring of polynomials over `R`.
|
WeierstrassCurve.Affine.nonsingular_add'
theorem WeierstrassCurve.Affine.nonsingular_add' :
∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
W.nonsingular x₁ y₁ →
W.nonsingular x₂ y₂ →
(x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) →
W.nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY' x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
This theorem, `WeierstrassCurve.Affine.nonsingular_add'`, states that for any field `F` and any affine Weierstrass curve `W` over `F`, if we have two points `(x₁, y₁)` and `(x₂, y₂)` on `W` that are nonsingular, then the addition of these two points is also nonsingular. The addition operation here is defined in terms of the `W.addX` and `W.addY'` functions, which in turn depend on the `W.slope` of the line between the two points. Additionally, the theorem requires that if the x-coordinates of the two points are the same, then their y-coordinates should not be negatives of each other. Note that the addition operation involves applying a negation that maps $Y$ to $-Y - a_1X - a_3$ on the sloped line, but the nonsingularity is checked before this final negation is applied.
More concisely: Given an affine Weierstrass curve `W` over a field `F` and two nonsingular points `(x₁, y₁)` and `(x₂, y₂)` on `W` with `x₁ ≠ x₂`, if `W.slope(x₁, y₁) ≠ W.slope(x₂, y₂)`, then the point sum `(x₁, y₁) + (x₂, y₂)` is also a nonsingular point on `W`.
|
WeierstrassCurve.Affine.natDegree_polynomial
theorem WeierstrassCurve.Affine.natDegree_polynomial :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) [inst_1 : Nontrivial R],
W.polynomial.natDegree = 2
This theorem states that for any commutative ring `R` and any affine Weierstrass curve `W` over `R` (where `R` is nontrivial), the natural degree of the polynomial representing the curve is always equal to 2. The "natural degree" here refers to the degree of the polynomial in the natural numbers, which is forced to be a natural number by defining the degree of the zero polynomial as zero. The Weierstrass curve in this context is a type of elliptic curve.
More concisely: For any commutative nontrivial ring `R` and affine Weierstrass curve `W` over `R`, the degree of its polynomial representation is equal to 2.
|
WeierstrassCurve.Affine.map_addX
theorem WeierstrassCurve.Affine.map_addX :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {A : Type v} [inst_1 : CommRing A] (φ : R →+* A)
(x₁ x₂ L : R), (W.map φ).toAffine.addX (φ x₁) (φ x₂) (φ L) = φ (W.addX x₁ x₂ L)
The theorem `WeierstrassCurve.Affine.map_addX` states that for any commutative ring `R`, a Weierstrass curve `W` over `R`, a commutative ring `A`, a ring homomorphism `φ` from `R` to `A`, and any three elements `x₁`, `x₂`, `L` of `R`, the result of adding `x₁` and `x₂` under the `addX` operation on the curve `W`, and then mapping the result via `φ` to the ring `A`, is the same as first mapping `x₁`, `x₂` and `L` to `A` via `φ` and then performing the `addX` operation in the affine Weierstrass curve over `A` obtained by mapping `W` via `φ`. This theorem essentially asserts that the `addX` operation on Weierstrass curves is compatible with ring homomorphisms.
More concisely: Given a Weierstrass curve `W` over a commutative ring `R`, a ring homomorphism `φ` from `R` to a commutative ring `A`, and elements `x₁`, `x₂`, `L` in `R`, the affine `addX` operation on `W` commutes with the application of `φ`, i.e., `φ(x₁ +ₗ[R] x₂) = φ(x₁) +ₗ[A] φ(x₂)` in the affine Weierstrass curve over `A`.
|
WeierstrassCurve.Affine.nonsingular_neg
theorem WeierstrassCurve.Affine.nonsingular_neg :
∀ {R : Type u} [inst : CommRing R] {W : WeierstrassCurve.Affine R} {x y : R},
W.nonsingular x y → W.nonsingular x (W.negY x y)
The theorem `WeierstrassCurve.Affine.nonsingular_neg` states that for any commutative ring `R`, and any Weierstrass curve `W` defined over `R`, along with any points `x, y` in `R`, if the point `(x, y)` is a nonsingular point on the curve `W`, then the point `(x, W.negY x y)` is also a nonsingular point on the curve `W`. In other words, the negation of a nonsingular affine point in a Weierstrass curve is also nonsingular.
More concisely: For any Weierstrass curve `W` over a commutative ring `R` and any nonsingular point `(x, y)` on `W`, the point `(x, W.negY x y)` is also a nonsingular point on `W`.
|
WeierstrassCurve.Affine.eval_polynomialX
theorem WeierstrassCurve.Affine.eval_polynomialX :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (x y : R),
Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialX) =
W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
This theorem states that for any commutative ring `R`, and for any Weierstrass curve `W` over `R` represented in affine coordinates, and any elements `x` and `y` from `R`, if you evaluate `W`'s `polynomialX` by first replacing every instance of `X` with the constant polynomial `y` and then evaluating the result at `x`, you get the result `W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)`. In other words, the polynomial `polynomialX` on `W` behaves in a certain way when evaluated at `(x, y)`.
More concisely: For any commutative ring `R`, Weierstrass curve `W` over `R` in affine coordinates, and elements `x, y` from `R`, the evaluation of `W.polynomialX` at `x` after substituting all occurrences of `X` with `y` is equal to `W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)`.
|
WeierstrassCurve.Affine.Point.add.proof_1
theorem WeierstrassCurve.Affine.Point.add.proof_1 :
∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (x₁ y₁ : F),
W.nonsingular x₁ y₁ →
∀ (x₂ y₂ : F),
W.nonsingular x₂ y₂ →
¬y₁ = W.negY x₂ y₂ →
W.nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
The theorem `WeierstrassCurve.Affine.Point.add.proof_1` states that for any field `F`, and for any Weierstrass curve `W` defined over this field, given two points `(x₁, y₁)` and `(x₂, y₂)` on this curve that are nonsingular, if `y₁` does not equal the negation of `y₂` under the curve `W`, then the point `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))` - which is the result of the "addition" operation defined on the curve between the two points - is also nonsingular. The slope used in the addition operation is computed with the function `W.slope` which is the slope of the line passing through `(x₁, y₁)` and `(x₂, y₂)`.
More concisely: Given a Weierstrass curve `W` over a field `F` and two nonsingular points `(x₁, y₁)` and `(x₂, y₂)` with distinct `y` coordinates, the point obtained by adding `(x₁, y₁)` and `(x₂, y₂)` according to the curve's addition operation is also a nonsingular point.
|
WeierstrassCurve.Affine.monic_polynomial
theorem WeierstrassCurve.Affine.monic_polynomial :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R), W.polynomial.Monic
The theorem states that for any commutative ring `R`, every affine Weierstrass curve `W` over `R` has a polynomial which is monic. Here, a polynomial being monic means that its leading coefficient is 1. Therefore, the leading coefficient of the polynomial of every affine Weierstrass curve over any commutative ring is 1.
More concisely: Every affine Weierstrass curve over a commutative ring has a monic polynomial defining it.
|
WeierstrassCurve.Affine.equation_neg_iff
theorem WeierstrassCurve.Affine.equation_neg_iff :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (x y : R),
W.equation x (W.negY x y) ↔ W.equation x y
The theorem `WeierstrassCurve.Affine.equation_neg_iff` states that for any type `R` which is a commutative ring, any Weierstrass curve `W` defined over `R`, and any elements `x` and `y` of `R`, the equation of the Weierstrass curve with `x` and the negation of `y` (as computed by the `negY` function of `W`) holds if and only if the equation of the Weierstrass curve with `x` and `y` holds. In other words, if a point `(x, y)` lies on the Weierstrass curve, then so does the point `(x, -y)`, and conversely. This theorem is a reflection property of Weierstrass curves.
More concisely: For any Weierstrass curve `W` over a commutative ring `R` and elements `x` and `y` of `R`, the point `(x, y)` lies on `W` if and only if the point `(x, -y)` lies on `W`.
|
WeierstrassCurve.Affine.nonsingular_add
theorem WeierstrassCurve.Affine.nonsingular_add :
∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
W.nonsingular x₁ y₁ →
W.nonsingular x₂ y₂ →
(x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) →
W.nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
The theorem `WeierstrassCurve.Affine.nonsingular_add` states that given a field `F`, a Weierstrass curve `W` in affine coordinates over `F`, and two nonsingular points (`x₁`, `y₁`) and (`x₂`, `y₂`) on `W`, if `x₁` equals `x₂` then `y₁` must not be the negative of `y₂` under the Weierstrass curve transformation. Under these conditions, the sum of these two points, calculated using the `W.addX` and `W.addY` operations with the slope of the line through the points, results in another point that is also nonsingular on the Weierstrass curve.
More concisely: Given a Weierstr Ross curve in affine coordinates over a field, if two nonsingular points on the curve have the same x-coordinate, then their sum, calculated using the curve's `addX` and `addY` operations and the slope of the line through them, is another nonsingular point on the curve, excluding the case where the y-coordinates are negatives of each other.
|
WeierstrassCurve.Affine.equation_add
theorem WeierstrassCurve.Affine.equation_add :
∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
W.equation x₁ y₁ →
W.equation x₂ y₂ →
(x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) →
W.equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
The theorem `WeierstrassCurve.Affine.equation_add` asserts that for any field `F` and any two points `(x₁, y₁)` and `(x₂, y₂)` on a Weierstrass curve `W` defined over `F`, if `(x₁, y₁)` and `(x₂, y₂)` satisfy the equation of `W` and if `x₁` equals `x₂` then `y₁` is not equal to the negation of `y₂` in `W`, then the point resulting from the addition of these two points, given by `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))`, also lies on `W`. Here, the addition of points is defined with respect to the group law on the Weierstrass curve, and `W.slope` is the slope of the line through `(x₁, y₁)` and `(x₂, y₂)`.
More concisely: Given a Weierstrass curve `W` over a field `F`, if two points `(x₁, y₁)` and `(x₂, y₂)` on `W` satisfy the equation of `W`, `x₁ = x₂`, and `y₁ ≠ -y₂`, then their sum `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))` also lies on `W`.
|
WeierstrassCurve.Affine.eval_polynomialY
theorem WeierstrassCurve.Affine.eval_polynomialY :
∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (x y : R),
Polynomial.eval x (Polynomial.eval (Polynomial.C y) W.polynomialY) = 2 * y + W.a₁ * x + W.a₃
This theorem states that for any commutative ring `R`, given a Weierstrass curve `W` in the affine coordinate system over `R`, and any elements `x` and `y` of `R`, the evaluation of the `W.polynomialY` at the point where the variable is replaced by the constant polynomial `y` and then evaluated at `x`, equals `2 * y + W.a₁ * x + W.a₃`. In other words, when you substitute `y` into `W.polynomialY` and then evaluate the resulting polynomial at `x`, you get `2 * y + W.a₁ * x + W.a₃`.
More concisely: For any commutative ring `R`, the evaluation of the polynomial `W.polynomialY` at a point (x, y) on a Weierstrass curve `W` over `R` equals `2 * y + W.a₁ * x + W.a₃`.
|
WeierstrassCurve.Affine.equation_neg
theorem WeierstrassCurve.Affine.equation_neg :
∀ {R : Type u} [inst : CommRing R] {W : WeierstrassCurve.Affine R} {x y : R},
W.equation x y → W.equation x (W.negY x y)
This theorem states that for any commutative ring `R` and any affine Weierstrass curve `W` over `R`, if a point `(x, y)` lies on `W`, then the point `(x, W.negY x y)`, which is the negation of the y-coordinate of the original point, also lies on `W`. This essentially says that if `y` satisfies the equation of the Weierstrass curve at a given `x`, then so does the negation of `y`.
More concisely: For any commutative ring `R` and affine Weierstrass curve `W` over `R`, if `(x, y)` is a point on `W`, then `(x, -y)` is also a point on `W`.
|
WeierstrassCurve.Affine.Point.add.proof_2
theorem WeierstrassCurve.Affine.Point.add.proof_2 :
∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (x₁ y₁ : F),
W.nonsingular x₁ y₁ →
∀ (x₂ y₂ : F),
W.nonsingular x₂ y₂ →
¬x₁ = x₂ → W.nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
This theorem states that for any field `F` and a Weierstrass curve `W` defined over `F`, given two points `(x₁, y₁)` and `(x₂, y₂)` on the curve that are non-singular (i.e., they do not represent singularities of the curve) and distinct (i.e., `x₁` is not equal to `x₂`), the point resulting from the addition of these two points `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))` is also non-singular on the curve. The addition here is defined in terms of the 'slope' function, which calculates the slope of the line joining `(x₁, y₁)` and `(x₂, y₂)`. The `W.addX` and `W.addY` functions compute the x-coordinate and y-coordinate of the sum of the two points, respectively.
More concisely: Given a Weierstrass curve `W` over a field `F` and two distinct non-singular points `(x₁, y₁)` and `(x₂, y₂)` on the curve, the point `(W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂), W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))` is also a non-singular point on `W`.
|
WeierstrassCurve.Affine.Point.some_add_some_of_Yne
theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne :
∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F} {h₁ : W.nonsingular x₁ y₁}
{h₂ : W.nonsingular x₂ y₂},
x₁ = x₂ →
∀ (hy : y₁ ≠ W.negY x₂ y₂),
WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ =
WeierstrassCurve.Affine.Point.some ⋯
This theorem states that given a field `F` and a Weierstrass curve `W` defined over `F`, for any two points `(x₁, y₁)` and `(x₂, y₂)` on the curve `W` that are nonsingular (meaning the tangent line is well defined at these points), if `x₁` equals `x₂` and `y₁` is not equal to the negative of `y₂` with respect to `x₂`, then the sum of these two points on the curve equals another specific point on the curve, the details of which are suppressed here. The operation `+` here stands for the addition operation in the group law of elliptic curves.
More concisely: Given a Weierstrass curve `W` over a field `F` and two nonsingular points `(x₁, y₁)` and `(x₂, y₂)` on `W` with `x₁ = x₂` and `y₁ ≠ -y₂`, their sum in the group law of `W` is a specific point on the curve.
|