The identity component in the first tame Tate branch

For an integral short Weierstrass equation whose special fibre is the standard cusp, the first case split in Tate's algorithm is whether a₆ lies in the square of the maximal ideal. If it does not, the equation has Kodaira type II. This file proves the exact pointwise consequence needed by the torsion argument without naming a Kodaira symbol or constructing a Néron model: every local point has nonsingular coordinate reduction, so the canonical nonsingular-reduction subgroup is the whole point group.

The affine calculation is supplied by TateFirstBlowup. Points in the formal kernel satisfy the canonical reduction predicate by definition; every other point has integral coordinates, and the order-one affine calculation shows that its specialization avoids the cusp.

theorem MazurTorsion.EllipticCurve.hasNonsingularReduction_of_firstBlowup_residue_b₆_ne_zero {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] (B : FirstBlowupEquationCharts W₀) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₆ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₆ ≠ 0) (P : W.Point) : WeierstrassCurve.Affine.HasNonsingularReduction hW P

In the order-one branch of the normalized tame equation, every local point belongs to the canonical nonsingular-reduction domain.

theorem MazurTorsion.EllipticCurve.nonsingularReductionSubgroup_eq_top_of_firstBlowup_residue_b₆_ne_zero {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] (B : FirstBlowupEquationCharts W₀) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₆ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₆ ≠ 0) : WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯ = ⊤

In the order-one branch, canonical nonsingular reduction is defined on the entire local point group. This is the precise identity-component statement consumed by the marked torsion argument.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_firstBlowup_residue_b₆_ne_zero {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] (B : FirstBlowupEquationCharts W₀) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₆ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₆ ≠ 0) (P : W.Point) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

Every multiplier of a local point, in particular the uniform tame exponent twelve, lies in the canonical identity subgroup in the order-one branch.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_nonsingularReductionSubgroup_of_integralVariableChange_firstBlowup {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) (C : WeierstrassCurve.VariableChange ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hWC : (C • W₀).map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) • W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [(C • W₀).IsShortNF] (B : FirstBlowupEquationCharts (C • W₀)) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hspecial : (C • W₀).map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) = cuspidalShortCurve (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) (hb₆ : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) B.coefficients.b₆ ≠ 0) (P : W.Point) : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯

The order-one component conclusion on an integrally normalized equation transports back to the original integral equation. The point equivalence is oriented from the transformed generic fibre to the original one, so the normalized marked point is the inverse image of P.