The divisor of a finite family of points on an elliptic curve

Let E be an elliptic curve over a scheme S and x : A → E(S) a finite family of S-points of E. Each x a is a section of the smooth separated curve E ⟶ S, so it cuts out a relative effective Cartier divisor [x a] on E. The divisor ∑_{a ∈ A} [x a] (EllipticCurveGeom.pointsDivisor) is the product of their ideal sheaves; points occurring several times in the family are counted with multiplicity.

The divisor ∑_a [x a] is a relative effective Cartier divisor on E over S, hence finite locally free over S since E is proper. It contains each of the points x a, its support is the union of their images, it does not depend on how the points are indexed, and it commutes with base change. Particular cases are the divisor [P] + [2P] + ⋯ + [NP] of points of exact order N (EllipticCurveGeom.multiplesDivisor) and the divisor ∑_{a ∈ (ℤ/Nℤ)²} [φ a] of Drinfeld bases (EllipticCurveGeom.IsDrinfeldBasis).

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor E x: the divisor ∑_a [x a] of a finite family of S-points of E, as an ideal sheaf on E.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isRelativeEffectiveCartier_pointsDivisor: ∑_a [x a] is a relative effective Cartier divisor on E over S.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_pointsDivisor, TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_pointsDivisor and TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyOfFinitePresentation_pointsDivisor: ∑_a [x a] is finite locally free over S.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.coe_support_pointsDivisor: the support of ∑_a [x a] is the union of the images of the sections x a; over a field, a point lies on ∑_a [x a] exactly when it is one of the x a (TauCeti.AlgebraicGeometry.EllipticCurveGeom.mem_support_pointsDivisor_iff).
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_comp_equiv: ∑_a [x a] does not depend on the indexing.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_pointsPullback: ∑_a [x a] commutes with base change.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_pointsDivisor: its rank is the number of sections, counted with multiplicity.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, Chapter 1 (sums of sections of a smooth curve).

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : E.carrier.IdealSheafData

The divisor ∑_{a ∈ A} [x a] of a finite family x of S-points of an elliptic curve E over S, as an ideal sheaf on E: the product of the ideal sheaves of the sections x a. Points occurring several times in the family are counted with multiplicity.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_def {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : E.pointsDivisor x = ∏ a : A, AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (x a))

The divisor ∑_a [x a] is the product of the ideal sheaves of the sections x a.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isRelativeEffectiveCartier_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : (E.pointsDivisor x).IsRelativeEffectiveCartier E.structureMap

∑_a [x a] is a relative effective Cartier divisor on E over S, as a sum of the divisors of sections of the smooth separated curve E ⟶ S.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp (E.pointsDivisor x).subschemeι E.structureMap)

The divisor ∑_a [x a] is finite over the base.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp (E.pointsDivisor x).subschemeι E.structureMap)

The divisor ∑_a [x a] is flat over the base.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyOfFinitePresentation_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp (E.pointsDivisor x).subschemeι E.structureMap)

The divisor ∑_a [x a] is locally of finite presentation over the base. Together with finiteness and flatness, this makes it finite locally free.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_le_ker {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) (a : A) : E.pointsDivisor x ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (x a))

Each of the points x a lies on the divisor ∑_a [x a].

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.coe_support_ker_left {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : ↑(AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left x)).support = Set.range ⇑(CategoryTheory.Over.Hom.left x)

The support of the ideal of a section is its image in the elliptic curve.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.coe_support_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : ↑(E.pointsDivisor x).support = ⋃ (a : A), Set.range ⇑(CategoryTheory.Over.Hom.left (x a))

The support of the divisor ∑_a [x a] is the union of the images of the sections x a.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mem_support_pointsDivisor_iff {A : Type u_1} [Fintype A] {K : Type u} [Field K] {E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)} (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap)) (y : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap) (p : ↥(AlgebraicGeometry.Spec ↧K)) : (CategoryTheory.Over.Hom.left y) p ∈ ↑(E.pointsDivisor x).support ↔ y ∈ Set.range x

Over a field, the points of E on ∑_a [x a] are the x a.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_comp_equiv {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] {A' : Type u_2} [Fintype A'] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) (e : A' ≃ A) : E.pointsDivisor (x ∘ ⇑e) = E.pointsDivisor x

The divisor ∑_a [x a] does not depend on the indexing of the family of points.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) (s : ↥S) : AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.CategoryStruct.comp (E.pointsDivisor x).subschemeι E.structureMap) s = Fintype.card A

A sum of section divisors has rank equal to the number of sections, with multiplicity.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pointsDivisor_pointsPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Fintype A] {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) (x : A → (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)) : E'.pointsDivisor (⇑(pointsPullback hg h0) ∘ x) = (E.pointsDivisor x).comap g

The divisor ∑_a [x a] commutes with base change: for the base changes x' a of the S-points x a of E, the divisor ∑_a [x' a] on E' is the inverse image along g of the divisor ∑_a [x a] on E.