From map to AddAction

Stream: Is there code for X?

[Marcello Seri]

Given $f : \alpha \to \alpha$, is there a convenient way to construct an $\mathrm{AddAction}\; \mathbb{N}\;\alpha$ from it?

[Eric Wieser]

Can you make a #mwe that shows the assumptions on \a and specified what you want the action to mean?

[Adam Topaz]

I assume you want n to act on alpha as n * x = f^[n](x)?

[Adam Topaz]

You can define it as follows:

import Mathlib.Algebra.Group.Nat
import Mathlib.Algebra.Group.Action.Defs

def foo {α : Type*} (f : α → α) : AddAction ℕ α where
  vadd n x := f^[n] x
  zero_vadd := fun _ => rfl
  add_vadd := by
    intros a b _
    show f^[a+b] _ = _
    rw [Function.iterate_add]
    rfl

[Adam Topaz]

It may be worthwhile to add somewhere if we don't already have it.

[Eric Wieser]

def foo {α : Type*} (f : α → α) : AddAction ℕ α :=
  AddAction.compHom _ <| MonoidHom.toAdditive'' <| powersHom (Function.End α) f

example (n a) : (foo f).vadd n a = f^[n] a := rfl

[Marcello Seri]

Thanks a lot, that's the kind of example I was looking for. Is it worth adding AddAction.ofFun (and maybe MulAction.ofFun) on the false line of foo to mathlib? This can get quite handy in the dynamics section

[Eric Wieser]

My initial impression is that AddAction is unlikely to be helpful to you here since you can't reasonably make it an instance, and so you should perhaps be working with

def foo {α : Type*} (f : α → α) : ℕ →+ Additive (Function.End α) :=
  MonoidHom.toAdditive'' <| powersHom (Function.End α) f

instead

[Eric Wieser]

@Yury G. Kudryashov might have some more informed opinions here about dynamics than I do

[Yury G. Kudryashov]

We don't have a canonical way to talk about it. One possible approach is docs#Flow.fromIter but Flow is used in a very small part of the library.