Iterating functions

module foundation.iterating-functions where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.function-extensionality

open import foundation-core.commuting-squares-of-maps
open import foundation-core.dependent-pair-types
open import foundation-core.endomorphisms
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.sets
open import foundation-core.universe-levels

open import group-theory.monoid-actions

Idea

Any map f : X → X can be iterated by repeatedly applying f

Definition

Iterating functions

module _
  {l : Level} {X : UU l}
  where

  iterate :   (X  X)  (X  X)
  iterate zero-ℕ f x = x
  iterate (succ-ℕ k) f x = f (iterate k f x)

  iterate' :   (X  X)  (X  X)
  iterate' zero-ℕ f x = x
  iterate' (succ-ℕ k) f x = iterate' k f (f x)

Homotopies of iterating functions

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (s : A  A) (t : B  B)
  where

  coherence-square-iterate :
    {f : A  B} (H : coherence-square-maps f s t f) 
    (n : )  coherence-square-maps f (iterate n s) (iterate n t) f
  coherence-square-iterate {f} H zero-ℕ x = refl
  coherence-square-iterate {f} H (succ-ℕ n) =
    pasting-vertical-coherence-square-maps
      ( f)
      ( iterate n s)
      ( iterate n t)
      ( f)
      ( s)
      ( t)
      ( f)
      ( coherence-square-iterate H n)
      ( H)

Properties

The two definitions of iterating are homotopic

module _
  {l : Level} {X : UU l}
  where

  iterate-succ-ℕ :
    (k : ) (f : X  X) (x : X)  iterate (succ-ℕ k) f x  iterate k f (f x)
  iterate-succ-ℕ zero-ℕ f x = refl
  iterate-succ-ℕ (succ-ℕ k) f x = ap f (iterate-succ-ℕ k f x)

  reassociate-iterate : (k : ) (f : X  X)  iterate k f ~ iterate' k f
  reassociate-iterate zero-ℕ f x = refl
  reassociate-iterate (succ-ℕ k) f x =
    iterate-succ-ℕ k f x  reassociate-iterate k f (f x)

For any map f : X → X, iterating f defines a monoid action of ℕ on X

module _
  {l : Level} {X : UU l}
  where

  iterate-add-ℕ :
    (k l : ) (f : X  X) (x : X) 
    iterate (k +ℕ l) f x  iterate k f (iterate l f x)
  iterate-add-ℕ k zero-ℕ f x = refl
  iterate-add-ℕ k (succ-ℕ l) f x =
    ap f (iterate-add-ℕ k l f x)  iterate-succ-ℕ k f (iterate l f x)

  left-unit-law-iterate-add-ℕ :
    (l : ) (f : X  X) (x : X) 
    iterate-add-ℕ 0 l f x  ap  t  iterate t f x) (left-unit-law-add-ℕ l)
  left-unit-law-iterate-add-ℕ zero-ℕ f x = refl
  left-unit-law-iterate-add-ℕ (succ-ℕ l) f x =
    ( right-unit) 
    ( ( ap (ap f) (left-unit-law-iterate-add-ℕ l f x)) 
      ( ( inv (ap-comp f  t  iterate t f x) (left-unit-law-add-ℕ l))) 
        ( ap-comp  t  iterate t f x) succ-ℕ (left-unit-law-add-ℕ l))))

  right-unit-law-iterate-add-ℕ :
    (k : ) (f : X  X) (x : X) 
    iterate-add-ℕ k 0 f x  ap  t  iterate t f x) (right-unit-law-add-ℕ k)
  right-unit-law-iterate-add-ℕ k f x = refl

  iterate-iterate :
    (k l : ) (f : X  X) (x : X) 
    iterate k f (iterate l f x)  iterate l f (iterate k f x)
  iterate-iterate k l f x =
    ( inv (iterate-add-ℕ k l f x)) 
    ( ( ap  t  iterate t f x) (commutative-add-ℕ k l)) 
      ( iterate-add-ℕ l k f x))

  iterate-mul-ℕ :
    (k l : ) (f : X  X) (x : X) 
    iterate (k *ℕ l) f x  iterate k (iterate l f) x
  iterate-mul-ℕ zero-ℕ l f x = refl
  iterate-mul-ℕ (succ-ℕ k) l f x =
    ( iterate-add-ℕ (k *ℕ l) l f x) 
    ( ( iterate-mul-ℕ k l f (iterate l f x)) 
      ( inv (iterate-succ-ℕ k (iterate l f) x)))

  iterate-exp-ℕ :
    (k l : ) (f : X  X) (x : X) 
    iterate (exp-ℕ l k) f x  iterate k (iterate l) f x
  iterate-exp-ℕ zero-ℕ l f x = refl
  iterate-exp-ℕ (succ-ℕ k) l f x =
    ( iterate-mul-ℕ (exp-ℕ l k) l f x) 
    ( ( iterate-exp-ℕ k l (iterate l f) x) 
      ( inv (htpy-eq (iterate-succ-ℕ k (iterate l) f) x)))

module _
  {l : Level} (X : Set l)
  where

  iterative-Monoid-Action : Monoid-Action l ℕ*-Monoid
  pr1 iterative-Monoid-Action = endo-Set X
  pr1 (pr1 (pr2 iterative-Monoid-Action)) k f = iterate k f
  pr2 (pr1 (pr2 iterative-Monoid-Action)) k l =
    eq-htpy  f  eq-htpy  x  iterate-mul-ℕ k l f x))
  pr2 (pr2 iterative-Monoid-Action) = refl