The moduli problem [Γ(N)]

Following Katz and Mazur, a [Γ(N)]-structure on an elliptic curve E over a scheme S is a Drinfeld basis of E[N]: a homomorphism φ : (ℤ/Nℤ)² →* E(S) such that the divisor ∑_{a ∈ (ℤ/Nℤ)²} [φ a] on E is the closed subscheme E[N] (EllipticCurveGeom.IsDrinfeldBasis). This is the notion of full level-N structure over every base, including bases on which N is not invertible; there the naive [Γ(N)]-structures (ModuliProblem.gammaNaive) are not the right notion.

An arrow (E'/S') ⟶ (E/S) of Ell/B exhibits E' as the base change of E, and Drinfeld bases pull back to Drinfeld bases under base change of points (EllipticCurveGeom.IsDrinfeldBasis.pointsPullback). Base change of points is functorial, so the [Γ(N)]-structures form a moduli problem over Ell/B (ModuliProblem.gamma), an instance of ModuliProblem.homLevel. Precomposing a Drinfeld basis with an automorphism of (ℤ/Nℤ)² gives another Drinfeld basis (EllipticCurveGeom.isDrinfeldBasis_comp_mulEquiv_iff), which defines the right action of GL₂(ℤ/Nℤ) on [Γ(N)] (ModuliProblem.gammaAction). For N = 1 every homomorphism from the trivial group is a Drinfeld basis, so [Γ(1)] is the trivial moduli problem (ModuliProblem.gammaLevelOneIso).

Main definitions

• TauCeti.AlgebraicGeometry.ModuliProblem.gamma B N: the moduli problem [Γ(N)] over Ell/B.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv: the [Γ(N)]-structures on an object (E/S) of Ell/B are the Drinfeld bases of E[N].
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaAction B N: the right action of GL₂(ℤ/Nℤ) on [Γ(N)].

Main results

• TauCeti.AlgebraicGeometry.EllObj.Hom.isDrinfeldBasis_pointsPullback: Drinfeld bases pull back along arrows of Ell/B.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_map: the pull-back of a [Γ(N)]-structure along an arrow of Ell/B is its composite with base change of points.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_gammaAction_hom_app: a matrix g in GL₂(ℤ/Nℤ) sends a [Γ(N)]-structure φ to φ ∘ g.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaLevelOneIso: [Γ(1)] is the trivial moduli problem.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, §3.1 (the moduli problem [Γ(N)]), Chapter 4, and §7.1 (the action of GL₂(ℤ/Nℤ) on [Γ(N)]).

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.isDrinfeldBasis_pointsPullback {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} {N : ℕ} [NeZero N] {φ : Multiplicative (ZMod N × ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y) (h : Y.curve.IsDrinfeldBasis N φ) : X.curve.IsDrinfeldBasis N ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)

Drinfeld bases pull back along arrows of Ell/B: an arrow f : X ⟶ Y exhibits X as a base change of Y, and a Drinfeld basis (ℤ/Nℤ)² →* E(S) of E[N] stays one after composing with base change of points along f.

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

The moduli problem [Γ(N)] over Ell/B (Katz–Mazur, §3.1). A [Γ(N)]-structure on an object (E/S) of Ell/B is a Drinfeld basis φ : (ℤ/Nℤ)² →* E(S) of E[N] (gammaEquiv), and it pulls back along an arrow of Ell/B by base change of points (gammaEquiv_map).

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) : (gamma B N).obj (Opposite.op X) ≃ { φ : Multiplicative (ZMod N × ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap) // X.curve.IsDrinfeldBasis N φ }

The [Γ(N)]-structures on an object (E/S) of Ell/B are the Drinfeld bases (ℤ/Nℤ)² →* E(S) of E[N].

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_map {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {X Y : EllObj B} (φ : X ⟶ Y) (α : (gamma B N).obj (Opposite.op Y)) : ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gamma B N).map φ.op)) α)) = (EllipticCurveGeom.pointsPullback ⋯ ⋯).comp ↑((gammaEquiv Y) α)

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

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gamma_hom_ext {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {P : ModuliProblem B} {f g : P ⟶ gamma B N} (h : ∀ (X : EllObj B) (α : P.obj (Opposite.op X)), ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) α)) = ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) α))) : f = g

Two morphisms of moduli problems into [Γ(N)] agree once they assign the same homomorphism (ℤ/Nℤ)² →* E(S) to every structure.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gamma_hom_ext_iff {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {P : ModuliProblem B} {f g : P ⟶ gamma B N} : f = g ↔ ∀ (X : EllObj B) (α : P.obj (Opposite.op X)), ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) α)) = ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) α))

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaAction (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] : (GL (Fin 2) (ZMod N))ᵐᵒᵖ →* CategoryTheory.Aut (gamma B N)

The right action of GL₂(ℤ/Nℤ) on the moduli problem [Γ(N)] (Katz–Mazur, §3.1 and §7.1). An invertible matrix g acts on (ℤ/Nℤ)² by TauCeti.zmodProdMulAutEquiv, and precomposing a Drinfeld basis φ : (ℤ/Nℤ)² →* E(S) with g gives another Drinfeld basis (EllipticCurveGeom.isDrinfeldBasis_comp_mulEquiv_iff). Since φ ∘ (g h) = (φ ∘ g) ∘ h, this is a right action, that is, a homomorphism from (GL₂(ℤ/Nℤ))ᵐᵒᵖ to Aut (gamma B N). No invertibility hypothesis on N is needed.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_gammaAction_hom_app {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) (X : EllObj B) (α : (gamma B N).obj (Opposite.op X)) : ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (((gammaAction B N) g).asIso.hom.app (Opposite.op X))) α)) = (↑((gammaEquiv X) α)).comp (MulEquiv.toMonoidHom ((zmodProdMulAutEquiv N) (MulOpposite.unop g)))

A matrix g sends a [Γ(N)]-structure φ : (ℤ/Nℤ)² →* E(S) to φ ∘ g.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_gammaAction_inv_app {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) (X : EllObj B) (α : (gamma B N).obj (Opposite.op X)) : ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom (((gammaAction B N) g).asIso.inv.app (Opposite.op X))) α)) = (↑((gammaEquiv X) α)).comp (MulEquiv.symm ((zmodProdMulAutEquiv N) (MulOpposite.unop g))).toMonoidHom

The inverse of the automorphism of [Γ(N)] given by a matrix g sends a [Γ(N)]-structure φ : (ℤ/Nℤ)² →* E(S) to φ ∘ g⁻¹.

@[instance_reducible]

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

Every homomorphism from the trivial group (ℤ/1ℤ)² is a Drinfeld basis of E[1], so an object of Ell/B has exactly one [Γ(1)]-structure.

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

[Γ(1)] is the trivial moduli problem: every homomorphism from the trivial group is a Drinfeld basis of E[1].