Finitely cyclic maps

module elementary-number-theory.finitely-cyclic-maps where
Imports
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.iterating-functions
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Definitions

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

  is-finitely-cyclic-map : (f : X  X)  UU l
  is-finitely-cyclic-map f = (x y : X)  Σ   k  iterate k f x  y)

  length-path-is-finitely-cyclic-map :
    {f : X  X}  is-finitely-cyclic-map f  X  X  
  length-path-is-finitely-cyclic-map H x y = pr1 (H x y)

  eq-is-finitely-cyclic-map :
    {f : X  X} (H : is-finitely-cyclic-map f) (x y : X) 
    iterate (length-path-is-finitely-cyclic-map H x y) f x  y
  eq-is-finitely-cyclic-map H x y = pr2 (H x y)

Properties

Finitely cyclic maps are equivalences

  map-inv-is-finitely-cyclic-map :
    (f : X  X) (H : is-finitely-cyclic-map f)  X  X
  map-inv-is-finitely-cyclic-map f H x =
    iterate (length-path-is-finitely-cyclic-map H (f x) x) f x

  issec-map-inv-is-finitely-cyclic-map :
    (f : X  X) (H : is-finitely-cyclic-map f) 
    (f  map-inv-is-finitely-cyclic-map f H) ~ id
  issec-map-inv-is-finitely-cyclic-map f H x =
    ( iterate-succ-ℕ (length-path-is-finitely-cyclic-map H (f x) x) f x) 
    ( eq-is-finitely-cyclic-map H (f x) x)

  isretr-map-inv-is-finitely-cyclic-map :
    (f : X  X) (H : is-finitely-cyclic-map f) 
    (map-inv-is-finitely-cyclic-map f H  f) ~ id
  isretr-map-inv-is-finitely-cyclic-map f H x =
    ( ap
      ( iterate (length-path-is-finitely-cyclic-map H (f (f x)) (f x)) f  f)
      ( inv (eq-is-finitely-cyclic-map H (f x) x))) 
    ( ( ap
        ( iterate (length-path-is-finitely-cyclic-map H (f (f x)) (f x)) f)
          ( iterate-succ-ℕ
            ( length-path-is-finitely-cyclic-map H (f x) x) f (f x))) 
      ( ( iterate-iterate
          ( length-path-is-finitely-cyclic-map H (f (f x)) (f x))
          ( length-path-is-finitely-cyclic-map H (f x) x) f (f (f x))) 
        ( ( ap
            ( iterate (length-path-is-finitely-cyclic-map H (f x) x) f)
            ( eq-is-finitely-cyclic-map H (f (f x)) (f x))) 
          ( eq-is-finitely-cyclic-map H (f x) x))))

  is-equiv-is-finitely-cyclic-map :
    (f : X  X)  is-finitely-cyclic-map f  is-equiv f
  is-equiv-is-finitely-cyclic-map f H =
    is-equiv-has-inverse
      ( map-inv-is-finitely-cyclic-map f H)
      ( issec-map-inv-is-finitely-cyclic-map f H)
      ( isretr-map-inv-is-finitely-cyclic-map f H)

The successor functions on standard finite types are finitely cyclic

compute-iterate-succ-Fin :
  {k : } (n : ) (x : Fin (succ-ℕ k)) 
  iterate n (succ-Fin (succ-ℕ k)) x  add-Fin (succ-ℕ k) x (mod-succ-ℕ k n)
compute-iterate-succ-Fin {k} zero-ℕ x = inv (right-unit-law-add-Fin k x)
compute-iterate-succ-Fin {k} (succ-ℕ n) x =
  ( ap (succ-Fin (succ-ℕ k)) (compute-iterate-succ-Fin n x)) 
  ( inv (right-successor-law-add-Fin (succ-ℕ k) x (mod-succ-ℕ k n)))

is-finitely-cyclic-succ-Fin : {k : }  is-finitely-cyclic-map (succ-Fin k)
pr1 (is-finitely-cyclic-succ-Fin {succ-ℕ k} x y) =
  nat-Fin (succ-ℕ k) (add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x))
pr2 (is-finitely-cyclic-succ-Fin {succ-ℕ k} x y) =
  ( compute-iterate-succ-Fin
    ( nat-Fin (succ-ℕ k) (add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x)))
    ( x)) 
    ( ( ap
        ( add-Fin (succ-ℕ k) x)
        ( issec-nat-Fin k (add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x)))) 
      ( ( commutative-add-Fin
          ( succ-ℕ k)
          ( x)
          ( add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x))) 
        ( ( associative-add-Fin (succ-ℕ k) y (neg-Fin (succ-ℕ k) x) x) 
          ( ( ap (add-Fin (succ-ℕ k) y) (left-inverse-law-add-Fin k x)) 
            ( right-unit-law-add-Fin k y)))))