Definitions/Def_CerednikDrinfeld_PeriodMapSpec.lean

The standing data are a prime p, an algebraically closed field k of characteristic p, and a ring homomorphism \iota\colon\mathbb Z_{p^2}\to W(k). Relative to these, IsPeriodMap is a predicate on a family of maps \theta, formulated against: a FormalODModule \Phi over W(k)/pW(k); a ModuliPackage M, which assigns a set M.obj B ψ hB to every commutative ring B with a ring homomorphism \psi\colon W(k)\to B in which p is nilpotent, together with transition maps M.map along ring homomorphisms commuting with the \psi's; a family \eta sending, for each such (B,\psi), an element of Rigidified p Φ B to an element of M.obj B ψ hB; the hypothesis hcΦ that the graded pieces of degrees 0 and 1 of the Cartier module of \Phi are complementary, the piece of degree n consisting of those f on which the action of the Teichmüller lift of c\in\mathbb F_{p^2} agrees with the homothety by j(\tau(c))^{p^n}, where j is \iota followed by reduction mod p; and an additive map r_\Phi from \mathbb Z_p^{2} into the NMod of the graded Cartier module data attached to \Phi by j and hcΦ. Finally \theta assigns, to each Noetherian \mathbb Z_p-algebra B with \psi\colon W(k)\to B and p nilpotent, a map from M.obj B ψ hB to the Deligne data over B for \mathcal O=\mathbb Z_p, K=\mathbb Q_p, \pi=p: families of B-submodules \mathcal L(N)\subseteq B\otimes_{\mathbb Z_p}N, indexed by the full \mathbb Z_p-lattices N\subset\mathbb Q_p^2, with invertible quotients, monotone under inclusions of lattices, equivariant for scalar homotheties, and nondegenerate at every prime of B.

The predicate is the conjunction of two conditions. First, compatibility with Cartier theory: for every such B, every t in Rigidified p Φ B satisfying IsAdmissible ι ψ, and every DrinfeldDatum Q over B which is a Cartier quadruple of t with respect to \iota, hcΦ, r_\Phi and \psi, one has that Q is a Drinfeld quadruple of the Deligne datum \theta_B(\eta_B(t)) — at every prime x of B the pair of lattices N_0(x)\subseteq N_1(x) is edge‑nondegenerate for that datum, and the kernels of u_0(x) and u_1(x) are exactly its lines at those two lattices after base change to the local ring at x. Second, compatibility with base change: for \mathbb Z_p-algebra homomorphisms f\colon B\to B' between Noetherian \mathbb Z_p-algebras with p nilpotent and \psi'=f\circ\psi, the Deligne datum attached by \theta to the image of x under M.map is the base change along f of \theta_B(x), i.e. each of its lines is the B'-span of the image of the corresponding line.