Reduction of Weierstrass curves over local fields

This file defines reduction of Weierstrass curves over local fields, or more generally, fraction fields of discrete valuation rings.

Main definitions

• IsIntegral: a predicate expressing that a given Weierstrass equation has integral coefficients.
• IsMinimal: a predicate expressing that a given Weierstrass equation has minimal valuation of discriminant among all isomorphic integral Weierstrass equations.
• reduction: the reduction of a Weierstrass curve given by a minimal Weierstrass equation, which is a Weierstrass curve over the residue field.
• IsGoodReduction: a predicate expressing that a given minimal Weierstrass equation has valuation of its discriminant equal to zero.

Main statements

• exists_isIntegral: any Weierstrass curve is isomorphic to one given by an integral Weierstrass equation.
• exists_isMinimal: any Weierstrass curve is isomorphic to one given by a minimal Weierstrass equation.

References

• J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, weierstrass equation, minimal weierstrass equation, reduction

class WeierstrassCurve.IsIntegral (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) : Prop

A Weierstrass equation over the fraction field K is integral if it has coefficients in the ring R.

• integral : ∃ (W_int : WeierstrassCurve R), W = W_int.baseChange K

theorem WeierstrassCurve.isIntegral_iff (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) : IsIntegral R W ↔ ∃ (W_int : WeierstrassCurve R), W = W_int.baseChange K

noncomputable def WeierstrassCurve.integralModel (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) [hW : IsIntegral R W] : WeierstrassCurve R

An integral model of an integral Weierstrass curve.

Equations

• WeierstrassCurve.integralModel R W = ⋯.choose

theorem WeierstrassCurve.baseChange_integralModel_eq (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) [hW : IsIntegral R W] : (integralModel R W).baseChange K = W

theorem WeierstrassCurve.isIntegral_of_exists_lift (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {W : WeierstrassCurve K} (h₁ : ∃ (r₁ : R), (algebraMap R K) r₁ = W.a₁) (h₂ : ∃ (r₂ : R), (algebraMap R K) r₂ = W.a₂) (h₃ : ∃ (r₃ : R), (algebraMap R K) r₃ = W.a₃) (h₄ : ∃ (r₄ : R), (algebraMap R K) r₄ = W.a₄) (h₆ : ∃ (r₆ : R), (algebraMap R K) r₆ = W.a₆) : IsIntegral R W

theorem WeierstrassCurve.Δ_integral_of_isIntegral (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) [IsIntegral R W] : ∃ (r : R), (algebraMap R K) r = W.Δ

theorem WeierstrassCurve.integralModel_Δ_eq (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (W : WeierstrassCurve K) [hW : IsIntegral R W] : (algebraMap R K) (integralModel R W).Δ = W.Δ

theorem WeierstrassCurve.exists_isIntegral (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsDomain R] [ValuationRing R] [IsFractionRing R K] (W : WeierstrassCurve K) : ∃ (C : VariableChange K), IsIntegral R (C • W)

noncomputable def WeierstrassCurve.valuation_Δ_aux (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : { v : WithZero (Multiplicative ℤ) // v ≤ 1 }

The valuation of the discriminant of a Weierstrass curve W, which is at most 1 if W is integral. Zero otherwise.

Equations

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

theorem WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) [hW : IsIntegral R W] : ↑(valuation_Δ_aux R W) = (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ

class WeierstrassCurve.IsMinimal (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : Prop

A Weierstrass equation over the fraction field K is minimal if the (multiplicative) valuation of its discriminant is maximal among all isomorphic integral Weierstrass equations. We still use 'minimal' for the naming, so as to standardize the naming with Silverman's book.

• val_Δ_maximal : MaximalFor (fun (C : VariableChange K) => IsIntegral R (C • W)) (fun (C : VariableChange K) => valuation_Δ_aux R (C • W)) 1

theorem WeierstrassCurve.isMinimal_iff (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : IsMinimal R W ↔ MaximalFor (fun (C : VariableChange K) => IsIntegral R (C • W)) (fun (C : VariableChange K) => valuation_Δ_aux R (C • W)) 1

instance WeierstrassCurve.instIsIntegralOfIsMinimal (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] : IsIntegral R W

theorem WeierstrassCurve.exists_isMinimal (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : ∃ (C : VariableChange K), IsMinimal R (C • W)

noncomputable def WeierstrassCurve.minimal (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : WeierstrassCurve K

A minimal Weierstrass equation for a given Weierstrass curve over K.

Equations

• WeierstrassCurve.minimal R W = ⋯.choose • W

instance WeierstrassCurve.instIsMinimalMinimal (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} : IsMinimal R (minimal R W)

noncomputable def WeierstrassCurve.reduction (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) [IsMinimal R W] : WeierstrassCurve (IsLocalRing.ResidueField R)

The reduction of a Weierstrass curve over K given by a minimal Weierstrass equation, which is a Weierstrass curve over the residue field of R.

Equations

• WeierstrassCurve.reduction R W = (WeierstrassCurve.integralModel R W).map (IsLocalRing.residue R)

class WeierstrassCurve.IsGoodReduction (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) [IsMinimal R W] : Prop

A minimal Weierstrass equation has good reduction if and only if the valuation of its discriminant is 1.

• goodReduction : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1

theorem WeierstrassCurve.isGoodReduction_iff (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) [IsMinimal R W] : IsGoodReduction R W ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1

theorem WeierstrassCurve.isGoodReduction_iff_isElliptic_reduction (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] : IsGoodReduction R W ↔ (reduction R W).IsElliptic