The following proposition is there in Pink’s lecture notes on finite group schemes.

Let $ k$ be an algebraically closed field of characteristic $ p$ . The category of finite length $ W(k)$ -modules $ N$ with a $ \sigma$ -linear automorphism ($ \sigma$ is the Witt vector frobenius) $ F: N \to N$ is equivalent to the category of finite length $ \mathbb Z_p$ modules (i.e., finite abelian $ p$ -groups). In particular, $ \text{length} _{W(k)} N = \text{log}_p |N^F|$ where $ N^F$ is the subset of $ N$ fixed by $ F$ .

In the lecture notes there is a proof by using Lang’s theorem. I think there is a more straightforward proof without using Lang theorem but just by following the technique of Fontaine’s Galois descent proof in the case of Witt-vectors.

Question: Does anyone have a reference to the theorem or any of the proofs?