Definitions/Def_CerednikDrinfeld_QMRigidificationLevel.lean

The single declaration IsNormLevelTransport is a relation between a full level-n structure on a fake elliptic curve E over an \mathcal O-algebra B, equipped with a rigidification along a leg \psi : O^{nr} \to B, and a level-n structure on the base curve A_0 over O^{nr}/(\pi), normalised by a power of r.

The data are: a prime r; a commutative ring \mathcal O with an element \pi; an \mathcal O-algebra O^{nr} with an \mathcal O-algebra automorphism \mathrm{Fr}; a fake elliptic curve A_0 for the order \Lambda and level N over O^{nr}/(\pi) together with formal coordinates \theta_0 of its structure morphism in dimension 2; a ring homomorphism \kappa : O^{nr}/(\pi) \to O^{nr}/\mathrm{pIdeal}\,r\,O^{nr}; a two-variable series \beta_0 and a formal \mathcal O_D-module \Phi over O^{nr}/\mathrm{pIdeal}\,r\,O^{nr}; a ring homomorphism \iota from \mathrm{Zp2}\,r to O^{nr}; a map \mathrm{coord} : \Lambda \to \mathrm{Zp2}\,r \times \mathrm{Zp2}\,r; a full level-n structure P_0 on A_0; and, over a further \mathcal O-algebra B with \psi : O^{nr} \to B, a fake elliptic curve E, a rigidification \varrho of E relative to A_0 along \psi, and a full level-n structure P_n on E.

The predicate asserts the existence of a morphism Q : \operatorname{Spec}(B/(\pi)) \to \varrho.\mathtt{Ab}.A which is a section of the structure morphism of \varrho.\mathtt{Ab} and which, composed with the comparison \varrho.\mathtt{gA} to A_0, is the base change of P_0 along \mathrm{Spec} of the induced map O^{nr}/(\pi) \to B/(\pi); together with a formal \mathcal O_D-module X over B, formal coordinates \theta of E exhibiting E as a formal module for X via \mathrm{coord} (the predicate IsFormalModuleVia: \theta are formal coordinates for the group law of E with underlying law X.F, and the action of each m \in \Lambda on points is computed, on nilpotent arguments, by the series attached to \mathrm{coord}\,m), an exponent j with j \le 1, and a rigidified special formal module t over B for \Phi with t.X = X, subject to three conditions. First, IsRigTransport θ₀ κ β₀ ϱ θ j t: there are a ring homomorphism \kappa_B : B/(\pi) \to B/\mathrm{pIdeal}\,r\,B compatible with the reductions and with \kappa, and a series \sigma over B/(\pi), such that on every algebra B'' receiving compatible maps from B, B/(\pi) and O^{nr}/(\pi), the composite of a \theta_0-point of \varrho.\mathtt{Ab} with argument in a nilpotent ideal with \varrho.\varphi' and \varrho.\mathtt{gb} is the \theta-point with argument \sigma evaluated there, and t.\rho is the reduction of \sigma composed with the reduction of \beta_0 and with X_i \mapsto X_i^{r^j}. Secondly, t is admissible for \iota and the Frobenius-twisted leg \psi \circ \mathrm{Fr}^{-j}. Thirdly, the normalised level equation: the reduction modulo \pi of the point r^{t.n} \cdot P_n of E equals Q followed by \varrho.\varphi' followed by \varrho.\mathtt{gb}. Thus the relation is a condition on chosen coordinates and a chosen rigidified model, with the multiplication by r^{t.n} making the transported level insensitive to re-presenting the rigidification with shifted r-powers.