This is a question about the category $F\text{-}D^b_\mathrm{coh}(\mathscr{D}^\dagger_{\mathscr{X},\mathbb{Q}})$ of complexes of arithmetic $\mathscr{D}$-modules with Frobenius structure on a smooth formal scheme $\mathscr{X}$ over a complete $p$-adic DVR, as constructed by Berthelot. Let's assume that we're in the situation where the Frobenius of the special fribre of $\mathscr{X}$ lifts to an endomorphism of $\mathscr{X}$.
My question is this - it seems to me from Berthelot's papers that this category is defined as follows. The objects are complexes $E\in D^b_\mathrm{coh}(\mathscr{D}^\dagger_{\mathscr{X},\mathbb{Q}})$, together with an isomorphism $\varphi:F^*E\rightarrow E$ in $D^b_\mathrm{coh}(\mathscr{D}^\dagger_{\mathscr{X},\mathbb{Q}})$. The morphism are then morphisms $E\rightarrow E'$ in $D^b_\mathrm{coh}(\mathscr{D}^\dagger_{\mathscr{X},\mathbb{Q}})$ which are compatible with Frobenius, that is one gets a commutative square $$ \begin{matrix} F^*E & \rightarrow & E \\\downarrow &&\downarrow\\F^*E' & \rightarrow & E'. \end{matrix} $$
Since the question of the definition of the category of complexes with Frobenius in Berthelot and Caro's papers is in fact rather brief (see for example 5.1.1 of this paper http://perso.univ-rennes1.fr/pierre.berthelot/publis/Intro._theo._D-mod._arith.pdf), and this point is not really expanded upon (at least, I couldn't fin it expanded upon) in any of Caro's later papers on the subject, I am not 100% sure that I've got this right.
My question is then very simply this - is this the correct interpretation of the definition of the category $F\text{-}D^b_\mathrm{coh}(\mathscr{D}^\dagger_{\mathscr{X},\mathbb{Q}})$? Or is there a subtlety that I've missed?
