Iterates of a self-map on one-parameter maps

A one-parameter map into a type G, with parameters in a monoid A, is a map x : A → G, and a self-map f of G raises its parameter to the p-th power when

f (x t) = x (t ^ p)

for every parameter t, the power being taken in A. This file records what the iterates of such an f do, and what the odd iterates of an f do when only its square raises the parameter that way, together with two bookkeeping identities for the iterates of a square root of a self-map, which is the shape a Suzuki--Ree Steinberg endomorphism has:

f^[n] (x t)         = x (t ^ p ^ n),
f^[2 * n + 1] (x t) = y (t ^ (p ^ n * e)).

In the second equation f is allowed to carry the one-parameter map x to another one-parameter map y and to raise the parameter to its e-th power, while f ∘ f is assumed to raise the parameter of y to the p-th power without moving y. An odd iterate is then f once followed by n iterates of f ∘ f, so the passage from x to y happens exactly once however large n is.

The application is a Steinberg endomorphism of Suzuki--Ree type. There x and y are two of the numbered simple root subgroups of an ambient group in characteristic p, each a homomorphism Multiplicative A →* G read below as the one-parameter map fun a => x (Multiplicative.ofAdd a); f is the exceptional isogeny with f ∘ f = Frob_p, which exchanges the long and short simple roots and raises the parameter to its first power on a long root and to its p-th on a short one, and the odd iterate f^[2 * n + 1] is the Steinberg endomorphism whose fixed points are taken. None of that structure is assumed below: G is a bare type, x and y are bare maps into it, and A carries only the multiplication raising the parameters to powers.

Main results

• TauCeti.iterate_apply_pow: the n-th iterate of a map raising a parameter to its p-th power raises that parameter to its p ^ n-th power.
• TauCeti.iterate_two_mul_add_one_apply_pow: the odd iterates of a square root of such a map, on a one-parameter map it may carry to another.
• TauCeti.iterate_iterate_apply and TauCeti.apply_iterate_two_mul_add_one: the iterates of a square root of a self-map, in terms of the iterates of that self-map.

References

• R. W. Carter, Simple Groups of Lie Type, §§12--13, for the Suzuki--Ree endomorphisms these equations are abstracted from.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

theorem TauCeti.iterate_apply_pow {G : Type u_1} {A : Type u_2} [Monoid A] {f : G → G} {x : A → G} {p : ℕ} (hf : ∀ (t : A), f (x t) = x (t ^ p)) (n : ℕ) (t : A) : f^[n] (x t) = x (t ^ p ^ n)

The iterates of a map that raises a parameter to its p-th power. If f (x t) = x (t ^ p) for every parameter t of the one-parameter map x, then f^[n] (x t) = x (t ^ p ^ n).

theorem TauCeti.iterate_iterate_apply {G : Type u_1} {f g : G → G} (h : ∀ (a : G), f (f a) = g a) (n : ℕ) (a : G) : f^[n] (f^[n] a) = g^[n] a

The iterates of a square root of a self-map. If f ∘ f = g then applying the n-th iterate of f twice is the n-th iterate of g.

theorem TauCeti.apply_iterate_two_mul_add_one {G : Type u_1} {f g : G → G} (h : ∀ (a : G), f (f a) = g a) (n : ℕ) (a : G) : f (f^[2 * n + 1] a) = g^[n + 1] a

One further application of a square root of a self-map after an odd iterate. If f ∘ f = g then f after f^[2 * n + 1] is g^[n + 1], the odd exponent becoming the even one 2 * (n + 1).

theorem TauCeti.iterate_two_mul_add_one_apply_pow {G : Type u_1} {A : Type u_2} [Monoid A] {f : G → G} {x y : A → G} {e p : ℕ} (hf : ∀ (t : A), f (x t) = y (t ^ e)) (hsq : ∀ (t : A), f (f (y t)) = y (t ^ p)) (n : ℕ) (t : A) : f^[2 * n + 1] (x t) = y (t ^ (p ^ n * e))

The odd iterates of a square root of a map that raises a parameter to its p-th power. Let f carry the one-parameter map x to the one-parameter map y, raising the parameter to its e-th power, and let f ∘ f raise the parameter of y to its p-th power without moving y. Then

f^[2 * n + 1] (x t) = y (t ^ (p ^ n * e)).