Documentation

MazurTorsion.Kubert.TateNormalForm

Tate normal form #

Reusable foundations for the Tate normal form

y² + (1-c)xy - by = x³ - bx²

with marked point P = (0,0). This file provides the normalization theorem retaining the discriminant scale and kernel-checked low-multiple coordinate formulas. It does not state an order classification theorem.

source
def MazurTorsion.Kubert.tateNormalCurve (b c : ℚ) :
WeierstrassCurve ℚ

Tate normal form y² + (1-c)xy - by = x³ - bx², with marked point (0,0).

Equations
Instances For
    source
    @[simp]
    theorem MazurTorsion.Kubert.tateNormalCurve_a₁ (b c : ℚ) :
    (tateNormalCurve b c).a₁ = 1 - c
    source
    @[simp]
    theorem MazurTorsion.Kubert.tateNormalCurve_a₂ (b c : ℚ) :
    (tateNormalCurve b c).a₂ = -b
    source
    @[simp]
    theorem MazurTorsion.Kubert.tateNormalCurve_a₃ (b c : ℚ) :
    (tateNormalCurve b c).a₃ = -b
    source
    @[simp]
    theorem MazurTorsion.Kubert.tateNormalCurve_a₄ (b c : ℚ) :
    (tateNormalCurve b c).a₄ = 0
    source
    @[simp]
    theorem MazurTorsion.Kubert.tateNormalCurve_a₆ (b c : ℚ) :
    (tateNormalCurve b c).a₆ = 0
    source
    theorem MazurTorsion.Kubert.tateNormalCurve_nonsingular_origin (b c : ℚ) (hb : b ≠ 0) :
    (tateNormalCurve b c).toAffine.Nonsingular 0 0

    The marked origin is nonsingular whenever the Tate parameter b is nonzero.

    source
    theorem MazurTorsion.Kubert.three_nsmul_origin_eq_zero (W : WeierstrassCurve ℚ) (ha₂ : W.a₂ = 0) (ha₄ : W.a₄ = 0) (ha₃ : W.a₃ ≠ 0) (h00 : W.toAffine.Nonsingular 0 0) :
    WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 = 0

    If the tangent at the origin has triple contact, then the origin is killed by three. This is the small group-law fact used during Tate normalization.

    source
    theorem MazurTorsion.Kubert.exists_tateNormalCurve_scaled (W : WeierstrassCurve ℚ) [W.IsElliptic] (P : W.toAffine.Point) (hP2 : P + P ≠ 0) (hP3 : P + P + P ≠ 0) :
    ∃ (b : ℚ) (c : ℚ) (u : ℚ) (_ : u ≠ 0) (_ : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) (e : W.toAffine.Point ≃+ (tateNormalCurve b c).toAffine.Point), e P = WeierstrassCurve.Affine.Point.some 0 0 h00 ∧ u ^ 12 * W.Δ = (tateNormalCurve b c).Δ ∧ u ^ 4 * W.c₄ = (tateNormalCurve b c).c₄ ∧ u ^ 6 * W.c₆ = (tateNormalCurve b c).c₆

    Tate normalization retaining the discriminant and c₄ scaling parameters.

    source
    theorem MazurTorsion.Kubert.two_mul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) :
    ∃ (h₂ : (tateNormalCurve b c).toAffine.Nonsingular b (b * c)), WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some b (b * c) h₂

    The marked point P = (0,0) doubles to (b,bc) on Tate normal form.

    source
    theorem MazurTorsion.Kubert.three_mul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) :
    ∃ (h₃ : (tateNormalCurve b c).toAffine.Nonsingular c (b - c)), WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some c (b - c) h₃

    The marked point P = (0,0) triples to (c,b-c) on Tate normal form.

    source
    theorem MazurTorsion.Kubert.two_nsmul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) :
    ∃ (h₂ : (tateNormalCurve b c).toAffine.Nonsingular b (b * c)), 2 • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some b (b * c) h₂

    In scalar-multiplication notation, 2P = (b,bc) for the marked Tate point.

    source
    theorem MazurTorsion.Kubert.three_nsmul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) :
    ∃ (h₃ : (tateNormalCurve b c).toAffine.Nonsingular c (b - c)), 3 • WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some c (b - c) h₃

    In scalar-multiplication notation, 3P = (c,b-c) for the marked Tate point.

    source
    theorem MazurTorsion.Kubert.four_mul_origin_coordinates (b c : ℚ) (hb : b ≠ 0) (hc : c ≠ 0) (h00 : (tateNormalCurve b c).toAffine.Nonsingular 0 0) :
    ∃ (h₄ : (tateNormalCurve b c).toAffine.Nonsingular (b * (b - c) / c ^ 2) (b ^ 2 * (c ^ 2 + c - b) / c ^ 3)), WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 + WeierstrassCurve.Affine.Point.some 0 0 h00 = WeierstrassCurve.Affine.Point.some (b * (b - c) / c ^ 2) (b ^ 2 * (c ^ 2 + c - b) / c ^ 3) h₄

    If also c ≠ 0, then 4P has the displayed rational coordinates.