Documentation

MazurTorsion.EllipticCurve.IntegerPrimeSpecialization

Integer-prime residue fields and formal-kernel torsion #

The exact-pinned EllipticCurves reduction library proves that the formal kernel over an adic completion contains no nonzero torsion when the absolute ramification index is less than p - 1. This file discharges that arithmetic condition for the two unramified completions of ℚ used by the formal-immersion route, at p = 5 and p = 11. It also exposes the canonical integer prime and residue-field identification at p = 3, consumed by explicit fixed-curve reductions.

These statements do not assume good reduction: they concern the formal filtration attached to an arbitrary integral Weierstrass equation whose generic fibre is elliptic. Thus they are the part of torsion specialization which can be checked before a Neron special fibre and its component map have been constructed.

def MazurTorsion.IntegerPrimeSpecialization.integerPrime (p : ℕ) [Fact (Nat.Prime p)] :

IsDedekindDomain.HeightOneSpectrum ℤ

The height-one prime (p) of ℤ.

Equations

MazurTorsion.IntegerPrimeSpecialization.integerPrime p = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯

Instances For

@[simp]

theorem MazurTorsion.IntegerPrimeSpecialization.integerPrime_asIdeal (p : ℕ) [Fact (Nat.Prime p)] :

(integerPrime p).asIdeal = Ideal.span {↑p}

def MazurTorsion.IntegerPrimeSpecialization.atThree :

IsDedekindDomain.HeightOneSpectrum ℤ

The integer height-one prime above three, with its primality witness fixed internally.

Equations

MazurTorsion.IntegerPrimeSpecialization.atThree = MazurTorsion.IntegerPrimeSpecialization.integerPrime 3

Instances For

def MazurTorsion.IntegerPrimeSpecialization.atFive :

IsDedekindDomain.HeightOneSpectrum ℤ

The integer height-one prime above five, with its primality witness fixed internally.

Equations

MazurTorsion.IntegerPrimeSpecialization.atFive = MazurTorsion.IntegerPrimeSpecialization.integerPrime 5

Instances For

def MazurTorsion.IntegerPrimeSpecialization.atEleven :

IsDedekindDomain.HeightOneSpectrum ℤ

The integer height-one prime above eleven, with its primality witness fixed internally.

Equations

MazurTorsion.IntegerPrimeSpecialization.atEleven = MazurTorsion.IntegerPrimeSpecialization.integerPrime 11

Instances For

@[simp]

theorem MazurTorsion.IntegerPrimeSpecialization.atThree_asIdeal :

atThree.asIdeal = Ideal.span {3}

@[simp]

theorem MazurTorsion.IntegerPrimeSpecialization.atFive_asIdeal :

atFive.asIdeal = Ideal.span {5}

@[simp]

theorem MazurTorsion.IntegerPrimeSpecialization.atEleven_asIdeal :

atEleven.asIdeal = Ideal.span {11}

theorem MazurTorsion.IntegerPrimeSpecialization.three_mem_atThree :

3 ∈ atThree.asIdeal

theorem MazurTorsion.IntegerPrimeSpecialization.three_not_mem_atThree_pow_two :

3 ∉ atThree.asIdeal ^ (3 - 1)

theorem MazurTorsion.IntegerPrimeSpecialization.five_mem_atFive :

5 ∈ atFive.asIdeal

theorem MazurTorsion.IntegerPrimeSpecialization.five_not_mem_atFive_pow_four :

5 ∉ atFive.asIdeal ^ (5 - 1)

theorem MazurTorsion.IntegerPrimeSpecialization.eleven_mem_atEleven :

11 ∈ atEleven.asIdeal

theorem MazurTorsion.IntegerPrimeSpecialization.eleven_not_mem_atEleven_pow_ten :

11 ∉ atEleven.asIdeal ^ (11 - 1)

@[instance_reducible]

instance MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtThree :

DecidableEq (ℤ ⧸ atThree.asIdeal)

Equations

MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtThree = (Int.quotientSpanNatEquivZMod 3).decidableEq

@[instance_reducible]

instance MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtFive :

DecidableEq (ℤ ⧸ atFive.asIdeal)

Equations

MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtFive = (Int.quotientSpanNatEquivZMod 5).decidableEq

@[instance_reducible]

instance MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtEleven :

DecidableEq (ℤ ⧸ atEleven.asIdeal)

Equations

MazurTorsion.IntegerPrimeSpecialization.instDecidableEqQuotientIntIdealAsIdealAtEleven = (Int.quotientSpanNatEquivZMod 11).decidableEq

noncomputable def MazurTorsion.IntegerPrimeSpecialization.residueThreeAlgEquiv :

(ℤ ⧸ atThree.asIdeal) ≃ₐ[ℤ ] ZMod 3

The residue field at the integer prime three, identified with ZMod 3.

Equations

MazurTorsion.IntegerPrimeSpecialization.residueThreeAlgEquiv = AlgEquiv.ofRingEquiv MazurTorsion.IntegerPrimeSpecialization.residueThreeAlgEquiv._proof_1

Instances For

noncomputable def MazurTorsion.IntegerPrimeSpecialization.residueFiveAlgEquiv :

(ℤ ⧸ atFive.asIdeal) ≃ₐ[ℤ ] ZMod 5

The residue field at the integer prime five, identified with ZMod 5.

Equations

MazurTorsion.IntegerPrimeSpecialization.residueFiveAlgEquiv = AlgEquiv.ofRingEquiv MazurTorsion.IntegerPrimeSpecialization.residueFiveAlgEquiv._proof_1

Instances For

noncomputable def MazurTorsion.IntegerPrimeSpecialization.residueElevenAlgEquiv :

(ℤ ⧸ atEleven.asIdeal) ≃ₐ[ℤ ] ZMod 11

The residue field at the integer prime eleven, identified with ZMod 11.

Equations

MazurTorsion.IntegerPrimeSpecialization.residueElevenAlgEquiv = AlgEquiv.ofRingEquiv MazurTorsion.IntegerPrimeSpecialization.residueElevenAlgEquiv._proof_1

Instances For

theorem MazurTorsion.IntegerPrimeSpecialization.natCast_mem_completion_maximalIdeal_pow_iff (v : IsDedekindDomain.HeightOneSpectrum ℤ) {p n : ℕ} :

↑p ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v) ^ n ↔ ↑p ∈ v.asIdeal ^ n

Membership in the maximal-ideal filtration of the completion is detected before completion. This is the integer-prime specialization of the exact-pin comparison theorem.

theorem MazurTorsion.IntegerPrimeSpecialization.five_mem_completion_maximalIdeal :

5 ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atFive)

theorem MazurTorsion.IntegerPrimeSpecialization.five_not_mem_completion_maximalIdeal_pow_four :

5 ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atFive) ^ (5 - 1)

theorem MazurTorsion.IntegerPrimeSpecialization.eleven_mem_completion_maximalIdeal :

11 ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atEleven)

theorem MazurTorsion.IntegerPrimeSpecialization.eleven_not_mem_completion_maximalIdeal_pow_ten :

11 ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atEleven) ^ (11 - 1)

At the unramified prime five, a torsion point in the formal kernel is zero. The integral model need not have good reduction.

At the unramified prime eleven, a torsion point in the formal kernel is zero. The integral model need not have good reduction.

theorem MazurTorsion.IntegerPrimeSpecialization.torsion_eq_of_sub_mem_formalKernel_atFive {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atFive)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atFive)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atFive)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atFive)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atFive)] {P Q : W.Point} (hP : IsOfFinAddOrder P) (hQ : IsOfFinAddOrder Q) (hPQ : P - Q ∈ WeierstrassCurve.Affine.filtration hW 0) :

P = Q

Two torsion points at five agree if their difference lies in the formal kernel. This is the collision statement consumed by torsion specialization.

theorem MazurTorsion.IntegerPrimeSpecialization.torsion_eq_of_sub_mem_formalKernel_atEleven {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atEleven)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atEleven)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ atEleven)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atEleven)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ atEleven)] {P Q : W.Point} (hP : IsOfFinAddOrder P) (hQ : IsOfFinAddOrder Q) (hPQ : P - Q ∈ WeierstrassCurve.Affine.filtration hW 0) :

P = Q

Two torsion points at eleven agree if their difference lies in the formal kernel.