Definitions/Def_ModularCurve_JZeroNeronIdentityComponent.lean

For a prime p, the structure ModularCurve.JZeroNeronIdentityComponent p packages a model over \operatorname{Spec}\mathbf Z of the group J_0(p) of the development, together with the properties of it that are used later. Its data are: a scheme G with a morphism g\colon G\to\operatorname{Spec}\mathbf Z; a term L : RelativeGroupLaw ℤ g, i.e. a group structure on the sets \{\varphi\colon T\to G\mid \varphi\text{ over }t\} for every t\colon T\to\operatorname{Spec}\mathbf Z, given by operations mul, one, inv satisfying the group axioms and compatible with base change T'\to T (no representing morphism G\times G\to G is part of the data); and a bijection pts between JZero p and the set of morphisms \operatorname{Spec}\overline{\mathbf Q}\to G over \operatorname{Spec}\mathbf Z. The fields then assert: L is commutative; g is smooth, separated, locally of finite type, quasi-compact and surjective, and each topological fibre g^{-1}(s) is preconnected; pts is additive for L and Galois-equivariant, \mathrm{pts}(\sigma\cdot x) being \operatorname{Spec}(\sigma) followed by \mathrm{pts}(x); every element t of HeckeAlg (acting on JZero p through heckeModuleBar p) is realised by some endomorphism \varphi of G over \operatorname{Spec}\mathbf Z which is additive on T-valued points for all T and satisfies \mathrm{pts}(t\cdot x)=\mathrm{pts}(x) followed by \varphi; for each n>0 the morphism L.schemeNsmul n (the underlying morphism of the n-fold L-sum of the identity point of g) is flat and surjective; the subgroup of JZero p generated by the pts-preimages of the \overline{\mathbf Q}-base changes of sections in G(\mathbf Z) meets the subgroup of Galois-fixed elements in a subgroup of finite index there; for every valuation subring A\subset\overline{\mathbf Q} lying over p and every m with p\nmid m, the m-torsion elements x whose point \mathrm{pts}(x) factors through an A-valued point of G are exactly jZeroToricTorsion p A m, namely the m-torsion elements of the form eisensteinNumerator p times an element fixed by the inertia subgroup of A over \mathbf Q; and finally the base change G\times_{\mathbf Z}\mathbf Z[1/p]\to\operatorname{Spec}\mathbf Z[1/p] (the second projection of the pullback along Localization.Away (p : ℤ)) is proper. Thus the structure records a list of properties of a chosen model, deliberately weaker than the Néron mapping property: only the consequences of it that the later arguments consume (Hecke action, integral sections of finite index, the description of torsion at p) appear.