Elliptic curves

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Hasse bound (Silverman V.1.1)#

an elliptic curve E over a field with q elements satisfies (#E(𝔽_q) - (q + 1))² ≤ 4q, that is |#E(𝔽_q) - (q + 1)| ≤ 2√q, where the count includes the point at infinity. frobeniusTrace_sq_le_four_mul_card is the same bound for the trace a_q.

WeierstrassCurve.hasse_bound.{u_1} {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F)
  [W.IsElliptic] : (↑(Nat.card W.toAffine.Point) - (↑(Nat.card F) + 1)) ^ 2 ≤ 4 * ↑(Nat.card F)

Lean

Formalized in Tau Ceti as WeierstrassCurve.hasse_bound.

Other forms

The Hasse bound, in trace form. Formalized in Tau Ceti as WeierstrassCurve.frobeniusTrace_sq_le_four_mul_card.

WeierstrassCurve.frobeniusTrace_sq_le_four_mul_card.{u_1} {F : Type u_1} [Field F] [Finite F]
  (W : WeierstrassCurve F) [W.IsElliptic] : W.frobeniusTrace ^ 2 ≤ 4 * ↑(Nat.card F)

Sources

LeanWeierstrassCurve.hasse_bound · WeierstrassCurve.frobeniusTrace_sq_le_four_mul_card

Uses 12

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The factorisation theorem · The factorisation theorem for isogenies (Silverman II.2.12) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The kernel form of the factorisation theorem (Silverman III.4.11) · Krull–Akizuki for Mathlib's integralClosure · 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 theorem

TheoremIsogenous curves over a finite field have the same zeta function `Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n)`#

TauCeti.Isogeny.zetaFunction_eq.{u_1} {F : Type u_1} [Field F] [Finite F]
  {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁]
  [WeierstrassCurve.IsElliptic W₂] (φ : TauCeti.Isogeny W₁ W₂) :
  WeierstrassCurve.zetaFunction W₁ = WeierstrassCurve.zetaFunction W₂

Lean

Formalized in Tau Ceti as TauCeti.Isogeny.zetaFunction_eq.

Sources

LeanTauCeti.Isogeny.zetaFunction_eq

Uses 10

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The factorisation theorem for isogenies (Silverman II.2.12) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · Krull–Akizuki for Mathlib's integralClosure · 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 theorem

TheoremThe Mordell–Weil theorem #

the group E(K) of K-rational points of an elliptic curve E over a number field K is finitely generated.

The square on the left-hand side is completed by an admissible change of variables, possible since K has characteristic zero, and the finiteness hypotheses of fg_point for the resulting model are the class number theorem and Dirichlet's unit theorem.

WeierstrassCurve.Affine.fg_point_of_numberField.{u_2} {F : Type u_2} [Field F] [NumberField F]
  [DecidableEq F] {W : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic (WeierstrassCurve.toAffine W)] : AddGroup.FG W.Point

Lean

Formalized in Tau Ceti as WeierstrassCurve.Affine.fg_point_of_numberField.

Other forms

The Mordell–Weil theorem, general version. Formalized in Tau Ceti as WeierstrassCurve.Affine.fg_point.

WeierstrassCurve.Affine.fg_point.{u_1, u_2} {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F}
  [Height.AdmissibleAbsValues F] [Northcott Height.logHeight₁] [DecidableEq F]
  [WeierstrassCurve.IsElliptic (WeierstrassCurve.toAffine W)] (R : Type u_2) [CommRing R]
  [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] [WeierstrassCurve.IsCharNeTwoNF W]
  [∀ (p : W.f.Factors), Finite (ClassGroup (W.ringOfIntegersFactor R p))]
  [∀ (p : W.f.Factors), Monoid.FG (W.ringOfIntegersFactor R p)ˣ] : AddGroup.FG W.Point

The Mordell–Weil theorem for an arbitrary Weierstrass curve. Formalized in Tau Ceti as WeierstrassCurve.Affine.fg_point_of_variableChange.

WeierstrassCurve.Affine.fg_point_of_variableChange.{u_1, u_2} {F : Type u_1} [Field F]
  {W : WeierstrassCurve.Affine F} [Height.AdmissibleAbsValues F] [Northcott Height.logHeight₁]
  [DecidableEq F] [WeierstrassCurve.IsElliptic (WeierstrassCurve.toAffine W)] (R : Type u_2)
  [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
  (C : WeierstrassCurve.VariableChange F) [WeierstrassCurve.IsCharNeTwoNF (C • W)]
  [∀ (p : (WeierstrassCurve.toAffine (C • W)).f.Factors),
      Finite (ClassGroup ((WeierstrassCurve.toAffine (C • W)).ringOfIntegersFactor R p))]
  [∀ (p : (WeierstrassCurve.toAffine (C • W)).f.Factors),
      Monoid.FG ((WeierstrassCurve.toAffine (C • W)).ringOfIntegersFactor R p)ˣ] :
  AddGroup.FG W.Point

The Mordell–Weil theorem as an instance. Formalized in Tau Ceti as WeierstrassCurve.Affine.moduleFinite_point_of_numberField.

WeierstrassCurve.Affine.moduleFinite_point_of_numberField.{u_2} {F : Type u_2} [Field F]
  [NumberField F] [DecidableEq F] {W : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic (WeierstrassCurve.toAffine W)] : Module.Finite ℤ W.Point

Sources

LeanWeierstrassCurve.Affine.fg_point_of_numberField · WeierstrassCurve.Affine.fg_point · WeierstrassCurve.Affine.fg_point_of_variableChange · WeierstrassCurve.Affine.moduleFinite_point_of_numberField

Uses 2 · Used by 2

Proof usesDirichlet's unit theorem (WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor) · The weak Mordell–Weil theorem

Used byThe Mordell–Weil rank bound from the 2-Selmer group · The Mordell–Weil group of y² = x³ - x + 1 over ℚ is ℤ

TheoremThe Mordell–Weil group of `y² = x³ - x + 1` over `ℚ` is `ℤ`#

It is finitely generated, torsion-free and of rank one.

TauCeti.WorkedExamples.nonempty_addEquiv_int_point_curveX3SubXAddOne :
  Nonempty ((TauCeti.WorkedExamples.curveX3SubXAddOne.baseChange ℚ).toAffine.Point ≃+ ℤ)

Lean

Formalized in Tau Ceti as TauCeti.WorkedExamples.nonempty_addEquiv_int_point_curveX3SubXAddOne.

Sources

LeanTauCeti.WorkedExamples.nonempty_addEquiv_int_point_curveX3SubXAddOne

Uses 4

Proof usesBrill's theorem, parity form · The Mordell–Weil rank bound from the 2-Selmer group · The Mordell–Weil theorem · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

TheoremThe `m`-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2)#

The local conditions are the images of the Kummer maps over the completions at all finite places. The conclusion holds for every nonzero natural number m.

WeierstrassCurve.finite_selmerGroup.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) [NeZero m]
  (τ :
    (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) →
      SeparableClosure K →ₐ[K]
        SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) :
  Finite ↥(W.selmerGroup τ m)

Lean

Formalized in Tau Ceti as WeierstrassCurve.finite_selmerGroup.

Sources

LeanWeierstrassCurve.finite_selmerGroup

Uses 13

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · Dedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · Krull–Akizuki for Mathlib's integralClosure · Riemann's theorem · TauCeti.algebraicExtensionNormedField · TauCeti.Ring.IsJapanese · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient · The weak approximation theorem

TheoremThe criterion of Néron, Ogg and Shafarevich for potential good reduction (Silverman AEC VII.7.3)#

Let W be an elliptic curve over a nonarchimedean local field K, and let ℓ be a prime different from the residue characteristic of K. Then W has potential good reduction exactly when the inertia subgroup of Gal(K^{alg}/K) acts on the ℓ-adic Tate module of W through a finite quotient.

WeierstrassCurve.hasPotentialGoodReduction_iff_finite_image_tateModuleGaloisRepresentation.{u_1}
  {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  {W : WeierstrassCurve K} [W.IsElliptic] [DecidableEq (AlgebraicClosure K)] {ℓ : ℕ}
  [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) :
  WeierstrassCurve.HasPotentialGoodReduction (↥(ValuativeRel.valuation K).integer) W ↔
    (⇑(W.tateModuleGaloisRepresentation ℓ) '' ↑(TauCeti.inertiaSubgroup K)).Finite

Lean

Formalized in Tau Ceti as WeierstrassCurve.hasPotentialGoodReduction_iff_finite_image_tateModuleGaloisRepresentation.

Sources

LeanWeierstrassCurve.hasPotentialGoodReduction_iff_finite_image_tateModuleGaloisRepresentation

Uses 6

Proof usesDedekind's different theorem, the tame case · The first half of Dedekind's different theorem · Hensel's lemma without monicity · Serre's lemma for the ℓ-adic representation · TauCeti.algebraicExtensionNormedField · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

TheoremThe criterion of Néron, Ogg and Shafarevich with finite coefficients (Serre–Tate)#

Let W be an elliptic curve over a nonarchimedean local field K, given by a minimal equation, with potential good reduction, and let N ≥ 3 be an integer that is nonzero in the residue field of K. Then W has good reduction exactly when the inertia subgroup of Gal(K^{alg}/K) fixes every point of E(K^{alg})[N].

WeierstrassCurve.HasPotentialGoodReduction.hasGoodReduction_iff_forall_mem_inertiaSubgroup.{u_1}
  {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  {W : WeierstrassCurve K} [W.IsElliptic]
  [WeierstrassCurve.IsMinimal (↥(ValuativeRel.valuation K).integer) W]
  (h : WeierstrassCurve.HasPotentialGoodReduction (↥(ValuativeRel.valuation K).integer) W) {N : ℕ}
  (hN : 3 ≤ N) (hNk : ↑N ≠ 0) :
  WeierstrassCurve.HasGoodReduction (↥(ValuativeRel.valuation K).integer) W ↔
    ∀ σ ∈ TauCeti.inertiaSubgroup K,
      ∀ (P : (W.baseChange (AlgebraicClosure K)).toAffine.Point),
        N • P = 0 → (WeierstrassCurve.Affine.Point.map ↑σ) P = P

Lean

Formalized in Tau Ceti as WeierstrassCurve.HasPotentialGoodReduction.hasGoodReduction_iff_forall_mem_inertiaSubgroup.

Sources

LeanWeierstrassCurve.HasPotentialGoodReduction.hasGoodReduction_iff_forall_mem_inertiaSubgroup

Uses 6

Proof usesDedekind's different theorem, the tame case · The first half of Dedekind's different theorem · Hensel's lemma without monicity · Serre's lemma for the ℓ-adic representation · TauCeti.algebraicExtensionNormedField · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

DefinitionPointed twists are classified by nonabelian Galois cohomology #

For a Galois extension L/K, the pointed twists of W split by L are in bijection with H¹(Gal(L/K), Aut(W_L)). The equivalence sends a trivialisation C to the class of the cocycle σ ↦ C (σ C)⁻¹.

WeierstrassCurve.pointedTwistEquivNonabelianH1.{u_1, u_3} {K : Type u_1} [Field K]
  (W : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] [IsGalois K L] :
  W.PointedTwist L ≃ TauCeti.NonabelianH1 Gal(L/K) (W.AutCoeff L)

Lean

Formalized in Tau Ceti as WeierstrassCurve.pointedTwistEquivNonabelianH1.

Sources

LeanWeierstrassCurve.pointedTwistEquivNonabelianH1

TheoremThe `φ`-descent sequence is exact at `H¹(G_K, E₁[φ])`#

the kernel of H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ] is the image of E₂(K) ⧸ φ(E₁(K)) under the Kummer map. Together with TauCeti.Isogeny.kummerClassMap_injective and TauCeti.Isogeny.kerCoeffInclH1_surjective this is the short exact sequence 0 → E₂(K) ⧸ φ(E₁(K)) → H¹(G_K, E₁[φ]) → H¹(G_K, E₁)[φ] → 0.

TauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1.{u_1} {K : Type u_1} [Field K]
  {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic]
  (φ : TauCeti.Isogeny W₁.toAffine W₂.toAffine)
  [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.toAffine.FunctionField] [DecidableEq K] :
  Function.Exact ⇑φ.kummerClassMap ⇑φ.kerCoeffInclH1

Lean

Formalized in Tau Ceti as TauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1.

Sources

LeanTauCeti.Isogeny.exact_kummerClassMap_kerCoeffInclH1

Uses 10

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The factorisation theorem for isogenies (Silverman II.2.12) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · Krull–Akizuki for Mathlib's integralClosure · 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 theorem

TheoremTate's local index is the point-group index (Silverman, Advanced Topics, IV.9, Table 4.1)#

Suppose that the valuation ring of v is Henselian with finite residue field, for instance the ring of integers of a nonarchimedean local field, and that Tate's algorithm, run on the integral model of W with a generator ϖ of the maximal ideal, stops with the symbol s. Then the local index the algorithm reports is [W(F) : E₀(F)], the index of the subgroup of points with nonsingular reduction.

Finiteness of the residue field is used only at nonsplit multiplicative reduction of even type I₂ₘ, to find a point with singular reduction; over a general perfect residue field the index can be 1 there.

WeierstrassCurve.Affine.index_nonsingularReduction_eq_tateLocalIndex.{u_1, u_2} {F : Type u_1}
  {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀)
  {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsIntegral (↥v.valuationSubring) W]
  [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring]
  [Finite (IsLocalRing.ResidueField ↥v.valuationSubring)] {ϖ : ↥v.valuationSubring}
  (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) {s : TauCeti.ReductionSymbol}
  (h : (WeierstrassCurve.integralModel (↥v.valuationSubring) W).IsTateTerminal ϖ s) :
  (WeierstrassCurve.Affine.nonsingularReduction v W).index =
    (WeierstrassCurve.integralModel (↥v.valuationSubring) W).tateLocalIndex ϖ s

Lean

Formalized in Tau Ceti as WeierstrassCurve.Affine.index_nonsingularReduction_eq_tateLocalIndex.

Sources

LeanWeierstrassCurve.Affine.index_nonsingularReduction_eq_tateLocalIndex

Uses 1

Proof usesHensel's lemma without monicity

TheoremDirichlet's unit theorem (`WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor`)#

Dirichlet's unit theorem for the field factors of the étale algebra of a curve over a number field: the ring of integers of each factor F[X] ⧸ (p) has finitely generated unit group.

WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor.{u_2} {F : Type u_2} [Field F] [NumberField F]
  (W : WeierstrassCurve.Affine F) (p : W.f.Factors) :
  Monoid.FG (W.ringOfIntegersFactor (NumberField.RingOfIntegers F) p)ˣ

Lean

Formalized in Tau Ceti as WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor.

Sources

LeanWeierstrassCurve.Affine.fg_units_ringOfIntegersFactor

Uses 1 · Used by 2

Proof usesDirichlet's unit theorem (NumberField.fg_units_integralClosure)

Used byThe Mordell–Weil rank bound from the 2-Selmer group · The Mordell–Weil theorem

TheoremSerre's lemma for the `ℓ`-adic representation #

An automorphism σ fixing every point of E[ℓ ^ k], with ℓ ^ k ≥ 3, and acting on T_ℓ E with finite order, acts trivially on T_ℓ E.

WeierstrassCurve.tateModuleGaloisRepresentation_eq_one_of_isOfFinOrder.{u_1, u_2} {F : Type u_1}
  {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] {W : WeierstrassCurve F} {ℓ : ℕ}
  [Fact (Nat.Prime ℓ)] {σ : Gal(K/F)} (hσ : IsOfFinOrder ((W.tateModuleGaloisRepresentation ℓ) σ))
  {k : ℕ} (hk : 3 ≤ ℓ ^ k)
  (hfix :
    ∀ (P : (W.baseChange K).toAffine.Point),
      ℓ ^ k • P = 0 → (WeierstrassCurve.Affine.Point.map ↑σ) P = P) :
  (W.tateModuleGaloisRepresentation ℓ) σ = 1

Lean

Formalized in Tau Ceti as WeierstrassCurve.tateModuleGaloisRepresentation_eq_one_of_isOfFinOrder.

Sources

LeanWeierstrassCurve.tateModuleGaloisRepresentation_eq_one_of_isOfFinOrder

Uses 1 · Used by 2

Proof usesSerre's lemma on the Tate module

Used byThe 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 dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Elliptic curves

TheoremThe Hasse bound (Silverman V.1.1)#

Lean

Other forms

Sources

TheoremIsogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n)#

Lean

Sources

TheoremThe Mordell–Weil theorem#

Lean

Other forms

Sources

TheoremThe Mordell–Weil group of y² = x³ - x + 1 over ℚ is ℤ#

Lean

Sources

TheoremThe m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2)#

Lean

Sources

TheoremThe criterion of Néron, Ogg and Shafarevich for potential good reduction (Silverman AEC VII.7.3)#

Lean

Sources

TheoremThe criterion of Néron, Ogg and Shafarevich with finite coefficients (Serre–Tate)#

Lean

Sources

DefinitionPointed twists are classified by nonabelian Galois cohomology#

Lean

Sources

TheoremThe φ-descent sequence is exact at H¹(G_K, E₁[φ])#

Lean

Sources

TheoremTate's local index is the point-group index (Silverman, *Advanced Topics*, IV.9, Table 4.1)#

Lean

Sources

TheoremDirichlet's unit theorem (WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor)#

Lean

Sources

TheoremSerre's lemma for the ℓ-adic representation#

Lean

Sources

TheoremIsogenous curves over a finite field have the same zeta function `Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n)`#

TheoremThe Mordell–Weil theorem #

TheoremThe Mordell–Weil group of `y² = x³ - x + 1` over `ℚ` is `ℤ`#

TheoremThe `m`-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2)#

DefinitionPointed twists are classified by nonabelian Galois cohomology #

TheoremThe `φ`-descent sequence is exact at `H¹(G_K, E₁[φ])`#

TheoremTate's local index is the point-group index (Silverman, Advanced Topics, IV.9, Table 4.1)#

TheoremDirichlet's unit theorem (`WeierstrassCurve.Affine.fg_units_ringOfIntegersFactor`)#

TheoremSerre's lemma for the `ℓ`-adic representation #