The criterion behind the weak… to The weak Mordell–Weil theorem
TheoremThe criterion behind the weak Mordell–Weil theorem#
2E(K) has finite index in E(K)
exactly when the image of the descent map is finite.
E(K)/2E(K) and the image of μ are the same group, so finiteness of either is finiteness of
the other.
WeierstrassCurve.Affine.finiteIndex_range_nsmulAddMonoidHom_two_iff.{u_1} {K : Type u_1} [Field K]
(W : WeierstrassCurve.Affine K) [WeierstrassCurve.IsElliptic W] [WeierstrassCurve.IsCharNeTwoNF W]
[DecidableEq K] :
(nsmulAddMonoidHom 2).range.FiniteIndex ↔ Finite ↥WeierstrassCurve.Affine.μ.range
Lean
Formalized in Tau Ceti as WeierstrassCurve.Affine.finiteIndex_range_nsmulAddMonoidHom_two_iff.
Sources
Used by 1
TheoremDeligne's theorem (WeierstrassCurve.IsIntegralModularForm.mem_adjoin)#
Every integral modular form lies in the subring ℤ[c₄, c₆, Δ].
WeierstrassCurve.IsIntegralModularForm.mem_adjoin {k : ℕ}
{f : MvPolynomial WeierstrassCurve.Coeff ℤ} (hf : WeierstrassCurve.IsIntegralModularForm k f) :
f ∈
ℤ[WeierstrassCurve.c₄ WeierstrassCurve.Universal.curve,
WeierstrassCurve.c₆ WeierstrassCurve.Universal.curve,
WeierstrassCurve.Δ WeierstrassCurve.Universal.curve]
TheoremThe factorisation theorem#
The factorisation theorem (Silverman, The Arithmetic of Elliptic Curves, III.4.11 in its
separable form): an isogeny ψ : W₁ → W₃ factors through an isogeny φ : W₁ → W₂, by a unique
isogeny λ : W₂ → W₃, exactly when the function field ψ pulls back sits inside the one φ
pulls back.
The criterion is on subfields of F(W₁), not on kernels of point maps, and that is what makes it
correct in general: over ℚ, a curve with no rational 2-torsion has ker [2](ℚ) = {O} without
the identity factoring through [2], and relative Frobenius has trivial geometric point kernel
without the identity factoring through it. In both cases the subfield containment fails, as it
should.
TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le.{u_1} {F : Type u_1} [Field F]
{W₁ W₂ W₃ : WeierstrassCurve.Affine F} (φ : TauCeti.Isogeny W₁ W₂) (ψ : TauCeti.Isogeny W₁ W₃) :
(∃! χ, χ.comp φ = ψ) ↔ ψ.fieldPullback.fieldRange ≤ φ.fieldPullback.fieldRange
Lean
Formalized in Tau Ceti as TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le.
Sources
TheoremThe factorisation theorem for isogenies (Silverman II.2.12)#
when p ^ r is the
inseparable degree of φ : W₁ → W₂, it factors through the r-fold relative Frobenius
F^r : W₁ → W₁⁽ᵖʳ⁾ as φ = χ ∘ F^r for a unique isogeny χ : W₁⁽ᵖʳ⁾ → W₂. The factor is
separable (isSeparable_of_comp_iterateRelativeFrobeniusIsogeny_eq), of degree the separable
degree of φ (degree_eq_separableDegree_of_comp_iterateRelativeFrobeniusIsogeny_eq).
TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq.{u_1} {F : Type u_1} [Field F]
(p : ℕ) [ExpChar F p] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : TauCeti.Isogeny W₁ W₂) {r : ℕ}
(hr : φ.inseparableDegree = p ^ r) :
∃! χ, χ.comp (TauCeti.Isogeny.iterateRelativeFrobeniusIsogeny p W₁ r) = φ
Lean
Formalized in Tau Ceti as TauCeti.Isogeny.existsUnique_comp_iterateRelativeFrobeniusIsogeny_eq.
Sources
Uses 1 · Used by 5
TheoremThe Galois cocycle carried by that isomorphism#
Conjugating
quadraticTwistOfTraceNormVariableChange by the nontrivial σ ∈ Gal(L/K) changes it by
negVariableChange, the change of variables [-1]: this is the cocycle identity for
H¹(Gal(L/K), Aut E).
It does not say the class is nontrivial. E here is an arbitrary Weierstrass curve, and when
negVariableChange = 1 — a singular curve in characteristic 2 with a₁ = a₃ = 0, say — the
identity below is plain equivariance. Nontriviality needs hypotheses this statement does not
carry.
WeierstrassCurve.map_quadraticTwistOfTraceNormVariableChange.{u_1, u_2} {K : Type u_1} [Field K]
{L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L]
[Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)}
(hσ : σ ≠ 1) :
(E.quadraticTwistOfTraceNormVariableChange hθ hσ).map ↑σ =
(E.baseChange L).negVariableChange * E.quadraticTwistOfTraceNormVariableChange hθ hσ
Lean
Formalized in Tau Ceti as WeierstrassCurve.map_quadraticTwistOfTraceNormVariableChange.
Sources
TheoremThe Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity#
with
e - 1 summed over the four ramified places,
2 g - 2 = [K(W) : K(x)] (2 g(K(x)) - 2) + ∑ (e - 1),
which reads 2 · 1 - 2 = 2 · (0 - 2) + 4. The genus g = 1 on the left is computed from the
Riemann–Roch spaces L(n · O) (WeierstrassCurve.Affine.genus_functionField), independently of
the ramification data on the right.
TauCeti.CurveX3SubX.hurwitz_genus_formula.{u_1} {K : Type u_1} [Field K] [NeZero 2] :
2 * ↑(TauCeti.genus K (TauCeti.CurveX3SubX.curve K).toAffine.FunctionField) - 2 =
↑(Module.finrank (RatFunc K) (TauCeti.CurveX3SubX.curve K).toAffine.FunctionField) *
(2 * ↑(TauCeti.genus K (RatFunc K)) - 2) +
(↑(TauCeti.Place.ramificationIdx (RatFunc K)
(TauCeti.Place.infinity (TauCeti.CurveX3SubX.curve K).toAffine)) -
1 +
(↑(TauCeti.Place.ramificationIdx (RatFunc K)
↑((TauCeti.CurveX3SubX.curve K).toAffine.pointEquivDegreeOnePlace
(TauCeti.CurveX3SubX.pointZero K))) -
1) +
(↑(TauCeti.Place.ramificationIdx (RatFunc K)
↑((TauCeti.CurveX3SubX.curve K).toAffine.pointEquivDegreeOnePlace
(TauCeti.CurveX3SubX.pointOne K))) -
1) +
(↑(TauCeti.Place.ramificationIdx (RatFunc K)
↑((TauCeti.CurveX3SubX.curve K).toAffine.pointEquivDegreeOnePlace
(TauCeti.CurveX3SubX.pointNegOne K))) -
1))
TheoremThe Jacobian criterion as two equalities, the form Nonsingular negates#
WeierstrassCurve.Affine.isSingular_iff.{u_1} {R : Type u_1} [CommRing R]
(W : WeierstrassCurve.Affine R) (x y : R) :
W.IsSingular x y ↔
W.Equation x y ∧ W.a₁ * y = 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∧ y = -y - W.a₁ * x - W.a₃
TheoremThe kernel form of the factorisation theorem (Silverman III.4.11)#
When the kernel of
φ : W₁ → W₂ has deg φ points, an isogeny ψ : W₁ → W₃ factors through φ, by a unique
isogeny, exactly when ker φ ≤ ker ψ.
Without the hypothesis only the forward implication holds (TauCeti.Isogeny.ker_le_ker_comp).
The subfield criterion TauCeti.Isogeny.existsUnique_comp_eq_iff_fieldRange_le needs no
hypothesis.
TauCeti.Isogeny.existsUnique_comp_eq_iff_ker_le.{u_1} {F : Type u_1} [Field F]
{W₁ W₂ W₃ : WeierstrassCurve.Affine F} [DecidableEq F] [WeierstrassCurve.IsElliptic W₁]
{φ : TauCeti.Isogeny W₁ W₂} (hφ : Nat.card ↥φ.ker = φ.degree) (ψ : TauCeti.Isogeny W₁ W₃) :
(∃! χ, χ.comp φ = ψ) ↔ φ.ker ≤ ψ.ker
Lean
Formalized in Tau Ceti as TauCeti.Isogeny.existsUnique_comp_eq_iff_ker_le.
Sources
Uses 1 · Used by 2
TheoremKraus's global criterion#
Let O be a Dedekind domain with fraction field K, in which
2 and 3 are invertible, and assume O has a height-one prime, as the ring of integers of a
number field does. Then the pair (c₄, c₆) is the pair of c-invariants of a nonsingular
Weierstrass equation with coefficients in O exactly when Kraus's local condition holds at every
height-one prime.
The equation produced is the (b₂/12, a₁/2, a₃/2)-transform of ofCInvariants c₄ c₆ for elements
a₁, b₂, a₃ of O approximating the local witnesses modulo 12. Without a height-one prime
the condition is vacuous and the statement fails, since nothing then forces c₄³ ≠ c₆².
TauCeti.krausGlobalCondition_iff_exists_integralModel.{u_2, u_3} {K : Type u_2} [Field K]
{c₄ c₆ : K} {O : Type u_3} [CommRing O] [IsDedekindDomain O] [Algebra O K] [IsFractionRing O K]
[Invertible 2] [Invertible 3] [Nonempty (IsDedekindDomain.HeightOneSpectrum O)] :
TauCeti.KrausGlobalCondition O c₄ c₆ ↔
∃ W, WeierstrassCurve.IsIntegral O W ∧ W.c₄ = c₄ ∧ W.c₆ = c₆ ∧ W.Δ ≠ 0
Lean
Formalized in Tau Ceti as TauCeti.krausGlobalCondition_iff_exists_integralModel.
Sources
Uses 1
TheoremKraus's local criterion#
For a local ring R with an algebra map to a field K in which
2 and 3 are invertible, the pair (c₄, c₆) is the pair of c-invariants of a nonsingular
Weierstrass equation with coefficients in R exactly when Kraus's local condition holds.
The correspondence is concrete in both directions: a witness of KrausLocalCondition is a change
of variables carrying ofCInvariants c₄ c₆ to an equation with coefficients in R, and that
transform is the model the equivalence produces.
TauCeti.krausLocalCondition_iff_exists_integralModel.{u_1, u_2} {R : Type u_1} [CommRing R]
{K : Type u_2} [Field K] [Algebra R K] {c₄ c₆ : K} [Invertible 2] [Invertible 3] [IsLocalRing R] :
TauCeti.KrausLocalCondition R c₄ c₆ ↔
∃ W, WeierstrassCurve.IsIntegral R W ∧ W.c₄ = c₄ ∧ W.c₆ = c₆ ∧ W.Δ ≠ 0
Lean
Formalized in Tau Ceti as TauCeti.krausLocalCondition_iff_exists_integralModel.
Sources
Used by 1
TheoremThe modified Szpiro conjecture implies Szpiro's conjecture, with the same constants#
the
relation 1728 Δ = c₄³ - c₆² on the reduced minimal model gives |Δ_min| ≤ max (|c₄|³, c₆²).
TauCeti.AlgorithmicModifiedSzpiroConjecture.algorithmicSzpiroConjecture
(h : TauCeti.AlgorithmicModifiedSzpiroConjecture) : TauCeti.AlgorithmicSzpiroConjecture
Lean
Formalized in Tau Ceti as TauCeti.AlgorithmicModifiedSzpiroConjecture.algorithmicSzpiroConjecture, assuming TauCeti.AlgorithmicModifiedSzpiroConjecture, a proposition Tau Ceti defines.
Sources
TheoremThe Mordell–Weil rank bound from the 2-Selmer group#
for an elliptic curve over a number
field F, 2 ^ rank W(F) * #W(F)[2] ≤ #Sel₂(W/F). The rank is that of the finitely generated
group W(F) (fg_point_of_numberField), and the right-hand side is finite by
finite_selmerGroup₂.
WeierstrassCurve.Affine.pow_rank_le_card_selmerGroup₂.{u_1, u_2, u_3} {F : Type u_1} [Field F]
[NumberField F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W]
[WeierstrassCurve.IsCharNeTwoNF W] {ι : Type u_2} (Loc : ι → Type u_3) [(i : ι) → Field (Loc i)]
[(i : ι) → Algebra F (Loc i)] :
2 ^ Module.finrank ℤ W.Point * Nat.card ↥(nsmulAddMonoidHom 2).ker ≤
Nat.card ↥(W.selmerGroup₂ (NumberField.RingOfIntegers F) Loc)
Lean
Formalized in Tau Ceti as WeierstrassCurve.Affine.pow_rank_le_card_selmerGroup₂.
Other forms
The Mordell–Weil rank bound from the units and class groups of the field factors. Formalized in Tau Ceti as WeierstrassCurve.Affine.pow_rank_add_one_le_prod.
WeierstrassCurve.Affine.pow_rank_add_one_le_prod.{u_1} {F : Type u_1} [Field F] [NumberField F]
(W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [WeierstrassCurve.IsCharNeTwoNF W]
[Fintype W.f.Factors]
(ha₂ :
∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)),
(IsDedekindDomain.HeightOneSpectrum.valuation F v) W.a₂ ≤ 1)
(ha₄ :
∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)),
(IsDedekindDomain.HeightOneSpectrum.valuation F v) W.a₄ ≤ 1)
(ha₆ :
∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)),
(IsDedekindDomain.HeightOneSpectrum.valuation F v) W.a₆ ≤ 1)
(hd :
∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)),
WithZero.exp (-1) ≤ (IsDedekindDomain.HeightOneSpectrum.valuation F v) W.f.discr)
(h : ¬IsSquare (-1)) :
2 ^ (Module.finrank ℤ W.Point + 1) * Nat.card ↥(nsmulAddMonoidHom 2).ker ≤
∏ p,
2 ^
(Module.finrank ℤ (Additive (W.ringOfIntegersFactor (NumberField.RingOfIntegers F) p)ˣ) +
1) *
Nat.card ↥(powMonoidHom 2).ker
Sources
TheoremThe Nagell–Lutz theorem#
Let A B : ℤ and let (x, y) be a nonzero rational point of
finite order on y² = x³ + Ax + B. Then x and y are integers, and either y = 0 or
y² ∣ Δ.
This is the classical statement, and the form TauCetiRoadmap/EllipticCurves/README.md:830 names
lutz_nagell. It is the specialisation of the two theorems above at a short model: Mathlib's
isCharNeTwoNF_of_isShortNF supplies the instance, so there is nothing to discharge. No hypothesis
Δ ≠ 0 is needed — see the module docstring.
WeierstrassCurve.lutz_nagell (A B : ℤ) {x y : ℚ}
(hns : ((WeierstrassCurve.shortCurve A B).baseChange ℚ).toAffine.Nonsingular x y)
(htor : IsOfFinAddOrder (WeierstrassCurve.Affine.Point.some x y hns)) :
∃ x₀ y₀, ↑x₀ = x ∧ ↑y₀ = y ∧ (y₀ = 0 ∨ y₀ ^ 2 ∣ (WeierstrassCurve.shortCurve A B).Δ)
Lean
Formalized in Tau Ceti as WeierstrassCurve.lutz_nagell.
Other forms
Nagell–Lutz over ℚ, the form the roadmap asks for. Formalized in Tau Ceti as WeierstrassCurve.isInteger_or_order_two_of_torsion_rat.
WeierstrassCurve.isInteger_or_order_two_of_torsion_rat {W : WeierstrassCurve ℤ} {x y : ℚ}
(hns : (W.baseChange ℚ).toAffine.Nonsingular x y)
(htor : IsOfFinAddOrder (WeierstrassCurve.Affine.Point.some x y hns)) :
IsLocalization.IsInteger ℤ x ∧ IsLocalization.IsInteger ℤ y ∨
addOrderOf (WeierstrassCurve.Affine.Point.some x y hns) = 2 ∧
IsLocalization.IsInteger ℤ (4 * x) ∧ IsLocalization.IsInteger ℤ (8 * y)
Nagell–Lutz, discriminant half. Formalized in Tau Ceti as WeierstrassCurve.y_eq_zero_or_sq_dvd_Δ_of_torsion.
WeierstrassCurve.y_eq_zero_or_sq_dvd_Δ_of_torsion {W : WeierstrassCurve ℤ} [W.IsCharNeTwoNF]
{x y : ℚ} (hns : (W.baseChange ℚ).toAffine.Nonsingular x y)
(htor : IsOfFinAddOrder (WeierstrassCurve.Affine.Point.some x y hns)) {x₀ y₀ : ℤ}
(hx : (algebraMap ℤ ℚ) x₀ = x) (hy : (algebraMap ℤ ℚ) y₀ = y) : y₀ = 0 ∨ y₀ ^ 2 ∣ W.Δ
Nagell–Lutz, integrality half. Formalized in Tau Ceti as WeierstrassCurve.isInteger_of_torsion.
WeierstrassCurve.isInteger_of_torsion {W : WeierstrassCurve ℤ} [W.IsCharNeTwoNF] {x y : ℚ}
(hns : (W.baseChange ℚ).toAffine.Nonsingular x y)
(htor : IsOfFinAddOrder (WeierstrassCurve.Affine.Point.some x y hns)) :
IsLocalization.IsInteger ℤ x ∧ IsLocalization.IsInteger ℤ y
Sources
TheoremPerfect local Tate duality for E[m]#
Pairing with a class gives a bijection from
H¹(K, E[m]) to its additive characters with values in ℤ/m.
WeierstrassCurve.localTateWeilPairing_bijective {K : Type} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) [W.IsElliptic]
(m : ℕ) (hm : IsUnit ↑m) : Function.Bijective ⇑(W.localTateWeilPairing m hm)
Lean
Formalized in Tau Ceti as WeierstrassCurve.localTateWeilPairing_bijective.
Other forms
Perfect local Tate duality for the kernels of an isogeny and of its dual. Formalized in Tau Ceti as TauCeti.Isogeny.localTateKerWeilPairing_bijective.
TauCeti.Isogeny.localTateKerWeilPairing_bijective {K : Type} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic]
[W₂.IsElliptic] (φ : TauCeti.Isogeny W₁.toAffine W₂.toAffine) (hn : IsUnit ↑φ.degree) :
Function.Bijective ⇑(φ.localTateKerWeilPairing hn)
Sources
Uses 14
integralClosure · Local Tate duality in degree one · Riemann's theorem · TauCeti.Ring.IsJapanese · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient · The weak approximation theoremTheoremSuyama's exact ellipticity criterion#
Under the denominator restrictions, precisely these five factors detect singular models. No odd characteristic is excluded.
TauCeti.Montgomery.isElliptic_model_suyama_iff.{u_1} {K : Type u_1} [Field K] {σ : K} (h₂ : 2 ≠ 0)
(hσ : σ ≠ 0) (hu : σ ^ 2 ≠ 5) :
(TauCeti.Montgomery.model (TauCeti.Montgomery.suyamaA σ)
(TauCeti.Montgomery.suyamaB σ)).IsElliptic ↔
(σ ^ 2 - 1) * (σ ^ 2 - 9) * (σ ^ 2 - 25) * (9 * σ ^ 2 - 25) * (σ ^ 2 + 5) ≠ 0
TheoremSzpiro's conjecture for Frey curves#
Under TauCeti.AlgorithmicSzpiroConjecture, for every
ε > 0 there is a constant C such that (A B (A + B))² ≤ C rad (A B (A + B)) ^ (6 + ε) for all
coprime integers A and B with A B (A + B) ≠ 0. This applies Szpiro's conjecture to the curve
of TauCeti.exists_natAbs_sq_le_absNorm_minimalDiscriminantIdeal.
TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le (h : TauCeti.AlgorithmicSzpiroConjecture) {ε : ℝ}
(hε : 0 < ε) :
∃ C,
∀ (A B : ℤ),
IsCoprime A B →
A * B * (A + B) ≠ 0 →
↑(A * B * (A + B)) ^ 2 ≤
C * ↑(UniqueFactorizationMonoid.radical (A * B * (A + B)).natAbs) ^ (6 + ε)
Lean
Formalized in Tau Ceti as TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le, assuming TauCeti.AlgorithmicSzpiroConjecture, a proposition Tau Ceti defines.
Other forms
Szpiro's conjecture for Frey curves. Formalized in Tau Ceti as TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le_mul_radical_rpow, assuming TauCeti.AlgorithmicSzpiroConjecture, a proposition Tau Ceti defines.
TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le_mul_radical_rpow
(h : TauCeti.AlgorithmicSzpiroConjecture) {ε : ℝ} (hε : 0 < ε) :
∃ C,
∀ (A B : ℤ),
IsCoprime A B →
4 ∣ A + 1 →
32 ∣ B →
B ≠ 0 →
↑(A * B * (A + B)) ^ 2 ≤
C * ↑(UniqueFactorizationMonoid.radical (A * B * (A + B))) ^ (6 + ε)
Sources
TheoremSzpiro's conjecture implies asymptotic Fermat#
If TauCeti.AlgorithmicSzpiroConjecture
holds, there is an N such that aⁿ + bⁿ = cⁿ has no solution in positive integers for any
exponent n ≥ N. The bound N depends on the constant of Szpiro's conjecture for ε = 1, so it
is ineffective.
TauCeti.AlgorithmicSzpiroConjecture.asymptoticFermat (h : TauCeti.AlgorithmicSzpiroConjecture) :
TauCeti.AsymptoticFermat
Lean
Formalized in Tau Ceti as TauCeti.AlgorithmicSzpiroConjecture.asymptoticFermat, assuming TauCeti.AlgorithmicSzpiroConjecture, a proposition Tau Ceti defines.
Sources
Uses 1
TheoremSzpiro's conjecture implies the abc conjecture with exponent 3 / 2#
under
TauCeti.AlgorithmicSzpiroConjecture, for every ε > 0 there is a constant C with
max (|a|, |b|, |c|) ≤ C rad (a b c) ^ (3 / 2 + ε) for all coprime a + b = c. For coprime
positive integers a + b = c, Szpiro's bound for Frey curves gives
(a b c)² ≪_ε rad (a b c) ^ (6 + 4 ε) (TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le), and
c² ≤ 2 a b c because a + b ≤ 2 a b.
TauCeti.AlgorithmicSzpiroConjecture.abcConjectureWithExponent
(h : TauCeti.AlgorithmicSzpiroConjecture) : TauCeti.AbcConjectureWithExponent (3 / 2)
Lean
Formalized in Tau Ceti as TauCeti.AlgorithmicSzpiroConjecture.abcConjectureWithExponent, assuming TauCeti.AlgorithmicSzpiroConjecture, a proposition Tau Ceti defines.
Sources
Uses 1
TheoremVieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient#
the third root satisfies
(1 + a₂λ + a₄λ² + a₆λ³)(t₃ + t₁ + t₂) = -(a₁λ + a₂ν + a₃λ² + 2a₄λν + 3a₆λ²ν).
WeierstrassCurve.formalThirdRootEval_relation.{u_1} {O : Type u_1} [CommRing O] [UniformSpace O]
[IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O]
(W : WeierstrassCurve O) {t₁ t₂ : O} (h₁ : PowerSeries.HasEval t₁) (h₂ : PowerSeries.HasEval t₂) :
(1 + W.a₂ * W.formalSlopeEval t₁ t₂ + W.a₄ * W.formalSlopeEval t₁ t₂ ^ 2 +
W.a₆ * W.formalSlopeEval t₁ t₂ ^ 3) *
(W.formalThirdRootEval t₁ t₂ + t₁ + t₂) =
-(W.a₁ * W.formalSlopeEval t₁ t₂ + W.a₂ * W.formalInterceptEval t₁ t₂ +
W.a₃ * W.formalSlopeEval t₁ t₂ ^ 2 +
2 * W.a₄ * W.formalSlopeEval t₁ t₂ * W.formalInterceptEval t₁ t₂ +
3 * W.a₆ * W.formalSlopeEval t₁ t₂ ^ 2 * W.formalInterceptEval t₁ t₂)
Used by 12
E[m] · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The criterion of Néron, Ogg and Shafarevich for potential good reduction (Silverman AEC VII.7.3) · The criterion of Néron, Ogg and Shafarevich with finite coefficients (Serre–Tate) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · The Mordell–Weil group of y² = x³ - x + 1 over ℚ is ℤ · Drinfeld and naive [Γ(N)]-structures coincide where N is invertible (Katz–Mazur, §3.7) · [Γ(N)] is rigid for N ≥ 3 where N is invertible (Katz–Mazur, 2.7.2) · The n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1)TheoremThe weak Mordell–Weil theorem#
E(K)/2E(K) is finite, for an elliptic curve in the normal
form y² = x³ + a₂x² + a₄x + a₆ over the fraction field K of a Dedekind domain R, provided
that for each irreducible factor p of the cubic the ring of integers of K[X] ⧸ (p) has finite
class group and finitely generated unit group.
This is the input to the descent argument in the Mordell–Weil theorem proper.
WeierstrassCurve.Affine.finiteIndex_range_nsmulAddMonoidHom_two.{u_1, u_2} {K : Type u_1} [Field K]
(W : WeierstrassCurve.Affine K) [WeierstrassCurve.IsElliptic W] [WeierstrassCurve.IsCharNeTwoNF W]
(R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K]
[∀ (p : W.f.Factors), Finite (ClassGroup (W.ringOfIntegersFactor R p))]
[∀ (p : W.f.Factors), Monoid.FG (W.ringOfIntegersFactor R p)ˣ] [DecidableEq K] :
(nsmulAddMonoidHom 2).range.FiniteIndex
Lean
Formalized in Tau Ceti as WeierstrassCurve.Affine.finiteIndex_range_nsmulAddMonoidHom_two.
Sources
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.