Integral models of Weierstrass curves over a local field

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

Let K be the fraction field of a Dedekind domain, v a height-one prime, and K_v the completion. WeierstrassCurve.Affine.exists_variableChange_map_eq shows that every Weierstrass curve over K_v has an integral model: after an admissible change of variables its coefficients lie in 𝒪_v.

This feeds the structure theorem WeierstrassCurve.Affine.exists_finiteIndex_addSubgroup_equiv_adicCompletionIntegers (the group E(K_v) has a finite-index subgroup isomorphic to (𝒪_v, +)), which lives in EllipticCurves.WeierstrassFormalGroup.

theorem WeierstrassCurve.Affine.exists_variableChange_map_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) : ∃ (C : VariableChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)), W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = C • W

Every Weierstrass curve over K_v has an integral model: after an admissible change of variables, the coefficients lie in 𝒪_v.