The scheme of points of exact order N

Let E be an elliptic curve over a scheme S. The exact-order locus E.exactOrderLocus N is an ideal sheaf on E whose closed subscheme carries the universal point of exact order N. This file regards that closed subscheme as a scheme over S, the exact-order scheme E.exactOrderScheme N, and shows that it represents the points of exact order N on base changes of E: for a scheme T over S and a base change E' of E along T ⟶ S, the T-points of E' of exact order N, in the sense of Drinfeld, are the morphisms T ⟶ E.exactOrderScheme N over S (EllipticCurveGeom.exactOrderPointsEquivOfIsPullback). No hypothesis is placed on S, which may be nonreduced, and N need not be invertible on it.

A point of exact order N is killed by N, so the exact-order scheme lies in the N-torsion E[N] (EllipticCurveGeom.exactOrderSchemeι_comp_mulBy). As a closed subscheme of E[N], it is finite over S for N ≠ 0 (EllipticCurveGeom.isFinite_exactOrderScheme_hom). This is the form in which points of exact order N relatively represent the moduli problem [Γ₁(N)] of Katz and Mazur, by a scheme finite over the base.

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderScheme E N: the closed subscheme of E cut out by the exact-order locus, as a scheme over S, with its inclusion TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι E N into E.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback: the points of exact order N of a base change of E along T ⟶ S are the morphisms from T to the exact-order scheme.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι_comp_mulBy: multiplication by N kills the exact-order scheme.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_exactOrderScheme_hom: for N ≠ 0, the exact-order scheme is finite over S.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, 1.6.2 (the closed locus of points of exact order N), 3.2 and 3.6.0 ([Γ₁(N)] is relatively representable and finite).

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderScheme {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : CategoryTheory.Over S

The exact-order scheme of E: the closed subscheme of E cut out by the exact-order locus E.exactOrderLocus N, as a scheme over S. Its points with values in a scheme T over S are the points of exact order N of the base change of E to T (exactOrderPointsEquivOfIsPullback).

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : E.exactOrderScheme N ⟶ CategoryTheory.Over.mk E.structureMap

The inclusion of the exact-order scheme in E, a closed immersion.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : CategoryTheory.Over.Hom.left (E.exactOrderSchemeι N) = (E.exactOrderLocus N).subschemeι

The inclusion of the exact-order scheme in E is the inclusion of the closed subscheme of the exact-order locus.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClosedImmersion_exactOrderSchemeι_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (E.exactOrderSchemeι N))

The inclusion of the exact-order scheme in E is a closed immersion.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.mono_exactOrderSchemeι {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : CategoryTheory.Mono (E.exactOrderSchemeι N)

The inclusion of the exact-order scheme in E is a monomorphism.

Points of exact order N on base changes

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) {T : CategoryTheory.Over S} {E' : EllipticCurveGeom T.left} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap T.hom) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp T.hom E.zero) : { P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over T.left) ⟶ CategoryTheory.Over.mk E'.structureMap // E'.IsOfExactOrder P N } ≃ (T ⟶ E.exactOrderScheme N)

The exact-order scheme represents points of exact order N (Katz–Mazur, 1.6.2). Let T be a scheme over S and g : E' ⟶ E a morphism of elliptic curves lying over T ⟶ S, forming a pullback square with the structure morphisms and carrying the zero section of E' to that of E; for instance E' is the base change E_T. Then the T-points of E' of exact order N are the morphisms T ⟶ E.exactOrderScheme N over S: a point P corresponds to the morphism whose image in E is P ≫ g (exactOrderPointsEquivOfIsPullback_apply_left_comp).

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback_apply_left_comp {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {T : CategoryTheory.Over S} {E' : EllipticCurveGeom T.left} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap T.hom) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp T.hom E.zero) (P : { P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over T.left) ⟶ CategoryTheory.Over.mk E'.structureMap // E'.IsOfExactOrder P N }) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((exactOrderPointsEquivOfIsPullback N hg h0) P)) (E.exactOrderLocus N).subschemeι = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑P) g

The morphism to the exact-order scheme of a point P of exact order N of E', followed by the inclusion in E, is P ≫ g.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback_apply_left_comp_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {T : CategoryTheory.Over S} {E' : EllipticCurveGeom T.left} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap T.hom) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp T.hom E.zero) (P : { P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over T.left) ⟶ CategoryTheory.Over.mk E'.structureMap // E'.IsOfExactOrder P N }) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((exactOrderPointsEquivOfIsPullback N hg h0) P)) (CategoryTheory.CategoryStruct.comp (E.exactOrderLocus N).subschemeι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑P) (CategoryTheory.CategoryStruct.comp g h)

The morphism to the exact-order scheme of a point P of exact order N of E', followed by the inclusion in E, is P ≫ g.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback_symm_apply_left_comp {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {T : CategoryTheory.Over S} {E' : EllipticCurveGeom T.left} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap T.hom) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp T.hom E.zero) (y : T ⟶ E.exactOrderScheme N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑((exactOrderPointsEquivOfIsPullback N hg h0).symm y)) g = CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp y (E.exactOrderSchemeι N))

The point of exact order N of E' attached to a morphism y from T to the exact-order scheme lies over the image of y in E.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderPointsEquivOfIsPullback_symm_apply_left_comp_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {T : CategoryTheory.Over S} {E' : EllipticCurveGeom T.left} {g : E'.carrier ⟶ E.carrier} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap T.hom) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp T.hom E.zero) (y : T ⟶ E.exactOrderScheme N) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑((exactOrderPointsEquivOfIsPullback N hg h0).symm y)) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp y (E.exactOrderSchemeι N))) h

The point of exact order N of E' attached to a morphism y from T to the exact-order scheme lies over the image of y in E.

The exact-order scheme lies in E[N]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι_comp_mulBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : CategoryTheory.CategoryStruct.comp (E.exactOrderSchemeι N) (E.mulBy ↑N) = 1

The exact-order scheme lies in the N-torsion: multiplication by N kills the inclusion of the exact-order scheme in E, scheme-theoretically. Equivalently (EllipticCurveGeom.exists_comp_torsionι_iff), the inclusion factors through E[N].

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exactOrderSchemeι_comp_mulBy_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) {Z : CategoryTheory.Over S} (h : CategoryTheory.Over.mk E.structureMap ⟶ Z) : CategoryTheory.CategoryStruct.comp (E.exactOrderSchemeι N) (CategoryTheory.CategoryStruct.comp (E.mulBy ↑N) h) = CategoryTheory.CategoryStruct.comp 1 h

The exact-order scheme lies in the N-torsion: multiplication by N kills the inclusion of the exact-order scheme in E, scheme-theoretically. Equivalently (EllipticCurveGeom.exists_comp_torsionι_iff), the inclusion factors through E[N].

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_exactOrderScheme_hom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) [NeZero N] : AlgebraicGeometry.IsFinite (E.exactOrderScheme N).hom

The exact-order scheme is finite over S for N ≠ 0: it is a closed subscheme of the N-torsion E[N], which is finite over S.