Canonical nonsingular reduction under integral changes of variables

An admissible change of variables over the completed valuation ring identifies both the formal kernel and the nonsingular locus of the special fibre. Consequently it transports the canonical nonsingular-reduction predicate and subgroup on the generic fibres.

The proof treats the formal-kernel gate separately from affine reduction. At a pole, adding an integral translation does not change the valuation of the x-coordinate. Away from the formal kernel, all coordinates are integral; reducing the integral coordinate formula then turns the claim into variableChange_nonsingular on the special fibre.

theorem WeierstrassCurve.Affine.hasNonsingularReduction_equivVariableChange_iff {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) (C : 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)] (P : (toAffine (C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) • W)).Point) : HasNonsingularReduction hWC P ↔ HasNonsingularReduction hW ((Point.equivVariableChange W (C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))) P)

An integral admissible change of variables transports the canonical nonsingular-reduction predicate. The displayed generic-fibre equality records that the integral transformed equation is the model used to define reduction on the transformed point group.

theorem WeierstrassCurve.Affine.equivVariableChange_mem_nonsingularReductionSubgroup_iff {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 : 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 : 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)] (P : (toAffine (C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) • W)).Point) : P ∈ nonsingularReductionSubgroup hWC ⋯ ↔ (Point.equivVariableChange W (C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))) P ∈ nonsingularReductionSubgroup hW ⋯

The point-group equivalence from an integral change identifies the two canonical nonsingular-reduction subgroups.

theorem WeierstrassCurve.Affine.nsmul_equivVariableChange_symm_mem_nonsingularReductionSubgroup_iff {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 : 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 : 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)] (n : ℕ) (P : W.Point) : n • (Point.equivVariableChange W (C.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))).symm P ∈ nonsingularReductionSubgroup hWC ⋯ ↔ n • P ∈ nonsingularReductionSubgroup hW ⋯

A marked component multiple can be checked before or after an integral admissible change. This is the downstream form used when a normalized Tate equation is accompanied by the inverse image of a marked point on the original equation.