Relative representability of [Γ(N)]

Let E/S be an elliptic curve and N a positive integer. The product E[N] ×_S E[N] carries the universal homomorphism (ℤ/Nℤ)² →* E. After base changing E to this product, being a Drinfeld basis is a closed condition. Its closed locus is the scheme EllObj.drinfeldBasisScheme X N.

For every scheme T over S, morphisms from T to this closed locus are naturally equivalent to Drinfeld bases of the base change E_T (ModuliProblem.gammaBaseChangeEquiv). Consequently the integral moduli problem [Γ(N)] is relatively representable by a finite scheme over every object of Ell/B (ModuliProblem.gammaRelRepData and ModuliProblem.hasProperty_isFinite_gammaRelRepData). No invertibility hypothesis on N is used.

Main definitions

• TauCeti.AlgebraicGeometry.EllObj.drinfeldBasisScheme: the closed subscheme of E[N] ×_S E[N] parametrising Drinfeld bases.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv: the natural equivalence between points of that scheme and [Γ(N)]-structures on a base change.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData: relative-representability data for [Γ(N)].

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, §3.1 and Theorem 3.6.0.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.EllObj.drinfeldBasisAmbient {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) : CategoryTheory.Over X.base

The ambient scheme E[N] ×_S E[N] carrying the universal pair of N-torsion points.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.universalDrinfeldBasisHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : Multiplicative (ZMod N × ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj (X.drinfeldBasisAmbient N)).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj (X.drinfeldBasisAmbient N)).curve.structureMap)

The universal homomorphism (ℤ/Nℤ)² →* E_H(H), where H = E[N] ×_S E[N], obtained from the universal pair of points after base changing E to H.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv_universalDrinfeldBasisHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] (a : Multiplicative (ZMod N × ZMod N)) : (X.baseChangePointsEquiv (X.drinfeldBasisAmbient N)) ((X.universalDrinfeldBasisHom N) a) = (X.curve.torsionPairHom N) a

The universal Drinfeld-basis homomorphism corresponds to the universal pair of torsion points under the equivalence between points of a base change and points with values in its base.

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv_pointsPullback_universalDrinfeldBasisHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) (a : Multiplicative (ZMod N × ZMod N)) : (X.baseChangePointsEquiv T) ((EllipticCurveGeom.pointsPullback ⋯ ⋯) ((X.universalDrinfeldBasisHom N) a)) = CategoryTheory.CategoryStruct.comp x ((X.curve.torsionPairHom N) a)

Pulling the universal Drinfeld-basis homomorphism back along a point x of E[N] ×_S E[N] gives the pair of torsion points classified by x.

theorem TauCeti.AlgebraicGeometry.EllObj.pointsPullback_comp_universalDrinfeldBasisHom_eq_iff {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) (ψ : Multiplicative (ZMod N × ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj T).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj T).curve.structureMap)) : (EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (X.universalDrinfeldBasisHom N) = ψ ↔ ∀ (a : Multiplicative (ZMod N × ZMod N)), CategoryTheory.CategoryStruct.comp x ((X.curve.torsionPairHom N) a) = (X.baseChangePointsEquiv T) (ψ a)

Pulling the universal Drinfeld-basis homomorphism back along a point x of E[N] ×_S E[N] gives ψ exactly when x classifies the pair of torsion points underlying ψ.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.universalDrinfeldBasisLocus {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : (X.drinfeldBasisAmbient N).left.IdealSheafData

The ideal sheaf on E[N] ×_S E[N] cutting out the locus where its universal pair is a Drinfeld basis.

theorem TauCeti.AlgebraicGeometry.EllObj.universalDrinfeldBasisLocus_eq {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : X.universalDrinfeldBasisLocus N = (X.baseChangeFunctor.obj (X.drinfeldBasisAmbient N)).curve.drinfeldBasisLocus N (X.universalDrinfeldBasisHom N)

The universal Drinfeld-basis locus is the Drinfeld-basis locus of the universal homomorphism on the base change of E to E[N] ×_S E[N].

theorem TauCeti.AlgebraicGeometry.EllObj.universalDrinfeldBasisLocus_le_ker_iff {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) : X.universalDrinfeldBasisLocus N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left x) ↔ (X.baseChangeFunctor.obj T).curve.IsDrinfeldBasis N ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (X.universalDrinfeldBasisHom N))

A point x of E[N] ×_S E[N] factors through the universal Drinfeld-basis locus exactly when the universal pair pulls back along x to a Drinfeld basis.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.EllObj.drinfeldBasisScheme {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : CategoryTheory.Over X.base

The finite S-scheme parametrising Drinfeld bases of E[N]: the closed subscheme of E[N] ×_S E[N] on which the universal pair is a Drinfeld basis.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.EllObj.drinfeldBasisSchemeι {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : X.drinfeldBasisScheme N ⟶ X.drinfeldBasisAmbient N

The closed immersion from the Drinfeld-basis scheme to E[N] ×_S E[N].

noncomputable def TauCeti.AlgebraicGeometry.EllObj.liftDrinfeldBasisScheme {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) (hx : (X.baseChangeFunctor.obj T).curve.IsDrinfeldBasis N ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (X.universalDrinfeldBasisHom N))) : T ⟶ X.drinfeldBasisScheme N

A point x of E[N] ×_S E[N] along which the universal pair pulls back to a Drinfeld basis lifts to the Drinfeld-basis scheme.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.liftDrinfeldBasisScheme_drinfeldBasisSchemeι {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) (hx : (X.baseChangeFunctor.obj T).curve.IsDrinfeldBasis N ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (X.universalDrinfeldBasisHom N))) : CategoryTheory.CategoryStruct.comp (X.liftDrinfeldBasisScheme N x hx) (X.drinfeldBasisSchemeι N) = x

The lift of x to the Drinfeld-basis scheme factors x through the closed immersion.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.liftDrinfeldBasisScheme_drinfeldBasisSchemeι_assoc {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] {T : CategoryTheory.Over X.base} (x : T ⟶ X.drinfeldBasisAmbient N) (hx : (X.baseChangeFunctor.obj T).curve.IsDrinfeldBasis N ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (X.universalDrinfeldBasisHom N))) {Z : CategoryTheory.Over X.base} (h : X.drinfeldBasisAmbient N ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.liftDrinfeldBasisScheme N x hx) (CategoryTheory.CategoryStruct.comp (X.drinfeldBasisSchemeι N) h) = CategoryTheory.CategoryStruct.comp x h

The lift of x to the Drinfeld-basis scheme factors x through the closed immersion.

instance TauCeti.AlgebraicGeometry.EllObj.isFinite_drinfeldBasisScheme_hom {B : AlgebraicGeometry.Scheme} (X : EllObj B) (N : ℕ) [NeZero N] : AlgebraicGeometry.IsFinite (X.drinfeldBasisScheme N).hom

The Drinfeld-basis scheme is finite over the base.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaStructureOfSchemeHom {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T : CategoryTheory.Over X.base} (y : T ⟶ X.drinfeldBasisScheme N) : Multiplicative (ZMod N × ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj T).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj T).curve.structureMap)

The homomorphism defining the [Γ(N)]-structure associated to a point of the Drinfeld-basis scheme.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.baseChangePointsEquiv_gammaStructureOfSchemeHom {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T : CategoryTheory.Over X.base} (y : T ⟶ X.drinfeldBasisScheme N) (a : Multiplicative (ZMod N × ZMod N)) : (X.baseChangePointsEquiv T) ((gammaStructureOfSchemeHom X y) a) = CategoryTheory.CategoryStruct.comp y (CategoryTheory.CategoryStruct.comp (X.drinfeldBasisSchemeι N) ((X.curve.torsionPairHom N) a))

theorem TauCeti.AlgebraicGeometry.ModuliProblem.isDrinfeldBasis_gammaStructureOfSchemeHom {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T : CategoryTheory.Over X.base} (y : T ⟶ X.drinfeldBasisScheme N) : (X.baseChangeFunctor.obj T).curve.IsDrinfeldBasis N (gammaStructureOfSchemeHom X y)

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) (T : CategoryTheory.Over X.base) : (gamma B N).obj (Opposite.op (X.baseChangeFunctor.obj T)) ≃ (T ⟶ X.drinfeldBasisScheme N)

[Γ(N)]-structures on base changes are points of the Drinfeld-basis scheme. For an object X = (E/S) of Ell/B and a scheme T over S, Drinfeld bases of E_T[N] correspond naturally to morphisms T ⟶ X.drinfeldBasisScheme N over S.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv_apply_symm_apply {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) (T : CategoryTheory.Over X.base) (y : T ⟶ X.drinfeldBasisScheme N) : (gammaBaseChangeEquiv X T) ((gammaEquiv (X.baseChangeFunctor.obj T)).symm ⟨gammaStructureOfSchemeHom X y, ⋯⟩) = y

The point of the Drinfeld-basis scheme attached to the structure defined by a point y is y itself.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv_symm_apply {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) (T : CategoryTheory.Over X.base) (y : T ⟶ X.drinfeldBasisScheme N) : (gammaBaseChangeEquiv X T).symm y = (gammaEquiv (X.baseChangeFunctor.obj T)).symm ⟨gammaStructureOfSchemeHom X y, ⋯⟩

The inverse of gammaBaseChangeEquiv sends a point to its associated universal [Γ(N)]-structure.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.pointsPullback_gammaStructureOfSchemeHom {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (y : T ⟶ X.drinfeldBasisScheme N) : (EllipticCurveGeom.pointsPullback ⋯ ⋯).comp (gammaStructureOfSchemeHom X y) = gammaStructureOfSchemeHom X (CategoryTheory.CategoryStruct.comp k y)

The [Γ(N)]-structure associated to a point commutes with base change.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv_map {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (α : (gamma B N).obj (Opposite.op (X.baseChangeFunctor.obj T))) : (gammaBaseChangeEquiv X T') ((CategoryTheory.ConcreteCategory.hom ((gamma B N).map (X.baseChangeFunctor.map k).op)) α) = CategoryTheory.CategoryStruct.comp k ((gammaBaseChangeEquiv X T) α)

Naturality of gammaBaseChangeEquiv: pulling a [Γ(N)]-structure back along k : T' ⟶ T precomposes its point of the Drinfeld-basis scheme with k.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaBaseChangeEquiv_symm_comp {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (y : T ⟶ X.drinfeldBasisScheme N) : (gammaBaseChangeEquiv X T').symm (CategoryTheory.CategoryStruct.comp k y) = (CategoryTheory.ConcreteCategory.hom ((gamma B N).map (X.baseChangeFunctor.map k).op)) ((gammaBaseChangeEquiv X T).symm y)

Naturality of gammaBaseChangeEquiv, read backwards.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] : (gamma B N).RelRepData

The integral moduli problem [Γ(N)] is relatively representable (Katz–Mazur, 3.6.0). For an elliptic curve E/S, it is represented by the closed Drinfeld-basis locus in E[N] ×_S E[N].

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData_rep {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) : (gammaRelRepData B N).rep X = X.drinfeldBasisScheme N

The scheme representing [Γ(N)]-structures on base changes of X = (E/S) is the closed Drinfeld-basis locus in E[N] ×_S E[N].

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData_homEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) {T : CategoryTheory.Over X.base} (y : T ⟶ (gammaRelRepData B N).rep X) : ((gammaRelRepData B N).representableBy X).homEquiv y = (gammaBaseChangeEquiv X T).symm (CategoryTheory.CategoryStruct.comp y (CategoryTheory.eqToHom ⋯))

The [Γ(N)]-structure on E_T of a morphism from T to the representing scheme is the one given by gammaBaseChangeEquiv, after identifying the representing scheme with the Drinfeld-basis scheme through gammaRelRepData_rep.

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

The integral moduli problem [Γ(N)] is finite over Ell/B (Katz–Mazur, 3.6.0): its representing scheme is a closed subscheme of E[N] ×_S E[N].