Moduli problems over Ell/B #
Following Katz and Mazur, a moduli problem over the category Ell/B of elliptic curves over
B-schemes is a contravariant functor π« from Ell/B to types: it assigns to an elliptic curve
E over a B-scheme S a type π«(E/S) of "level structures" on E, and to every cartesian
arrow (E'/S') βΆ (E/S) a pull-back map π«(E/S) βΆ π«(E'/S').
For an object X = (E/S) of Ell/B, the fibre π«.fibre X is the functor T β¦ π«(E_T/T) on
schemes over S. The problem π« is relatively representable when every fibre is
representable by a scheme π«_{E/S} over S; ModuliProblem.RelRepData packages a choice of these
representing schemes. This is the notion all later constructions of moduli schemes are phrased in:
a relatively representable problem is affine, finite, flat, Γ©tale, β¦ over Ell/B when
every representing morphism π«_{E/S} βΆ S is (RelRepData.HasProperty).
Relative representability is a condition on each elliptic curve separately: unlike Mathlib's
CategoryTheory.Functor.relativelyRepresentable, whose representing objects lie in the source
category of a fixed functor, the representing objects here are schemes over the varying bases S.
Because every arrow of Ell/B is cartesian, these representing schemes are automatically
compatible with base change (RelRepData.isPullback), so any base-change-stable property of the
representing morphisms propagates along arrows of Ell/B (RelRepData.rep_mem_of_hom), and
RelRepData.HasProperty does not depend on the choice of representing schemes
(RelRepData.hasProperty_congr).
The trivial problem [Ξ(1)] is the terminal presheaf π_, relatively represented by the
identities of the bases (RelRepData.tensorUnit); every problem with exactly one level structure
on each object is isomorphic to it (ModuliProblem.isoTensorUnitOfUnique). The simultaneous
problem (π«, π¬) is the product presheaf π« β π¬, relatively represented by the fibre products
π«_{E/S} Γ_S π¬_{E/S} (RelRepData.tensor).
A moduli problem is rigid when no automorphism of an elliptic curve E/S other than the
identity fixes a level structure on E/S (ModuliProblem.IsRigid). Rigidity passes to every
problem with a morphism to a rigid one (IsRigid.of_hom), in particular to simultaneous problems,
and every problem representable by an object of Ell/B is rigid (isRigid_of_representableBy).
Main definitions #
TauCeti.AlgebraicGeometry.ModuliProblem B: moduli problems overEll/B.TauCeti.AlgebraicGeometry.ModuliProblem.fibre: the functorT β¦ π«(E_T/T)on schemes over the base ofE.TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData: relative-representability data.TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.universal: the universal level structure over the representing schemeπ«_{E/S}.TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.HasProperty: a property of morphisms of schemes holds for every representing morphism.TauCeti.AlgebraicGeometry.ModuliProblem.IsRigid: rigidity.TauCeti.AlgebraicGeometry.ModuliProblem.isoTensorUnitOfUnique: a moduli problem with exactly one level structure on every object is the trivial problem[Ξ(1)].
Main results #
TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.isPullback: for an arrow(E'/S') βΆ (E/S)ofEll/B,π«_{E'/S'}is the base change ofπ«_{E/S}alongS' βΆ S.TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.hasProperty_surjective_iff: a relatively representable problem is surjective overEll/Bexactly when every point of the base of every object lies under a scheme over which the base-changed curve carries a level structure.TauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.tensorandTauCeti.AlgebraicGeometry.ModuliProblem.RelRepData.HasProperty.tensor: the simultaneous problem of two relatively representable problems is relatively representable, and inherits every property stable under base change and composition.TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_of_representableBy: a representable moduli problem is rigid.
References #
- N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Chapter 4, and Appendix A.4.1.
A moduli problem over Ell/B: a contravariant functor from the category Ell/B of
elliptic curves over B-schemes to types. Its values lie in Type (u + 1), one universe above the
schemes, so that level structures may carry scheme-valued data such as subgroup schemes.
Instances For
The fibre of a moduli problem π« over an object X = (E/S) of Ell/B: the functor
T β¦ π«(E_T/T) on schemes over S, where E_T is the base change of E along T βΆ S.
Instances For
Base change of fibres along an arrow of Ell/B. For an arrow f : X βΆ Y of Ell/B
over f.base : S' βΆ S, the fibre of π« over X is the fibre of π« over Y restricted to
schemes over S', through EllObj.baseChangeFunctorIso.
Instances For
A moduli problem with exactly one level structure on every object is trivial: if π«(E/S)
has exactly one element for every object (E/S) of Ell/B, then π« is the trivial moduli
problem [Ξ(1)], the terminal presheaf π_.
Instances For
Relative-representability data for a moduli problem π« (KatzβMazur 4.2): for every
object X = (E/S) of Ell/B, a scheme rep X = π«_{E/S} over S representing the fibre
T β¦ π«(E_T/T).
- rep (X : EllObj B) : CategoryTheory.Over X.base
The representing scheme
π«_{E/S}over the baseSofX = (E/S). - representableBy (X : EllObj B) : (P.fibre X).RepresentableBy (self.rep X)
The scheme
rep Xrepresents the fibre of the problem overX.
Instances For
The universal level structure of a relatively representable moduli problem π« over an
object X = (E/S) of Ell/B: the π«-structure on the base change of E to the representing
scheme π«_{E/S} which corresponds to the identity of π«_{E/S}. Every level structure on a base
change of E is pulled back from it (Functor.RepresentableBy.homEquiv_eq together with
RelRepData.representableBy_homEquiv_id).
Instances For
The universal level structure corresponds to the identity of the representing scheme.
Along an arrow f : X βΆ Y of Ell/B, the base change of the representing scheme over Y
along f.base represents the fibre of the problem over X.
Instances For
Representing schemes commute with base change. For an arrow f : X βΆ Y of Ell/B, the
representing scheme over X is the base change of the representing scheme over Y along
f.base.
Instances For
Representing schemes commute with base change, as a pullback square: for an arrow
f : (E'/S') βΆ (E/S) of Ell/B, the square formed by π«_{E'/S'} βΆ π«_{E/S}, the two representing
morphisms and f.base : S' βΆ S is cartesian.
A property of morphisms of schemes which is stable under base change propagates from the
representing morphism over Y to the representing morphism over X, along any arrow
X βΆ Y of Ell/B.
A relatively representable moduli problem has the property W of morphisms of schemes
over Ell/B (for instance is affine, finite, flat or Γ©tale over Ell/B) when every representing
morphism π«_{E/S} βΆ S has W.
Instances For
The defining condition of RelRepData.HasProperty: every representing morphism has W.
For a property W respecting isomorphisms, HasProperty W does not depend on the choice of
representing schemes.
Transport relative-representability data along an isomorphism of moduli problems.
Instances For
Isomorphic moduli problems have the same isomorphism-invariant properties of representing morphisms.
Surjectivity over Ell/B. A relatively representable moduli problem π« is surjective
over Ell/B, that is, every representing morphism π«_{E/S} βΆ S is surjective, exactly when every
point s of the base of every object (E/S) lies in the image of a scheme T over S such that
the base change E_T carries a π«-structure.
The trivial moduli problem [Ξ(1)], the terminal presheaf π_ on Ell/B, is relatively
representable: its fibre over (E/S) is represented by S itself.
Instances For
The trivial moduli problem has every property of morphisms of schemes which holds for identities.
The simultaneous problem (π«, π¬), the product presheaf π« β π¬, of two relatively
representable moduli problems is relatively representable: its fibre over (E/S) is represented
by the fibre product π«_{E/S} Γ_S π¬_{E/S} of the two representing schemes.
Instances For
The simultaneous problem of two relatively representable moduli problems with a property of morphisms of schemes stable under base change and composition has that property.
A moduli problem π« is rigid when, for every elliptic curve E/S, the automorphism group
of E/S acts freely on π«(E/S): an arrow Ο : X βΆ X of Ell/B over the identity of the base
(such an arrow is an automorphism, by EllObj.isIso_iff_isIso_base) which fixes some level
structure Ξ± β π«(X) is the identity.
Instances For
The defining condition of IsRigid: an arrow over the identity of the base fixing some level
structure is the identity.
A moduli problem with a morphism to a rigid moduli problem is rigid.
For a rigid π«, two arrows Ο Ο : X βΆ Y of Ell/B with the same morphism of bases, with
Ο an isomorphism, which pull back some level structure Ξ± β π«(Y) to the same element, are
equal: the automorphism Ο β« Οβ»ΒΉ of X lies over the identity and fixes Ο^* Ξ±.
The simultaneous problem (π«, π¬) is rigid when π« is.
The simultaneous problem (π«, π¬) is rigid when π¬ is.
A representable moduli problem is rigid (KatzβMazur A.4.1.2): if π« is represented by an
object U of Ell/B, in the sense that arrows X βΆ U of Ell/B correspond naturally to
elements of π«(X), then π« is rigid.