Rational points on the X₀(49) model

The two-isogeny descent proves that the rational point group of

y² = x(x² + 21x + 112)

is finite with no point of order four. Good reduction at three bounds the cardinality by four, and an element of order three would force the cardinality to be at least six. Hence every rational point is killed by two, and the group is exactly {0, (0,0)}: the two rational cusps of X₀(49).

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

def MazurTorsion.XZeroFortyNine.integralCurve : WeierstrassCurve ℤ

The integral model used for reduction at three.

Equations

• MazurTorsion.XZeroFortyNine.integralCurve = { a₁ := 0, a₂ := 21, a₃ := 0, a₄ := 112, a₆ := 0 }

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

theorem MazurTorsion.XZeroFortyNine.discriminant_integralCurve : integralCurve.Δ = -1404928

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

The height-one prime (p) of ℤ.

Equations

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

@[simp]

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

@[instance_reducible]

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

Equations

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

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

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

The concrete reduction over ZMod 3.

Equations

• MazurTorsion.XZeroFortyNine.curveModThree = { a₁ := 0, a₂ := 21, a₃ := 0, a₄ := 112, a₆ := 0 }

instance MazurTorsion.XZeroFortyNine.instIsEllipticZModOfNatNatCurveModThree : curveModThree.IsElliptic

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

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

Equations

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

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

noncomputable def MazurTorsion.XZeroFortyNine.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.XZeroFortyNine.instFinitePointQuotientIntIdealAsIdealIntPrimeOfNatNatRedCurveIntegralCurve : Finite (WeierstrassCurve.Affine.redCurve (intPrime 3) integralCurve).Point

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

The reduction modulo three has exactly four points.

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

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

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

Reduction at three is injective on the finite rational point group.

theorem MazurTorsion.XZeroFortyNine.point_card_le_four : Nat.card curve.toAffine.Point ≤ 4

There are at most four rational points on the X₀(49) model.

theorem MazurTorsion.XZeroFortyNine.point_eq_zero_or_T (P : curve.toAffine.Point) : P = 0 ∨ P = T

Every rational point of the X₀(49) model is 0 or (0,0): the two rational cusps.