Reduction of the exceptional cubic modulo five

This file is an exact-pin integration test for the reduction-at-a-prime API. It treats the integral model

y² = x³ + 2x² - 3x

of the exceptional cubic used in the Mazur theorem development. Reduction at (5) is injective on rational torsion, and the reduced curve has exactly eight points. Consequently, once finiteness of the rational point group is supplied by the independent descent argument, the rational point group has cardinality at most eight.

instance ExceptionalCubicReduction.instFactPrimeOfNatNat_ellipticCurves : Fact (Nat.Prime 5)

def ExceptionalCubicReduction.integralCurve : WeierstrassCurve ℤ

The exceptional cubic as an integral Weierstrass model.

Equations

• ExceptionalCubicReduction.integralCurve = { a₁ := 0, a₂ := 2, a₃ := 0, a₄ := -3, a₆ := 0 }

def ExceptionalCubicReduction.curve : WeierstrassCurve.Affine ℚ

The exceptional cubic over the rationals.

Equations

• ExceptionalCubicReduction.curve = { a₁ := 0, a₂ := 2, a₃ := 0, a₄ := -3, a₆ := 0 }

theorem ExceptionalCubicReduction.map_integralCurve : integralCurve.map (algebraMap ℤ ℚ) = curve

theorem ExceptionalCubicReduction.discriminant_integralCurve : integralCurve.Δ = 2304

instance ExceptionalCubicReduction.instIsEllipticRatCurve : WeierstrassCurve.IsElliptic curve

def ExceptionalCubicReduction.intPrime (p : ℕ) [Fact (Nat.Prime p)] : IsDedekindDomain.HeightOneSpectrum ℤ

The height-one prime (p) of ℤ.

Equations

• ExceptionalCubicReduction.intPrime p = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯

@[simp]

theorem ExceptionalCubicReduction.intPrime_asIdeal (p : ℕ) [Fact (Nat.Prime p)] : (intPrime p).asIdeal = Ideal.span {↑p}

@[instance_reducible]

instance ExceptionalCubicReduction.instDecidableEqQuotientIntIdealAsIdealIntPrime (p : ℕ) [Fact (Nat.Prime p)] : DecidableEq (ℤ ⧸ (intPrime p).asIdeal)

Equations

• ExceptionalCubicReduction.instDecidableEqQuotientIntIdealAsIdealIntPrime p = (Int.quotientSpanNatEquivZMod p).decidableEq

theorem ExceptionalCubicReduction.isElliptic_redCurve {p : ℕ} [Fact (Nat.Prime p)] (h : ¬↑p ∣ integralCurve.Δ) : WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve (intPrime p) integralCurve)

instance ExceptionalCubicReduction.instIsEllipticQuotientIntIdealAsIdealIntPrimeOfNatNatRedCurveIntegralCurve : WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve (intPrime 5) integralCurve)

def ExceptionalCubicReduction.curveModFive : WeierstrassCurve (ZMod 5)

The concrete reduction over ZMod 5.

Equations

• ExceptionalCubicReduction.curveModFive = { a₁ := 0, a₂ := 2, a₃ := 0, a₄ := -3, a₆ := 0 }

instance ExceptionalCubicReduction.instIsEllipticZModOfNatNatCurveModFive : curveModFive.IsElliptic

noncomputable def ExceptionalCubicReduction.residueFiveAlgEquiv : (ℤ ⧸ (intPrime 5).asIdeal) ≃ₐ[ℤ] ZMod 5

The canonical identification of the residue field at 5 with ZMod 5, as a ℤ-algebra equivalence.

Equations

• ExceptionalCubicReduction.residueFiveAlgEquiv = AlgEquiv.ofRingEquiv ⋯

theorem ExceptionalCubicReduction.baseChange_modFive : WeierstrassCurve.toAffine (integralCurve.toAffine.baseChange (ZMod 5)) = curveModFive.toAffine

noncomputable def ExceptionalCubicReduction.reducedPointEquiv : (WeierstrassCurve.Affine.redCurve (intPrime 5) integralCurve).Point ≃+ curveModFive.toAffine.Point

Identification of the abstract residue-field point group with the computable ZMod 5 point group.

Equations

• One or more equations did not get rendered due to their size.

instance ExceptionalCubicReduction.instFinitePointQuotientIntIdealAsIdealIntPrimeOfNatNatRedCurveIntegralCurve : Finite (WeierstrassCurve.Affine.redCurve (intPrime 5) integralCurve).Point

theorem ExceptionalCubicReduction.card_reducedCurve : Nat.card (WeierstrassCurve.Affine.redCurve (intPrime 5) integralCurve).Point = 8

The reduction modulo five has exactly eight points.

theorem ExceptionalCubicReduction.five_mem_prime : 5 ∈ (intPrime 5).asIdeal

theorem ExceptionalCubicReduction.five_not_mem_prime_pow_four : 5 ∉ (intPrime 5).asIdeal ^ (5 - 1)

noncomputable def ExceptionalCubicReduction.torsionReduction : ↥(AddCommGroup.torsion curve.Point) →+ (WeierstrassCurve.Affine.redCurve (intPrime 5) integralCurve).Point

Reduction at five, restricted to the rational torsion subgroup.

Equations

• One or more equations did not get rendered due to their size.

theorem ExceptionalCubicReduction.torsionReduction_injective : Function.Injective ⇑torsionReduction

Reduction at five is injective on rational torsion.

theorem ExceptionalCubicReduction.reduction_injective_of_finite [Finite curve.Point] : Function.Injective ⇑(WeierstrassCurve.Affine.redHom (intPrime 5) map_integralCurve)

If the rational point group is finite, reduction at five is injective on all of it.

theorem ExceptionalCubicReduction.point_card_le_eight [Finite curve.Point] : Nat.card curve.Point ≤ 8

Once an independent descent supplies finiteness, the exceptional cubic has at most eight rational points.