The 61/2-functor formalism of Cartier modules

Let p be a prime. We construct a coherent formalism of geometric operations on Cartier modules with coefficients in ind-coherent sheaves on noetherian derived Fₚ-schemes. For such a scheme X, we consider the stable presentable category Cart(X) of ind-coherent sheaves M equipped with a structural morphism F*,XM → M, where FX denotes the Frobenius endomorphism. We construct pushforward functors for arbitrary morphisms and exceptional pullback functors for separated morphisms almost of finite type, together with coherent composition and base-change equivalences. We single out conditions under which these functors admit further adjoints. On derived schemes separated and almost of finite type over Fₚ, we construct compatible closed symmetric monoidal structures given by shriek tensor products, and establish which functors are symmetric monoidal. The constructions arise from a general procedure for forming functor formalisms of Cartier objects, using their description as lax limits and the universal properties of span $2$-categories developed by Cnossen--Lenz--Linskens [arXiv:2505.19192].