Comparison of Drinfeld and naive [Γ₁(N)]- and [Γ(N)]-structures

This file compares the integral Drinfeld moduli problems [Γ₁(N)] (ModuliProblem.gammaOne) and [Γ(N)] (ModuliProblem.gamma) over Ell/B with their naive counterparts (ModuliProblem.gammaOneNaive, ModuliProblem.gammaNaive), following Katz–Mazur §3.7:

1. For [Γ₁(N)]: over a base scheme B on which N is invertible, a point P of exact order N on an elliptic curve E/S over B gives the naive [Γ₁(N)]-structure a ↦ aP, injective on every fibre (EllipticCurveGeom.IsOfExactOrder.isFiberwiseInjective). This defines an isomorphism [Γ₁(N)] ⟶ [Γ₁(N)]_naive (ModuliProblem.gammaOneToGammaOneNaive). Consequently [Γ₁(N)] inherits rigidity (ModuliProblem.isRigid_gammaOne) and is represented by the fine curve Y₁(N) (ModuliProblem.gammaOneRepresentableBy) for N ≥ 4.
2. For [Γ(N)]: over an arbitrary base B, every naive [Γ(N)]-structure is a Drinfeld basis (EllipticCurveGeom.IsFiberwiseInjective.isDrinfeldBasis), giving a GL₂(ℤ/Nℤ)-equivariant monomorphism [Γ(N)]_naive ⟶ [Γ(N)] (ModuliProblem.gammaNaiveToGamma). Over a base B on which N is invertible, every Drinfeld basis is conversely a naive [Γ(N)]-structure (EllipticCurveGeom.IsDrinfeldBasis.isFiberwiseInjective), giving the inverse morphism [Γ(N)] ⟶ [Γ(N)]_naive (ModuliProblem.gammaToGammaNaive) and the isomorphism [Γ(N)] ≅ [Γ(N)]_naive (ModuliProblem.gammaIsoGammaNaive). Over such a base, [Γ(N)] therefore inherits from [Γ(N)]_naive freeness of the GL₂(ℤ/Nℤ)-action over nonempty bases (ModuliProblem.eq_one_of_gammaAction_hom_app_eq_self), rigidity for N ≥ 3 (ModuliProblem.isRigid_gamma), and étaleness over Ell/B (ModuliProblem.hasProperty_etale_gammaRelRepData), making [Γ(N)] finite étale over Ell/B together with ModuliProblem.hasProperty_isFinite_gammaRelRepData.

Main definitions

• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneToGammaOneNaive B N hN: the morphism from Drinfeld to naive [Γ₁(N)]-structures over a base B on which N is invertible.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveToGamma B N: the morphism from naive to Drinfeld [Γ(N)]-structures over an arbitrary base B.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaToGammaNaive B N hN and TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive B N hN: the inverse morphism and isomorphism [Γ(N)] ≅ [Γ(N)]_naive over a base B on which N is invertible.

Main results

• TauCeti.AlgebraicGeometry.ModuliProblem.naiveLevelEquiv_gammaOneToGammaOneNaive_app_apply: the naive structure of a point P of exact order N sends a to aP.
• TauCeti.AlgebraicGeometry.ModuliProblem.isIso_gammaOneToGammaOneNaive: the comparison is an isomorphism.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy: Y₁(N) represents the Drinfeld problem for N ≥ 4 invertible on the base.
• TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gammaOne: where N is invertible on B, Drinfeld [Γ₁(N)]-structures are rigid for N ≥ 4.
• TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveAction_hom_comp_gammaNaiveToGamma and TauCeti.AlgebraicGeometry.ModuliProblem.gammaAction_hom_comp_gammaToGammaNaive: the comparison morphisms between [Γ(N)] and [Γ(N)]_naive are GL₂(ℤ/Nℤ)-equivariant.
• TauCeti.AlgebraicGeometry.ModuliProblem.eq_one_of_gammaAction_hom_app_eq_self: where N is invertible on B, GL₂(ℤ/Nℤ) acts freely on [Γ(N)] over a nonempty base.
• TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gamma: where N is invertible on B, [Γ(N)] is rigid for N ≥ 3 (Katz–Mazur 2.7.2).
• TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_etale_gammaRelRepData: where N is invertible on B, [Γ(N)] is étale over Ell/B (Katz–Mazur 3.7.1).

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.7.2 (rigidity for N ≥ 3), §3.1 ([Γ(N)]-structures), §3.2 ([Γ₁(N)]-structures), and §3.7 / 3.7.1 (comparison with naive level structures where N is invertible).

[Γ₁(N)] where N is invertible

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneToGammaOneNaive (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) : gammaOne B N ⟶ gammaOneNaive B N

Drinfeld [Γ₁(N)]-structures are naive where N is invertible. Over a base B on which N is invertible, the point P of exact order N of a [Γ₁(N)]-structure gives the naive [Γ₁(N)]-structure a ↦ aP, injective on every fibre by EllipticCurveGeom.IsOfExactOrder.isFiberwiseInjective. This is natural in the object of Ell/B.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.naiveLevelEquiv_gammaOneToGammaOneNaive_app_apply {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (X : EllObj B) (α : (gammaOne B N).obj (Opposite.op X)) (a : ZMod N) : ↑((naiveLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gammaOneToGammaOneNaive B N hN).app (Opposite.op X))) α)) (Multiplicative.ofAdd a) = ↑((gammaOneEquiv X) α) ^ a.val

The naive [Γ₁(N)]-structure of a point P of exact order N sends a to aP.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.naiveLevelEquiv_gammaOneToGammaOneNaive_app_one {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (X : EllObj B) (α : (gammaOne B N).obj (Opposite.op X)) : ↑((naiveLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gammaOneToGammaOneNaive B N hN).app (Opposite.op X))) α)) (Multiplicative.ofAdd 1) = ↑((gammaOneEquiv X) α)

The naive level structure associated to a Drinfeld point sends 1 to that point, including when N = 1.

instance TauCeti.AlgebraicGeometry.ModuliProblem.isIso_gammaOneToGammaOneNaive {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : CategoryTheory.IsIso (gammaOneToGammaOneNaive B N hN)

Where N is invertible, the comparison from Drinfeld to naive [Γ₁(N)] is an isomorphism of moduli problems.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv_inv_gammaOneToGammaOneNaive_app {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (X : EllObj B) (α : (gammaOneNaive B N).obj (Opposite.op X)) : ↑((gammaOneEquiv X) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((gammaOneToGammaOneNaive B N hN).app (Opposite.op X)))) α)) = ↑((naiveLevelEquiv X) α) (Multiplicative.ofAdd 1)

The inverse comparison retains the point given by the image of 1 under the naive level structure.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (h4 : 4 ≤ N) : CategoryTheory.Functor.RepresentableBy (gammaOne B N) (EllObj.yOne B N)

For N ≥ 4 invertible on B, the existing fine curve Y₁(N) also represents the integral Drinfeld [Γ₁(N)] problem restricted to B.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneEquiv_gammaOneRepresentableBy_homEquiv {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (h4 : 4 ≤ N) {X : EllObj B} (k : X ⟶ EllObj.yOne B N) : ↑((gammaOneEquiv X) ((gammaOneRepresentableBy h4).homEquiv k)) = (EllipticCurveGeom.pointsPullback ⋯ ⋯) (EllObj.universalTatePoint B)

The Drinfeld point classified by an arrow to Y₁(N) is the pullback of the universal Tate point (0, 0).

theorem TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gammaOne (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) (hN4 : 4 ≤ N) : (gammaOne B N).IsRigid

[Γ₁(N)] is rigid for N ≥ 4 where N is invertible. Over a base B on which N is invertible, [Γ₁(N)] maps to the rigid naive problem [Γ₁(N)]_naive (ModuliProblem.isRigid_gammaOneNaive).

[Γ(N)] and [Γ(N)]_naive

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

Naive [Γ(N)]-structures are Drinfeld bases over every base. The morphism of moduli problems [Γ(N)]_naive ⟶ [Γ(N)] over Ell/B sending a homomorphism (ℤ/Nℤ)² →* E(S) injective on every fibre to the Drinfeld basis it defines (EllipticCurveGeom.IsFiberwiseInjective.isDrinfeldBasis). No invertibility hypothesis on N is needed.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaEquiv_gammaNaiveToGamma_app {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (X : EllObj B) (α : (gammaNaive B N).obj (Opposite.op X)) : ↑((gammaEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gammaNaiveToGamma B N).app (Opposite.op X))) α)) = ↑((naiveLevelEquiv X) α)

gammaNaiveToGamma preserves the underlying homomorphism (ℤ/Nℤ)² →* E(S).

instance TauCeti.AlgebraicGeometry.ModuliProblem.mono_gammaNaiveToGamma {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] : CategoryTheory.Mono (gammaNaiveToGamma B N)

Naive [Γ(N)]-structures form a subproblem of Drinfeld [Γ(N)]-structures over every base.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveAction_hom_comp_gammaNaiveToGamma (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) : CategoryTheory.CategoryStruct.comp ((gammaNaiveAction B N) g).asIso.hom (gammaNaiveToGamma B N) = CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) ((gammaAction B N) g).asIso.hom

The comparison [Γ(N)]_naive ⟶ [Γ(N)] is GL₂(ℤ/Nℤ)-equivariant.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveAction_hom_comp_gammaNaiveToGamma_assoc (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) {Z : ModuliProblem B} (h : gamma B N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((gammaNaiveAction B N) g).asIso.hom (CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) h) = CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) (CategoryTheory.CategoryStruct.comp ((gammaAction B N) g).asIso.hom h)

The comparison [Γ(N)]_naive ⟶ [Γ(N)] is GL₂(ℤ/Nℤ)-equivariant.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaToGammaNaive (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) : gamma B N ⟶ gammaNaive B N

Drinfeld [Γ(N)]-structures are naive where N is invertible (Katz–Mazur, §3.7). Over a base B on which N is invertible, every Drinfeld basis (ℤ/Nℤ)² →* E(S) is injective on every fibre (EllipticCurveGeom.IsDrinfeldBasis.isFiberwiseInjective), defining a morphism of moduli problems [Γ(N)] ⟶ [Γ(N)]_naive inverse to gammaNaiveToGamma.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.naiveLevelEquiv_gammaToGammaNaive_app {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (X : EllObj B) (α : (gamma B N).obj (Opposite.op X)) : ↑((naiveLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom ((gammaToGammaNaive B N hN).app (Opposite.op X))) α)) = ↑((gammaEquiv X) α)

gammaToGammaNaive preserves the underlying homomorphism (ℤ/Nℤ)² →* E(S).

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaToGammaNaive_comp_gammaNaiveToGamma {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) (gammaNaiveToGamma B N) = CategoryTheory.CategoryStruct.id (gamma B N)

gammaToGammaNaive and gammaNaiveToGamma compose to the identity on [Γ(N)].

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaToGammaNaive_comp_gammaNaiveToGamma_assoc {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} {Z : ModuliProblem B} (h : gamma B N ⟶ Z) : CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) (CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) h) = h

gammaToGammaNaive and gammaNaiveToGamma compose to the identity on [Γ(N)].

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveToGamma_comp_gammaToGammaNaive {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) (gammaToGammaNaive B N hN) = CategoryTheory.CategoryStruct.id (gammaNaive B N)

gammaNaiveToGamma and gammaToGammaNaive compose to the identity on [Γ(N)]_naive.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveToGamma_comp_gammaToGammaNaive_assoc {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} {Z : ModuliProblem B} (h : gammaNaive B N ⟶ Z) : CategoryTheory.CategoryStruct.comp (gammaNaiveToGamma B N) (CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) h) = h

gammaNaiveToGamma and gammaToGammaNaive compose to the identity on [Γ(N)]_naive.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) : gamma B N ≅ gammaNaive B N

Drinfeld and naive [Γ(N)]-structures coincide where N is invertible (Katz–Mazur, §3.7): over a base B on which N is invertible, gammaToGammaNaive and gammaNaiveToGamma are mutually inverse isomorphisms between [Γ(N)] and [Γ(N)]_naive.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive_hom {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : (gammaIsoGammaNaive B N hN).hom = gammaToGammaNaive B N hN

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive_inv {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : (gammaIsoGammaNaive B N hN).inv = gammaNaiveToGamma B N

instance TauCeti.AlgebraicGeometry.ModuliProblem.isIso_gammaToGammaNaive {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} : CategoryTheory.IsIso (gammaToGammaNaive B N hN)

Where N is invertible on B, gammaToGammaNaive is an isomorphism.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.isIso_gammaNaiveToGamma {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) : CategoryTheory.IsIso (gammaNaiveToGamma B N)

Where N is invertible on B, gammaNaiveToGamma is an isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaAction_hom_comp_gammaToGammaNaive {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) : CategoryTheory.CategoryStruct.comp ((gammaAction B N) g).asIso.hom (gammaToGammaNaive B N hN) = CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) ((gammaNaiveAction B N) g).asIso.hom

The comparison [Γ(N)] ⟶ [Γ(N)]_naive is GL₂(ℤ/Nℤ)-equivariant.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.gammaAction_hom_comp_gammaToGammaNaive_assoc {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ) {Z : ModuliProblem B} (h : gammaNaive B N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((gammaAction B N) g).asIso.hom (CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) h) = CategoryTheory.CategoryStruct.comp (gammaToGammaNaive B N hN) (CategoryTheory.CategoryStruct.comp ((gammaNaiveAction B N) g).asIso.hom h)

The comparison [Γ(N)] ⟶ [Γ(N)]_naive is GL₂(ℤ/Nℤ)-equivariant.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.eq_one_of_gammaAction_hom_app_eq_self {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] {X : EllObj B} [Nonempty ↥X.base] (hN : ∀ (b : ↥B), ↑N ≠ 0) {g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ} {α : (gamma B N).obj (Opposite.op X)} (h : (CategoryTheory.ConcreteCategory.hom (((gammaAction B N) g).asIso.hom.app (Opposite.op X))) α = α) : g = 1

Where N is invertible, GL₂(ℤ/Nℤ) acts freely on [Γ(N)] over a nonempty base.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gamma (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) (hN3 : 3 ≤ N) : (gamma B N).IsRigid

[Γ(N)] is rigid for N ≥ 3 where N is invertible (Katz–Mazur, 2.7.2). Over a base B on which N is invertible, [Γ(N)] is isomorphic to the rigid naive problem [Γ(N)]_naive (ModuliProblem.isRigid_gammaNaive).

theorem TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_etale_gammaRelRepData (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) : (gammaRelRepData B N).HasProperty @AlgebraicGeometry.Etale

The moduli problem [Γ(N)] is étale over Ell/B when N is invertible on B (Katz–Mazur, 3.7.1): where N is invertible on B, [Γ(N)] is isomorphic to [Γ(N)]_naive, whose representing schemes are étale over their bases. Together with ModuliProblem.hasProperty_isFinite_gammaRelRepData, this makes [Γ(N)] finite étale over Ell/B.