Definitions/Def_CerednikDrinfeld_PeriodMap.lean

Throughout, p is a prime, O a commutative ring, \Phi a FormalODModule over O/pO, and B a commutative ring. Fixed once and for all are a ring homomorphism \iota\colon \mathbb{Z}_{p^2}\to O, a proof hc\Phi that the two graded pieces \Phi.gradedPiece (jbar \iota) 0 and ... 1 are complementary submodules, and an additive map r_\Phi from \mathbb{Z}_p^{\,2} into the NMod of the graded Cartier module data attached to \Phi along the reduction of \iota (that data being a Witt-vector module with Frobenius, Verschiebung, a square root \varpi of p and a \mathbb{Z}/2-grading). Given \psi\colon O\to B and a rigidified object t of Rigidified p \Phi B, the predicate IsPeriodValue on a point d of \hat\Omega(B) — that is, on a Deligne datum for K=\mathbb{Q}_p, \pi=p, consisting of a line bundle-quotient datum M\mapsto \mathrm{line}(M)\subseteq B\otimes_{\mathbb{Z}_p}M on full lattices, monotone, homothety-equivariant and nondegenerate at every prime of B — asserts the existence of a Drinfeld datum Q over B (lattice chains N_0\subseteq N_1 over \operatorname{Spec}B together with invertible modules T_0,T_1, maps \Pi_0,\Pi_1 with both composites multiplication by p, and surjections u_0,u_1 onto the stalks) such that the predicate IsCartierQuadruple holds for t and Q relative to (\iota,h_{c\Phi},r_\Phi,\psi) and such that Q IsQuadrupleOf d, i.e. at every prime x the datum d is edge-nondegenerate for (N_0(x),N_1(x)) and the kernels of u_0(x),u_1(x) are the lines of the localised d at those two lattices. periodValue extracts such a d from a proof of its existence, and periodValue_spec records that the extracted value satisfies IsPeriodValue.

Finally, IsPeriodMapOn fixes k algebraically closed of characteristic p, \iota\colon\mathbb{Z}_{p^2}\to W(k), \Phi over W(k)/p, a moduli package M with a comparison family \eta from rigidified objects to M, and a candidate period map \theta defined on M.\mathrm{obj}\,B\,\psi for Noetherian \mathbb{Z}_p-algebras B with p nilpotent; it asserts that for every such B, every \psi\colon W(k)\to B and every admissible t, the Deligne datum \theta(\eta(t)) is a period value of t. This is the existential form of the condition; the predicate IsPeriodMap of the imported specification instead requires that every Cartier quadruple of t be a quadruple of \theta(\eta(t)) and adds compatibility of \theta with base change along \mathbb{Z}_p-algebra maps.