Conditional rational-point classification on X₁(11)

The selected model is

v² + v = u³ - u².

It has good reduction at three, and its reduced point group has exactly five elements. Reduction is injective on a finite rational point group. Consequently, under the explicit hypothesis

[Finite curve.toAffine.Point],

the five visible rational points exhaust the group: the point at infinity and the four affine points with u = 0 or u = 1 and v = 0 or v = -1.

This file deliberately does not manufacture the finiteness hypothesis. Proving Mordell--Weil rank zero (or otherwise proving Finite curve.toAffine.Point) is the remaining unconditional boundary.

instance MazurTorsion.XOneEleven.instFactPrimeOfNatNat_mazurTorsion : Fact (Nat.Prime 3)

def MazurTorsion.XOneEleven.integralCurve : WeierstrassCurve ℤ

The integral model used for reduction at three.

Equations

• MazurTorsion.XOneEleven.integralCurve = { a₁ := 0, a₂ := -1, a₃ := 1, a₄ := 0, a₆ := 0 }

theorem MazurTorsion.XOneEleven.map_integralCurve : (integralCurve.map (algebraMap ℤ ℚ)).toAffine = curve.toAffine

theorem MazurTorsion.XOneEleven.discriminant_integralCurve : integralCurve.Δ = -11

instance MazurTorsion.XOneEleven.instIsEllipticRatCurve : curve.IsElliptic

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

The height-one prime (p) of ℤ.

Equations

• MazurTorsion.XOneEleven.intPrime p = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯

@[simp]

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

@[instance_reducible]

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

Equations

• MazurTorsion.XOneEleven.instDecidableEqQuotientIntIdealAsIdealIntPrime p = (Int.quotientSpanNatEquivZMod p).decidableEq

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

instance MazurTorsion.XOneEleven.instIsEllipticQuotientIntIdealAsIdealIntPrimeOfNatNatRedCurveIntegralCurve : WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve)

theorem MazurTorsion.XOneEleven.good_reduction_at_three : WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve)

The integral model has good reduction at three.

def MazurTorsion.XOneEleven.curveModThree : WeierstrassCurve (ZMod 3)

The concrete reduction over ZMod 3.

Equations

• MazurTorsion.XOneEleven.curveModThree = { a₁ := 0, a₂ := -1, a₃ := 1, a₄ := 0, a₆ := 0 }

instance MazurTorsion.XOneEleven.instIsEllipticZModOfNatNatCurveModThree : curveModThree.IsElliptic

noncomputable def MazurTorsion.XOneEleven.residueThreeAlgEquiv : (ℤ ⧸ (intPrime 3).asIdeal) ≃ₐ[ℤ] ZMod 3

The canonical identification of the integer residue field at three with ZMod 3.

Equations

• MazurTorsion.XOneEleven.residueThreeAlgEquiv = AlgEquiv.ofRingEquiv MazurTorsion.XOneEleven.residueThreeAlgEquiv._proof_1

theorem MazurTorsion.XOneEleven.baseChange_modThree : WeierstrassCurve.toAffine (integralCurve.toAffine.baseChange (ZMod 3)) = curveModThree.toAffine

noncomputable def MazurTorsion.XOneEleven.reducedPointEquiv : (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve).Point ≃+ curveModThree.toAffine.Point

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

Equations

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

instance MazurTorsion.XOneEleven.instFinitePointQuotientIntIdealAsIdealIntPrimeOfNatNatRedCurveIntegralCurve : Finite (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve).Point

theorem MazurTorsion.XOneEleven.card_reducedCurve : Nat.card (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve).Point = 5

The reduction modulo three has exactly five points.

theorem MazurTorsion.XOneEleven.three_mem_prime : 3 ∈ (intPrime 3).asIdeal

theorem MazurTorsion.XOneEleven.three_not_mem_prime_pow_two : 3 ∉ (intPrime 3).asIdeal ^ (3 - 1)

theorem MazurTorsion.XOneEleven.reduction_injective [Finite curve.toAffine.Point] : Function.Injective ⇑(WeierstrassCurve.Affine.redHom (intPrime 3) map_integralCurve)

Reduction at three is injective whenever the rational point group is finite. Finiteness is an explicit input, not a conclusion of this file.

theorem MazurTorsion.XOneEleven.point_card_le_five [Finite curve.toAffine.Point] : Nat.card curve.toAffine.Point ≤ 5

Under the explicit finiteness hypothesis, the rational point group has at most five elements.

def MazurTorsion.XOneEleven.P00 : curve.toAffine.Point

The rational point (0,0).

Equations

• MazurTorsion.XOneEleven.P00 = WeierstrassCurve.Affine.Point.some 0 0 MazurTorsion.XOneEleven.nonsingular_zero_zero✝

def MazurTorsion.XOneEleven.P0n1 : curve.toAffine.Point

The rational point (0,-1).

Equations

• MazurTorsion.XOneEleven.P0n1 = WeierstrassCurve.Affine.Point.some 0 (-1) MazurTorsion.XOneEleven.nonsingular_zero_neg_one✝

def MazurTorsion.XOneEleven.P10 : curve.toAffine.Point

The rational point (1,0).

Equations

• MazurTorsion.XOneEleven.P10 = WeierstrassCurve.Affine.Point.some 1 0 MazurTorsion.XOneEleven.nonsingular_one_zero✝

def MazurTorsion.XOneEleven.P1n1 : curve.toAffine.Point

The rational point (1,-1).

Equations

• MazurTorsion.XOneEleven.P1n1 = WeierstrassCurve.Affine.Point.some 1 (-1) MazurTorsion.XOneEleven.nonsingular_one_neg_one✝

def MazurTorsion.XOneEleven.fiveVisiblePoints : Fin 5 → curve.toAffine.Point

The point at infinity and the four visible affine rational points.

Equations

• MazurTorsion.XOneEleven.fiveVisiblePoints 0 = 0
• MazurTorsion.XOneEleven.fiveVisiblePoints 1 = MazurTorsion.XOneEleven.P00
• MazurTorsion.XOneEleven.fiveVisiblePoints 2 = MazurTorsion.XOneEleven.P0n1
• MazurTorsion.XOneEleven.fiveVisiblePoints 3 = MazurTorsion.XOneEleven.P10
• MazurTorsion.XOneEleven.fiveVisiblePoints 4 = MazurTorsion.XOneEleven.P1n1

theorem MazurTorsion.XOneEleven.fiveVisiblePoints_injective : Function.Injective fiveVisiblePoints

theorem MazurTorsion.XOneEleven.fiveVisiblePoints_bijective [Finite curve.toAffine.Point] : Function.Bijective fiveVisiblePoints

Under the explicit finiteness hypothesis, the five visible points exhaust the rational point group.

theorem MazurTorsion.XOneEleven.point_card_eq_five [Finite curve.toAffine.Point] : Nat.card curve.toAffine.Point = 5

Under the explicit finiteness hypothesis, the rational point group has exactly five elements.

theorem MazurTorsion.XOneEleven.point_abscissa_eq_zero_or_one [Finite curve.toAffine.Point] {U V : ℚ} (hP : curve.toAffine.Nonsingular U V) : U = 0 ∨ U = 1

Under the explicit finiteness hypothesis, every affine rational point has abscissa zero or one.

theorem MazurTorsion.XOneEleven.finite_implies_five_point_classification (hfinite : Finite curve.toAffine.Point) : Nat.card curve.toAffine.Point = 5 ∧ ∀ {U V : ℚ}, curve.toAffine.Nonsingular U V → U = 0 ∨ U = 1

Proposition-level restatement that makes the sole remaining boundary explicit: finiteness of the rational point group implies the complete five-point classification.