Comparison of naive and Drinfeld exact order #
Where the level is invertible, a point has Drinfeld exact order precisely when it has exact order in every geometric fibre. This comparison holds over arbitrary, possibly nonreduced base schemes and identifies the Drinfeld and naive moduli problems for points of exact order.
References #
- N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.4 and §3.7.
theorem
TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.isOfExactOrder
{S : AlgebraicGeometry.Scheme}
{E : EllipticCurveGeom S}
{N : ℕ}
{P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap}
(hP : E.IsOfNaiveExactOrder P N)
(hN : ∀ (s : ↥S), ↑N ≠ 0)
:
E.IsOfExactOrder P N
A naive point of exact order is a Drinfeld point of exact order where the level is invertible. This implication is valid over arbitrary, possibly nonreduced base schemes.
@[simp]
theorem
TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff_isOfNaiveExactOrder
{S : AlgebraicGeometry.Scheme}
{E : EllipticCurveGeom S}
{N : ℕ}
{P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap}
(hN : ∀ (s : ↥S), ↑N ≠ 0)
:
Drinfeld and naive exact order agree where the level is invertible.