Additivity of reduction to the nonsingular locus

This file proves that the canonical nonsingular-reduction domain of an integral local Weierstrass equation is an additive subgroup and that coordinatewise reduction is a homomorphism on it. The proof adapts the exact-pinned good-reduction argument from EllipticCurves.WeierstrassFormalGroup.Reduction: wherever that argument used smoothness of the whole special cubic, we instead use the nonsingularity carried by HasNonsingularReduction.

The two substantive local steps are:

• equal nonsingular coordinate reductions differ by the formal kernel; and
• translation by a formal-kernel point preserves nonsingular coordinate reduction.

Together with the already checked slope calculation away from the reduced anti-diagonal, these give unconditional additivity on the canonical domain. No Neron model or good-reduction hypothesis is used.

@[instance_reducible]

noncomputable def WeierstrassCurve.Affine.instDecidableEqResidueFieldSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_mazurTorsion_1 {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} : DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

Equations

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

theorem WeierstrassCurve.Affine.add_mem_filtration_of_slope {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {x₁ y₁ x₂ y₂ : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxx : x₁ ≠ x₂) (hx₁ : Valued.v x₁ ≤ 1) (hx₂ : Valued.v x₂ ≤ 1) (hs : WithZero.exp 1 ≤ Valued.v ((y₁ - y₂) / (x₁ - x₂))) : Point.some x₁ y₁ h₁ + Point.some x₂ y₂ h₂ ∈ filtration hW 0

Two affine points with integral abscissas add into the formal kernel when their secant slope has a pole of order at least one. The distinct-abscissa premise selects the ordinary secant formula; vertical and equal-point cases are intentionally left to the caller.

theorem WeierstrassCurve.Affine.add_self_mem_filtration_of_slope {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {x₀ y₀ : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h₀ : W.Nonsingular x₀ y₀) (hx₀ : Valued.v x₀ ≤ 1) (hψ : y₀ ≠ W.negY x₀ y₀) (hs : WithZero.exp 1 ≤ Valued.v (W.slope x₀ x₀ y₀ y₀)) : Point.some x₀ y₀ h₀ + Point.some x₀ y₀ h₀ ∈ filtration hW 0

An affine point with integral abscissa whose tangent slope has a pole of order at least one doubles into the formal kernel. This valuation-only statement is useful for the marked-point branches of Tate's algorithm and does not assume that the source has nonsingular reduction.

theorem WeierstrassCurve.Affine.sub_mem_filtration_of_nonsingularReduction_eq {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {P Q : W.Point} (hP : HasNonsingularReduction hW P) (hQ : HasNonsingularReduction hW Q) (hPQ : nonsingularReduction hW ⟨P, hP⟩ = nonsingularReduction hW ⟨Q, hQ⟩) : P - Q ∈ filtration hW 0

Equal coordinatewise reductions in the nonsingular locus differ by the exact formal filtration. This is the singular-special-fibre version of the exact-pin congruence criterion; only nonsingularity of the displayed common reduction is used.

theorem WeierstrassCurve.Affine.nonsingularReduction_add_of_mem_filtration_left {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {P Q : W.Point} (hP : P ∈ filtration hW 0) (hQ : HasNonsingularReduction hW Q) : ∃ (hPQ : HasNonsingularReduction hW (P + Q)), nonsingularReduction hW ⟨P + Q, hPQ⟩ = nonsingularReduction hW ⟨Q, hQ⟩

Translation by a point of the formal kernel preserves the canonical nonsingular-reduction domain and does not change coordinatewise reduction.

theorem WeierstrassCurve.Affine.nonsingularReduction_isAdditive {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] : NonsingularReductionIsAdditive hW

Coordinatewise reduction to the nonsingular locus is additive on its canonical domain. This discharges the sole group-law premise left by NonsingularReductionIsAdditive.

@[instance_reducible]

noncomputable def MazurTorsion.EllipticCurve.instDecidableEqResidueFieldSubtypeAdicCompletionIntRatAtFiveMemValuationSubringAdicCompletionIntegers_1 : DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive))

Equations

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

@[instance_reducible]

noncomputable def MazurTorsion.EllipticCurve.instDecidableEqResidueFieldSubtypeAdicCompletionIntRatAtElevenMemValuationSubringAdicCompletionIntegers_1 : DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven))

Equations

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

noncomputable def MazurTorsion.EllipticCurve.TameAdditiveReductionDataAtFive.ofCanonicalNonsingularReduction {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atFive)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)} {hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atFive)) = W} [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atFive)] (especial : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)) (hcomponent : Nat.card (W.Point ⧸ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯) ≤ 4) : TameAdditiveReductionDataAtFive hW

Construct the five-adic tame-additive handoff from canonical nonsingular reduction. The group-law premise is discharged by nonsingularReduction_isAdditive; the remaining arguments are exactly the special-cubic classification and component bound.

Equations

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

noncomputable def MazurTorsion.EllipticCurve.TameAdditiveReductionDataAtEleven.ofCanonicalNonsingularReduction {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)} {hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)) = W} [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)] (especial : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (hcomponent : Nat.card (W.Point ⧸ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯) ≤ 4) : TameAdditiveReductionDataAtEleven hW

The identical canonical construction at eleven, for the order-35 additive branch.

Equations

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