Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.TateCurve.Specialization

Specialization of the Tate equation #

The coefficients of the Tate equation are formal power series with integer coefficients. In a complete non-archimedean normed ring with ‖1‖ = 1, their sums converge at every parameter of norm less than one. This remains true in residue characteristics 2 and 3: the sixth coefficient is summed from its integral coefficients, with no division in the target ring.

For a unit parameter in the open unit ball of a complete non-archimedean normed commutative ring with ‖1‖ = 1, these sums give a nonsingular Tate equation. Its discriminant has the same norm as the parameter, even when the ring norm is only submultiplicative. Point uniformisation requires further arguments.

References #

source
noncomputable def TauCeti.tateCurveA₄ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) :
K

The analytic fourth Tate coefficient, obtained from the integral formal series.

Equations
Instances For
    source
    noncomputable def TauCeti.tateCurveA₆ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) :
    K

    The analytic sixth Tate coefficient, obtained from integral coefficients before reducing to the residue characteristic of the ring.

    Equations
    Instances For
      source
      theorem TauCeti.tateCurveA₆_def {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) :
      tateCurveA₆ q hq = ∑' (n : ℕ), ↑((PowerSeries.coeff n) tateCurve.a₆) * q ^ n

      The sixth Tate coefficient is the sum of its evaluated integral coefficients.

      source
      @[simp]
      theorem TauCeti.tateCurveA₄_eq {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : K) (hq : ‖q‖ < 1) :
      tateCurveA₄ q hq = -5 * divisorSumAt 3 q

      The fourth coefficient equals -5 s₃(q).

      source
      @[simp]
      theorem TauCeti.twelve_mul_tateCurveA₆ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] {q : K} (hq : ‖q‖ < 1) :
      12 * tateCurveA₆ q hq = -(5 * divisorSumAt 3 q + 7 * divisorSumAt 5 q)

      The integral identity 12 a₆(q) = -(5 s₃(q) + 7 s₅(q)) holds in every complete non-archimedean normed commutative ring with ‖1‖ = 1, even when 12 = 0 there.

      source
      noncomputable def TauCeti.tateCurveAt {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
      WeierstrassCurve K

      The Tate equation obtained by evaluating the integral formal curve at a unit parameter of norm less than one. The unit parameter will also support its integer powers in uniformisation.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.tateCurveAt_a₁ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).a₁ = 1
        source
        @[simp]
        theorem TauCeti.tateCurveAt_a₂ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).a₂ = 0
        source
        @[simp]
        theorem TauCeti.tateCurveAt_a₃ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).a₃ = 0
        source
        @[simp]
        theorem TauCeti.tateCurveAt_a₄ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).a₄ = tateCurveA₄ (↑q) hq

        The analytic fourth coefficient is the evaluation of the formal fourth coefficient.

        source
        @[simp]
        theorem TauCeti.tateCurveAt_a₆ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).a₆ = tateCurveA₆ (↑q) hq

        The analytic sixth coefficient is the evaluation of the formal sixth coefficient.

        source
        theorem TauCeti.isUnit_tateCurveAt_Δ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        IsUnit (tateCurveAt q hq).Δ

        The discriminant of the specialized Tate equation is a unit.

        source
        instance TauCeti.isElliptic_tateCurveAt {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        (tateCurveAt q hq).IsElliptic

        A unit parameter of norm below one gives an elliptic curve over the complete normed ring, with no discreteness or characteristic assumption.

        source
        @[simp]
        theorem TauCeti.norm_tateCurveAt_Δ {K : Type u_1} [NormedCommRing K] [NormOneClass K] [CompleteSpace K] [IsUltrametricDist K] (q : Kˣ) (hq : ‖↑q‖ < 1) :
        ‖(tateCurveAt q hq).Δ‖ = ‖↑q‖

        The specialized Tate discriminant has the same norm as the parameter, even for a submultiplicative ring norm.