Documentation

MazurTorsion.PrimeOrder.TorsionSpecialization

Exact-order consumers for reduction at five and eleven #

This file applies the integer-prime formal-kernel certificate to the actual global reduction map at a prime of good reduction. It supplies the exact-order statements needed after the Mazur local argument has established good reduction, together with cardinality-divisibility consumers.

The suffix of_goodReduction is intentional. Before good reduction has been proved, the marked point specializes to a Neron special fibre rather than to the group of points of the possibly singular Weierstrass reduction. Constructing that special-fibre map and its component quotient remains a separate geometric boundary; this module does not hide it behind an assumed map.

source
@[reducible, inline]
abbrev MazurTorsion.PrimeOrder.reductionCurveAtFive (W₀ : WeierstrassCurve ℤ) :
WeierstrassCurve.Affine (ZMod 5)

The coefficientwise reduction of an integral Weierstrass equation over ZMod 5.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MazurTorsion.PrimeOrder.reductionCurveAtEleven (W₀ : WeierstrassCurve ℤ) :
    WeierstrassCurve.Affine (ZMod 11)

    The coefficientwise reduction of an integral Weierstrass equation over ZMod 11.

    Equations
    Instances For
      source
      theorem MazurTorsion.PrimeOrder.reductionCurveAtFive_eq_map (W₀ : WeierstrassCurve ℤ) :
      reductionCurveAtFive W₀ = (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀).map ↑IntegerPrimeSpecialization.residueFiveAlgEquiv.toRingEquiv

      Identifying the residue field at five with ZMod 5 carries the abstract reduced equation to the concrete coefficientwise reduction.

      source
      theorem MazurTorsion.PrimeOrder.reductionCurveAtEleven_eq_map (W₀ : WeierstrassCurve ℤ) :
      reductionCurveAtEleven W₀ = (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀).map ↑IntegerPrimeSpecialization.residueElevenAlgEquiv.toRingEquiv

      Identifying the residue field at eleven with ZMod 11 carries the abstract reduced equation to the concrete coefficientwise reduction.

      source
      theorem MazurTorsion.PrimeOrder.reductionCurveAtFive_isElliptic (W₀ : WeierstrassCurve ℤ) [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] :
      WeierstrassCurve.IsElliptic (reductionCurveAtFive W₀)

      Good reduction at the abstract residue field transfers to the concrete ZMod 5 equation.

      source
      theorem MazurTorsion.PrimeOrder.reductionCurveAtEleven_isElliptic (W₀ : WeierstrassCurve ℤ) [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] :
      WeierstrassCurve.IsElliptic (reductionCurveAtEleven W₀)

      Good reduction at the abstract residue field transfers to the concrete ZMod 11 equation.

      source
      noncomputable def MazurTorsion.PrimeOrder.reductionAtFiveToZMod {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] :
      E.Point →+ (reductionCurveAtFive W₀).Point

      Reduction at five followed by the canonical identification of the residue field with ZMod 5.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MazurTorsion.PrimeOrder.reductionAtElevenToZMod {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] :
        E.Point →+ (reductionCurveAtEleven W₀).Point

        Reduction at eleven followed by the canonical identification of the residue field with ZMod 11.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MazurTorsion.PrimeOrder.specializedPoint_addOrderOf_eq_atFive_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) :
          addOrderOf (WeierstrassCurve.Affine.red IntegerPrimeSpecialization.atFive hE P) = addOrderOf P

          At good reduction over five, specialization preserves the exact additive order of every torsion point.

          source
          theorem MazurTorsion.PrimeOrder.specializedPoint_addOrderOf_eq_atEleven_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) :
          addOrderOf (WeierstrassCurve.Affine.red IntegerPrimeSpecialization.atEleven hE P) = addOrderOf P

          At good reduction over eleven, specialization preserves the exact additive order of every torsion point.

          source
          theorem MazurTorsion.PrimeOrder.specializedPointZMod_addOrderOf_eq_atFive_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) :
          addOrderOf ((reductionAtFiveToZMod hE) P) = addOrderOf P

          Concrete ZMod 5 specialization preserves exact additive order at good reduction.

          source
          theorem MazurTorsion.PrimeOrder.specializedPointZMod_addOrderOf_eq_atEleven_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) :
          addOrderOf ((reductionAtElevenToZMod hE) P) = addOrderOf P

          Concrete ZMod 11 specialization preserves exact additive order at good reduction.

          source
          theorem MazurTorsion.PrimeOrder.exactOrder_dvd_reduction_card_atFive_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) {N : ℕ} (horder : addOrderOf P = N) :
          N ∣ Nat.card (reductionCurveAtFive W₀).Point

          A point of exact order N at good reduction over five forces N to divide the cardinality of the reduced point group. This is a downstream consumer of exact-order preservation, not just a restatement of the reduction map.

          source
          theorem MazurTorsion.PrimeOrder.exactOrder_dvd_reduction_card_atEleven_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] {P : E.Point} (hP : IsOfFinAddOrder P) {N : ℕ} (horder : addOrderOf P = N) :
          N ∣ Nat.card (reductionCurveAtEleven W₀).Point

          A point of exact order N at good reduction over eleven forces N to divide the cardinality of the reduced point group.

          source
          theorem MazurTorsion.PrimeOrder.addOrderOf_ne_of_reduction_card_lt_atFive_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atFive W₀)] [Finite (reductionCurveAtFive W₀).Point] {P : E.Point} (hP : IsOfFinAddOrder P) {N : ℕ} (hcard : Nat.card (reductionCurveAtFive W₀).Point < N) :
          addOrderOf P ≠ N

          A finite reduction at five cannot receive a torsion point whose exact order is larger than the reduced point group.

          source
          theorem MazurTorsion.PrimeOrder.addOrderOf_ne_of_reduction_card_lt_atEleven_of_goodReduction {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] [Finite (reductionCurveAtEleven W₀).Point] {P : E.Point} (hP : IsOfFinAddOrder P) {N : ℕ} (hcard : Nat.card (reductionCurveAtEleven W₀).Point < N) :
          addOrderOf P ≠ N

          A finite reduction at eleven cannot receive a torsion point whose exact order is larger than the reduced point group.