p-adic valuation of detγ as Witt-vector colength

Let $p$ be a prime, and let $K$ be a field of characteristic $p$ which is perfect in the sense that the $p$-th power map (Frobenius) is bijective. Let $c \colon \mathbb{Z}_p \to \mathbb{W}(K)$ be a ring homomorphism into the ring of Witt vectors of $K$, let $\gamma$ be a $2 \times 2$ matrix with entries in $\mathbb{Z}_p$, indexed by Fin 2, and let $h$ be a natural number. The assertion is an equivalence of two conditions. The first is that there exists a unit $u \in \mathbb{Z}_p^{\times}$ with $\det \gamma = u\,p^{h}$, i.e.\ that $\det\gamma$ is nonzero of $p$-adic valuation exactly $h$. The second is that the $\mathbb{W}(K)$-module length of the quotient of the free module $\mathbb{W}(K)^2$ (written as functions Fin 2 → WittVector p K) by the range of the $\mathbb{W}(K)$-linear map $v \mapsto \gamma^{c} v$, where $\gamma^{c}$ is the matrix obtained from $\gamma$ by applying $c$ entrywise, equals $h$. Since the length takes values in $\mathbb{N} \cup \{\infty\}$, the case $\det\gamma = 0$ is covered: the quotient then has infinite length and neither side holds.

This is the statement that the colength over $\mathbb{W}(K)$ of an integral $p$-adic $2 \times 2$ matrix acting on $\mathbb{W}(K)^2$ computes the $p$-adic valuation of its determinant, $\mathbb{W}(K)$ being a discrete valuation ring with uniformiser $p$ when $K$ is perfect of characteristic $p$. It serves as the index (height) computation in the Čerednik–Drinfeld material, where it is used to read off the valuation of the determinant of a matrix from the height of an isogeny or from a rigidification datum.