Affine charts for the first Tate blowup

Let W be an integral Weierstrass equation over a discrete valuation ring and suppose that all five coefficients vanish on the special fibre. After choosing a uniformizer ϖ, write each coefficient as ϖ bᵢ. This file records the quotients obtained after removing one exceptional factor on the three standard affine charts of the blowup of the closed point (ϖ, X, Y).

Mathlib does not yet provide a scheme-theoretic blowup API at the pinned revision. Accordingly, the interface here makes no universal-property or regularity claim: it gives the exact three coordinate substitutions, factors the total transform once by the exceptional coordinate, and computes the resulting equations on each exceptional chart. If the original equation has higher order at the center, this one-factor quotient need not yet be the scheme-theoretic strict transform. These identities are the reusable algebraic input for the subsequent valuation case split in Tate's algorithm.

structure MazurTorsion.EllipticCurve.FirstBlowupCoefficientData {R : Type u} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) : Type u

Quotients bᵢ witnessing aᵢ = ϖ bᵢ for an integral Weierstrass equation.

• b₁ : R
• b₂ : R
• b₃ : R
• b₄ : R
• b₆ : R
• a₁_eq : W.a₁ = ϖ * self.b₁
• a₂_eq : W.a₂ = ϖ * self.b₂
• a₃_eq : W.a₃ = ϖ * self.b₃
• a₄_eq : W.a₄ = ϖ * self.b₄
• a₆_eq : W.a₆ = ϖ * self.b₆

def MazurTorsion.EllipticCurve.FirstBlowupCoefficientData.uniformizerChartQuotient {R : Type u} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (D : FirstBlowupCoefficientData W ϖ) (X₁ Y₁ : R) : R

The one-factor quotient on the chart where the uniformizer is the exceptional coordinate, obtained from X = ϖ X₁ and Y = ϖ Y₁ after removing one factor of ϖ.

Equations

• D.uniformizerChartQuotient X₁ Y₁ = ϖ * Y₁ ^ 2 + ϖ ^ 2 * D.b₁ * X₁ * Y₁ + ϖ * D.b₃ * Y₁ - (ϖ ^ 2 * X₁ ^ 3 + ϖ ^ 2 * D.b₂ * X₁ ^ 2 + ϖ * D.b₄ * X₁ + D.b₆)

theorem MazurTorsion.EllipticCurve.FirstBlowupCoefficientData.evalEval_polynomial_uniformizerChart_factorization {R : Type u} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (D : FirstBlowupCoefficientData W ϖ) (X₁ Y₁ : R) : Polynomial.evalEval (ϖ * X₁) (ϖ * Y₁) W.toAffine.polynomial = ϖ * D.uniformizerChartQuotient X₁ Y₁

Exact total-transform factorization on the uniformizer-exceptional chart.

theorem MazurTorsion.EllipticCurve.FirstBlowupCoefficientData.map_uniformizerChartQuotient_of_map_uniformizer_eq_zero {R : Type u} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {S : Type v} [CommRing S] (D : FirstBlowupCoefficientData W ϖ) (f : R →+* S) (hϖ : f ϖ = 0) (X₁ Y₁ : R) : f (D.uniformizerChartQuotient X₁ Y₁) = -f D.b₆

On the exceptional divisor of the uniformizer chart, the one-factor quotient restricts to the negative residue of b₆.

theorem MazurTorsion.EllipticCurve.FirstBlowupCoefficientData.residue_b₆_ne_zero_iff_a₆_not_mem_maximalIdeal_sq {R : Type u} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] (hϖ : Irreducible ϖ) (D : FirstBlowupCoefficientData W ϖ) : (IsLocalRing.residue R) D.b₆ ≠ 0 ↔ W.a₆ ∉ IsLocalRing.maximalIdeal R ^ 2

The exceptional restriction b₆ is nonzero precisely in the order-one branch a₆ ∈ 𝔪 \ 𝔪². This is the first valuation split following the one-factor chart factorizations.

theorem MazurTorsion.EllipticCurve.FirstBlowupCoefficientData.residue_b₄_ne_zero_iff_a₄_not_mem_maximalIdeal_sq {R : Type u} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] (hϖ : Irreducible ϖ) (D : FirstBlowupCoefficientData W ϖ) : (IsLocalRing.residue R) D.b₄ ≠ 0 ↔ W.a₄ ∉ IsLocalRing.maximalIdeal R ^ 2

The exceptional restriction b₄ is nonzero precisely when a₄ ∈ 𝔪 \ 𝔪². This is the coefficient split used after the order-one b₆ branch has been excluded.

theorem MazurTorsion.EllipticCurve.cuspidalShortCurve_nonsingular_of_ne_origin {F : Type u_1} [Field F] [Invertible 2] [Invertible 3] {x y : F} (heq : (cuspidalShortCurve F).toAffine.Equation x y) (hne : x ≠ 0 ∨ y ≠ 0) : (cuspidalShortCurve F).toAffine.Nonsingular x y

Every affine point of the standard cusp away from its origin is nonsingular when two and three are invertible.

structure MazurTorsion.EllipticCurve.FirstBlowupEquationCharts {R : Type u} [CommRing R] (W : WeierstrassCurve R) [IsDomain R] [IsDiscreteValuationRing R] : Type u

The three affine one-factor equation quotients attached to a choice of DVR uniformizer.

• uniformizer : R
• uniformizer_irreducible : Irreducible self.uniformizer
• coefficients : FirstBlowupCoefficientData W self.uniformizer

theorem MazurTorsion.EllipticCurve.FirstBlowupEquationCharts.evalEval_polynomial_uniformizerChart_factorization {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} (B : FirstBlowupEquationCharts W) (X₁ Y₁ : R) : Polynomial.evalEval (B.uniformizer * X₁) (B.uniformizer * Y₁) W.toAffine.polynomial = B.uniformizer * B.coefficients.uniformizerChartQuotient X₁ Y₁

The uniformizer-chart factorization exposed directly from a bundled chart choice.

theorem MazurTorsion.EllipticCurve.FirstBlowupEquationCharts.residue_b₆_ne_zero_iff_a₆_not_mem_maximalIdeal_sq {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} (B : FirstBlowupEquationCharts W) : (IsLocalRing.residue R) B.coefficients.b₆ ≠ 0 ↔ W.a₆ ∉ IsLocalRing.maximalIdeal R ^ 2

For a bundled chart choice, nonvanishing of the exceptional b₆ is exactly failure of a₆ to lie in the square of the maximal ideal.

theorem MazurTorsion.EllipticCurve.FirstBlowupEquationCharts.residue_b₄_ne_zero_iff_a₄_not_mem_maximalIdeal_sq {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} (B : FirstBlowupEquationCharts W) : (IsLocalRing.residue R) B.coefficients.b₄ ≠ 0 ↔ W.a₄ ∉ IsLocalRing.maximalIdeal R ^ 2

For bundled first-blowup data, nonvanishing of the exceptional b₄ is exactly failure of a₄ to lie in the square of the maximal ideal.

theorem MazurTorsion.EllipticCurve.FirstBlowupEquationCharts.not_both_mem_maximalIdeal_of_residue_b₆_ne_zero {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} (B : FirstBlowupEquationCharts W) [W.IsShortNF] {x y : R} (heq : W.toAffine.Equation x y) (hb₆ : (IsLocalRing.residue R) B.coefficients.b₆ ≠ 0) : ¬(x ∈ IsLocalRing.maximalIdeal R ∧ y ∈ IsLocalRing.maximalIdeal R)

In the order-one b₆ ≠ 0 branch, an integral point on a short equation cannot have both affine coordinates reduce to the cusp.

theorem MazurTorsion.EllipticCurve.FirstBlowupEquationCharts.nonsingular_reduction_of_equation_of_residue_b₆_ne_zero {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} (B : FirstBlowupEquationCharts W) [W.IsShortNF] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W.map (IsLocalRing.residue R) = cuspidalShortCurve (IsLocalRing.ResidueField R)) {x y : R} (heq : W.toAffine.Equation x y) (hb₆ : (IsLocalRing.residue R) B.coefficients.b₆ ≠ 0) : (W.map (IsLocalRing.residue R)).toAffine.Nonsingular ((IsLocalRing.residue R) x) ((IsLocalRing.residue R) y)

In the order-one b₆ ≠ 0 branch, every integral affine point on the bundled short equation specializes to a nonsingular point of its standard cuspidal special fibre.

theorem MazurTorsion.EllipticCurve.nonempty_firstBlowupEquationCharts_of_coefficients_mem_maximalIdeal {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (W : WeierstrassCurve R) (ha₁ : W.a₁ ∈ IsLocalRing.maximalIdeal R) (ha₂ : W.a₂ ∈ IsLocalRing.maximalIdeal R) (ha₃ : W.a₃ ∈ IsLocalRing.maximalIdeal R) (ha₄ : W.a₄ ∈ IsLocalRing.maximalIdeal R) (ha₆ : W.a₆ ∈ IsLocalRing.maximalIdeal R) : Nonempty (FirstBlowupEquationCharts W)

Maximal-ideal divisibility of all five coefficients constructs the three affine first-blowup charts, with no extra choice of coefficient quotients required from the caller.