Moduli problems of homomorphisms to the group of points

Let A be a group. Many level structures on an elliptic curve E over a scheme S are homomorphisms φ : A →* E(S) to the group of S-points of E satisfying a condition p: the naive level structures (ModuliProblem.naiveLevel) ask that φ be injective on every fibre, and the [Γ(N)]-structures (ModuliProblem.gamma) that φ be a Drinfeld basis of E[N].

An arrow (E'/S') ⟶ (E/S) of Ell/B exhibits E' as the base change of E, and composing with base change of points (EllipticCurveGeom.pointsPullback) turns a homomorphism A →* E(S) into a homomorphism A →* E'(S'). When the condition p is stable under this pull-back, the homomorphisms satisfying it form a moduli problem over Ell/B (ModuliProblem.homLevel). Restriction along a homomorphism A' →* A which carries the condition on A to the condition on A' is a morphism of such moduli problems (ModuliProblem.homLevelMap).

Main definitions

• TauCeti.AlgebraicGeometry.ModuliProblem.homLevel B A p hp: the moduli problem of homomorphisms A →* E(S) satisfying a condition p stable under base change.
• TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv: its level structures on an object (E/S) of Ell/B are the homomorphisms A →* E(S) satisfying p.
• TauCeti.AlgebraicGeometry.ModuliProblem.homLevelMap: restriction of level structures along a homomorphism of groups.
• TauCeti.AlgebraicGeometry.ModuliProblem.homLevelAction: the right action of automorphisms of the source group, for a condition invariant under precomposition.

Main results

• TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_map: the pull-back of a level structure along an arrow of Ell/B is its composite with base change of points.
• TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_homLevelMap_app: restriction along ψ composes a level structure with ψ.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Chapter 4.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.homLevel (B : AlgebraicGeometry.Scheme) (A : Type) [Group A] (p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop) (hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)) : ModuliProblem B

The moduli problem of homomorphisms A →* E(S) satisfying p over Ell/B, for a condition p stable under base change of points. Its level structures on an object (E/S) of Ell/B are the homomorphisms A →* E(S) satisfying p (homLevelEquiv), and they pull back along an arrow of Ell/B by base change of points (homLevelEquiv_map). The group A lies in Type, as the groups (ℤ/Nℤ)ʳ of level structures do, so that the level structures lie in the universe Type (u + 1) of moduli problems.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (X : EllObj B) : (homLevel B A p ⋯).obj (Opposite.op X) ≃ { φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap) // p X φ }

The level structures of homLevel B A p hp on an object (E/S) of Ell/B are the homomorphisms A →* E(S) satisfying p. Unification cannot recover the proof hp from the type of a level structure, by proof irrelevance, so instances of homLevel pass it by name.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_map {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} {X Y : EllObj B} (f : X ⟶ Y) (α : (homLevel B A p ⋯).obj (Opposite.op Y)) : ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom ((homLevel B A p ⋯).map f.op)) α)) = (EllipticCurveGeom.pointsPullback ⋯ ⋯).comp ↑((homLevelEquiv Y) α)

The pull-back of a level structure of homLevel B A p hp along an arrow f of Ell/B is its composite with base change of points along f.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevel_hom_ext {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} {P : ModuliProblem B} {f g : P ⟶ homLevel B A p ⋯} (h : ∀ (X : EllObj B) (α : P.obj (Opposite.op X)), ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) α)) = ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) α))) : f = g

Two morphisms into homLevel agree if their underlying homomorphisms agree on every level structure.

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevel_hom_ext_iff {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} {P : ModuliProblem B} {f g : P ⟶ homLevel B A p ⋯} : f = g ↔ ∀ (X : EllObj B) (α : P.obj (Opposite.op X)), ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) α)) = ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op X))) α))

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.homLevelMap (B : AlgebraicGeometry.Scheme) {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} {A' : Type} [Group A'] {p' : (X : EllObj B) → (A' →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp' : ∀ {X Y : EllObj B} {φ : A' →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p' Y φ → p' X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (ψ : A' →* A) (hψ : ∀ (X : EllObj B) (φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)), p X φ → p' X (φ.comp ψ)) : homLevel B A p ⋯ ⟶ homLevel B A' p' ⋯

Restriction of level structures. A homomorphism ψ : A' →* A carrying homomorphisms satisfying p to homomorphisms satisfying p' restricts level structures of homLevel B A p hp to level structures of homLevel B A' p' hp', φ ↦ φ ∘ ψ.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_homLevelMap_app {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} {A' : Type} [Group A'] {p' : (X : EllObj B) → (A' →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp' : ∀ {X Y : EllObj B} {φ : A' →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p' Y φ → p' X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (ψ : A' →* A) (hψ : ∀ (X : EllObj B) (φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)), p X φ → p' X (φ.comp ψ)) (X : EllObj B) (α : (homLevel B A p ⋯).obj (Opposite.op X)) : ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom ((homLevelMap B ψ hψ).app (Opposite.op X))) α)) = (↑((homLevelEquiv X) α)).comp ψ

Restriction along ψ composes a level structure with ψ.

noncomputable def TauCeti.AlgebraicGeometry.ModuliProblem.homLevelAction (B : AlgebraicGeometry.Scheme) (A : Type) [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (hσ : ∀ (X : EllObj B) (φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) (σ : MulAut A), p X φ → p X (φ.comp (MulEquiv.toMonoidHom σ))) : (MulAut A)ᵐᵒᵖ →* CategoryTheory.Aut (homLevel B A p ⋯)

The right action of automorphisms of A on level structures whose condition is invariant under precomposition. An automorphism σ sends a homomorphism φ to φ ∘ σ.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_homLevelAction_hom_app {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (hσ : ∀ (X : EllObj B) (φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) (σ : MulAut A), p X φ → p X (φ.comp (MulEquiv.toMonoidHom σ))) (σ : (MulAut A)ᵐᵒᵖ) (X : EllObj B) (α : (homLevel B A p ⋯).obj (Opposite.op X)) : ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (((homLevelAction B A hσ) σ).asIso.hom.app (Opposite.op X))) α)) = (↑((homLevelEquiv X) α)).comp (MulEquiv.toMonoidHom (MulOpposite.unop σ))

The action of σ precomposes a level structure with σ.

@[simp]

theorem TauCeti.AlgebraicGeometry.ModuliProblem.homLevelEquiv_homLevelAction_inv_app {B : AlgebraicGeometry.Scheme} {A : Type} [Group A] {p : (X : EllObj B) → (A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) → Prop} {hp : ∀ {X Y : EllObj B} {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over Y.base) ⟶ CategoryTheory.Over.mk Y.curve.structureMap)} (f : X ⟶ Y), p Y φ → p X ((EllipticCurveGeom.pointsPullback ⋯ ⋯).comp φ)} (hσ : ∀ (X : EllObj B) (φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap)) (σ : MulAut A), p X φ → p X (φ.comp (MulEquiv.toMonoidHom σ))) (σ : (MulAut A)ᵐᵒᵖ) (X : EllObj B) (α : (homLevel B A p ⋯).obj (Opposite.op X)) : ↑((homLevelEquiv X) ((CategoryTheory.ConcreteCategory.hom (((homLevelAction B A hσ) σ).asIso.inv.app (Opposite.op X))) α)) = (↑((homLevelEquiv X) α)).comp (MulEquiv.symm (MulOpposite.unop σ)).toMonoidHom

The inverse action precomposes a level structure with σ⁻¹.