The moduli problem [Γ₁(N)]

Following Katz and Mazur, a [Γ₁(N)]-structure on an elliptic curve E over a scheme S is an S-point P of E of exact order N: the divisor [P] + [2P] + ⋯ + [NP] on E is a subgroup scheme (EllipticCurveGeom.IsOfExactOrder). This is Drinfeld's notion, which makes sense over every base, including bases on which N is not invertible.

An arrow (E'/S') ⟶ (E/S) of Ell/B exhibits E' as the base change of E, so every S-point of E has a base change, an S'-point of E' (EllipticCurveGeom.pointsPullback), and points of exact order N pull back to points of exact order N (EllipticCurveGeom.IsOfExactOrder.pointsPullback). Base change of points is functorial, so the [Γ₁(N)]-structures form a moduli problem over Ell/B (ModuliProblem.gammaOne). For N = 1 the only point of exact order one is the zero section, so [Γ₁(1)] is the trivial moduli problem [Γ(1)] (ModuliProblem.gammaOneOneIso).

The problem [Γ₁(N)] is relatively representable (ModuliProblem.gammaOneRelRepData): for an object (E/S) and a scheme T over S, the [Γ₁(N)]-structures on the base change E_T are the morphisms from T to the exact-order scheme E.exactOrderScheme N over S (ModuliProblem.gammaOneBaseChangeEquiv), the closed subscheme of E on which the universal point has exact order N. It lies in E[N], so for N ≠ 0 the problem [Γ₁(N)] is finite over Ell/B (ModuliProblem.hasProperty_isFinite_gammaOneRelRepData). No hypothesis is placed on B.

Main definitions

• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOne B N: the moduli problem [Γ₁(N)] over Ell/B.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv: the [Γ₁(N)]-structures on an object (E/S) of Ell/B are the S-points of E of exact order N.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv: the [Γ₁(N)]-structures on the base change E_T are the morphisms from T to the exact-order scheme of E.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData: [Γ₁(N)] is relatively representable, by the exact-order scheme.

Main results

• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv_map: the pull-back of a [Γ₁(N)]-structure along an arrow of Ell/B is the base change of its point.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneOneIso: [Γ₁(1)] is the trivial moduli problem.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv_map: the correspondence with morphisms to the exact-order scheme is natural in T.
• TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_isFinite_gammaOneRelRepData: for N ≠ 0, [Γ₁(N)] is finite over Ell/B.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.4 (points of exact order N), §3.2 (the moduli problem [Γ₁(N)]), 3.6.0 (its relative representability by a finite scheme) and Chapter 4.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOne (B : AlgebraicGeometry.Scheme) (N : ℕ) : ModuliProblem B

The moduli problem [Γ₁(N)] over Ell/B (Katz–Mazur, §3.2). A [Γ₁(N)]-structure on an object (E/S) of Ell/B is an S-point of E of exact order N (gammaOneEquiv), and it pulls back along an arrow of Ell/B by base change of points (gammaOneEquiv_map).

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) : (gammaOne B N).obj (Opposite.op X) ≃ { P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap // X.curve.IsOfExactOrder P N }

The [Γ₁(N)]-structures on an object (E/S) of Ell/B are the S-points of E of exact order N.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv_map {B : AlgebraicGeometry.Scheme} {N : ℕ} {X Y : EllObj B} (φ : X ⟶ Y) (α : (gammaOne B N).obj (Opposite.op Y)) : ↑((gammaOneEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gammaOne B N).map φ.op)) α)) = (EllipticCurveGeom.pointsPullback ⋯ ⋯) ↑((gammaOneEquiv Y) α)

The pull-back of a [Γ₁(N)]-structure along an arrow φ of Ell/B is the base change of its point along φ.

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.ModuliProblem.instUniqueObjOppositeEllObjGammaOneOfNatNat {B : AlgebraicGeometry.Scheme} (X : (EllObj B)ᵒᵖ) : Unique ((gammaOne B 1).obj X)

An S-point of exact order one is the zero section, so an object of Ell/B has exactly one [Γ₁(1)]-structure.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneOneIso (B : AlgebraicGeometry.Scheme) : gammaOne B 1 ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuliProblem B)

[Γ₁(1)] is the trivial moduli problem [Γ(1)]: the only point of exact order one of an elliptic curve is its zero section.

Relative representability of [Γ₁(N)]

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) (T : CategoryTheory.Over X.base) : (gammaOne B N).obj (Opposite.op (X.baseChangeFunctor.obj T)) ≃ (T ⟶ X.curve.exactOrderScheme N)

[Γ₁(N)]-structures on base changes are points of the exact-order scheme. For an object X = (E/S) of Ell/B and a scheme T over S, the [Γ₁(N)]-structures on the base change E_T of E correspond to the morphisms T ⟶ E.exactOrderScheme N over S: a structure, a T-point P of E_T of exact order N, corresponds to the morphism whose image in E is P followed by the projection E_T ⟶ E (gammaOneBaseChangeEquiv_apply_left_comp).

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv_apply_left_comp {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) (T : CategoryTheory.Over X.base) (α : (gammaOne B N).obj (Opposite.op (X.baseChangeFunctor.obj T))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((gammaOneBaseChangeEquiv X T) α)) (X.curve.exactOrderLocus N).subschemeι = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑((gammaOneEquiv (X.baseChangeFunctor.obj T)) α)) (CategoryTheory.CategoryStruct.comp (X.curve.baseChangeIso T.hom).hom (CategoryTheory.Limits.pullback.fst X.curve.structureMap T.hom))

The morphism T ⟶ E.exactOrderScheme N of a [Γ₁(N)]-structure on E_T, followed by the inclusion of the exact-order scheme in E, is the point of the structure followed by the projection E_T ⟶ E.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv_apply_left_comp_assoc {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) (T : CategoryTheory.Over X.base) (α : (gammaOne B N).obj (Opposite.op (X.baseChangeFunctor.obj T))) {Z : AlgebraicGeometry.Scheme} (h : X.curve.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((gammaOneBaseChangeEquiv X T) α)) (CategoryTheory.CategoryStruct.comp (X.curve.exactOrderLocus N).subschemeι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ↑((gammaOneEquiv (X.baseChangeFunctor.obj T)) α)) (CategoryTheory.CategoryStruct.comp (X.curve.baseChangeIso T.hom).hom (CategoryTheory.Limits.pullback.fst X.curve.structureMap T.hom))) h

The morphism T ⟶ E.exactOrderScheme N of a [Γ₁(N)]-structure on E_T, followed by the inclusion of the exact-order scheme in E, is the point of the structure followed by the projection E_T ⟶ E.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv_map {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (α : (gammaOne B N).obj (Opposite.op (X.baseChangeFunctor.obj T))) : (gammaOneBaseChangeEquiv X T') ((CategoryTheory.ConcreteCategory.hom ((gammaOne B N).map (X.baseChangeFunctor.map k).op)) α) = CategoryTheory.CategoryStruct.comp k ((gammaOneBaseChangeEquiv X T) α)

Naturality of gammaOneBaseChangeEquiv. Along a morphism k : T' ⟶ T of schemes over the base of X, the morphism T' ⟶ E.exactOrderScheme N of the pull-back to E_{T'} of a [Γ₁(N)]-structure on E_T is the composite of k with the morphism of the structure.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneBaseChangeEquiv_symm_comp {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (a : T ⟶ X.curve.exactOrderScheme N) : (gammaOneBaseChangeEquiv X T').symm (CategoryTheory.CategoryStruct.comp k a) = (CategoryTheory.ConcreteCategory.hom ((gammaOne B N).map (X.baseChangeFunctor.map k).op)) ((gammaOneBaseChangeEquiv X T).symm a)

Naturality of gammaOneBaseChangeEquiv, read backwards: the [Γ₁(N)]-structure on E_{T'} of the composite of k : T' ⟶ T with a morphism T ⟶ E.exactOrderScheme N is the pull-back of the structure on E_T of that morphism.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData (B : AlgebraicGeometry.Scheme) (N : ℕ) : (gammaOne B N).RelRepData

The moduli problem [Γ₁(N)] is relatively representable (Katz–Mazur, 3.6.0). For an object X = (E/S) of Ell/B, the functor T ↦ [Γ₁(N)](E_T/T) on schemes over S is represented by the exact-order scheme E.exactOrderScheme N, the closed subscheme of E of points of exact order N, through gammaOneBaseChangeEquiv. No hypothesis is placed on B, and N need not be invertible on it.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData_rep {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) : (gammaOneRelRepData B N).rep X = X.curve.exactOrderScheme N

The scheme representing [Γ₁(N)]-structures on base changes of X = (E/S) is the exact-order scheme of E.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData_homEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} (X : EllObj B) {T : CategoryTheory.Over X.base} (a : T ⟶ (gammaOneRelRepData B N).rep X) : ((gammaOneRelRepData B N).representableBy X).homEquiv a = (gammaOneBaseChangeEquiv X T).symm (CategoryTheory.CategoryStruct.comp a (CategoryTheory.eqToHom ⋯))

The [Γ₁(N)]-structure on E_T of a morphism from T to the representing scheme is the one given by gammaOneBaseChangeEquiv, after identifying the representing scheme with the exact-order scheme through gammaOneRelRepData_rep.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_isFinite_gammaOneRelRepData (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] : (gammaOneRelRepData B N).HasProperty @AlgebraicGeometry.IsFinite

The moduli problem [Γ₁(N)] is finite over Ell/B (Katz–Mazur, 3.6.0) for N ≠ 0: each representing scheme, the exact-order scheme of an elliptic curve E/S, is a closed subscheme of E[N] and hence finite over S.