The subgroup divisor of a point of exact order

For a point P of an elliptic curve E/S, the divisor [P] + ⋯ + [NP] is finite locally free of rank N. If P has exact order N in the sense of Drinfeld, this divisor is a commutative subgroup scheme. Deligne's rank theorem therefore kills the entire subgroup by N, including its infinitesimal points, and gives its scheme-theoretic containment in E[N].

The rank computation does not require exact order. The killing statement holds over arbitrary, possibly nonreduced bases and is an equality of scheme morphisms. Containment in E[N] is stated as an inclusion of ideal sheaves, so the existing closed-subscheme factorization API applies directly.

This annihilation result is intrinsic to the subgroup divisor and its rank. It applies directly to the subgroup-divisor formulation of exact order, independently of generator schemes or a comparison with full sets of sections.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §§1.4 and 1.12.
• FiniteFlatCommGroupScheme.pow_eq_one_of_finrank: Deligne's theorem for finite locally free commutative group schemes.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι E.structureMap)

The divisor of the first N positive multiples of a point is finite over the base.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.flat_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι E.structureMap)

The divisor of the first N positive multiples of a point is flat over the base.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyOfFinitePresentation_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι E.structureMap)

The divisor of the first N positive multiples of a point is locally of finite presentation over the base. Together with finiteness and flatness, this makes it finite locally free.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.finrank_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι E.structureMap) = fun (x : ↥S) => N

The divisor [P] + ⋯ + [NP] has constant rank N, whether or not P has exact order.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder.subschemeι_comp_mulBy {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfExactOrder P N) : CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι (CategoryTheory.Over.Hom.left (E.mulBy ↑N)) = CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι (CategoryTheory.CategoryStruct.comp E.structureMap E.zero)

Multiplication by N kills the entire subgroup divisor of a point of exact order N, scheme-theoretically, including all its infinitesimal points.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder.ker_torsionι_le {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfExactOrder P N) : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (E.torsionι ↑N)) ≤ E.multiplesDivisor P N

The subgroup divisor of a point of exact order N is contained in E[N] as a closed subscheme. The order on ideal sheaves reverses containment of their closed subschemes.