The marked simple-root branch of the exceptional star cubic

For an integral short equation with a₄ ∈ 𝔪² and a₆ ∈ 𝔪³, a point specializing to the cusp has coordinates x = ϖ X and y ∈ 𝔪². Removing the common factor ϖ³ from its equation gives the pointwise exceptional-cubic relation

X̄³ + Ā X̄ + B̄ = 0,

where a₄ = ϖ² A and a₆ = ϖ³ B. This file proves exactly the branch needed downstream: if the derivative 3 X̄² + Ā at that marked root is nonzero, then the double of the marked point has canonical nonsingular reduction.

The proof uses only the selected equation and its tangent formula. It does not identify a Kodaira symbol, construct a regular model, classify all roots, or assert component incidence or cardinality.

structure MazurTorsion.EllipticCurve.MarkedExceptionalCubicData {O : Type u} {F : Type v} [CommRing O] [IsLocalRing O] [Field F] [Algebra O F] (W₀ : WeierstrassCurve O) (W : WeierstrassCurve.Affine F) (P : W.Point) : Type u

Integral coordinates and coefficient quotients defining the exceptional cubic at one marked point. The root assertion is only for the displayed marked quotient X; no assertion about any other root is bundled.

• uniformizer : O
• uniformizer_irreducible : Irreducible self.uniformizer
• x : O
• y : O
• nonsingular : W.Nonsingular ((algebraMap O F) self.x) ((algebraMap O F) self.y)
• point_eq : P = WeierstrassCurve.Affine.Point.some ((algebraMap O F) self.x) ((algebraMap O F) self.y) ⋯
• X : O
• A : O
• B : O
• x_eq : self.x = self.uniformizer * self.X
• a₄_eq : W₀.a₄ = self.uniformizer ^ 2 * self.A
• a₆_eq : W₀.a₆ = self.uniformizer ^ 3 * self.B
• y_mem_maximalIdeal_sq : self.y ∈ IsLocalRing.maximalIdeal O ^ 2
• exceptionalCubic_root : (IsLocalRing.residue O) self.X ^ 3 + (IsLocalRing.residue O) self.A * (IsLocalRing.residue O) self.X + (IsLocalRing.residue O) self.B = 0

noncomputable def MazurTorsion.EllipticCurve.MarkedExceptionalCubicData.derivativeResidue {O : Type u} {F : Type v} [CommRing O] [IsLocalRing O] [Field F] [Algebra O F] {W₀ : WeierstrassCurve O} {W : WeierstrassCurve.Affine F} {P : W.Point} (D : MarkedExceptionalCubicData W₀ W P) : IsLocalRing.ResidueField O

The derivative of the exceptional cubic at the bundled marked root.

Equations

• D.derivativeResidue = (IsLocalRing.residue O) (3 * D.X ^ 2 + D.A)

noncomputable def MazurTorsion.EllipticCurve.markedExceptionalCubicData_of_cusp {O : Type u} {F : Type v} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [Field F] [Algebra O F] (W₀ : WeierstrassCurve O) [W₀.IsShortNF] (W : WeierstrassCurve.Affine F) (ϖ : O) (hϖ : Irreducible ϖ) {x y X A B : O} (heq : W₀.toAffine.Equation x y) (hxy : W.Nonsingular ((algebraMap O F) x) ((algebraMap O F) y)) (hx : x ∈ IsLocalRing.maximalIdeal O) (hy : y ∈ IsLocalRing.maximalIdeal O) (ha₄ : W₀.a₄ ∈ IsLocalRing.maximalIdeal O ^ 2) (ha₆ : W₀.a₆ ∈ IsLocalRing.maximalIdeal O ^ 3) (hx_eq : x = ϖ * X) (ha₄_eq : W₀.a₄ = ϖ ^ 2 * A) (ha₆_eq : W₀.a₆ = ϖ ^ 3 * B) : MarkedExceptionalCubicData W₀ W (WeierstrassCurve.Affine.Point.some ((algebraMap O F) x) ((algebraMap O F) y) hxy)

A cusp-specializing integral point with the displayed coefficient quotients determines a marked root of the exceptional cubic. The square-depth assertion for y is the checked weighted coordinate consequence of the short equation.

Equations

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

theorem MazurTorsion.EllipticCurve.exists_markedExceptionalCubicData_of_not_hasNonsingularReduction {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.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)] [W₀.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (ϖ : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hϖ : Irreducible ϖ) (ha₄ : W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 2) (ha₆ : W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ 3) (P : W.Point) (hP : ¬WeierstrassCurve.Affine.HasNonsingularReduction hW P) : ∃ (D : MarkedExceptionalCubicData W₀ W P), D.uniformizer = ϖ

A local point outside canonical nonsingular reduction supplies integral coordinates at the cusp and hence marked exceptional-cubic data for any chosen uniformizer. The returned data uses that exact uniformizer.

theorem MazurTorsion.EllipticCurve.two_nsmul_mem_nonsingularReductionSubgroup_of_markedExceptionalCubic_simpleRoot {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [W₀.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (D : MarkedExceptionalCubicData W₀ W P) (hsimple : D.derivativeResidue ≠ 0) : 2 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

If the bundled marked exceptional root is simple, the double of the marked local point has canonical nonsingular reduction. A deep ordinate makes the tangent slope have a pole; an ordinate of exact depth two makes the tangent slope a unit and the double reduces away from the cusp.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_markedExceptionalCubic_simpleRoot {R : Type u} [CommRing R] [IsDedekindDomain R] {K : Type v} [Field K] [Algebra R K] [IsFractionRing R K] [CharZero K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} {P : W.Point} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [W₀.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (D : MarkedExceptionalCubicData W₀ W P) (hsimple : D.derivativeResidue ≠ 0) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The simple-root branch supplies the exponent twelve required by the arithmetic consumers: it is six times the checked double.