Unit-root idempotent for an element of a module-finite ℤₚ-algebra

Let $p$ be a prime and let $A$ be a commutative ring equipped with a $\mathbb{Z}_p$-algebra structure making $A$ a finite $\mathbb{Z}_p$-module, and let $a \in A$. Then there exists an element $e \in A$ with the following four properties. First, $e$ is idempotent, $e \cdot e = e$. Second, $e$ lies in the $\mathbb{Z}_p$-subalgebra of $A$ generated by $a$, that is, in $\mathrm{Algebra.adjoin}\ \mathbb{Z}_p\ \{a\}$, so $e$ is a polynomial in $a$ with $\mathbb{Z}_p$-coefficients. Third, $a$ divides $e$ within that subalgebra: there is a $b$ in the same subalgebra $\mathbb{Z}_p[a]$ with $a b = e$, so that $a$ becomes invertible after multiplication by $e$. Fourth, there is a natural number $N$ with $a^N (1 - e)$ lying in the ideal of $A$ generated by the image of $p$; thus $a$ is nilpotent modulo $p$ on the complementary factor $(1-e)A$. No nondegeneracy hypothesis on $a$ or on $A$ is imposed, and $N$ is not required to be positive.

This is the unit-root (slope-zero) idempotent attached to an element of a module-finite $p$-adic algebra: the Fitting-type splitting of $A$ into a part where $a$ acts invertibly and a part where $a$ is topologically nilpotent, obtained by lifting an idempotent power of $a$ modulo $p$ along the henselian local ring $\mathbb{Z}_p$ via HenselianLocalRing.existsUnique_isIdempotentElem_mk_eq_of_moduleFinite. It is used in the analysis of $p$-divisible groups, in the step producing a representative whose reduction interchanges Frobenius and Verschiebung up to the cyclotomic character.