Definitions/Def_CerednikDrinfeld_CartierLMapFibre.lean

Throughout, p is a prime, B a commutative ring (of characteristic p where Verschiebung is involved), X a FormalODModule p B with underlying formal group law X.F, M = CartierModule p X.F its Cartier module, and j\colon \mathbb{Z}_{p^2} \to B a ring homomorphism. piOp is the additive endomorphism \Pi of M obtained by functoriality from the endomorphism X.varpiEnd of X.F; piOp_apply identifies it with the action CartierModule.endAct X.varpiEnd, and piOp_comp_verschiebung records \Pi V = V\Pi in characteristic p. On top of the abstract constructions of CartierN applied to the pair (V,\Pi) one gets: NMod, the quotient of M \times M by the image of m \mapsto (Vm, -\Pi m); lambdaN, the induced additive map sending the class of (m,m') to \Pi m + V m'; and NPiece j n, the image in NMod of M_n \times M_n, where M_n = X.gradedPiece j n consists of those f with \mathrm{endAct}\,(X.\mathrm{actEnd}(\tau(c)))\,f = \mathrm{homothety}\,(j(\tau(c))^{p^n})\,f for all c in \mathbb{F}_{p^2}, \tau the Teichmüller lift. Two characterisations are recorded: CritChart.IsCritical X j n holds exactly when \Pi f \in V M for every f \in M_n, and CritChart.invariants X j n consists of the m \in M_n with \Pi m = V m.

IsPiBijective X j n is the conjunction of: for f \in M_n, \Pi f \in VM implies f \in VM; and every h \in M_{n+1} is of the form \Pi f + Vg with f \in M_n and g \in M. IsLMap X j L, for an additive map L\colon M \to NMod, is a structure whose four fields are the assertions that \lambda \circ L is the Frobenius of M; that L(Vx) is the class of (\Pi x, 0); that L(M_n) \subseteq NPiece j n for every n; and that if n is critical, f \in M_n and Vg = \Pi f, then L(f) is the class of (g,0). For such an L the module provides \varphi, the endomorphism of NMod sending the class of (m,m') to L(m) + the class of (m',0); \eta, its fixed subgroup; and u\colon \eta \to M/VM, the restriction of the map taking the class of (m,m') to m \bmod VM.