On the decomposition of the De Rham complex on formal schemes

We show that, for a pseudo-proper smooth noetherian formal scheme $\mathfrak{X}$ over a positive characteristic $p$ field, its truncated De Rham complex up to the characteristic $p$ is decomposable. Moreover, if the dimension of $\mathfrak{X}$ is exactly $p$, then the full De Rham complex is decomposable. Along the way we establish the Cartier isomorphism associated to a smooth morphism of positive characteristic noetherian formal schemes.