The Weierstrass class of an elliptic curve

Let O be a Dedekind domain with fraction field K. An integral elliptic Weierstrass equation W has a defect ideal 𝔍_W, whose exponent at a height-one prime is the local obstruction to minimality. Under an admissible change of variables C, two integral equations satisfy

𝔍_(C • W) · (C.u) = 𝔍_W.

Consequently their defect ideals determine the same element of ClassGroup O. This file packages that element as weierstrassDefectClass, defines its inverse weierstrassClass in Silverman's orientation, and constructs the choice-independent curve-level invariant globalMinimalityClass.

Main definitions

• WeierstrassCurve.weierstrassDefectClass: the positive defect class [𝔍_W] of an integral equation.
• WeierstrassCurve.weierstrassClass: the inverse class [𝔍_W]⁻¹, in Silverman's orientation.
• WeierstrassCurve.globalMinimalityClass: the choice-independent defect class of a curve over K.

Main results

• WeierstrassCurve.globalMinimalityClass_eq_weierstrassDefectClass: comparison with an integral model.
• WeierstrassCurve.globalMinimalityClass_eq_mk0_weierstrassDefectIdeal: for an integral equation over K, the class of its defect ideal.
• WeierstrassCurve.globalMinimalityClass_variableChange: invariance under an admissible change of variables.
• WeierstrassCurve.IsGlobalMinimal.weierstrassDefectClass_eq_one: a globally minimal equation has trivial defect class.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.8.

noncomputable def WeierstrassCurve.weierstrassDefectClass (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : ClassGroup O

The positive Weierstrass defect class [𝔍_W] of an integral equation W over O.

This convention records the excess of the equation's discriminant over the minimal discriminant. It is inverse to weierstrassClass, the orientation used in Silverman VIII.8.

Equations

• WeierstrassCurve.weierstrassDefectClass O W = WeierstrassCurve.defectClassOfIsIntegral✝ O (W.baseChange K)

@[simp]

theorem WeierstrassCurve.weierstrassDefectClass_def (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : have x := ⋯; weierstrassDefectClass O W = ClassGroup.mk0 ⟨weierstrassDefectIdeal O (W.baseChange K), ⋯⟩

The positive Weierstrass defect class is the ideal class of the defect ideal.

noncomputable def WeierstrassCurve.weierstrassClass (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : ClassGroup O

The Weierstrass class in Silverman's orientation, namely the inverse [𝔍_W]⁻¹ of the positive defect class.

Equations

• WeierstrassCurve.weierstrassClass O W = (WeierstrassCurve.weierstrassDefectClass O W)⁻¹

@[simp]

theorem WeierstrassCurve.weierstrassClass_eq_inv_weierstrassDefectClass (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : weierstrassClass O W = (weierstrassDefectClass O W)⁻¹

The Weierstrass class is the inverse of the positive defect class.

noncomputable def WeierstrassCurve.globalMinimalityClass (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (E : WeierstrassCurve K) [E.IsElliptic] : ClassGroup O

The curve-level global-minimality obstruction. It is the defect class of any integral equation obtained from E; the change-of-variables formula makes the choice immaterial.

Equations

• WeierstrassCurve.globalMinimalityClass O E = WeierstrassCurve.defectClassOfIsIntegral✝ O (Classical.choose ⋯ • E)

@[simp]

theorem WeierstrassCurve.globalMinimalityClass_eq_weierstrassDefectClass (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : globalMinimalityClass O (W.baseChange K) = weierstrassDefectClass O W

The curve-level obstruction agrees with the defect class of every integral model.

theorem WeierstrassCurve.globalMinimalityClass_eq_mk0_weierstrassDefectIdeal (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral O W] : globalMinimalityClass O W = ClassGroup.mk0 ⟨weierstrassDefectIdeal O W, ⋯⟩

The curve-level obstruction of an integral equation is the class of its defect ideal. This is globalMinimalityClass_eq_weierstrassDefectClass for an equation over K that is integral, rather than one given as the base change of an equation over O.

@[simp]

theorem WeierstrassCurve.globalMinimalityClass_variableChange (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (E : WeierstrassCurve K) [E.IsElliptic] (C : VariableChange K) : globalMinimalityClass O (C • E) = globalMinimalityClass O E

The global-minimality obstruction is invariant under an admissible change of variables.

theorem WeierstrassCurve.globalMinimalityClass_eq_weierstrassDefectClass_of_variableChange (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] (E : WeierstrassCurve K) [E.IsElliptic] (C : VariableChange K) (hC : C • W.baseChange K = E) : globalMinimalityClass O E = weierstrassDefectClass O W

Compare the curve-level obstruction with an integral model presented together with an admissible change of variables to the target curve.

theorem WeierstrassCurve.weierstrassDefectClass_eq_of_variableChange (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W₁ W₂ : WeierstrassCurve O) [(W₁.baseChange K).IsElliptic] [(W₂.baseChange K).IsElliptic] (C : VariableChange K) (hC : C • W₁.baseChange K = W₂.baseChange K) : weierstrassDefectClass O W₁ = weierstrassDefectClass O W₂

Integral models related over K have the same positive defect class.

theorem WeierstrassCurve.weierstrassClass_eq_of_variableChange (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W₁ W₂ : WeierstrassCurve O) [(W₁.baseChange K).IsElliptic] [(W₂.baseChange K).IsElliptic] (C : VariableChange K) (hC : C • W₁.baseChange K = W₂.baseChange K) : weierstrassClass O W₁ = weierstrassClass O W₂

Integral models related over K have the same Weierstrass class.

theorem WeierstrassCurve.IsGlobalMinimal.weierstrassDefectClass_eq_one (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] {W : WeierstrassCurve O} [(W.baseChange K).IsElliptic] (hW : IsGlobalMinimal O (W.baseChange K)) : weierstrassDefectClass O W = 1

A globally minimal integral equation has trivial positive defect class.

theorem WeierstrassCurve.IsGlobalMinimal.weierstrassClass_eq_one (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] {W : WeierstrassCurve O} [(W.baseChange K).IsElliptic] (hW : IsGlobalMinimal O (W.baseChange K)) : weierstrassClass O W = 1

A globally minimal integral equation has trivial Weierstrass class.

theorem WeierstrassCurve.weierstrassClass_eq_one_iff (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve O) [(W.baseChange K).IsElliptic] : weierstrassClass O W = 1 ↔ weierstrassDefectClass O W = 1

Triviality is unchanged by passing between the positive defect convention and Silverman's inverse convention.