Field points of the elliptic curve of a Weierstrass equation

Let W be an elliptic Weierstrass curve over a field K and let E = toEllipticCurveGeom W be the elliptic curve over Spec K given by its projective model, with its scheme-theoretic group law (EllipticCurveGeom.grpObj). This file identifies the group of points of E with values in the base Spec K with the group W.toAffine.Point of Mathlib, and reads multiplication by an integer [n] : E ⟶ E (EllipticCurveGeom.mulBy) on these points: it is P ↦ n • P.

Through this dictionary the equation-level theory of torsion points applies to the scheme morphism [n]. The points of E killed by [n] are the n-torsion points of W, so there are finitely many of them for n ≠ 0, and exactly n.natAbs ^ 2 of them over a separably closed field in which n is invertible. When W has infinitely many points over K, as over a separably closed field, [n] is not the zero endomorphism for n ≠ 0, since the n-torsion is finite.

The same dictionary identifies the field points of the scheme-theoretic n-torsion E[n] (EllipticCurveGeom.torsion) with the n-torsion subgroup of W.toAffine.Point. Over a separably closed field in which N is invertible, the group of field points of E[N] is therefore isomorphic to (ℤ/Nℤ)².

Every elliptic curve over Spec K is the curve of a Weierstrass equation (EllipticCurveGeom.exists_iso_toEllipticCurveGeom), so the finiteness of its n-torsion points holds for every elliptic curve over a field, and so does the count of n² field points of E[n] over a separably closed field in which n is invertible.

Main definitions

• WeierstrassCurve.toEllipticCurveGeomPointsMulEquiv W: the isomorphism between the group of points of toEllipticCurveGeom W with values in Spec K and Multiplicative W.toAffine.Point.
• WeierstrassCurve.toEllipticCurveGeomTorsionPointsMulEquiv W n: the isomorphism between the group of points of the n-torsion of toEllipticCurveGeom W with values in Spec K and the n-torsion subgroup of W.toAffine.Point.

Main results

• WeierstrassCurve.toAdd_toEllipticCurveGeomPointsMulEquiv and WeierstrassCurve.toEllipticCurveGeomPointsMulEquiv_symm_apply_left: the isomorphism is the dictionary projModelPointsEquiv of sections of the projective model.
• WeierstrassCurve.toAdd_toEllipticCurveGeomPointsMulEquiv_comp_mulBy: multiplication by n on points of toEllipticCurveGeom W is multiplication by n on W.toAffine.Point.
• WeierstrassCurve.comp_mulBy_eq_one_iff: a point is killed by [n] exactly when the corresponding point of W is n-torsion.
• WeierstrassCurve.finite_comp_mulBy_eq_one: for n ≠ 0, finitely many points are killed by [n].
• WeierstrassCurve.natCard_comp_mulBy_eq_one: over a separably closed field in which n is invertible, n.natAbs ^ 2 points are killed by [n].
• WeierstrassCurve.toEllipticCurveGeom_mulBy_ne_one: when W has infinitely many points over K, for instance over a separably closed field, [n] is not the zero endomorphism for n ≠ 0.
• WeierstrassCurve.natCard_toEllipticCurveGeom_torsion: over a separably closed field in which n is invertible, E[n] has n.natAbs ^ 2 points with values in Spec K.
• WeierstrassCurve.nonempty_toEllipticCurveGeom_torsion_mulEquiv_prod: over a separably closed field in which N is invertible, the group of points of E[N] with values in Spec K is isomorphic to (ℤ/Nℤ)².
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_one_iff_left_apply_eq_zero: a point of an elliptic curve over Spec K is zero exactly when it meets the zero section.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.finite_comp_mulBy_eq_one: for n ≠ 0, finitely many points of any elliptic curve over Spec K are killed by [n].
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_natCard_torsion_eq: the field points of the n-torsion of any elliptic curve over Spec K are counted by the n-torsion of a Weierstrass equation of the curve.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.natCard_torsion: over a separably closed field in which n is invertible, the n-torsion of any elliptic curve has n.natAbs ^ 2 points with values in Spec K.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.3.1.
• J. H. Silverman, The Arithmetic of Elliptic Curves, III.6.4.

noncomputable def WeierstrassCurve.toEllipticCurveGeomPointsMulEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap) ≃* Multiplicative W.toAffine.Point

The group of points of the elliptic curve of W over a field. For an elliptic Weierstrass curve W over a field K, the points of the elliptic curve toEllipticCurveGeom W with values in the base Spec K, with its group law EllipticCurveGeom.grpObj, form a group isomorphic to the group W.toAffine.Point of Mathlib. It is the isomorphism projModelPointsMulEquiv of the group of points of the projective model, transported along the identification toEllipticCurveGeomOverIso of group schemes.

@[simp]

theorem WeierstrassCurve.toAdd_toEllipticCurveGeomPointsMulEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap) : Multiplicative.toAdd (W.toEllipticCurveGeomPointsMulEquiv x) = W.projModelPointsEquiv ⟨CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) W.toEllipticCurveGeomIso.hom, ⋯⟩

The point of W corresponding to a point x of toEllipticCurveGeom W over Spec K is the point corresponding under projModelPointsEquiv to the section x.left of the projective model, read through toEllipticCurveGeomIso.

@[simp]

theorem WeierstrassCurve.toEllipticCurveGeomPointsMulEquiv_symm_apply_left {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (P : Multiplicative W.toAffine.Point) : CategoryTheory.Over.Hom.left (W.toEllipticCurveGeomPointsMulEquiv.symm P) = CategoryTheory.CategoryStruct.comp (↑(W.projModelPointsEquiv.symm (Multiplicative.toAdd P))) W.toEllipticCurveGeomIso.inv

The point of toEllipticCurveGeom W over Spec K corresponding to a point P of W is the section of the projective model corresponding to P under projModelPointsEquiv, read through toEllipticCurveGeomIso.

theorem WeierstrassCurve.toAdd_toEllipticCurveGeomPointsMulEquiv_comp_mulBy {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap) (n : ℤ) : Multiplicative.toAdd (W.toEllipticCurveGeomPointsMulEquiv (CategoryTheory.CategoryStruct.comp x (W.toEllipticCurveGeom.mulBy n))) = n • Multiplicative.toAdd (W.toEllipticCurveGeomPointsMulEquiv x)

Multiplication by n on field points. Through toEllipticCurveGeomPointsMulEquiv, multiplication by an integer n on the elliptic curve toEllipticCurveGeom W sends the point corresponding to P to the point corresponding to n • P.

theorem WeierstrassCurve.comp_mulBy_eq_one_iff {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap) (n : ℤ) : CategoryTheory.CategoryStruct.comp x (W.toEllipticCurveGeom.mulBy n) = 1 ↔ n • Multiplicative.toAdd (W.toEllipticCurveGeomPointsMulEquiv x) = 0

A point of toEllipticCurveGeom W with values in Spec K is killed by multiplication by n exactly when the corresponding point of W is an n-torsion point.

theorem WeierstrassCurve.finite_comp_mulBy_eq_one {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {n : ℤ} (hn : n ≠ 0) : Finite { x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap // CategoryTheory.CategoryStruct.comp x (W.toEllipticCurveGeom.mulBy n) = 1 }

For a nonzero integer n, only finitely many points of toEllipticCurveGeom W with values in Spec K are killed by multiplication by n.

theorem WeierstrassCurve.natCard_comp_mulBy_eq_one {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {n : ℤ} (hn : ↑n ≠ 0) : Nat.card { x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.toEllipticCurveGeom.structureMap // CategoryTheory.CategoryStruct.comp x (W.toEllipticCurveGeom.mulBy n) = 1 } = n.natAbs ^ 2

The field points of E[n]. Over a separably closed field K in which the integer n is invertible, exactly n.natAbs ^ 2 points of toEllipticCurveGeom W with values in Spec K are killed by multiplication by n.

theorem WeierstrassCurve.toEllipticCurveGeom_mulBy_ne_one {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [Infinite W.toAffine.Point] {n : ℤ} (hn : n ≠ 0) : W.toEllipticCurveGeom.mulBy n ≠ 1

Multiplication by a nonzero integer is not the zero endomorphism of the elliptic curve toEllipticCurveGeom W, when W has infinitely many points over K: only finitely many of them are n-torsion. This holds over every separably closed field (WeierstrassCurve.Affine.infinite_point).

The field points of E[n]

noncomputable def WeierstrassCurve.toEllipticCurveGeomTorsionPointsMulEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (n : ℤ) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (W.toEllipticCurveGeom.torsion n).X) ≃* Multiplicative ↥(AddSubgroup.torsionBy W.toAffine.Point n)

The field points of E[n]. For an elliptic Weierstrass curve W over a field K, the points of the n-torsion E[n] of toEllipticCurveGeom W with values in the base Spec K form a group isomorphic to the n-torsion subgroup of W.toAffine.Point. A point y of E[n] is sent to the point of W corresponding to its image in toEllipticCurveGeom W (toAdd_toEllipticCurveGeomTorsionPointsMulEquiv).

@[simp]

theorem WeierstrassCurve.toAdd_toEllipticCurveGeomTorsionPointsMulEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] (n : ℤ) (y : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (W.toEllipticCurveGeom.torsion n).X) : ↑(Multiplicative.toAdd ((W.toEllipticCurveGeomTorsionPointsMulEquiv n) y)) = Multiplicative.toAdd (W.toEllipticCurveGeomPointsMulEquiv (CategoryTheory.CategoryStruct.comp y (W.toEllipticCurveGeom.torsionι n)))

The point of W corresponding to a point y of E[n] over Spec K is the point corresponding to its image in toEllipticCurveGeom W.

theorem WeierstrassCurve.natCard_toEllipticCurveGeom_torsion {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] {n : ℤ} (hn : ↑n ≠ 0) : Nat.card (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (W.toEllipticCurveGeom.torsion n).X) = n.natAbs ^ 2

The number of field points of E[n]. Over a separably closed field K in which the integer n is invertible, the n-torsion E[n] of toEllipticCurveGeom W has exactly n.natAbs ^ 2 points with values in Spec K.

theorem WeierstrassCurve.nonempty_toEllipticCurveGeom_torsion_mulEquiv_prod {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [IsSepClosed K] (N : ℕ) (hN : ↑N ≠ 0) : Nonempty ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (W.toEllipticCurveGeom.torsion ↑N).X) ≃* Multiplicative (ZMod N × ZMod N))

E[N](K) ≅ (ℤ/Nℤ)². Over a separably closed field K in which the natural number N is invertible, the group of points of the N-torsion E[N] of toEllipticCurveGeom W with values in Spec K is isomorphic to (ℤ/Nℤ)². The isomorphism is noncanonical, so the result asserts its existence.

Elliptic curves over a field

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_one_iff_left_apply_eq_zero {K : Type u} [Field K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap) (p : ↥(AlgebraicGeometry.Spec ↧K)) : x = 1 ↔ (CategoryTheory.Over.Hom.left x) p = E.zero p

A point of an elliptic curve over a field K with values in Spec K is the zero point exactly when it meets the zero section at the point p of Spec K.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.finite_comp_mulBy_eq_one {K : Type u} [Field K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) {n : ℤ} (hn : n ≠ 0) : Finite { x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap // CategoryTheory.CategoryStruct.comp x (E.mulBy n) = 1 }

An elliptic curve over a field has finitely many n-torsion points. For an elliptic curve E over Spec K and a nonzero integer n, only finitely many points of E with values in Spec K are killed by multiplication by n.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_natCard_torsion_eq {K : Type u} [Field K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) : ∃ (W : WeierstrassCurve K) (_ : W.IsElliptic), ∀ (n : ℤ), Nat.card (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (E.torsion n).X) = Nat.card ↥(AddSubgroup.torsionBy W.toAffine.Point n)

The field points of E[n] are the n-torsion of a Weierstrass equation. An elliptic curve E over Spec K is the curve of an elliptic Weierstrass equation W, and for every integer n the points of E[n] with values in Spec K are as many as the n-torsion points of W.toAffine.Point.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.natCard_torsion {K : Type u} [Field K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) [IsSepClosed K] {n : ℤ} (hn : ↑n ≠ 0) : Nat.card (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ (E.torsion n).X) = n.natAbs ^ 2

The number of field points of E[n]. For an elliptic curve E over a separably closed field K in which the integer n is invertible, the n-torsion E[n] has exactly n.natAbs ^ 2 points with values in Spec K.