Documentation

MazurTorsion.Kubert.OrderSevenHauptmodul

The Hauptmodul attached to an exact order-seven point #

Tate normalization of an exact order-seven point produces a nonzero level-seven Hauptmodul. This file retains the cleared j-identity against the original Weierstrass curve, so consumers need not expose the auxiliary normal-form coordinate change.

source
def MazurTorsion.Kubert.pointTateBeta (W : WeierstrassCurve ℚ) (x y : ℚ) :
ℚ

The vertical tangent denominator used to normalize a marked affine point to Tate normal form.

Equations
Instances For
    source
    def MazurTorsion.Kubert.pointTateLambda (W : WeierstrassCurve ℚ) (x y : ℚ) :
    ℚ

    The tangent slope used in the first translation-shear of Tate normalization.

    Equations
    Instances For
      source
      def MazurTorsion.Kubert.pointTateAlpha (W : WeierstrassCurve ℚ) (x y : ℚ) :
      ℚ

      The quadratic coefficient after translating a marked affine point to the origin and making its tangent horizontal.

      Equations
      Instances For
        source
        def MazurTorsion.Kubert.pointTateParameter (W : WeierstrassCurve ℚ) (x y : ℚ) :
        ℚ

        The d = b / c parameter obtained by the explicit Tate normalization at an affine point.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MazurTorsion.Kubert.orderSevenHauptmodulAt (W : WeierstrassCurve ℚ) (x y : ℚ) :
          ℚ

          The level-seven Hauptmodul obtained by explicit Tate normalization at an affine point.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MazurTorsion.Kubert.orderSevenHauptmodulAt_spec (W : WeierstrassCurve ℚ) [W.IsElliptic] {X Y : ℚ} (hns : W.toAffine.Nonsingular X Y) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some X Y hns) = 7) :
            orderSevenHauptmodulAt W X Y ≠ 0 ∧ orderSevenJNumerator (orderSevenHauptmodulAt W X Y) * W.Δ = W.c₄ ^ 3 * orderSevenHauptmodulAt W X Y ^ 7

            The explicit Tate-normalization formula at an affine point of exact order seven is noncuspidal and satisfies the cleared level-seven Hauptmodul identity.

            source
            theorem MazurTorsion.Kubert.exists_orderSevenHauptmodul_of_exactOrder (W : WeierstrassCurve ℚ) [W.IsElliptic] (R : W.toAffine.Point) (hR : addOrderOf R = 7) :
            ∃ (B : ℚ), B ≠ 0 ∧ orderSevenJNumerator B * W.Δ = W.c₄ ^ 3 * B ^ 7

            An exact order-seven point supplies a noncuspidal level-seven Hauptmodul whose cleared j-identity is measured against the original curve.