Documentation

Atlas.ArithmeticGeometry.code.Lemma2417

theorem Lemma2417.dvd_mul_of_pow_dvd {p : } [hp : Fact (Nat.Prime p)] {a b : ℤ_[p]} {m n : } (ha : p ^ m a) (hb : p ^ n b) :
p ^ (m + n) a * b

If $p^m \mid a$ and $p^n \mid b$ in $\mathbb{Z}_p$, then $p^{m+n} \mid a \cdot b$.

theorem Lemma2417.padic_norm_lt_one_of_dvd_p {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : p x) :

Any element of $\mathbb{Z}_p$ divisible by $p$ has norm strictly less than $1$.

theorem Lemma2417.padic_isUnit_one_add {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : p x) :
IsUnit (1 + x)

If $x \in \mathbb{Z}_p$ is divisible by $p$, then $1 + x$ is a unit (by the ultrametric inequality, $\|1 + x\| = 1$).

structure Lemma2417.IsInEn {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ : ℤ_[p]) (n : ) (x z : ℤ_[p]) :

The condition that a (projective-like) point $(x, z)$ on the dehomogenized Weierstrass curve $z = x^3 + a_4 x z^2 + a_6 z^3$ lies in the $n$-th piece $E_n$ of the $p$-adic filtration: $p^n \mid x$ and $p^{3n} \mid z$.

  • on_curve : z = x ^ 3 + a₄ * x * z ^ 2 + a₆ * z ^ 3
  • val_x : p ^ n x
  • val_z : p ^ (3 * n) z
Instances For
    theorem Lemma2417.cubic_diff_factor {R : Type u_1} [CommRing R] (c₃ c₂ c₁ a b : R) :
    c₃ * a ^ 3 + c₂ * a ^ 2 + c₁ * a - (c₃ * b ^ 3 + c₂ * b ^ 2 + c₁ * b) = (a - b) * (c₃ * (a ^ 2 + a * b + b ^ 2) + c₂ * (a + b) + c₁)

    Factorization of the difference of two cubic evaluations: $f(a) - f(b) = (a - b) \cdot q(a, b)$ where $q$ is symmetric in $a, b$.

    theorem Lemma2417.vieta_sum_distinct {R : Type u_1} [CommRing R] [IsDomain R] (c₃ c₂ c₁ c₀ x₁ x₂ x₃ : R) (h1 : c₃ * x₁ ^ 3 + c₂ * x₁ ^ 2 + c₁ * x₁ + c₀ = 0) (h2 : c₃ * x₂ ^ 3 + c₂ * x₂ ^ 2 + c₁ * x₂ + c₀ = 0) (h3 : c₃ * x₃ ^ 3 + c₂ * x₃ ^ 2 + c₁ * x₃ + c₀ = 0) (h12 : x₁ x₂) (h13 : x₁ x₃) (h23 : x₂ x₃) :
    c₃ * (x₁ + x₂ + x₃) + c₂ = 0

    Vieta's formula (distinct roots case). If $x_1, x_2, x_3$ are three distinct roots of a cubic $c_3 X^3 + c_2 X^2 + c_1 X + c_0$ in a domain, then $c_3 (x_1 + x_2 + x_3) + c_2 = 0$.

    theorem Lemma2417.cubic_from_curve_and_line {R : Type u_1} [CommRing R] (a₄ a₆ α β x z : R) (hcurve : z = x ^ 3 + a₄ * x * z ^ 2 + a₆ * z ^ 3) (hline : z = α * x + β) :
    (1 + a₄ * α ^ 2 + a₆ * α ^ 3) * x ^ 3 + (2 * a₄ * α * β + 3 * a₆ * α ^ 2 * β) * x ^ 2 + (a₄ * β ^ 2 + 3 * a₆ * α * β ^ 2 - α) * x + (a₆ * β ^ 3 - β) = 0

    Substituting the line $z = \alpha x + \beta$ into the Weierstrass equation $z = x^3 + a_4 x z^2 + a_6 z^3$ yields a cubic in $x$ with explicit coefficients.

    theorem Lemma2417.vieta_from_curve_distinct {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₂ x₃ z₁ z₂ z₃ : ℤ_[p]) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hcurve2 : z₂ = x₂ ^ 3 + a₄ * x₂ * z₂ ^ 2 + a₆ * z₂ ^ 3) (hcurve3 : z₃ = x₃ ^ 3 + a₄ * x₃ * z₃ ^ 2 + a₆ * z₃ ^ 3) (hline1 : z₁ = α * x₁ + β) (hline2 : z₂ = α * x₂ + β) (hline3 : z₃ = α * x₃ + β) (h12 : x₁ x₂) (h13 : x₁ x₃) (h23 : x₂ x₃) :
    (1 + a₄ * α ^ 2 + a₆ * α ^ 3) * (x₁ + x₂ + x₃) + (2 * a₄ * α * β + 3 * a₆ * α ^ 2 * β) = 0

    Vieta's formula applied to three distinct collinear points on the Weierstrass curve: the sum of the $x$-coordinates satisfies $(1 + a_4 \alpha^2 + a_6 \alpha^3)(x_1 + x_2 + x_3) + (2 a_4 \alpha \beta + 3 a_6 \alpha^2 \beta) = 0$.

    theorem Lemma2417.slope_identity_precancellation {R : Type u_1} [CommRing R] (a₄ a₆ x₁ x₂ z₁ z₂ : R) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hcurve2 : z₂ = x₂ ^ 3 + a₄ * x₂ * z₂ ^ 2 + a₆ * z₂ ^ 3) :
    (z₂ - z₁) * (1 - a₄ * x₁ * (z₂ + z₁) - a₆ * (z₂ ^ 2 + z₁ * z₂ + z₁ ^ 2)) = (x₂ - x₁) * (x₂ ^ 2 + x₁ * x₂ + x₁ ^ 2 + a₄ * z₂ ^ 2)

    Algebraic identity relating the differences $z_2 - z_1$ and $x_2 - x_1$ for two points on the Weierstrass curve, before cancelling $x_2 - x_1$.

    theorem Lemma2417.slope_identity {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₂ z₁ z₂ : ℤ_[p]) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hcurve2 : z₂ = x₂ ^ 3 + a₄ * x₂ * z₂ ^ 2 + a₆ * z₂ ^ 3) (hline1 : z₁ = α * x₁ + β) (hline2 : z₂ = α * x₂ + β) (hne : x₁ x₂) :
    α * (1 - a₄ * x₁ * (z₂ + z₁) - a₆ * (z₂ ^ 2 + z₁ * z₂ + z₁ ^ 2)) = x₂ ^ 2 + x₁ * x₂ + x₁ ^ 2 + a₄ * z₂ ^ 2

    Identity expressing the slope $\alpha$ of a chord through two distinct points on the Weierstrass curve: $\alpha \cdot D = N$, where $D$ is the slope denominator and $N$ is the numerator.

    theorem Lemma2417.slope_denom_isUnit {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ x₁ z₁ z₂ : ℤ_[p]) (n : ) (hn : 0 < n) (hx1 : p ^ n x₁) (hz1 : p ^ (3 * n) z₁) (hz2 : p ^ (3 * n) z₂) :
    IsUnit (1 - a₄ * x₁ * (z₂ + z₁) - a₆ * (z₂ ^ 2 + z₁ * z₂ + z₁ ^ 2))

    The slope denominator $D = 1 - a_4 x_1 (z_2 + z_1) - a_6 (z_2^2 + z_1 z_2 + z_1^2)$ is a $p$-adic unit when $x_1, z_1, z_2$ lie in the filtration $E_n$ (since $D$ is $1$ plus a multiple of $p$).

    theorem Lemma2417.slope_numer_dvd {p : } [hp : Fact (Nat.Prime p)] (a₄ x₁ x₂ z₂ : ℤ_[p]) (n : ) (hx1 : p ^ n x₁) (hx2 : p ^ n x₂) (hz2 : p ^ (3 * n) z₂) :
    p ^ (2 * n) x₂ ^ 2 + x₁ * x₂ + x₁ ^ 2 + a₄ * z₂ ^ 2

    The slope numerator $N = x_2^2 + x_1 x_2 + x_1^2 + a_4 z_2^2$ is divisible by $p^{2n}$ when $x_1, x_2$ lie in $p^n \mathbb{Z}_p$ and $z_2$ lies in $p^{3n} \mathbb{Z}_p$.

    theorem Lemma2417.slope_in_p2n {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₂ z₁ z₂ : ℤ_[p]) (n : ) (hn : 0 < n) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hcurve2 : z₂ = x₂ ^ 3 + a₄ * x₂ * z₂ ^ 2 + a₆ * z₂ ^ 3) (hline1 : z₁ = α * x₁ + β) (hline2 : z₂ = α * x₂ + β) (hne : x₁ x₂) (hx1 : p ^ n x₁) (hx2 : p ^ n x₂) (hz1 : p ^ (3 * n) z₁) (hz2 : p ^ (3 * n) z₂) :
    p ^ (2 * n) α

    If two distinct points in the filtration $E_n$ lie on a line $z = \alpha x + \beta$, then $p^{2n}$ divides the slope $\alpha$ (chord case).

    theorem Lemma2417.intercept_in_p3n {p : } [hp : Fact (Nat.Prime p)] (α β x₁ z₁ : ℤ_[p]) (n : ) (hline1 : z₁ = α * x₁ + β) (hx1 : p ^ n x₁) (hz1 : p ^ (3 * n) z₁) ( : p ^ (2 * n) α) :
    p ^ (3 * n) β

    Given a line $z_1 = \alpha x_1 + \beta$ through a point in $E_n$, if $p^{2n} \mid \alpha$ then $p^{3n} \mid \beta$ (the intercept lies in $p^{3n} \mathbb{Z}_p$).

    theorem Lemma2417.valuation_from_vieta {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₂ x₃ : ℤ_[p]) (n : ) (hn : 0 < n) (hvieta : (1 + a₄ * α ^ 2 + a₆ * α ^ 3) * (x₁ + x₂ + x₃) + (2 * a₄ * α * β + 3 * a₆ * α ^ 2 * β) = 0) ( : p ^ (2 * n) α) ( : p ^ (3 * n) β) :
    p ^ (5 * n) x₁ + x₂ + x₃

    From Vieta's relation $(1 + a_4 \alpha^2 + a_6 \alpha^3)(x_1 + x_2 + x_3) + (2 a_4 \alpha \beta + 3 a_6 \alpha^2 \beta) = 0$, together with $p^{2n} \mid \alpha$ and $p^{3n} \mid \beta$, conclude $p^{5n} \mid x_1 + x_2 + x_3$.

    theorem Lemma2417.lemma_24_17_from_En {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₂ x₃ z₁ z₂ z₃ : ℤ_[p]) (n : ) (hn : 0 < n) (hP1 : IsInEn a₄ a₆ n x₁ z₁) (hP2 : IsInEn a₄ a₆ n x₂ z₂) (hP3 : IsInEn a₄ a₆ n x₃ z₃) (hline1 : z₁ = α * x₁ + β) (hline2 : z₂ = α * x₂ + β) (hline3 : z₃ = α * x₃ + β) (h12 : x₁ x₂) (h13 : x₁ x₃) (h23 : x₂ x₃) :
    p ^ (5 * n) x₁ + x₂ + x₃

    Lemma 24.17 (distinct collinear points case). Three distinct collinear points $P_1, P_2, P_3$ in the filtration $E_n$ of the Weierstrass curve satisfy $p^{5n} \mid x_1 + x_2 + x_3$.

    def Lemma2417.AreCollinear {p : } [hp : Fact (Nat.Prime p)] (x₁ z₁ x₂ z₂ x₃ z₃ : ℤ_[p]) :

    Three points $(x_1, z_1), (x_2, z_2), (x_3, z_3) \in \mathbb{Z}_p^2$ are collinear if they lie on a common line $z = \alpha x + \beta$ for some $\alpha, \beta \in \mathbb{Z}_p$.

    Instances For
      theorem Lemma2417.vieta_tangent_case {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ x₃ z₁ z₃ : ℤ_[p]) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hcurve3 : z₃ = x₃ ^ 3 + a₄ * x₃ * z₃ ^ 2 + a₆ * z₃ ^ 3) (hline1 : z₁ = α * x₁ + β) (hline3 : z₃ = α * x₃ + β) (hne : x₁ x₃) :
      (1 + a₄ * α ^ 2 + a₆ * α ^ 3) * (x₁ + x₁ + x₃) + (2 * a₄ * α * β + 3 * a₆ * α ^ 2 * β) = 0

      Vieta's relation (tangent case). When the line is tangent to the curve at $P_1$ and meets again at $P_3 \neq P_1$, the Vieta sum identity holds with multiplicity: $x_1 + x_1 + x_3$.

      theorem Lemma2417.vieta_flex_case {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ z₁ : ℤ_[p]) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hline1 : z₁ = α * x₁ + β) :
      (1 + a₄ * α ^ 2 + a₆ * α ^ 3) * (x₁ + x₁ + x₁) + (2 * a₄ * α * β + 3 * a₆ * α ^ 2 * β) = 0

      Vieta's relation (flex/triple-tangent case). When the line is a flex tangent to the curve at $P_1$ (intersecting with multiplicity $3$), the Vieta sum is $x_1 + x_1 + x_1 = 3 x_1$.

      theorem Lemma2417.slope_in_p2n_flex {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ α β x₁ z₁ : ℤ_[p]) (n : ) (hn : 0 < n) (hcurve1 : z₁ = x₁ ^ 3 + a₄ * x₁ * z₁ ^ 2 + a₆ * z₁ ^ 3) (hline1 : z₁ = α * x₁ + β) (hx1 : p ^ n x₁) (hz1 : p ^ (3 * n) z₁) :
      p ^ (2 * n) α

      The flex-case analogue of slope_in_p2n: when a flex tangent line passes through a point in $E_n$, the slope $\alpha$ satisfies $p^{2n} \mid \alpha$.

      theorem Lemma2417.lemma_24_17 {p : } [hp : Fact (Nat.Prime p)] (a₄ a₆ x₁ x₂ x₃ z₁ z₂ z₃ : ℤ_[p]) (n : ) (hn : 0 < n) (hP1 : IsInEn a₄ a₆ n x₁ z₁) (hP2 : IsInEn a₄ a₆ n x₂ z₂) (hP3 : IsInEn a₄ a₆ n x₃ z₃) (hcollinear : AreCollinear x₁ z₁ x₂ z₂ x₃ z₃) :
      p ^ (5 * n) x₁ + x₂ + x₃

      Lemma 24.17 (full statement). Three collinear points $P_1, P_2, P_3$ in the filtration $E_n$ of the Weierstrass curve over $\mathbb{Z}_p$ satisfy $p^{5n} \mid x_1 + x_2 + x_3$. The proof case-splits on which of the $x$-coordinates coincide (chord, tangent, or flex), invoking the corresponding Vieta and slope-divisibility lemmas.