The exact-order locus

Let E be an elliptic curve over a scheme S and D ⊆ E a closed subscheme which is finite locally free over S. Whether the base change of D to a scheme S' over S is a subgroup scheme of the base change of E is a closed condition on S': there is an ideal sheaf E.subgroupLocus D on S such that D_{S'} is a subgroup scheme of E_{S'} exactly when S' ⟶ S factors through its closed subscheme (EllipticCurveGeom.subgroupLocus_le_ker_iff).

By the closed-subgroup criterion, D_{S'} is a subgroup scheme exactly when the zero section, the sum of two points of D_{S'} and the negative of a point of D_{S'} all lie in D_{S'}. The first is the condition that S' ⟶ S factors through the inverse image of D under the zero section. The other two say that a family parametrised by the finite locally free scheme D ×_S D, respectively D, lies in D; such a condition is cut out by a Weil restriction of a closed subscheme (AlgebraicGeometry.Scheme.IdealSheafData.weilRestriction_comap_le_ker_iff).

Applied to the divisor [P] + [2P] + ⋯ + [NP] of an S-point P, this shows that having exact order N in the sense of Drinfeld is a closed condition on the base: the base change of P along S' ⟶ S has exact order N exactly when S' ⟶ S factors through a closed subscheme of S (EllipticCurveGeom.isOfExactOrder_pointsPullback_iff). Applied to the universal point, the diagonal section of E ×_S E over E, it gives the exact-order locus E.exactOrderLocus N, a closed subscheme of E: for every base change E' of E, an S'-point P' of E' has exact order N exactly when the corresponding morphism S' ⟶ E factors through the exact-order locus (EllipticCurveGeom.isOfExactOrder_iff_exactOrderLocus_le_ker_comp). No hypothesis is placed on S, which may be nonreduced, and N need not be invertible on it.

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.subgroupLocus E D: the ideal sheaf on S of the locus over which the finite locally free closed subscheme V(D) of E is a subgroup scheme.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderLocus E N: the ideal sheaf on E of the exact-order locus, the closed subscheme of E representing points of exact order N.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.subgroupLocus_le_ker_iff: the universal property of the subgroup locus.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_pointsPullback_iff: having exact order N is a closed condition on the base.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff_exactOrderLocus_le_ker_comp: the universal property of the exact-order locus; isOfExactOrder_iff_exactOrderLocus_le_ker is its special case for S-points of E.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, 1.3.7 (the subgroup condition on a finite locally free closed subscheme is closed), §1.4 (points of exact order N), 1.6.2 (the closed locus cut out by the subgroup condition) and §3.2 ([Γ₁(N)]-structures).

The subgroup locus of a finite locally free closed subscheme

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.subgroupLocus {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (D : E.carrier.IdealSheafData) [AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] [AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] : S.IdealSheafData

The ideal sheaf on S of the subgroup locus of a closed subscheme V(D) of E which is finite locally free over S (Katz–Mazur, 1.3.7): a morphism S' ⟶ S factors through its closed subscheme exactly when the base change of V(D) to S' is a subgroup scheme of the base change of E (EllipticCurveGeom.subgroupLocus_le_ker_iff). It is the supremum of the ideal sheaves of three loci: where the zero section lies in V(D), where the sum of two points of V(D) lies in V(D), and where the negative of a point of V(D) lies in V(D).

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.subgroupLocus_le_ker_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (D : E.carrier.IdealSheafData) [AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] [AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] [AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp D.subschemeι E.structureMap)] {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) : E.subgroupLocus D ≤ AlgebraicGeometry.Scheme.Hom.ker f ↔ ∃ (x : CategoryTheory.GrpObj (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp (D.comap g).subschemeι E'.structureMap))), CategoryTheory.IsMonHom (CategoryTheory.Over.homMk (D.comap g).subschemeι ⋯)

The universal property of the subgroup locus (Katz–Mazur, 1.3.7). Let g : E' ⟶ E be a morphism of elliptic curves lying over f : S' ⟶ S, forming a pullback square with the structure morphisms and carrying the zero section of E' to that of E, and let V(D) ⊆ E be finite locally free over S. Then the inverse image of V(D) in E' is a subgroup scheme of E' exactly when f factors through the closed subscheme of E.subgroupLocus D.

Exact order is a closed condition

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_pointsPullback_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {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) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : E'.IsOfExactOrder ((pointsPullback hg h0) P) N ↔ E.subgroupLocus (E.multiplesDivisor P N) ≤ AlgebraicGeometry.Scheme.Hom.ker f

Having exact order N is a closed condition on the base (Katz–Mazur, 1.6.2). For a pullback square of elliptic curves over f : S' ⟶ S and an S-point P of E, the base change of P has exact order N exactly when f factors through the closed subscheme of the subgroup locus of the divisor [P] + ⋯ + [NP].

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff_subgroupLocus_eq_bot {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : E.IsOfExactOrder P N ↔ E.subgroupLocus (E.multiplesDivisor P N) = ⊥

A point has exact order N exactly when the subgroup locus of the divisor [P] + ⋯ + [NP] is all of S.

The exact-order locus in E

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderLocus {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : E.carrier.IdealSheafData

The ideal sheaf of the exact-order locus in E: the closed subscheme of E over which the universal point has exact order N. A point of a base change of E has exact order N exactly when the corresponding morphism to E factors through it (EllipticCurveGeom.isOfExactOrder_iff_exactOrderLocus_le_ker_comp).

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff_exactOrderLocus_le_ker_comp {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {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) (P' : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S') ⟶ CategoryTheory.Over.mk E'.structureMap) (N : ℕ) : E'.IsOfExactOrder P' N ↔ E.exactOrderLocus N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left P') g)

The universal property of the exact-order locus (Katz–Mazur, 1.6.2). For a pullback square of elliptic curves g : E' ⟶ E over f : S' ⟶ S, an S'-point P' of E' has exact order N exactly when the morphism S' ⟶ E given by P' factors through the exact-order locus.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff_exactOrderLocus_le_ker {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : E.IsOfExactOrder P N ↔ E.exactOrderLocus N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left P)

An S-point of E has exact order N exactly when it factors through the exact-order locus.