Iterates of lifts of power maps

Let φ be a ring endomorphism of a commutative ring R that lifts the q-th power map modulo an element c, in the sense that c ∣ φ a - a ^ q for every a. The typical case is a lift of the Frobenius of R / p R, for a prime p, with c = p and q = p. Then the i-th iterate of φ lifts the q ^ i-th power map modulo c. This is the congruence σⁱ(a) ≡ a ^ (pⁱ) modulo p used in integrality arguments for Hazewinkel's functional equation.

Main results

• TauCeti.dvd_pow_apply_sub_pow_pow: if c ∣ φ a - a ^ q for all a, then c ∣ φⁱ a - a ^ q ^ i.

theorem TauCeti.dvd_pow_apply_sub_pow_pow {R : Type u_1} [CommRing R] {c : R} {q : ℕ} {φ : R →+* R} (hφ : ∀ (a : R), c ∣ φ a - a ^ q) (i : ℕ) (a : R) : c ∣ (φ ^ i) a - a ^ q ^ i

If a ring endomorphism φ lifts the q-th power map modulo c, that is c ∣ φ a - a ^ q for every a, then its i-th iterate lifts the q ^ i-th power map: c ∣ φⁱ a - a ^ q ^ i.