On lifting commutative dynamical systems

We construct a lifting of commuting power series from a residue field of positive characteristic to a local ring, in a manner similar to the formal group cohomologies of Lubin–Tate. This lifting is then used to prove that a nontorsion automorphism and a multiplication-by-p endomorphism uniquely define a formal group over fields of a positive characteristic. This suggests that a characteristic 0 conjecture by Lubin could be approached with residue field considerations.