Reduction of integral equations at primes

An integral Weierstrass equation has good reduction at a height-one prime when its discriminant lies outside that prime. For equations over ℤ, the valuation residue field at (p) is ZMod p. Thus counting points on the equation over ZMod p gives the order of the reduced point group, and that order annihilates every reduced rational point. These comparisons let finite point counts supply torsion certificates for rational curves.

Over the completion F_u at a height-one prime u with finite residue field, the ring of integers 𝒪[F_u] of the valuative relation is O_u. So an elliptic equation over O_u has good reduction at 𝒪[F_u] (WeierstrassCurve.hasGoodReduction_baseChange_adicCompletion), and its reduction there has as many points as the reduction used by the reduction homomorphism (WeierstrassCurve.natCard_point_reduction_baseChange_adicCompletion).

theorem WeierstrassCurve.isElliptic_integralModel_baseChange {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (E : WeierstrassCurve R) (v : IsDedekindDomain.HeightOneSpectrum R) [Algebra R ↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring] [IsScalarTower R (↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring) K] (hΔ : E.Δ ∉ v.asIdeal) : (integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring) (E.baseChange K)).IsElliptic

An integral equation has good reduction at v when its discriminant lies outside v.

theorem WeierstrassCurve.map_integralModel_baseChange_eq_map (E : WeierstrassCurve ℤ) (v : IsDedekindDomain.HeightOneSpectrum ℤ) {p : ℕ} (f : ZMod p →+* IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring) : (integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring) (E.baseChange ℚ)).map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring) = (E.map (Int.castRingHom (ZMod p))).map f

Reducing the integral model of an equation over ℤ agrees with mapping its reduction over ZMod p along any homomorphism into the valuation residue field.

theorem WeierstrassCurve.card_point_reduction_baseChange (E : WeierstrassCurve ℤ) (v : IsDedekindDomain.HeightOneSpectrum ℤ) (p : ℕ) (hv : v.asIdeal = Ideal.span {↑p}) : Nat.card ((integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring) (E.baseChange ℚ)).map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring)).toAffine.Point = Nat.card (E.map (Int.castRingHom (ZMod p))).toAffine.Point

At the prime (p), the valuation reduction of an integral equation has as many points as its reduction over ZMod p.

theorem WeierstrassCurve.card_nsmul_reductionHom_baseChange_eq_zero (E : WeierstrassCurve ℤ) (v : IsDedekindDomain.HeightOneSpectrum ℤ) (p : ℕ) (hv : v.asIdeal = Ideal.span {↑p}) [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring)] [(integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).valuationSubring) (E.baseChange ℚ)).IsElliptic] (P : (E.baseChange ℚ).toAffine.Point) : Nat.card (E.map (Int.castRingHom (ZMod p))).toAffine.Point • (Affine.Point.reductionHom (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)) P = 0

At good reduction at (p), the order of the point group over ZMod p annihilates the reduction of every rational point of an integral equation.

instance WeierstrassCurve.hasGoodReduction_baseChange_adicCompletion {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] {u : IsDedekindDomain.HeightOneSpectrum A} [Finite (A ⧸ u.asIdeal)] (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [C.IsElliptic] : HasGoodReduction (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).integer) (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u))

An elliptic equation over O_u has good reduction at the ring of integers 𝒪[F_u] of the valuative relation of F_u, which is O_u.

theorem WeierstrassCurve.natCard_point_reduction_baseChange_adicCompletion {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] {u : IsDedekindDomain.HeightOneSpectrum A} [Finite (A ⧸ u.asIdeal)] (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [C.IsElliptic] : Nat.card (reduction (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).integer) (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u))).toAffine.Point = Nat.card ((integralModel (↥Valued.v.valuationSubring) (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u))).map (IsLocalRing.residue ↥Valued.v.valuationSubring)).toAffine.Point

The reduction at 𝒪[F_u] of an elliptic equation over O_u has as many points as its reduction at Valued.v.valuationSubring, the ring used by the reduction homomorphism.