Powers of an additively indexed family of endomorphisms

A family f : ℕ → M →* M of endomorphisms of a type with multiplication and a distinguished one, indexed additively so that f 0 is the identity and f (a + b) is the composite of f a and f b, is an additive character AddChar ℕ (Monoid.End M). Thus multiplication of indices corresponds to powers in the endomorphism monoid: the m-th power of f k is f (k * m). No associativity or identity laws for multiplication on M are needed.

This is the shape of the iteration laws of an iterated Frobenius, Frob_0 = id and Frob_(a + b) = Frob_a ∘ Frob_b, and the lemma packages Mathlib's AddChar.map_nsmul_eq_pow for that shape once, so that each Chevalley carrier only supplies its two iteration laws.

Main results

• TauCeti.Monoid.End.pow_eq_of_add_eq_comp: f k ^ m = f (k * m) in Monoid.End M.

theorem TauCeti.Monoid.End.pow_eq_of_add_eq_comp {M : Type u_1} [MulOne M] (f : ℕ → M →* M) (h0 : f 0 = MonoidHom.id M) (hadd : ∀ (a b : ℕ), f (a + b) = (f a).comp (f b)) (k m : ℕ) : (have this := f k; this) ^ m = f (k * m)

Indices multiply under taking powers in the endomorphism monoid: if f 0 is the identity and f (a + b) = f a ∘ f b, then the m-th power of f k is f (k * m).